{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}

module Test.Ouroboros.Consensus.ChainGenerator.Slot (
    -- * Counting
    E (ActiveSlotE, EmptySlotE, SlotE)
  , complementActive
  , complementEmpty
    -- * Slot
  , S
  , Test.Ouroboros.Consensus.ChainGenerator.Slot.showS
  , genS
    -- * Reuse
  , POL (mkActive, test)
  , Pol (Inverted, NotInverted)
  , PreImage
  , inverted
  , notInverted
  ) where

import           Data.Coerce (coerce)
import           Data.Proxy (Proxy (Proxy))
import qualified Data.Vector.Generic as VG
import qualified Data.Vector.Generic.Mutable as MVG
import qualified Data.Vector.Unboxed as V
import qualified Data.Vector.Unboxed.Mutable as MV
import qualified System.Random.Stateful as R
import qualified Test.Ouroboros.Consensus.ChainGenerator.Counting as C
import           Test.Ouroboros.Consensus.ChainGenerator.Params (Asc, ascVal)
import qualified Test.QuickCheck as QC

-- | The activeness of some slot
newtype S = S Bool
  deriving (Gen S
Gen S -> (S -> [S]) -> Arbitrary S
S -> [S]
forall a. Gen a -> (a -> [a]) -> Arbitrary a
$carbitrary :: Gen S
arbitrary :: Gen S
$cshrink :: S -> [S]
shrink :: S -> [S]
QC.Arbitrary, S -> S -> Bool
(S -> S -> Bool) -> (S -> S -> Bool) -> Eq S
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: S -> S -> Bool
== :: S -> S -> Bool
$c/= :: S -> S -> Bool
/= :: S -> S -> Bool
Eq, Eq S
Eq S =>
(S -> S -> Ordering)
-> (S -> S -> Bool)
-> (S -> S -> Bool)
-> (S -> S -> Bool)
-> (S -> S -> Bool)
-> (S -> S -> S)
-> (S -> S -> S)
-> Ord S
S -> S -> Bool
S -> S -> Ordering
S -> S -> S
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: S -> S -> Ordering
compare :: S -> S -> Ordering
$c< :: S -> S -> Bool
< :: S -> S -> Bool
$c<= :: S -> S -> Bool
<= :: S -> S -> Bool
$c> :: S -> S -> Bool
> :: S -> S -> Bool
$c>= :: S -> S -> Bool
>= :: S -> S -> Bool
$cmax :: S -> S -> S
max :: S -> S -> S
$cmin :: S -> S -> S
min :: S -> S -> S
Ord, ReadPrec [S]
ReadPrec S
Int -> ReadS S
ReadS [S]
(Int -> ReadS S)
-> ReadS [S] -> ReadPrec S -> ReadPrec [S] -> Read S
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS S
readsPrec :: Int -> ReadS S
$creadList :: ReadS [S]
readList :: ReadS [S]
$creadPrec :: ReadPrec S
readPrec :: ReadPrec S
$creadListPrec :: ReadPrec [S]
readListPrec :: ReadPrec [S]
Read, Int -> S -> ShowS
[S] -> ShowS
S -> String
(Int -> S -> ShowS) -> (S -> String) -> ([S] -> ShowS) -> Show S
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> S -> ShowS
showsPrec :: Int -> S -> ShowS
$cshow :: S -> String
show :: S -> String
$cshowList :: [S] -> ShowS
showList :: [S] -> ShowS
Show)

newtype instance MV.MVector s S = MV_S (MV.MVector s Bool)
newtype instance V.Vector     S = V_S (V.Vector Bool)
deriving newtype instance MVG.MVector MV.MVector S
deriving newtype instance VG.Vector   V.Vector   S
instance V.Unbox S

-----

genS :: R.RandomGen g => Asc -> g -> (S, g)
genS :: forall g. RandomGen g => Asc -> g -> (S, g)
genS Asc
asc g
g =
    Bool
bool Bool -> (S, g) -> (S, g)
forall a b. a -> b -> b
`seq` (Bool -> S
S Bool
bool, g
g')
  where
    (Double
q, g
g') = g -> (Double, g)
forall g. RandomGen g => g -> (Double, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
R.random g
g   -- note 0 <= q <= 1

    bool :: Bool
bool = Double
q Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Asc -> Double
ascVal Asc
asc

showS :: S -> ShowS
showS :: S -> ShowS
showS (S Bool
bool) = Char -> ShowS
showChar (Char -> ShowS) -> Char -> ShowS
forall a b. (a -> b) -> a -> b
$ if Bool
bool then Char
'1' else Char
'0'

-----

-- | Type-level names for the different kinds of slots counted in this library
--
-- The data constructors of this type are used in promoted form with
-- @-XDataKinds@.
--
data E =
     -- | Active slots must be filled on the honest chain and may be filled on an alternative chain.
     ActiveSlotE
     -- | Empty slots may be filled on the honest chain and must not be filled on an alternative chain.
   | EmptySlotE
     -- | @SlotE@ is the union of 'ActiveSlotE' and 'EmptySlotE'
   | SlotE

inverted :: Proxy Inverted
inverted :: Proxy 'Inverted
inverted = Proxy 'Inverted
forall {k} (t :: k). Proxy t
Proxy

notInverted :: Proxy NotInverted
notInverted :: Proxy 'NotInverted
notInverted = Proxy 'NotInverted
forall {k} (t :: k). Proxy t
Proxy

-- | The polarity of a type
--
-- This is used to toggle how functions in this library interact with vectors
-- of 'S' values.
--
-- If the polarity is 'Inverted', then the function will treat all 'S' values as
-- if they were first complemented.
--
-- The 'PreImage' type family does the corresponding parameterization of
-- 'ActiveSlotE' and 'EmptySlotE' at the type level.
--
-- NOTE: No 'S' value is ever actually complemented because of 'Inverted', but
-- the functions parameterized by 'pol' will treat them as if they were.
data Pol = Inverted | NotInverted

-- | Overloaded slot operations for the two polarities
class POL (pol :: Pol) where
    -- | Make an active slot
    mkActive :: proxy pol -> S
    -- | Test whether @pol@ maps the given bit to one
    test :: proxy pol -> S -> Bool

-- Both 'complementActive' and 'complementEmpty' are offered for simplicity
-- instead of a generalized function that works in both cases (it would need
-- another proxy parameter for the element type).

-- | Every slot is either active or empty
complementActive ::
     proxy pol
  -> C.Size base SlotE
  -> C.Count base (PreImage pol ActiveSlotE) which
  -> C.Count base (PreImage pol EmptySlotE ) which
complementActive :: forall (proxy :: Pol -> *) (pol :: Pol) base which.
proxy pol
-> Size base 'SlotE
-> Count base (PreImage pol 'ActiveSlotE) which
-> Count base (PreImage pol 'EmptySlotE) which
complementActive proxy pol
_pol (C.Count Int
n) (C.Count Int
i) = Int -> Count base (PreImage pol 'EmptySlotE) which
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i)

-- | Every slot is either active or empty
complementEmpty ::
     proxy pol
  -> C.Size base SlotE
  -> C.Count base (PreImage pol EmptySlotE ) which
  -> C.Count base (PreImage pol ActiveSlotE) which
complementEmpty :: forall (proxy :: Pol -> *) (pol :: Pol) base which.
proxy pol
-> Size base 'SlotE
-> Count base (PreImage pol 'EmptySlotE) which
-> Count base (PreImage pol 'ActiveSlotE) which
complementEmpty proxy pol
_pol (C.Count Int
n) (C.Count Int
i) = Int -> Count base (PreImage pol 'ActiveSlotE) which
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i)

instance POL Inverted where
    mkActive :: forall (proxy :: Pol -> *). proxy 'Inverted -> S
mkActive proxy 'Inverted
_pol = Bool -> S
forall a b. Coercible a b => a -> b
coerce Bool
False
    test :: forall (proxy :: Pol -> *). proxy 'Inverted -> S -> Bool
test     proxy 'Inverted
_pol = (Bool -> Bool) -> S -> Bool
forall a b. Coercible a b => a -> b
coerce Bool -> Bool
not

instance POL NotInverted where
    mkActive :: forall (proxy :: Pol -> *). proxy 'NotInverted -> S
mkActive proxy 'NotInverted
_pol = Bool -> S
forall a b. Coercible a b => a -> b
coerce Bool
True
    test :: forall (proxy :: Pol -> *). proxy 'NotInverted -> S -> Bool
test     proxy 'NotInverted
_pol = S -> Bool
forall a b. Coercible a b => a -> b
coerce

-- | @PreImage pol e@ is the complement of @e@ if @pol@ is 'Inverted' and simply @e@ if it's 'NotInverted'
type family PreImage (pol :: Pol) (e :: E) where
    PreImage Inverted    EmptySlotE  = ActiveSlotE
    PreImage Inverted    ActiveSlotE = EmptySlotE
    PreImage NotInverted e           = e