{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Byron.Spec.Ledger.Delegation (
SDELEG,
SDELEGS,
DSState (DSState),
_dSStateScheduledDelegations,
_dSStateKeyEpochDelegations,
DCert (DCert),
delegator,
delegate,
depoch,
dwho,
mkDCert,
signature,
ADELEG,
ADELEGS,
DSEnv (
DSEnv,
_dSEnvAllowedDelegators,
_dSEnvEpoch,
_dSEnvSlot,
_dSEnvK
),
allowedDelegators,
DState (
DState,
_dStateDelegationMap,
_dStateLastDelegation
),
DELEG,
DIEnv,
DIState (DIState),
_dIStateDelegationMap,
_dIStateLastDelegation,
_dIStateScheduledDelegations,
_dIStateKeyEpochDelegations,
liveAfter,
EpochDiff (..),
slot,
epoch,
delegationMap,
HasScheduledDelegations,
scheduledDelegations,
dmsL,
dcertGen,
dcertsGen,
initialEnvFromGenesisKeys,
randomDCertGen,
delegatorOf,
delegatorDelegate,
emptyDelegationPayloadRatio,
thisEpochDelegationsRatio,
nextEpochDelegationsRatio,
selfDelegationsRatio,
multipleDelegationsRatio,
maxDelegationsTo,
changedDelegationsRatio,
maxChangedDelegations,
repeatedDelegationsRatio,
maxRepeatedDelegations,
maxCertsPerBlock,
AdelegPredicateFailure (..),
AdelegsPredicateFailure (..),
SdelegPredicateFailure (..),
SdelegsPredicateFailure (..),
MsdelegPredicateFailure (..),
DelegPredicateFailure (..),
) where
import Byron.Spec.Ledger.Core (
BlockCount,
Epoch (Epoch),
HasHash,
Hash (Hash),
Owner (Owner),
Sig,
Slot (Slot),
SlotCount (SlotCount),
VKey (VKey),
VKeyGenesis (VKeyGenesis),
addSlot,
hash,
mkVkGenesisSet,
owner,
range,
unBlockCount,
unVKeyGenesis,
verify,
(∈),
(∉),
(⨃),
)
import Byron.Spec.Ledger.Core.Generators (epochGen, slotGen)
import qualified Byron.Spec.Ledger.Core.Generators as CoreGen
import Byron.Spec.Ledger.Core.Omniscient (signWithGenesisKey)
import Control.Arrow ((&&&))
import Control.State.Transition (
Embed,
Environment,
IRC (IRC),
PredicateFailure,
STS (..),
Signal,
State,
TRC (TRC),
initialRules,
judgmentContext,
trans,
transitionRules,
wrapFailed,
(?!),
)
import Data.AbstractSize
import Data.Bimap (Bimap, (!>))
import qualified Data.Bimap as Bimap
import Data.Data (Data)
import Data.Hashable (Hashable)
import qualified Data.Hashable as H
import qualified Data.List as List
import Data.List.Unique (count)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (catMaybes)
import Data.Set (Set, (\\))
import qualified Data.Set as Set
import Data.Word (Word64, Word8)
import GHC.Generics (Generic)
import Hedgehog (Gen)
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import Lens.Micro (Lens', lens, to, (%~), (&), (.~), (<>~), (^.), _1)
import Lens.Micro.TH (makeFields)
import NoThunks.Class (NoThunks (..), allNoThunks, noThunksInKeysAndValues)
import Test.Control.State.Transition.Generator (
HasTrace,
envGen,
genTrace,
sigGen,
)
import Test.Control.State.Transition.Trace (TraceOrder (OldestFirst), traceSignals)
data DCert = DCert
{ DCert -> VKeyGenesis
delegator :: VKeyGenesis
, DCert -> VKey
delegate :: VKey
, DCert -> Epoch
depoch :: Epoch
, DCert -> Sig (VKey, Epoch)
signature :: Sig (VKey, Epoch)
}
deriving (Int -> DCert -> ShowS
[DCert] -> ShowS
DCert -> String
(Int -> DCert -> ShowS)
-> (DCert -> String) -> ([DCert] -> ShowS) -> Show DCert
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DCert -> ShowS
showsPrec :: Int -> DCert -> ShowS
$cshow :: DCert -> String
show :: DCert -> String
$cshowList :: [DCert] -> ShowS
showList :: [DCert] -> ShowS
Show, DCert -> DCert -> Bool
(DCert -> DCert -> Bool) -> (DCert -> DCert -> Bool) -> Eq DCert
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DCert -> DCert -> Bool
== :: DCert -> DCert -> Bool
$c/= :: DCert -> DCert -> Bool
/= :: DCert -> DCert -> Bool
Eq, Eq DCert
Eq DCert =>
(DCert -> DCert -> Ordering)
-> (DCert -> DCert -> Bool)
-> (DCert -> DCert -> Bool)
-> (DCert -> DCert -> Bool)
-> (DCert -> DCert -> Bool)
-> (DCert -> DCert -> DCert)
-> (DCert -> DCert -> DCert)
-> Ord DCert
DCert -> DCert -> Bool
DCert -> DCert -> Ordering
DCert -> DCert -> DCert
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 :: DCert -> DCert -> Ordering
compare :: DCert -> DCert -> Ordering
$c< :: DCert -> DCert -> Bool
< :: DCert -> DCert -> Bool
$c<= :: DCert -> DCert -> Bool
<= :: DCert -> DCert -> Bool
$c> :: DCert -> DCert -> Bool
> :: DCert -> DCert -> Bool
$c>= :: DCert -> DCert -> Bool
>= :: DCert -> DCert -> Bool
$cmax :: DCert -> DCert -> DCert
max :: DCert -> DCert -> DCert
$cmin :: DCert -> DCert -> DCert
min :: DCert -> DCert -> DCert
Ord, (forall x. DCert -> Rep DCert x)
-> (forall x. Rep DCert x -> DCert) -> Generic DCert
forall x. Rep DCert x -> DCert
forall x. DCert -> Rep DCert x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DCert -> Rep DCert x
from :: forall x. DCert -> Rep DCert x
$cto :: forall x. Rep DCert x -> DCert
to :: forall x. Rep DCert x -> DCert
Generic, Eq DCert
Eq DCert =>
(Int -> DCert -> Int) -> (DCert -> Int) -> Hashable DCert
Int -> DCert -> Int
DCert -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> DCert -> Int
hashWithSalt :: Int -> DCert -> Int
$chash :: DCert -> Int
hash :: DCert -> Int
Hashable, Typeable DCert
Typeable DCert =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DCert -> c DCert)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DCert)
-> (DCert -> Constr)
-> (DCert -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DCert))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DCert))
-> ((forall b. Data b => b -> b) -> DCert -> DCert)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r)
-> (forall u. (forall d. Data d => d -> u) -> DCert -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> DCert -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert)
-> Data DCert
DCert -> Constr
DCert -> DataType
(forall b. Data b => b -> b) -> DCert -> DCert
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DCert -> u
forall u. (forall d. Data d => d -> u) -> DCert -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DCert
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DCert -> c DCert
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DCert)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DCert)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DCert -> c DCert
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DCert -> c DCert
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DCert
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DCert
$ctoConstr :: DCert -> Constr
toConstr :: DCert -> Constr
$cdataTypeOf :: DCert -> DataType
dataTypeOf :: DCert -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DCert)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DCert)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DCert)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DCert)
$cgmapT :: (forall b. Data b => b -> b) -> DCert -> DCert
gmapT :: (forall b. Data b => b -> b) -> DCert -> DCert
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DCert -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DCert -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> DCert -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DCert -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DCert -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DCert -> m DCert
Data, Context -> DCert -> IO (Maybe ThunkInfo)
Proxy DCert -> String
(Context -> DCert -> IO (Maybe ThunkInfo))
-> (Context -> DCert -> IO (Maybe ThunkInfo))
-> (Proxy DCert -> String)
-> NoThunks DCert
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> DCert -> IO (Maybe ThunkInfo)
noThunks :: Context -> DCert -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> DCert -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> DCert -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy DCert -> String
showTypeOf :: Proxy DCert -> String
NoThunks)
instance HasTypeReps DCert
instance HasHash [DCert] where
hash :: [DCert] -> Hash
hash = Maybe Int -> Hash
Hash (Maybe Int -> Hash) -> ([DCert] -> Maybe Int) -> [DCert] -> Hash
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> ([DCert] -> Int) -> [DCert] -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DCert] -> Int
forall a. Hashable a => a -> Int
H.hash
mkDCert ::
VKeyGenesis ->
Sig (VKey, Epoch) ->
VKey ->
Epoch ->
DCert
mkDCert :: VKeyGenesis -> Sig (VKey, Epoch) -> VKey -> Epoch -> DCert
mkDCert VKeyGenesis
vkg Sig (VKey, Epoch)
s VKey
vkd Epoch
e =
DCert
{ delegator :: VKeyGenesis
delegator = VKeyGenesis
vkg
, delegate :: VKey
delegate = VKey
vkd
, depoch :: Epoch
depoch = Epoch
e
, signature :: Sig (VKey, Epoch)
signature = Sig (VKey, Epoch)
s
}
dwho :: DCert -> (VKeyGenesis, VKey)
dwho :: DCert -> (VKeyGenesis, VKey)
dwho = DCert -> VKeyGenesis
delegator (DCert -> VKeyGenesis)
-> (DCert -> VKey) -> DCert -> (VKeyGenesis, VKey)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& DCert -> VKey
delegate
dbody :: DCert -> (VKey, Epoch)
dbody :: DCert -> (VKey, Epoch)
dbody = DCert -> VKey
delegate (DCert -> VKey) -> (DCert -> Epoch) -> DCert -> (VKey, Epoch)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& DCert -> Epoch
depoch
data DSEnv = DSEnv
{ DSEnv -> Set VKeyGenesis
_dSEnvAllowedDelegators :: Set VKeyGenesis
, DSEnv -> Epoch
_dSEnvEpoch :: Epoch
, DSEnv -> Slot
_dSEnvSlot :: Slot
, DSEnv -> BlockCount
_dSEnvK :: BlockCount
}
deriving (Int -> DSEnv -> ShowS
[DSEnv] -> ShowS
DSEnv -> String
(Int -> DSEnv -> ShowS)
-> (DSEnv -> String) -> ([DSEnv] -> ShowS) -> Show DSEnv
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DSEnv -> ShowS
showsPrec :: Int -> DSEnv -> ShowS
$cshow :: DSEnv -> String
show :: DSEnv -> String
$cshowList :: [DSEnv] -> ShowS
showList :: [DSEnv] -> ShowS
Show, DSEnv -> DSEnv -> Bool
(DSEnv -> DSEnv -> Bool) -> (DSEnv -> DSEnv -> Bool) -> Eq DSEnv
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DSEnv -> DSEnv -> Bool
== :: DSEnv -> DSEnv -> Bool
$c/= :: DSEnv -> DSEnv -> Bool
/= :: DSEnv -> DSEnv -> Bool
Eq, (forall x. DSEnv -> Rep DSEnv x)
-> (forall x. Rep DSEnv x -> DSEnv) -> Generic DSEnv
forall x. Rep DSEnv x -> DSEnv
forall x. DSEnv -> Rep DSEnv x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DSEnv -> Rep DSEnv x
from :: forall x. DSEnv -> Rep DSEnv x
$cto :: forall x. Rep DSEnv x -> DSEnv
to :: forall x. Rep DSEnv x -> DSEnv
Generic, Context -> DSEnv -> IO (Maybe ThunkInfo)
Proxy DSEnv -> String
(Context -> DSEnv -> IO (Maybe ThunkInfo))
-> (Context -> DSEnv -> IO (Maybe ThunkInfo))
-> (Proxy DSEnv -> String)
-> NoThunks DSEnv
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> DSEnv -> IO (Maybe ThunkInfo)
noThunks :: Context -> DSEnv -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> DSEnv -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> DSEnv -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy DSEnv -> String
showTypeOf :: Proxy DSEnv -> String
NoThunks)
makeFields ''DSEnv
data DSState = DSState
{ DSState -> [(Slot, (VKeyGenesis, VKey))]
_dSStateScheduledDelegations :: [(Slot, (VKeyGenesis, VKey))]
, DSState -> Set (Epoch, VKeyGenesis)
_dSStateKeyEpochDelegations :: Set (Epoch, VKeyGenesis)
}
deriving (Int -> DSState -> ShowS
[DSState] -> ShowS
DSState -> String
(Int -> DSState -> ShowS)
-> (DSState -> String) -> ([DSState] -> ShowS) -> Show DSState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DSState -> ShowS
showsPrec :: Int -> DSState -> ShowS
$cshow :: DSState -> String
show :: DSState -> String
$cshowList :: [DSState] -> ShowS
showList :: [DSState] -> ShowS
Show, DSState -> DSState -> Bool
(DSState -> DSState -> Bool)
-> (DSState -> DSState -> Bool) -> Eq DSState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DSState -> DSState -> Bool
== :: DSState -> DSState -> Bool
$c/= :: DSState -> DSState -> Bool
/= :: DSState -> DSState -> Bool
Eq, (forall x. DSState -> Rep DSState x)
-> (forall x. Rep DSState x -> DSState) -> Generic DSState
forall x. Rep DSState x -> DSState
forall x. DSState -> Rep DSState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DSState -> Rep DSState x
from :: forall x. DSState -> Rep DSState x
$cto :: forall x. Rep DSState x -> DSState
to :: forall x. Rep DSState x -> DSState
Generic, Context -> DSState -> IO (Maybe ThunkInfo)
Proxy DSState -> String
(Context -> DSState -> IO (Maybe ThunkInfo))
-> (Context -> DSState -> IO (Maybe ThunkInfo))
-> (Proxy DSState -> String)
-> NoThunks DSState
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> DSState -> IO (Maybe ThunkInfo)
noThunks :: Context -> DSState -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> DSState -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> DSState -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy DSState -> String
showTypeOf :: Proxy DSState -> String
NoThunks)
makeFields ''DSState
data DState = DState
{ DState -> Bimap VKeyGenesis VKey
_dStateDelegationMap :: Bimap VKeyGenesis VKey
, DState -> Map VKeyGenesis Slot
_dStateLastDelegation :: Map VKeyGenesis Slot
}
deriving (DState -> DState -> Bool
(DState -> DState -> Bool)
-> (DState -> DState -> Bool) -> Eq DState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DState -> DState -> Bool
== :: DState -> DState -> Bool
$c/= :: DState -> DState -> Bool
/= :: DState -> DState -> Bool
Eq, Int -> DState -> ShowS
[DState] -> ShowS
DState -> String
(Int -> DState -> ShowS)
-> (DState -> String) -> ([DState] -> ShowS) -> Show DState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DState -> ShowS
showsPrec :: Int -> DState -> ShowS
$cshow :: DState -> String
show :: DState -> String
$cshowList :: [DState] -> ShowS
showList :: [DState] -> ShowS
Show, (forall x. DState -> Rep DState x)
-> (forall x. Rep DState x -> DState) -> Generic DState
forall x. Rep DState x -> DState
forall x. DState -> Rep DState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DState -> Rep DState x
from :: forall x. DState -> Rep DState x
$cto :: forall x. Rep DState x -> DState
to :: forall x. Rep DState x -> DState
Generic)
instance NoThunks DState where
wNoThunks :: Context -> DState -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt (DState Bimap VKeyGenesis VKey
dmap Map VKeyGenesis Slot
lastDeleg) =
[IO (Maybe ThunkInfo)] -> IO (Maybe ThunkInfo)
allNoThunks
[ Context -> [(VKeyGenesis, VKey)] -> IO (Maybe ThunkInfo)
forall k v.
(NoThunks k, NoThunks v) =>
Context -> [(k, v)] -> IO (Maybe ThunkInfo)
noThunksInKeysAndValues Context
ctxt ([(VKeyGenesis, VKey)] -> IO (Maybe ThunkInfo))
-> [(VKeyGenesis, VKey)] -> IO (Maybe ThunkInfo)
forall a b. (a -> b) -> a -> b
$ Bimap VKeyGenesis VKey -> [(VKeyGenesis, VKey)]
forall a b. Bimap a b -> [(a, b)]
Bimap.toList Bimap VKeyGenesis VKey
dmap
, Context -> [(VKeyGenesis, Slot)] -> IO (Maybe ThunkInfo)
forall k v.
(NoThunks k, NoThunks v) =>
Context -> [(k, v)] -> IO (Maybe ThunkInfo)
noThunksInKeysAndValues Context
ctxt ([(VKeyGenesis, Slot)] -> IO (Maybe ThunkInfo))
-> [(VKeyGenesis, Slot)] -> IO (Maybe ThunkInfo)
forall a b. (a -> b) -> a -> b
$ Map VKeyGenesis Slot -> [(VKeyGenesis, Slot)]
forall k a. Map k a -> [(k, a)]
Map.toList Map VKeyGenesis Slot
lastDeleg
]
makeFields ''DState
delegatorOf :: Bimap VKeyGenesis VKey -> VKey -> Maybe VKeyGenesis
delegatorOf :: Bimap VKeyGenesis VKey -> VKey -> Maybe VKeyGenesis
delegatorOf = (VKey -> Bimap VKeyGenesis VKey -> Maybe VKeyGenesis)
-> Bimap VKeyGenesis VKey -> VKey -> Maybe VKeyGenesis
forall a b c. (a -> b -> c) -> b -> a -> c
flip VKey -> Bimap VKeyGenesis VKey -> Maybe VKeyGenesis
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
b -> Bimap a b -> m a
Bimap.lookupR
type DIEnv = DSEnv
data DIState = DIState
{ DIState -> Bimap VKeyGenesis VKey
_dIStateDelegationMap :: Bimap VKeyGenesis VKey
, DIState -> Map VKeyGenesis Slot
_dIStateLastDelegation :: Map VKeyGenesis Slot
, DIState -> [(Slot, (VKeyGenesis, VKey))]
_dIStateScheduledDelegations :: [(Slot, (VKeyGenesis, VKey))]
, DIState -> Set (Epoch, VKeyGenesis)
_dIStateKeyEpochDelegations :: Set (Epoch, VKeyGenesis)
}
deriving (Int -> DIState -> ShowS
[DIState] -> ShowS
DIState -> String
(Int -> DIState -> ShowS)
-> (DIState -> String) -> ([DIState] -> ShowS) -> Show DIState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DIState -> ShowS
showsPrec :: Int -> DIState -> ShowS
$cshow :: DIState -> String
show :: DIState -> String
$cshowList :: [DIState] -> ShowS
showList :: [DIState] -> ShowS
Show, DIState -> DIState -> Bool
(DIState -> DIState -> Bool)
-> (DIState -> DIState -> Bool) -> Eq DIState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DIState -> DIState -> Bool
== :: DIState -> DIState -> Bool
$c/= :: DIState -> DIState -> Bool
/= :: DIState -> DIState -> Bool
Eq, (forall x. DIState -> Rep DIState x)
-> (forall x. Rep DIState x -> DIState) -> Generic DIState
forall x. Rep DIState x -> DIState
forall x. DIState -> Rep DIState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DIState -> Rep DIState x
from :: forall x. DIState -> Rep DIState x
$cto :: forall x. Rep DIState x -> DIState
to :: forall x. Rep DIState x -> DIState
Generic)
makeFields ''DIState
instance NoThunks DIState where
wNoThunks :: Context -> DIState -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt (DIState Bimap VKeyGenesis VKey
dmap Map VKeyGenesis Slot
lastDeleg [(Slot, (VKeyGenesis, VKey))]
sds Set (Epoch, VKeyGenesis)
sked) =
[IO (Maybe ThunkInfo)] -> IO (Maybe ThunkInfo)
allNoThunks
[ Context -> [(VKeyGenesis, VKey)] -> IO (Maybe ThunkInfo)
forall k v.
(NoThunks k, NoThunks v) =>
Context -> [(k, v)] -> IO (Maybe ThunkInfo)
noThunksInKeysAndValues Context
ctxt ([(VKeyGenesis, VKey)] -> IO (Maybe ThunkInfo))
-> [(VKeyGenesis, VKey)] -> IO (Maybe ThunkInfo)
forall a b. (a -> b) -> a -> b
$ Bimap VKeyGenesis VKey -> [(VKeyGenesis, VKey)]
forall a b. Bimap a b -> [(a, b)]
Bimap.toList Bimap VKeyGenesis VKey
dmap
, Context -> [(VKeyGenesis, Slot)] -> IO (Maybe ThunkInfo)
forall k v.
(NoThunks k, NoThunks v) =>
Context -> [(k, v)] -> IO (Maybe ThunkInfo)
noThunksInKeysAndValues Context
ctxt ([(VKeyGenesis, Slot)] -> IO (Maybe ThunkInfo))
-> [(VKeyGenesis, Slot)] -> IO (Maybe ThunkInfo)
forall a b. (a -> b) -> a -> b
$ Map VKeyGenesis Slot -> [(VKeyGenesis, Slot)]
forall k a. Map k a -> [(k, a)]
Map.toList Map VKeyGenesis Slot
lastDeleg
, Context -> [(Slot, (VKeyGenesis, VKey))] -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt [(Slot, (VKeyGenesis, VKey))]
sds
, Context -> Set (Epoch, VKeyGenesis) -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt Set (Epoch, VKeyGenesis)
sked
]
dmsL ::
HasDelegationMap a (Bimap VKeyGenesis VKey) =>
Lens' a (Bimap VKeyGenesis VKey)
dmsL :: forall a.
HasDelegationMap a (Bimap VKeyGenesis VKey) =>
Lens' a (Bimap VKeyGenesis VKey)
dmsL = (Bimap VKeyGenesis VKey -> f (Bimap VKeyGenesis VKey)) -> a -> f a
forall s a. HasDelegationMap s a => Lens' s a
Lens' a (Bimap VKeyGenesis VKey)
delegationMap
dIStateDSState :: Lens' DIState DSState
dIStateDSState :: Lens' DIState DSState
dIStateDSState =
(DIState -> DSState)
-> (DIState -> DSState -> DIState) -> Lens' DIState DSState
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
(\DIState
dis -> [(Slot, (VKeyGenesis, VKey))]
-> Set (Epoch, VKeyGenesis) -> DSState
DSState (DIState
dis DIState
-> Getting
[(Slot, (VKeyGenesis, VKey))] DIState [(Slot, (VKeyGenesis, VKey))]
-> [(Slot, (VKeyGenesis, VKey))]
forall s a. s -> Getting a s a -> a
^. Getting
[(Slot, (VKeyGenesis, VKey))] DIState [(Slot, (VKeyGenesis, VKey))]
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DIState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations) (DIState
dis DIState
-> Getting
(Set (Epoch, VKeyGenesis)) DIState (Set (Epoch, VKeyGenesis))
-> Set (Epoch, VKeyGenesis)
forall s a. s -> Getting a s a -> a
^. Getting
(Set (Epoch, VKeyGenesis)) DIState (Set (Epoch, VKeyGenesis))
forall s a. HasKeyEpochDelegations s a => Lens' s a
Lens' DIState (Set (Epoch, VKeyGenesis))
keyEpochDelegations))
( \DIState
dis DSState
dss ->
DIState
dis
DIState -> (DIState -> DIState) -> DIState
forall a b. a -> (a -> b) -> b
& ([(Slot, (VKeyGenesis, VKey))]
-> Identity [(Slot, (VKeyGenesis, VKey))])
-> DIState -> Identity DIState
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DIState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations
(([(Slot, (VKeyGenesis, VKey))]
-> Identity [(Slot, (VKeyGenesis, VKey))])
-> DIState -> Identity DIState)
-> [(Slot, (VKeyGenesis, VKey))] -> DIState -> DIState
forall s t a b. ASetter s t a b -> b -> s -> t
.~ DSState
dss
DSState
-> Getting
[(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
-> [(Slot, (VKeyGenesis, VKey))]
forall s a. s -> Getting a s a -> a
^. Getting
[(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DSState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations
DIState -> (DIState -> DIState) -> DIState
forall a b. a -> (a -> b) -> b
& (Set (Epoch, VKeyGenesis) -> Identity (Set (Epoch, VKeyGenesis)))
-> DIState -> Identity DIState
forall s a. HasKeyEpochDelegations s a => Lens' s a
Lens' DIState (Set (Epoch, VKeyGenesis))
keyEpochDelegations
((Set (Epoch, VKeyGenesis) -> Identity (Set (Epoch, VKeyGenesis)))
-> DIState -> Identity DIState)
-> Set (Epoch, VKeyGenesis) -> DIState -> DIState
forall s t a b. ASetter s t a b -> b -> s -> t
.~ DSState
dss
DSState
-> Getting
(Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
-> Set (Epoch, VKeyGenesis)
forall s a. s -> Getting a s a -> a
^. Getting
(Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
forall s a. HasKeyEpochDelegations s a => Lens' s a
Lens' DSState (Set (Epoch, VKeyGenesis))
keyEpochDelegations
)
dIStateDState :: Lens' DIState DState
dIStateDState :: Lens' DIState DState
dIStateDState =
(DIState -> DState)
-> (DIState -> DState -> DIState) -> Lens' DIState DState
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
(\DIState
dis -> Bimap VKeyGenesis VKey -> Map VKeyGenesis Slot -> DState
DState (DIState
dis DIState
-> Getting
(Bimap VKeyGenesis VKey) DIState (Bimap VKeyGenesis VKey)
-> Bimap VKeyGenesis VKey
forall s a. s -> Getting a s a -> a
^. Getting (Bimap VKeyGenesis VKey) DIState (Bimap VKeyGenesis VKey)
forall s a. HasDelegationMap s a => Lens' s a
Lens' DIState (Bimap VKeyGenesis VKey)
delegationMap) (DIState
dis DIState
-> Getting (Map VKeyGenesis Slot) DIState (Map VKeyGenesis Slot)
-> Map VKeyGenesis Slot
forall s a. s -> Getting a s a -> a
^. Getting (Map VKeyGenesis Slot) DIState (Map VKeyGenesis Slot)
forall s a. HasLastDelegation s a => Lens' s a
Lens' DIState (Map VKeyGenesis Slot)
lastDelegation))
( \DIState
dis DState
dss ->
DIState
dis
DIState -> (DIState -> DIState) -> DIState
forall a b. a -> (a -> b) -> b
& (Bimap VKeyGenesis VKey -> Identity (Bimap VKeyGenesis VKey))
-> DIState -> Identity DIState
forall s a. HasDelegationMap s a => Lens' s a
Lens' DIState (Bimap VKeyGenesis VKey)
delegationMap
((Bimap VKeyGenesis VKey -> Identity (Bimap VKeyGenesis VKey))
-> DIState -> Identity DIState)
-> Bimap VKeyGenesis VKey -> DIState -> DIState
forall s t a b. ASetter s t a b -> b -> s -> t
.~ DState
dss
DState
-> Getting (Bimap VKeyGenesis VKey) DState (Bimap VKeyGenesis VKey)
-> Bimap VKeyGenesis VKey
forall s a. s -> Getting a s a -> a
^. Getting (Bimap VKeyGenesis VKey) DState (Bimap VKeyGenesis VKey)
forall s a. HasDelegationMap s a => Lens' s a
Lens' DState (Bimap VKeyGenesis VKey)
delegationMap
DIState -> (DIState -> DIState) -> DIState
forall a b. a -> (a -> b) -> b
& (Map VKeyGenesis Slot -> Identity (Map VKeyGenesis Slot))
-> DIState -> Identity DIState
forall s a. HasLastDelegation s a => Lens' s a
Lens' DIState (Map VKeyGenesis Slot)
lastDelegation
((Map VKeyGenesis Slot -> Identity (Map VKeyGenesis Slot))
-> DIState -> Identity DIState)
-> Map VKeyGenesis Slot -> DIState -> DIState
forall s t a b. ASetter s t a b -> b -> s -> t
.~ DState
dss
DState
-> Getting (Map VKeyGenesis Slot) DState (Map VKeyGenesis Slot)
-> Map VKeyGenesis Slot
forall s a. s -> Getting a s a -> a
^. Getting (Map VKeyGenesis Slot) DState (Map VKeyGenesis Slot)
forall s a. HasLastDelegation s a => Lens' s a
Lens' DState (Map VKeyGenesis Slot)
lastDelegation
)
data SDELEG deriving (Typeable SDELEG
Typeable SDELEG =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SDELEG -> c SDELEG)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SDELEG)
-> (SDELEG -> Constr)
-> (SDELEG -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SDELEG))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SDELEG))
-> ((forall b. Data b => b -> b) -> SDELEG -> SDELEG)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SDELEG -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SDELEG -> r)
-> (forall u. (forall d. Data d => d -> u) -> SDELEG -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SDELEG -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SDELEG -> m SDELEG)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SDELEG -> m SDELEG)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SDELEG -> m SDELEG)
-> Data SDELEG
SDELEG -> Constr
SDELEG -> DataType
(forall b. Data b => b -> b) -> SDELEG -> SDELEG
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SDELEG -> u
forall u. (forall d. Data d => d -> u) -> SDELEG -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SDELEG -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SDELEG -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SDELEG -> m SDELEG
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SDELEG -> m SDELEG
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SDELEG
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SDELEG -> c SDELEG
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SDELEG)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SDELEG)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SDELEG -> c SDELEG
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SDELEG -> c SDELEG
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SDELEG
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SDELEG
$ctoConstr :: SDELEG -> Constr
toConstr :: SDELEG -> Constr
$cdataTypeOf :: SDELEG -> DataType
dataTypeOf :: SDELEG -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SDELEG)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SDELEG)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SDELEG)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SDELEG)
$cgmapT :: (forall b. Data b => b -> b) -> SDELEG -> SDELEG
gmapT :: (forall b. Data b => b -> b) -> SDELEG -> SDELEG
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SDELEG -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SDELEG -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SDELEG -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SDELEG -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SDELEG -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> SDELEG -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SDELEG -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SDELEG -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SDELEG -> m SDELEG
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SDELEG -> m SDELEG
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SDELEG -> m SDELEG
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SDELEG -> m SDELEG
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SDELEG -> m SDELEG
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SDELEG -> m SDELEG
Data)
data EpochDiff = EpochDiff {EpochDiff -> Epoch
currentEpoch :: Epoch, EpochDiff -> Epoch
certEpoch :: Epoch}
deriving (EpochDiff -> EpochDiff -> Bool
(EpochDiff -> EpochDiff -> Bool)
-> (EpochDiff -> EpochDiff -> Bool) -> Eq EpochDiff
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EpochDiff -> EpochDiff -> Bool
== :: EpochDiff -> EpochDiff -> Bool
$c/= :: EpochDiff -> EpochDiff -> Bool
/= :: EpochDiff -> EpochDiff -> Bool
Eq, Int -> EpochDiff -> ShowS
[EpochDiff] -> ShowS
EpochDiff -> String
(Int -> EpochDiff -> ShowS)
-> (EpochDiff -> String)
-> ([EpochDiff] -> ShowS)
-> Show EpochDiff
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EpochDiff -> ShowS
showsPrec :: Int -> EpochDiff -> ShowS
$cshow :: EpochDiff -> String
show :: EpochDiff -> String
$cshowList :: [EpochDiff] -> ShowS
showList :: [EpochDiff] -> ShowS
Show, Typeable EpochDiff
Typeable EpochDiff =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EpochDiff -> c EpochDiff)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EpochDiff)
-> (EpochDiff -> Constr)
-> (EpochDiff -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EpochDiff))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EpochDiff))
-> ((forall b. Data b => b -> b) -> EpochDiff -> EpochDiff)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r)
-> (forall u. (forall d. Data d => d -> u) -> EpochDiff -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> EpochDiff -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff)
-> Data EpochDiff
EpochDiff -> Constr
EpochDiff -> DataType
(forall b. Data b => b -> b) -> EpochDiff -> EpochDiff
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> EpochDiff -> u
forall u. (forall d. Data d => d -> u) -> EpochDiff -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EpochDiff
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EpochDiff -> c EpochDiff
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EpochDiff)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EpochDiff)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EpochDiff -> c EpochDiff
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EpochDiff -> c EpochDiff
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EpochDiff
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EpochDiff
$ctoConstr :: EpochDiff -> Constr
toConstr :: EpochDiff -> Constr
$cdataTypeOf :: EpochDiff -> DataType
dataTypeOf :: EpochDiff -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EpochDiff)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EpochDiff)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EpochDiff)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EpochDiff)
$cgmapT :: (forall b. Data b => b -> b) -> EpochDiff -> EpochDiff
gmapT :: (forall b. Data b => b -> b) -> EpochDiff -> EpochDiff
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EpochDiff -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EpochDiff -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> EpochDiff -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EpochDiff -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EpochDiff -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EpochDiff -> m EpochDiff
Data, (forall x. EpochDiff -> Rep EpochDiff x)
-> (forall x. Rep EpochDiff x -> EpochDiff) -> Generic EpochDiff
forall x. Rep EpochDiff x -> EpochDiff
forall x. EpochDiff -> Rep EpochDiff x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. EpochDiff -> Rep EpochDiff x
from :: forall x. EpochDiff -> Rep EpochDiff x
$cto :: forall x. Rep EpochDiff x -> EpochDiff
to :: forall x. Rep EpochDiff x -> EpochDiff
Generic, Context -> EpochDiff -> IO (Maybe ThunkInfo)
Proxy EpochDiff -> String
(Context -> EpochDiff -> IO (Maybe ThunkInfo))
-> (Context -> EpochDiff -> IO (Maybe ThunkInfo))
-> (Proxy EpochDiff -> String)
-> NoThunks EpochDiff
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> EpochDiff -> IO (Maybe ThunkInfo)
noThunks :: Context -> EpochDiff -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> EpochDiff -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> EpochDiff -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy EpochDiff -> String
showTypeOf :: Proxy EpochDiff -> String
NoThunks)
data SdelegPredicateFailure
= IsNotGenesisKey
| EpochInThePast EpochDiff
| EpochPastNextEpoch EpochDiff
| HasAlreadyDelegated
| IsAlreadyScheduled
| DoesNotVerify
deriving (SdelegPredicateFailure -> SdelegPredicateFailure -> Bool
(SdelegPredicateFailure -> SdelegPredicateFailure -> Bool)
-> (SdelegPredicateFailure -> SdelegPredicateFailure -> Bool)
-> Eq SdelegPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SdelegPredicateFailure -> SdelegPredicateFailure -> Bool
== :: SdelegPredicateFailure -> SdelegPredicateFailure -> Bool
$c/= :: SdelegPredicateFailure -> SdelegPredicateFailure -> Bool
/= :: SdelegPredicateFailure -> SdelegPredicateFailure -> Bool
Eq, Int -> SdelegPredicateFailure -> ShowS
[SdelegPredicateFailure] -> ShowS
SdelegPredicateFailure -> String
(Int -> SdelegPredicateFailure -> ShowS)
-> (SdelegPredicateFailure -> String)
-> ([SdelegPredicateFailure] -> ShowS)
-> Show SdelegPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SdelegPredicateFailure -> ShowS
showsPrec :: Int -> SdelegPredicateFailure -> ShowS
$cshow :: SdelegPredicateFailure -> String
show :: SdelegPredicateFailure -> String
$cshowList :: [SdelegPredicateFailure] -> ShowS
showList :: [SdelegPredicateFailure] -> ShowS
Show, Typeable SdelegPredicateFailure
Typeable SdelegPredicateFailure =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegPredicateFailure
-> c SdelegPredicateFailure)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegPredicateFailure)
-> (SdelegPredicateFailure -> Constr)
-> (SdelegPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegPredicateFailure))
-> ((forall b. Data b => b -> b)
-> SdelegPredicateFailure -> SdelegPredicateFailure)
-> (forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r)
-> (forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r)
-> (forall u.
(forall d. Data d => d -> u) -> SdelegPredicateFailure -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> SdelegPredicateFailure -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure)
-> Data SdelegPredicateFailure
SdelegPredicateFailure -> Constr
SdelegPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> SdelegPredicateFailure -> SdelegPredicateFailure
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> SdelegPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> SdelegPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegPredicateFailure
-> c SdelegPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegPredicateFailure
-> c SdelegPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegPredicateFailure
-> c SdelegPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegPredicateFailure
$ctoConstr :: SdelegPredicateFailure -> Constr
toConstr :: SdelegPredicateFailure -> Constr
$cdataTypeOf :: SdelegPredicateFailure -> DataType
dataTypeOf :: SdelegPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> SdelegPredicateFailure -> SdelegPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> SdelegPredicateFailure -> SdelegPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegPredicateFailure
-> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> SdelegPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> SdelegPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SdelegPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SdelegPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegPredicateFailure -> m SdelegPredicateFailure
Data, (forall x. SdelegPredicateFailure -> Rep SdelegPredicateFailure x)
-> (forall x.
Rep SdelegPredicateFailure x -> SdelegPredicateFailure)
-> Generic SdelegPredicateFailure
forall x. Rep SdelegPredicateFailure x -> SdelegPredicateFailure
forall x. SdelegPredicateFailure -> Rep SdelegPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SdelegPredicateFailure -> Rep SdelegPredicateFailure x
from :: forall x. SdelegPredicateFailure -> Rep SdelegPredicateFailure x
$cto :: forall x. Rep SdelegPredicateFailure x -> SdelegPredicateFailure
to :: forall x. Rep SdelegPredicateFailure x -> SdelegPredicateFailure
Generic, Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
Proxy SdelegPredicateFailure -> String
(Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy SdelegPredicateFailure -> String)
-> NoThunks SdelegPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> SdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy SdelegPredicateFailure -> String
showTypeOf :: Proxy SdelegPredicateFailure -> String
NoThunks)
instance STS SDELEG where
type State SDELEG = DSState
type Signal SDELEG = DCert
type Environment SDELEG = DSEnv
type PredicateFailure SDELEG = SdelegPredicateFailure
initialRules :: [InitialRule SDELEG]
initialRules =
[ DSState -> F (Clause SDELEG 'Initial) DSState
forall a. a -> F (Clause SDELEG 'Initial) a
forall (m :: * -> *) a. Monad m => a -> m a
return
DSState
{ _dSStateScheduledDelegations :: [(Slot, (VKeyGenesis, VKey))]
_dSStateScheduledDelegations = []
, _dSStateKeyEpochDelegations :: Set (Epoch, VKeyGenesis)
_dSStateKeyEpochDelegations = Set (Epoch, VKeyGenesis)
forall a. Set a
Set.empty
}
]
transitionRules :: [TransitionRule SDELEG]
transitionRules =
[ do
TRC (Environment SDELEG
env, State SDELEG
st, Signal SDELEG
cert) <- Rule SDELEG 'Transition (RuleContext 'Transition SDELEG)
F (Clause SDELEG 'Transition) (TRC SDELEG)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
VKey -> (VKey, Epoch) -> Sig (VKey, Epoch) -> Bool
forall a. Eq a => VKey -> a -> Sig a -> Bool
verify
(VKeyGenesis -> VKey
unVKeyGenesis (VKeyGenesis -> VKey) -> VKeyGenesis -> VKey
forall a b. (a -> b) -> a -> b
$ DCert -> VKeyGenesis
delegator Signal SDELEG
DCert
cert)
(DCert -> (VKey, Epoch)
dbody Signal SDELEG
DCert
cert)
(DCert -> Sig (VKey, Epoch)
signature Signal SDELEG
DCert
cert)
Bool -> PredicateFailure SDELEG -> Rule SDELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure SDELEG
SdelegPredicateFailure
DoesNotVerify
DSState -> DCert -> Bool
notAlreadyDelegated State SDELEG
DSState
st Signal SDELEG
DCert
cert Bool -> PredicateFailure SDELEG -> Rule SDELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure SDELEG
SdelegPredicateFailure
HasAlreadyDelegated
let d :: SlotCount
d = BlockCount -> SlotCount
liveAfter (Environment SDELEG
DSEnv
env DSEnv -> Getting BlockCount DSEnv BlockCount -> BlockCount
forall s a. s -> Getting a s a -> a
^. Getting BlockCount DSEnv BlockCount
forall s a. HasK s a => Lens' s a
Lens' DSEnv BlockCount
k)
SlotCount -> DSEnv -> DSState -> DCert -> Bool
notAlreadyScheduled SlotCount
d Environment SDELEG
DSEnv
env State SDELEG
DSState
st Signal SDELEG
DCert
cert Bool -> PredicateFailure SDELEG -> Rule SDELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure SDELEG
SdelegPredicateFailure
IsAlreadyScheduled
VKeyGenesis -> Set VKeyGenesis -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Signal SDELEG
DCert
cert DCert -> Getting VKeyGenesis DCert VKeyGenesis -> VKeyGenesis
forall s a. s -> Getting a s a -> a
^. (DCert -> (VKeyGenesis, VKey))
-> SimpleGetter DCert (VKeyGenesis, VKey)
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> (VKeyGenesis, VKey)
dwho Getting VKeyGenesis DCert (VKeyGenesis, VKey)
-> ((VKeyGenesis -> Const VKeyGenesis VKeyGenesis)
-> (VKeyGenesis, VKey) -> Const VKeyGenesis (VKeyGenesis, VKey))
-> Getting VKeyGenesis DCert VKeyGenesis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VKeyGenesis -> Const VKeyGenesis VKeyGenesis)
-> (VKeyGenesis, VKey) -> Const VKeyGenesis (VKeyGenesis, VKey)
forall s t a b. Field1 s t a b => Lens s t a b
Lens
(VKeyGenesis, VKey) (VKeyGenesis, VKey) VKeyGenesis VKeyGenesis
_1) (Environment SDELEG
DSEnv
env DSEnv
-> Getting (Set VKeyGenesis) DSEnv (Set VKeyGenesis)
-> Set VKeyGenesis
forall s a. s -> Getting a s a -> a
^. Getting (Set VKeyGenesis) DSEnv (Set VKeyGenesis)
forall s a. HasAllowedDelegators s a => Lens' s a
Lens' DSEnv (Set VKeyGenesis)
allowedDelegators) Bool -> PredicateFailure SDELEG -> Rule SDELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure SDELEG
SdelegPredicateFailure
IsNotGenesisKey
Environment SDELEG
DSEnv
env
DSEnv -> Getting Epoch DSEnv Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. Getting Epoch DSEnv Epoch
forall s a. HasEpoch s a => Lens' s a
Lens' DSEnv Epoch
epoch
Epoch -> Epoch -> Bool
forall a. Ord a => a -> a -> Bool
<= Signal SDELEG
DCert
cert
DCert -> Getting Epoch DCert Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. (DCert -> Epoch) -> SimpleGetter DCert Epoch
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch
Bool -> PredicateFailure SDELEG -> Rule SDELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! EpochDiff -> SdelegPredicateFailure
EpochInThePast
EpochDiff
{ currentEpoch :: Epoch
currentEpoch = Environment SDELEG
DSEnv
env DSEnv -> Getting Epoch DSEnv Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. Getting Epoch DSEnv Epoch
forall s a. HasEpoch s a => Lens' s a
Lens' DSEnv Epoch
epoch
, certEpoch :: Epoch
certEpoch = Signal SDELEG
DCert
cert DCert -> Getting Epoch DCert Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. (DCert -> Epoch) -> SimpleGetter DCert Epoch
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch
}
Signal SDELEG
DCert
cert
DCert -> Getting Epoch DCert Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. (DCert -> Epoch) -> SimpleGetter DCert Epoch
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch
Epoch -> Epoch -> Bool
forall a. Ord a => a -> a -> Bool
<= Environment SDELEG
DSEnv
env
DSEnv -> Getting Epoch DSEnv Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. Getting Epoch DSEnv Epoch
forall s a. HasEpoch s a => Lens' s a
Lens' DSEnv Epoch
epoch
Epoch -> Epoch -> Epoch
forall a. Num a => a -> a -> a
+ Epoch
1
Bool -> PredicateFailure SDELEG -> Rule SDELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! EpochDiff -> SdelegPredicateFailure
EpochPastNextEpoch
EpochDiff
{ currentEpoch :: Epoch
currentEpoch = Environment SDELEG
DSEnv
env DSEnv -> Getting Epoch DSEnv Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. Getting Epoch DSEnv Epoch
forall s a. HasEpoch s a => Lens' s a
Lens' DSEnv Epoch
epoch
, certEpoch :: Epoch
certEpoch = Signal SDELEG
DCert
cert DCert -> Getting Epoch DCert Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. (DCert -> Epoch) -> SimpleGetter DCert Epoch
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch
}
DSState -> F (Clause SDELEG 'Transition) DSState
forall a. a -> F (Clause SDELEG 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return (DSState -> F (Clause SDELEG 'Transition) DSState)
-> DSState -> F (Clause SDELEG 'Transition) DSState
forall a b. (a -> b) -> a -> b
$
State SDELEG
DSState
st
DSState -> (DSState -> DSState) -> DSState
forall a b. a -> (a -> b) -> b
& ([(Slot, (VKeyGenesis, VKey))]
-> Identity [(Slot, (VKeyGenesis, VKey))])
-> DSState -> Identity DSState
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DSState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations
(([(Slot, (VKeyGenesis, VKey))]
-> Identity [(Slot, (VKeyGenesis, VKey))])
-> DSState -> Identity DSState)
-> [(Slot, (VKeyGenesis, VKey))] -> DSState -> DSState
forall a s t. Monoid a => ASetter s t a a -> a -> s -> t
<>~ [
( (Environment SDELEG
DSEnv
env DSEnv -> Getting Slot DSEnv Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot DSEnv Slot
forall s a. HasSlot s a => Lens' s a
Lens' DSEnv Slot
slot) Slot -> SlotCount -> Slot
`addSlot` SlotCount
d
, Signal SDELEG
DCert
cert DCert
-> Getting (VKeyGenesis, VKey) DCert (VKeyGenesis, VKey)
-> (VKeyGenesis, VKey)
forall s a. s -> Getting a s a -> a
^. (DCert -> (VKeyGenesis, VKey))
-> SimpleGetter DCert (VKeyGenesis, VKey)
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> (VKeyGenesis, VKey)
dwho
)
]
DSState -> (DSState -> DSState) -> DSState
forall a b. a -> (a -> b) -> b
& (Set (Epoch, VKeyGenesis) -> Identity (Set (Epoch, VKeyGenesis)))
-> DSState -> Identity DSState
forall s a. HasKeyEpochDelegations s a => Lens' s a
Lens' DSState (Set (Epoch, VKeyGenesis))
keyEpochDelegations ((Set (Epoch, VKeyGenesis) -> Identity (Set (Epoch, VKeyGenesis)))
-> DSState -> Identity DSState)
-> (Set (Epoch, VKeyGenesis) -> Set (Epoch, VKeyGenesis))
-> DSState
-> DSState
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Epoch, VKeyGenesis)
-> Set (Epoch, VKeyGenesis) -> Set (Epoch, VKeyGenesis)
forall a. Ord a => a -> Set a -> Set a
Set.insert (DCert -> (Epoch, VKeyGenesis)
epochDelegator Signal SDELEG
DCert
cert)
]
where
notAlreadyDelegated :: DSState -> DCert -> Bool
notAlreadyDelegated :: DSState -> DCert -> Bool
notAlreadyDelegated DSState
st DCert
cert =
(Epoch, VKeyGenesis) -> Set (Epoch, VKeyGenesis) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember (DCert -> (Epoch, VKeyGenesis)
epochDelegator DCert
cert) (DSState
st DSState
-> Getting
(Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
-> Set (Epoch, VKeyGenesis)
forall s a. s -> Getting a s a -> a
^. Getting
(Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
forall s a. HasKeyEpochDelegations s a => Lens' s a
Lens' DSState (Set (Epoch, VKeyGenesis))
keyEpochDelegations)
epochDelegator :: DCert -> (Epoch, VKeyGenesis)
epochDelegator :: DCert -> (Epoch, VKeyGenesis)
epochDelegator DCert
cert = (DCert
cert DCert -> Getting Epoch DCert Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. (DCert -> Epoch) -> SimpleGetter DCert Epoch
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> Epoch
depoch, DCert
cert DCert -> Getting VKeyGenesis DCert VKeyGenesis -> VKeyGenesis
forall s a. s -> Getting a s a -> a
^. (DCert -> (VKeyGenesis, VKey))
-> SimpleGetter DCert (VKeyGenesis, VKey)
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> (VKeyGenesis, VKey)
dwho Getting VKeyGenesis DCert (VKeyGenesis, VKey)
-> ((VKeyGenesis -> Const VKeyGenesis VKeyGenesis)
-> (VKeyGenesis, VKey) -> Const VKeyGenesis (VKeyGenesis, VKey))
-> Getting VKeyGenesis DCert VKeyGenesis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VKeyGenesis -> Const VKeyGenesis VKeyGenesis)
-> (VKeyGenesis, VKey) -> Const VKeyGenesis (VKeyGenesis, VKey)
forall s t a b. Field1 s t a b => Lens s t a b
Lens
(VKeyGenesis, VKey) (VKeyGenesis, VKey) VKeyGenesis VKeyGenesis
_1)
notAlreadyScheduled :: SlotCount -> DSEnv -> DSState -> DCert -> Bool
notAlreadyScheduled :: SlotCount -> DSEnv -> DSState -> DCert -> Bool
notAlreadyScheduled SlotCount
d DSEnv
env DSState
st DCert
cert =
(Slot, VKeyGenesis) -> [(Slot, VKeyGenesis)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
List.notElem
((DSEnv
env DSEnv -> Getting Slot DSEnv Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot DSEnv Slot
forall s a. HasSlot s a => Lens' s a
Lens' DSEnv Slot
slot) Slot -> SlotCount -> Slot
`addSlot` SlotCount
d, DCert
cert DCert -> Getting VKeyGenesis DCert VKeyGenesis -> VKeyGenesis
forall s a. s -> Getting a s a -> a
^. (DCert -> (VKeyGenesis, VKey))
-> SimpleGetter DCert (VKeyGenesis, VKey)
forall s a. (s -> a) -> SimpleGetter s a
to DCert -> (VKeyGenesis, VKey)
dwho Getting VKeyGenesis DCert (VKeyGenesis, VKey)
-> ((VKeyGenesis -> Const VKeyGenesis VKeyGenesis)
-> (VKeyGenesis, VKey) -> Const VKeyGenesis (VKeyGenesis, VKey))
-> Getting VKeyGenesis DCert VKeyGenesis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VKeyGenesis -> Const VKeyGenesis VKeyGenesis)
-> (VKeyGenesis, VKey) -> Const VKeyGenesis (VKeyGenesis, VKey)
forall s t a b. Field1 s t a b => Lens s t a b
Lens
(VKeyGenesis, VKey) (VKeyGenesis, VKey) VKeyGenesis VKeyGenesis
_1)
(DSState
st DSState
-> Getting [(Slot, VKeyGenesis)] DSState [(Slot, VKeyGenesis)]
-> [(Slot, VKeyGenesis)]
forall s a. s -> Getting a s a -> a
^. ([(Slot, (VKeyGenesis, VKey))]
-> Const [(Slot, VKeyGenesis)] [(Slot, (VKeyGenesis, VKey))])
-> DSState -> Const [(Slot, VKeyGenesis)] DSState
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DSState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations (([(Slot, (VKeyGenesis, VKey))]
-> Const [(Slot, VKeyGenesis)] [(Slot, (VKeyGenesis, VKey))])
-> DSState -> Const [(Slot, VKeyGenesis)] DSState)
-> (([(Slot, VKeyGenesis)]
-> Const [(Slot, VKeyGenesis)] [(Slot, VKeyGenesis)])
-> [(Slot, (VKeyGenesis, VKey))]
-> Const [(Slot, VKeyGenesis)] [(Slot, (VKeyGenesis, VKey))])
-> Getting [(Slot, VKeyGenesis)] DSState [(Slot, VKeyGenesis)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Slot, (VKeyGenesis, VKey))] -> [(Slot, VKeyGenesis)])
-> SimpleGetter [(Slot, (VKeyGenesis, VKey))] [(Slot, VKeyGenesis)]
forall s a. (s -> a) -> SimpleGetter s a
to (((Slot, (VKeyGenesis, VKey)) -> (Slot, VKeyGenesis))
-> [(Slot, (VKeyGenesis, VKey))] -> [(Slot, VKeyGenesis)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Slot, (VKeyGenesis, VKey)) -> (Slot, VKeyGenesis))
-> [(Slot, (VKeyGenesis, VKey))] -> [(Slot, VKeyGenesis)])
-> ((Slot, (VKeyGenesis, VKey)) -> (Slot, VKeyGenesis))
-> [(Slot, (VKeyGenesis, VKey))]
-> [(Slot, VKeyGenesis)]
forall a b. (a -> b) -> a -> b
$ ((VKeyGenesis, VKey) -> VKeyGenesis)
-> (Slot, (VKeyGenesis, VKey)) -> (Slot, VKeyGenesis)
forall a b. (a -> b) -> (Slot, a) -> (Slot, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VKeyGenesis, VKey) -> VKeyGenesis
forall a b. (a, b) -> a
fst))
liveAfter :: BlockCount -> SlotCount
liveAfter :: BlockCount -> SlotCount
liveAfter BlockCount
bc = Word64 -> SlotCount
SlotCount (Word64 -> SlotCount) -> Word64 -> SlotCount
forall a b. (a -> b) -> a -> b
$ Word64
2 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* BlockCount -> Word64
unBlockCount BlockCount
bc
data AdelegPredicateFailure
= S_BeforeExistingDelegation
| S_NoLastDelegation
| S_AfterExistingDelegation
| S_AlreadyADelegateOf VKey VKeyGenesis
deriving (AdelegPredicateFailure -> AdelegPredicateFailure -> Bool
(AdelegPredicateFailure -> AdelegPredicateFailure -> Bool)
-> (AdelegPredicateFailure -> AdelegPredicateFailure -> Bool)
-> Eq AdelegPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AdelegPredicateFailure -> AdelegPredicateFailure -> Bool
== :: AdelegPredicateFailure -> AdelegPredicateFailure -> Bool
$c/= :: AdelegPredicateFailure -> AdelegPredicateFailure -> Bool
/= :: AdelegPredicateFailure -> AdelegPredicateFailure -> Bool
Eq, Int -> AdelegPredicateFailure -> ShowS
[AdelegPredicateFailure] -> ShowS
AdelegPredicateFailure -> String
(Int -> AdelegPredicateFailure -> ShowS)
-> (AdelegPredicateFailure -> String)
-> ([AdelegPredicateFailure] -> ShowS)
-> Show AdelegPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AdelegPredicateFailure -> ShowS
showsPrec :: Int -> AdelegPredicateFailure -> ShowS
$cshow :: AdelegPredicateFailure -> String
show :: AdelegPredicateFailure -> String
$cshowList :: [AdelegPredicateFailure] -> ShowS
showList :: [AdelegPredicateFailure] -> ShowS
Show, Typeable AdelegPredicateFailure
Typeable AdelegPredicateFailure =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegPredicateFailure
-> c AdelegPredicateFailure)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegPredicateFailure)
-> (AdelegPredicateFailure -> Constr)
-> (AdelegPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegPredicateFailure))
-> ((forall b. Data b => b -> b)
-> AdelegPredicateFailure -> AdelegPredicateFailure)
-> (forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r)
-> (forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r)
-> (forall u.
(forall d. Data d => d -> u) -> AdelegPredicateFailure -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> AdelegPredicateFailure -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure)
-> Data AdelegPredicateFailure
AdelegPredicateFailure -> Constr
AdelegPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> AdelegPredicateFailure -> AdelegPredicateFailure
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> AdelegPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> AdelegPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegPredicateFailure
-> c AdelegPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegPredicateFailure
-> c AdelegPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegPredicateFailure
-> c AdelegPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegPredicateFailure
$ctoConstr :: AdelegPredicateFailure -> Constr
toConstr :: AdelegPredicateFailure -> Constr
$cdataTypeOf :: AdelegPredicateFailure -> DataType
dataTypeOf :: AdelegPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> AdelegPredicateFailure -> AdelegPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> AdelegPredicateFailure -> AdelegPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegPredicateFailure
-> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> AdelegPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> AdelegPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> AdelegPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> AdelegPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegPredicateFailure -> m AdelegPredicateFailure
Data, (forall x. AdelegPredicateFailure -> Rep AdelegPredicateFailure x)
-> (forall x.
Rep AdelegPredicateFailure x -> AdelegPredicateFailure)
-> Generic AdelegPredicateFailure
forall x. Rep AdelegPredicateFailure x -> AdelegPredicateFailure
forall x. AdelegPredicateFailure -> Rep AdelegPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AdelegPredicateFailure -> Rep AdelegPredicateFailure x
from :: forall x. AdelegPredicateFailure -> Rep AdelegPredicateFailure x
$cto :: forall x. Rep AdelegPredicateFailure x -> AdelegPredicateFailure
to :: forall x. Rep AdelegPredicateFailure x -> AdelegPredicateFailure
Generic, Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
Proxy AdelegPredicateFailure -> String
(Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy AdelegPredicateFailure -> String)
-> NoThunks AdelegPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> AdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy AdelegPredicateFailure -> String
showTypeOf :: Proxy AdelegPredicateFailure -> String
NoThunks)
data ADELEG deriving (Typeable ADELEG
Typeable ADELEG =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ADELEG -> c ADELEG)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ADELEG)
-> (ADELEG -> Constr)
-> (ADELEG -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ADELEG))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ADELEG))
-> ((forall b. Data b => b -> b) -> ADELEG -> ADELEG)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ADELEG -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ADELEG -> r)
-> (forall u. (forall d. Data d => d -> u) -> ADELEG -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> ADELEG -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ADELEG -> m ADELEG)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ADELEG -> m ADELEG)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ADELEG -> m ADELEG)
-> Data ADELEG
ADELEG -> Constr
ADELEG -> DataType
(forall b. Data b => b -> b) -> ADELEG -> ADELEG
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ADELEG -> u
forall u. (forall d. Data d => d -> u) -> ADELEG -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ADELEG -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ADELEG -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ADELEG -> m ADELEG
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ADELEG -> m ADELEG
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ADELEG
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ADELEG -> c ADELEG
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ADELEG)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ADELEG)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ADELEG -> c ADELEG
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ADELEG -> c ADELEG
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ADELEG
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ADELEG
$ctoConstr :: ADELEG -> Constr
toConstr :: ADELEG -> Constr
$cdataTypeOf :: ADELEG -> DataType
dataTypeOf :: ADELEG -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ADELEG)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ADELEG)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ADELEG)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ADELEG)
$cgmapT :: (forall b. Data b => b -> b) -> ADELEG -> ADELEG
gmapT :: (forall b. Data b => b -> b) -> ADELEG -> ADELEG
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ADELEG -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ADELEG -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ADELEG -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ADELEG -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ADELEG -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> ADELEG -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ADELEG -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ADELEG -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ADELEG -> m ADELEG
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ADELEG -> m ADELEG
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ADELEG -> m ADELEG
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ADELEG -> m ADELEG
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ADELEG -> m ADELEG
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ADELEG -> m ADELEG
Data)
instance STS ADELEG where
type State ADELEG = DState
type Signal ADELEG = (Slot, (VKeyGenesis, VKey))
type Environment ADELEG = Set VKeyGenesis
type PredicateFailure ADELEG = AdelegPredicateFailure
initialRules :: [InitialRule ADELEG]
initialRules =
[ do
IRC Environment ADELEG
env <- Rule ADELEG 'Initial (RuleContext 'Initial ADELEG)
F (Clause ADELEG 'Initial) (IRC ADELEG)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
DState -> F (Clause ADELEG 'Initial) DState
forall a. a -> F (Clause ADELEG 'Initial) a
forall (m :: * -> *) a. Monad m => a -> m a
return
DState
{ _dStateDelegationMap :: Bimap VKeyGenesis VKey
_dStateDelegationMap =
[(VKeyGenesis, VKey)] -> Bimap VKeyGenesis VKey
forall a b. (Ord a, Ord b) => [(a, b)] -> Bimap a b
Bimap.fromList ([(VKeyGenesis, VKey)] -> Bimap VKeyGenesis VKey)
-> [(VKeyGenesis, VKey)] -> Bimap VKeyGenesis VKey
forall a b. (a -> b) -> a -> b
$
(VKeyGenesis -> (VKeyGenesis, VKey))
-> [VKeyGenesis] -> [(VKeyGenesis, VKey)]
forall a b. (a -> b) -> [a] -> [b]
map (\vkg :: VKeyGenesis
vkg@(VKeyGenesis VKey
key) -> (VKeyGenesis
vkg, VKey
key)) (Set VKeyGenesis -> [VKeyGenesis]
forall a. Set a -> [a]
Set.toList Set VKeyGenesis
Environment ADELEG
env)
, _dStateLastDelegation :: Map VKeyGenesis Slot
_dStateLastDelegation = (VKeyGenesis -> Slot) -> Set VKeyGenesis -> Map VKeyGenesis Slot
forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (Slot -> VKeyGenesis -> Slot
forall a b. a -> b -> a
const (Word64 -> Slot
Slot Word64
0)) Set VKeyGenesis
Environment ADELEG
env
}
]
transitionRules :: [TransitionRule ADELEG]
transitionRules =
[ do
TRC
( Environment ADELEG
_env
, DState
{ _dStateDelegationMap :: DState -> Bimap VKeyGenesis VKey
_dStateDelegationMap = Bimap VKeyGenesis VKey
dms
, _dStateLastDelegation :: DState -> Map VKeyGenesis Slot
_dStateLastDelegation = Map VKeyGenesis Slot
dws
}
, (Slot
s, (VKeyGenesis
vks, VKey
vkd))
) <-
Rule ADELEG 'Transition (RuleContext 'Transition ADELEG)
F (Clause ADELEG 'Transition) (TRC ADELEG)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
VKey
vkd VKey -> Set VKey -> Bool
forall a (f :: * -> *). (Eq a, Foldable f) => a -> f a -> Bool
∉ Bimap VKeyGenesis VKey -> Set (Range (Bimap VKeyGenesis VKey))
forall m. (Relation m, Ord (Range m)) => m -> Set (Range m)
range Bimap VKeyGenesis VKey
dms Bool -> PredicateFailure ADELEG -> Rule ADELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! VKey -> VKeyGenesis -> AdelegPredicateFailure
S_AlreadyADelegateOf VKey
vkd (Bimap VKeyGenesis VKey
dms Bimap VKeyGenesis VKey -> VKey -> VKeyGenesis
forall a b. (Ord a, Ord b) => Bimap a b -> b -> a
!> VKey
vkd)
case VKeyGenesis -> Map VKeyGenesis Slot -> Maybe Slot
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VKeyGenesis
vks Map VKeyGenesis Slot
dws of
Maybe Slot
Nothing -> () -> Rule ADELEG 'Transition ()
forall a. a -> F (Clause ADELEG 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just Slot
sp -> Slot
sp Slot -> Slot -> Bool
forall a. Ord a => a -> a -> Bool
< Slot
s Bool -> PredicateFailure ADELEG -> Rule ADELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure ADELEG
AdelegPredicateFailure
S_BeforeExistingDelegation
DState -> F (Clause ADELEG 'Transition) DState
forall a. a -> F (Clause ADELEG 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return (DState -> F (Clause ADELEG 'Transition) DState)
-> DState -> F (Clause ADELEG 'Transition) DState
forall a b. (a -> b) -> a -> b
$!
DState
{ _dStateDelegationMap :: Bimap VKeyGenesis VKey
_dStateDelegationMap = Bimap VKeyGenesis VKey
dms Bimap VKeyGenesis VKey
-> [(Domain (Bimap VKeyGenesis VKey),
Range (Bimap VKeyGenesis VKey))]
-> Bimap VKeyGenesis VKey
forall m (f :: * -> *).
(Relation m, Ord (Domain m), Ord (Range m), Foldable f) =>
m -> f (Domain m, Range m) -> m
forall (f :: * -> *).
(Ord (Domain (Bimap VKeyGenesis VKey)),
Ord (Range (Bimap VKeyGenesis VKey)), Foldable f) =>
Bimap VKeyGenesis VKey
-> f (Domain (Bimap VKeyGenesis VKey),
Range (Bimap VKeyGenesis VKey))
-> Bimap VKeyGenesis VKey
⨃ [(VKeyGenesis
vks, VKey
vkd)]
, _dStateLastDelegation :: Map VKeyGenesis Slot
_dStateLastDelegation = Map VKeyGenesis Slot
dws Map VKeyGenesis Slot
-> [(Domain (Map VKeyGenesis Slot), Range (Map VKeyGenesis Slot))]
-> Map VKeyGenesis Slot
forall m (f :: * -> *).
(Relation m, Ord (Domain m), Ord (Range m), Foldable f) =>
m -> f (Domain m, Range m) -> m
forall (f :: * -> *).
(Ord (Domain (Map VKeyGenesis Slot)),
Ord (Range (Map VKeyGenesis Slot)), Foldable f) =>
Map VKeyGenesis Slot
-> f (Domain (Map VKeyGenesis Slot), Range (Map VKeyGenesis Slot))
-> Map VKeyGenesis Slot
⨃ [(VKeyGenesis
vks, Slot
s)]
}
, do
TRC
( Environment ADELEG
_env
, st :: State ADELEG
st@DState
{ _dStateDelegationMap :: DState -> Bimap VKeyGenesis VKey
_dStateDelegationMap = Bimap VKeyGenesis VKey
dms
, _dStateLastDelegation :: DState -> Map VKeyGenesis Slot
_dStateLastDelegation = Map VKeyGenesis Slot
dws
}
, (Slot
s, (VKeyGenesis
vks, VKey
vkd))
) <-
Rule ADELEG 'Transition (RuleContext 'Transition ADELEG)
F (Clause ADELEG 'Transition) (TRC ADELEG)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
if VKey
vkd VKey -> Set VKey -> Bool
forall a (f :: * -> *). (Eq a, Foldable f) => a -> f a -> Bool
∈ Bimap VKeyGenesis VKey -> Set (Range (Bimap VKeyGenesis VKey))
forall m. (Relation m, Ord (Range m)) => m -> Set (Range m)
range Bimap VKeyGenesis VKey
dms
then DState -> F (Clause ADELEG 'Transition) DState
forall a. a -> F (Clause ADELEG 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return State ADELEG
DState
st
else do
case VKeyGenesis -> Map VKeyGenesis Slot -> Maybe Slot
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VKeyGenesis
vks Map VKeyGenesis Slot
dws of
Just Slot
sp -> Slot
sp Slot -> Slot -> Bool
forall a. Ord a => a -> a -> Bool
>= Slot
s Bool -> PredicateFailure ADELEG -> Rule ADELEG 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure ADELEG
AdelegPredicateFailure
S_AfterExistingDelegation
Maybe Slot
Nothing ->
String -> Rule ADELEG 'Transition ()
forall a. HasCallStack => String -> a
error (String -> Rule ADELEG 'Transition ())
-> String -> Rule ADELEG 'Transition ()
forall a b. (a -> b) -> a -> b
$
String
"This can't happen since otherwise "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"the previous rule would have been triggered."
DState -> F (Clause ADELEG 'Transition) DState
forall a. a -> F (Clause ADELEG 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return State ADELEG
DState
st
]
data SDELEGS deriving (Typeable SDELEGS
Typeable SDELEGS =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SDELEGS -> c SDELEGS)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SDELEGS)
-> (SDELEGS -> Constr)
-> (SDELEGS -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SDELEGS))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SDELEGS))
-> ((forall b. Data b => b -> b) -> SDELEGS -> SDELEGS)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SDELEGS -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SDELEGS -> r)
-> (forall u. (forall d. Data d => d -> u) -> SDELEGS -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SDELEGS -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SDELEGS -> m SDELEGS)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SDELEGS -> m SDELEGS)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SDELEGS -> m SDELEGS)
-> Data SDELEGS
SDELEGS -> Constr
SDELEGS -> DataType
(forall b. Data b => b -> b) -> SDELEGS -> SDELEGS
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SDELEGS -> u
forall u. (forall d. Data d => d -> u) -> SDELEGS -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SDELEGS -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SDELEGS -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SDELEGS -> m SDELEGS
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SDELEGS -> m SDELEGS
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SDELEGS
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SDELEGS -> c SDELEGS
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SDELEGS)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SDELEGS)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SDELEGS -> c SDELEGS
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SDELEGS -> c SDELEGS
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SDELEGS
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SDELEGS
$ctoConstr :: SDELEGS -> Constr
toConstr :: SDELEGS -> Constr
$cdataTypeOf :: SDELEGS -> DataType
dataTypeOf :: SDELEGS -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SDELEGS)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SDELEGS)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SDELEGS)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SDELEGS)
$cgmapT :: (forall b. Data b => b -> b) -> SDELEGS -> SDELEGS
gmapT :: (forall b. Data b => b -> b) -> SDELEGS -> SDELEGS
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SDELEGS -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SDELEGS -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SDELEGS -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SDELEGS -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SDELEGS -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> SDELEGS -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SDELEGS -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SDELEGS -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SDELEGS -> m SDELEGS
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SDELEGS -> m SDELEGS
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SDELEGS -> m SDELEGS
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SDELEGS -> m SDELEGS
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SDELEGS -> m SDELEGS
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SDELEGS -> m SDELEGS
Data)
data SdelegsPredicateFailure
= SDelegFailure (PredicateFailure SDELEG)
deriving (SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
(SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool)
-> (SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool)
-> Eq SdelegsPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
== :: SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
$c/= :: SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
/= :: SdelegsPredicateFailure -> SdelegsPredicateFailure -> Bool
Eq, Int -> SdelegsPredicateFailure -> ShowS
[SdelegsPredicateFailure] -> ShowS
SdelegsPredicateFailure -> String
(Int -> SdelegsPredicateFailure -> ShowS)
-> (SdelegsPredicateFailure -> String)
-> ([SdelegsPredicateFailure] -> ShowS)
-> Show SdelegsPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SdelegsPredicateFailure -> ShowS
showsPrec :: Int -> SdelegsPredicateFailure -> ShowS
$cshow :: SdelegsPredicateFailure -> String
show :: SdelegsPredicateFailure -> String
$cshowList :: [SdelegsPredicateFailure] -> ShowS
showList :: [SdelegsPredicateFailure] -> ShowS
Show, Typeable SdelegsPredicateFailure
Typeable SdelegsPredicateFailure =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegsPredicateFailure
-> c SdelegsPredicateFailure)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegsPredicateFailure)
-> (SdelegsPredicateFailure -> Constr)
-> (SdelegsPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegsPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegsPredicateFailure))
-> ((forall b. Data b => b -> b)
-> SdelegsPredicateFailure -> SdelegsPredicateFailure)
-> (forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r)
-> (forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r)
-> (forall u.
(forall d. Data d => d -> u) -> SdelegsPredicateFailure -> [u])
-> (forall u.
Int
-> (forall d. Data d => d -> u) -> SdelegsPredicateFailure -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure)
-> Data SdelegsPredicateFailure
SdelegsPredicateFailure -> Constr
SdelegsPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> SdelegsPredicateFailure -> SdelegsPredicateFailure
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> SdelegsPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> SdelegsPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegsPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegsPredicateFailure
-> c SdelegsPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegsPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegsPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegsPredicateFailure
-> c SdelegsPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> SdelegsPredicateFailure
-> c SdelegsPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegsPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SdelegsPredicateFailure
$ctoConstr :: SdelegsPredicateFailure -> Constr
toConstr :: SdelegsPredicateFailure -> Constr
$cdataTypeOf :: SdelegsPredicateFailure -> DataType
dataTypeOf :: SdelegsPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegsPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SdelegsPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegsPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SdelegsPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> SdelegsPredicateFailure -> SdelegsPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> SdelegsPredicateFailure -> SdelegsPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> SdelegsPredicateFailure
-> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> SdelegsPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> SdelegsPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SdelegsPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> SdelegsPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> SdelegsPredicateFailure -> m SdelegsPredicateFailure
Data, (forall x.
SdelegsPredicateFailure -> Rep SdelegsPredicateFailure x)
-> (forall x.
Rep SdelegsPredicateFailure x -> SdelegsPredicateFailure)
-> Generic SdelegsPredicateFailure
forall x. Rep SdelegsPredicateFailure x -> SdelegsPredicateFailure
forall x. SdelegsPredicateFailure -> Rep SdelegsPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SdelegsPredicateFailure -> Rep SdelegsPredicateFailure x
from :: forall x. SdelegsPredicateFailure -> Rep SdelegsPredicateFailure x
$cto :: forall x. Rep SdelegsPredicateFailure x -> SdelegsPredicateFailure
to :: forall x. Rep SdelegsPredicateFailure x -> SdelegsPredicateFailure
Generic, Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
Proxy SdelegsPredicateFailure -> String
(Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy SdelegsPredicateFailure -> String)
-> NoThunks SdelegsPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> SdelegsPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy SdelegsPredicateFailure -> String
showTypeOf :: Proxy SdelegsPredicateFailure -> String
NoThunks)
instance STS SDELEGS where
type State SDELEGS = DSState
type Signal SDELEGS = [DCert]
type Environment SDELEGS = DSEnv
type PredicateFailure SDELEGS = SdelegsPredicateFailure
initialRules :: [InitialRule SDELEGS]
initialRules =
[ do
IRC Environment SDELEGS
env <- Rule SDELEGS 'Initial (RuleContext 'Initial SDELEGS)
F (Clause SDELEGS 'Initial) (IRC SDELEGS)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEG (RuleContext 'Initial SDELEG
-> Rule SDELEGS 'Initial (State SDELEG))
-> RuleContext 'Initial SDELEG
-> Rule SDELEGS 'Initial (State SDELEG)
forall a b. (a -> b) -> a -> b
$ Environment SDELEG -> IRC SDELEG
forall sts. Environment sts -> IRC sts
IRC Environment SDELEGS
Environment SDELEG
env
]
transitionRules :: [TransitionRule SDELEGS]
transitionRules =
[ do
TRC (Environment SDELEGS
env, State SDELEGS
st, Signal SDELEGS
sig) <- Rule SDELEGS 'Transition (RuleContext 'Transition SDELEGS)
F (Clause SDELEGS 'Transition) (TRC SDELEGS)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
case Signal SDELEGS
sig of
[] -> DSState -> F (Clause SDELEGS 'Transition) DSState
forall a. a -> F (Clause SDELEGS 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return State SDELEGS
DSState
st
(DCert
x : [DCert]
xs) -> do
DSState
dss' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEG (RuleContext 'Transition SDELEG
-> Rule SDELEGS 'Transition (State SDELEG))
-> RuleContext 'Transition SDELEG
-> Rule SDELEGS 'Transition (State SDELEG)
forall a b. (a -> b) -> a -> b
$ (Environment SDELEG, State SDELEG, Signal SDELEG) -> TRC SDELEG
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment SDELEGS
Environment SDELEG
env, State SDELEGS
State SDELEG
st, Signal SDELEG
DCert
x)
DSState
dss'' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEGS (RuleContext 'Transition SDELEGS -> TransitionRule SDELEGS)
-> RuleContext 'Transition SDELEGS -> TransitionRule SDELEGS
forall a b. (a -> b) -> a -> b
$ (Environment SDELEGS, State SDELEGS, Signal SDELEGS) -> TRC SDELEGS
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment SDELEGS
env, State SDELEGS
DSState
dss', [DCert]
Signal SDELEGS
xs)
DSState -> F (Clause SDELEGS 'Transition) DSState
forall a. a -> F (Clause SDELEGS 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return DSState
dss''
]
instance Embed SDELEG SDELEGS where
wrapFailed :: PredicateFailure SDELEG -> PredicateFailure SDELEGS
wrapFailed = PredicateFailure SDELEG -> PredicateFailure SDELEGS
PredicateFailure SDELEG -> SdelegsPredicateFailure
SDelegFailure
data ADELEGS deriving (Typeable ADELEGS
Typeable ADELEGS =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ADELEGS -> c ADELEGS)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ADELEGS)
-> (ADELEGS -> Constr)
-> (ADELEGS -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ADELEGS))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ADELEGS))
-> ((forall b. Data b => b -> b) -> ADELEGS -> ADELEGS)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ADELEGS -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ADELEGS -> r)
-> (forall u. (forall d. Data d => d -> u) -> ADELEGS -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> ADELEGS -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ADELEGS -> m ADELEGS)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ADELEGS -> m ADELEGS)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ADELEGS -> m ADELEGS)
-> Data ADELEGS
ADELEGS -> Constr
ADELEGS -> DataType
(forall b. Data b => b -> b) -> ADELEGS -> ADELEGS
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ADELEGS -> u
forall u. (forall d. Data d => d -> u) -> ADELEGS -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ADELEGS -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ADELEGS -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ADELEGS -> m ADELEGS
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ADELEGS -> m ADELEGS
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ADELEGS
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ADELEGS -> c ADELEGS
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ADELEGS)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ADELEGS)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ADELEGS -> c ADELEGS
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ADELEGS -> c ADELEGS
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ADELEGS
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ADELEGS
$ctoConstr :: ADELEGS -> Constr
toConstr :: ADELEGS -> Constr
$cdataTypeOf :: ADELEGS -> DataType
dataTypeOf :: ADELEGS -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ADELEGS)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ADELEGS)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ADELEGS)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ADELEGS)
$cgmapT :: (forall b. Data b => b -> b) -> ADELEGS -> ADELEGS
gmapT :: (forall b. Data b => b -> b) -> ADELEGS -> ADELEGS
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ADELEGS -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ADELEGS -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ADELEGS -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ADELEGS -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ADELEGS -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> ADELEGS -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ADELEGS -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ADELEGS -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ADELEGS -> m ADELEGS
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ADELEGS -> m ADELEGS
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ADELEGS -> m ADELEGS
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ADELEGS -> m ADELEGS
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ADELEGS -> m ADELEGS
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ADELEGS -> m ADELEGS
Data)
data AdelegsPredicateFailure
= ADelegFailure (PredicateFailure ADELEG)
deriving (AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
(AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool)
-> (AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool)
-> Eq AdelegsPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
== :: AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
$c/= :: AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
/= :: AdelegsPredicateFailure -> AdelegsPredicateFailure -> Bool
Eq, Int -> AdelegsPredicateFailure -> ShowS
[AdelegsPredicateFailure] -> ShowS
AdelegsPredicateFailure -> String
(Int -> AdelegsPredicateFailure -> ShowS)
-> (AdelegsPredicateFailure -> String)
-> ([AdelegsPredicateFailure] -> ShowS)
-> Show AdelegsPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AdelegsPredicateFailure -> ShowS
showsPrec :: Int -> AdelegsPredicateFailure -> ShowS
$cshow :: AdelegsPredicateFailure -> String
show :: AdelegsPredicateFailure -> String
$cshowList :: [AdelegsPredicateFailure] -> ShowS
showList :: [AdelegsPredicateFailure] -> ShowS
Show, Typeable AdelegsPredicateFailure
Typeable AdelegsPredicateFailure =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegsPredicateFailure
-> c AdelegsPredicateFailure)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegsPredicateFailure)
-> (AdelegsPredicateFailure -> Constr)
-> (AdelegsPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegsPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegsPredicateFailure))
-> ((forall b. Data b => b -> b)
-> AdelegsPredicateFailure -> AdelegsPredicateFailure)
-> (forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r)
-> (forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r)
-> (forall u.
(forall d. Data d => d -> u) -> AdelegsPredicateFailure -> [u])
-> (forall u.
Int
-> (forall d. Data d => d -> u) -> AdelegsPredicateFailure -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure)
-> Data AdelegsPredicateFailure
AdelegsPredicateFailure -> Constr
AdelegsPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> AdelegsPredicateFailure -> AdelegsPredicateFailure
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> AdelegsPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> AdelegsPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegsPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegsPredicateFailure
-> c AdelegsPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegsPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegsPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegsPredicateFailure
-> c AdelegsPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> AdelegsPredicateFailure
-> c AdelegsPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegsPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AdelegsPredicateFailure
$ctoConstr :: AdelegsPredicateFailure -> Constr
toConstr :: AdelegsPredicateFailure -> Constr
$cdataTypeOf :: AdelegsPredicateFailure -> DataType
dataTypeOf :: AdelegsPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegsPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AdelegsPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegsPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AdelegsPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> AdelegsPredicateFailure -> AdelegsPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> AdelegsPredicateFailure -> AdelegsPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> AdelegsPredicateFailure
-> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> AdelegsPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> AdelegsPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> AdelegsPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> AdelegsPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> AdelegsPredicateFailure -> m AdelegsPredicateFailure
Data, (forall x.
AdelegsPredicateFailure -> Rep AdelegsPredicateFailure x)
-> (forall x.
Rep AdelegsPredicateFailure x -> AdelegsPredicateFailure)
-> Generic AdelegsPredicateFailure
forall x. Rep AdelegsPredicateFailure x -> AdelegsPredicateFailure
forall x. AdelegsPredicateFailure -> Rep AdelegsPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AdelegsPredicateFailure -> Rep AdelegsPredicateFailure x
from :: forall x. AdelegsPredicateFailure -> Rep AdelegsPredicateFailure x
$cto :: forall x. Rep AdelegsPredicateFailure x -> AdelegsPredicateFailure
to :: forall x. Rep AdelegsPredicateFailure x -> AdelegsPredicateFailure
Generic, Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
Proxy AdelegsPredicateFailure -> String
(Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy AdelegsPredicateFailure -> String)
-> NoThunks AdelegsPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> AdelegsPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy AdelegsPredicateFailure -> String
showTypeOf :: Proxy AdelegsPredicateFailure -> String
NoThunks)
instance STS ADELEGS where
type State ADELEGS = DState
type Signal ADELEGS = [(Slot, (VKeyGenesis, VKey))]
type Environment ADELEGS = Set VKeyGenesis
type
PredicateFailure ADELEGS =
AdelegsPredicateFailure
initialRules :: [InitialRule ADELEGS]
initialRules =
[ do
IRC Environment ADELEGS
env <- Rule ADELEGS 'Initial (RuleContext 'Initial ADELEGS)
F (Clause ADELEGS 'Initial) (IRC ADELEGS)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @ADELEG (RuleContext 'Initial ADELEG
-> Rule ADELEGS 'Initial (State ADELEG))
-> RuleContext 'Initial ADELEG
-> Rule ADELEGS 'Initial (State ADELEG)
forall a b. (a -> b) -> a -> b
$ Environment ADELEG -> IRC ADELEG
forall sts. Environment sts -> IRC sts
IRC Environment ADELEGS
Environment ADELEG
env
]
transitionRules :: [TransitionRule ADELEGS]
transitionRules =
[ do
TRC (Environment ADELEGS
env, State ADELEGS
st, Signal ADELEGS
sig) <- Rule ADELEGS 'Transition (RuleContext 'Transition ADELEGS)
F (Clause ADELEGS 'Transition) (TRC ADELEGS)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
case Signal ADELEGS
sig of
[] -> DState -> F (Clause ADELEGS 'Transition) DState
forall a. a -> F (Clause ADELEGS 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return State ADELEGS
DState
st
((Slot, (VKeyGenesis, VKey))
x : [(Slot, (VKeyGenesis, VKey))]
xs) -> do
DState
ds' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @ADELEG (RuleContext 'Transition ADELEG
-> Rule ADELEGS 'Transition (State ADELEG))
-> RuleContext 'Transition ADELEG
-> Rule ADELEGS 'Transition (State ADELEG)
forall a b. (a -> b) -> a -> b
$ (Environment ADELEG, State ADELEG, Signal ADELEG) -> TRC ADELEG
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment ADELEGS
Environment ADELEG
env, State ADELEGS
State ADELEG
st, (Slot, (VKeyGenesis, VKey))
Signal ADELEG
x)
DState
ds'' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @ADELEGS (RuleContext 'Transition ADELEGS -> TransitionRule ADELEGS)
-> RuleContext 'Transition ADELEGS -> TransitionRule ADELEGS
forall a b. (a -> b) -> a -> b
$ (Environment ADELEGS, State ADELEGS, Signal ADELEGS) -> TRC ADELEGS
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment ADELEGS
env, State ADELEGS
DState
ds', [(Slot, (VKeyGenesis, VKey))]
Signal ADELEGS
xs)
DState -> F (Clause ADELEGS 'Transition) DState
forall a. a -> F (Clause ADELEGS 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return DState
ds''
]
instance Embed ADELEG ADELEGS where
wrapFailed :: PredicateFailure ADELEG -> PredicateFailure ADELEGS
wrapFailed = PredicateFailure ADELEG -> PredicateFailure ADELEGS
PredicateFailure ADELEG -> AdelegsPredicateFailure
ADelegFailure
data DELEG deriving (Typeable DELEG
Typeable DELEG =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DELEG -> c DELEG)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DELEG)
-> (DELEG -> Constr)
-> (DELEG -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DELEG))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DELEG))
-> ((forall b. Data b => b -> b) -> DELEG -> DELEG)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DELEG -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DELEG -> r)
-> (forall u. (forall d. Data d => d -> u) -> DELEG -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> DELEG -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DELEG -> m DELEG)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DELEG -> m DELEG)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DELEG -> m DELEG)
-> Data DELEG
DELEG -> Constr
DELEG -> DataType
(forall b. Data b => b -> b) -> DELEG -> DELEG
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DELEG -> u
forall u. (forall d. Data d => d -> u) -> DELEG -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DELEG -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DELEG -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DELEG -> m DELEG
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DELEG -> m DELEG
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DELEG
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DELEG -> c DELEG
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DELEG)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DELEG)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DELEG -> c DELEG
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DELEG -> c DELEG
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DELEG
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DELEG
$ctoConstr :: DELEG -> Constr
toConstr :: DELEG -> Constr
$cdataTypeOf :: DELEG -> DataType
dataTypeOf :: DELEG -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DELEG)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DELEG)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DELEG)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DELEG)
$cgmapT :: (forall b. Data b => b -> b) -> DELEG -> DELEG
gmapT :: (forall b. Data b => b -> b) -> DELEG -> DELEG
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DELEG -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DELEG -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DELEG -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DELEG -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DELEG -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> DELEG -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DELEG -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DELEG -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DELEG -> m DELEG
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DELEG -> m DELEG
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DELEG -> m DELEG
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DELEG -> m DELEG
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DELEG -> m DELEG
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DELEG -> m DELEG
Data)
data DelegPredicateFailure
= SDelegSFailure (PredicateFailure SDELEGS)
| ADelegSFailure (PredicateFailure ADELEGS)
deriving (DelegPredicateFailure -> DelegPredicateFailure -> Bool
(DelegPredicateFailure -> DelegPredicateFailure -> Bool)
-> (DelegPredicateFailure -> DelegPredicateFailure -> Bool)
-> Eq DelegPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DelegPredicateFailure -> DelegPredicateFailure -> Bool
== :: DelegPredicateFailure -> DelegPredicateFailure -> Bool
$c/= :: DelegPredicateFailure -> DelegPredicateFailure -> Bool
/= :: DelegPredicateFailure -> DelegPredicateFailure -> Bool
Eq, Int -> DelegPredicateFailure -> ShowS
[DelegPredicateFailure] -> ShowS
DelegPredicateFailure -> String
(Int -> DelegPredicateFailure -> ShowS)
-> (DelegPredicateFailure -> String)
-> ([DelegPredicateFailure] -> ShowS)
-> Show DelegPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DelegPredicateFailure -> ShowS
showsPrec :: Int -> DelegPredicateFailure -> ShowS
$cshow :: DelegPredicateFailure -> String
show :: DelegPredicateFailure -> String
$cshowList :: [DelegPredicateFailure] -> ShowS
showList :: [DelegPredicateFailure] -> ShowS
Show, Typeable DelegPredicateFailure
Typeable DelegPredicateFailure =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DelegPredicateFailure
-> c DelegPredicateFailure)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DelegPredicateFailure)
-> (DelegPredicateFailure -> Constr)
-> (DelegPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DelegPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DelegPredicateFailure))
-> ((forall b. Data b => b -> b)
-> DelegPredicateFailure -> DelegPredicateFailure)
-> (forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> DelegPredicateFailure
-> r)
-> (forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> DelegPredicateFailure
-> r)
-> (forall u.
(forall d. Data d => d -> u) -> DelegPredicateFailure -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> DelegPredicateFailure -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure)
-> Data DelegPredicateFailure
DelegPredicateFailure -> Constr
DelegPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> DelegPredicateFailure -> DelegPredicateFailure
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> DelegPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> DelegPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DelegPredicateFailure -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DelegPredicateFailure -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DelegPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DelegPredicateFailure
-> c DelegPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DelegPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DelegPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DelegPredicateFailure
-> c DelegPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DelegPredicateFailure
-> c DelegPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DelegPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DelegPredicateFailure
$ctoConstr :: DelegPredicateFailure -> Constr
toConstr :: DelegPredicateFailure -> Constr
$cdataTypeOf :: DelegPredicateFailure -> DataType
dataTypeOf :: DelegPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DelegPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DelegPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DelegPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DelegPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> DelegPredicateFailure -> DelegPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> DelegPredicateFailure -> DelegPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DelegPredicateFailure -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DelegPredicateFailure -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DelegPredicateFailure -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DelegPredicateFailure -> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> DelegPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> DelegPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> DelegPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> DelegPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DelegPredicateFailure -> m DelegPredicateFailure
Data, (forall x. DelegPredicateFailure -> Rep DelegPredicateFailure x)
-> (forall x. Rep DelegPredicateFailure x -> DelegPredicateFailure)
-> Generic DelegPredicateFailure
forall x. Rep DelegPredicateFailure x -> DelegPredicateFailure
forall x. DelegPredicateFailure -> Rep DelegPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DelegPredicateFailure -> Rep DelegPredicateFailure x
from :: forall x. DelegPredicateFailure -> Rep DelegPredicateFailure x
$cto :: forall x. Rep DelegPredicateFailure x -> DelegPredicateFailure
to :: forall x. Rep DelegPredicateFailure x -> DelegPredicateFailure
Generic, Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
Proxy DelegPredicateFailure -> String
(Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy DelegPredicateFailure -> String)
-> NoThunks DelegPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> DelegPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy DelegPredicateFailure -> String
showTypeOf :: Proxy DelegPredicateFailure -> String
NoThunks)
instance STS DELEG where
type State DELEG = DIState
type Signal DELEG = [DCert]
type Environment DELEG = DIEnv
type PredicateFailure DELEG = DelegPredicateFailure
initialRules :: [InitialRule DELEG]
initialRules =
[ do
IRC Environment DELEG
env <- Rule DELEG 'Initial (RuleContext 'Initial DELEG)
F (Clause DELEG 'Initial) (IRC DELEG)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
DState
initADelegsState <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @ADELEGS (RuleContext 'Initial ADELEGS
-> Rule DELEG 'Initial (State ADELEGS))
-> RuleContext 'Initial ADELEGS
-> Rule DELEG 'Initial (State ADELEGS)
forall a b. (a -> b) -> a -> b
$ Environment ADELEGS -> IRC ADELEGS
forall sts. Environment sts -> IRC sts
IRC (Environment DELEG
DSEnv
env DSEnv
-> Getting (Set VKeyGenesis) DSEnv (Set VKeyGenesis)
-> Set VKeyGenesis
forall s a. s -> Getting a s a -> a
^. Getting (Set VKeyGenesis) DSEnv (Set VKeyGenesis)
forall s a. HasAllowedDelegators s a => Lens' s a
Lens' DSEnv (Set VKeyGenesis)
allowedDelegators)
DSState
initSDelegsState <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEGS (RuleContext 'Initial SDELEGS
-> Rule DELEG 'Initial (State SDELEGS))
-> RuleContext 'Initial SDELEGS
-> Rule DELEG 'Initial (State SDELEGS)
forall a b. (a -> b) -> a -> b
$ Environment SDELEGS -> IRC SDELEGS
forall sts. Environment sts -> IRC sts
IRC Environment DELEG
Environment SDELEGS
env
DIState -> F (Clause DELEG 'Initial) DIState
forall a. a -> F (Clause DELEG 'Initial) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DIState -> F (Clause DELEG 'Initial) DIState)
-> DIState -> F (Clause DELEG 'Initial) DIState
forall a b. (a -> b) -> a -> b
$!
DIState
{ _dIStateDelegationMap :: Bimap VKeyGenesis VKey
_dIStateDelegationMap = DState
initADelegsState DState
-> Getting (Bimap VKeyGenesis VKey) DState (Bimap VKeyGenesis VKey)
-> Bimap VKeyGenesis VKey
forall s a. s -> Getting a s a -> a
^. Getting (Bimap VKeyGenesis VKey) DState (Bimap VKeyGenesis VKey)
forall s a. HasDelegationMap s a => Lens' s a
Lens' DState (Bimap VKeyGenesis VKey)
delegationMap
, _dIStateLastDelegation :: Map VKeyGenesis Slot
_dIStateLastDelegation = DState
initADelegsState DState
-> Getting (Map VKeyGenesis Slot) DState (Map VKeyGenesis Slot)
-> Map VKeyGenesis Slot
forall s a. s -> Getting a s a -> a
^. Getting (Map VKeyGenesis Slot) DState (Map VKeyGenesis Slot)
forall s a. HasLastDelegation s a => Lens' s a
Lens' DState (Map VKeyGenesis Slot)
lastDelegation
, _dIStateScheduledDelegations :: [(Slot, (VKeyGenesis, VKey))]
_dIStateScheduledDelegations = DSState
initSDelegsState DSState
-> Getting
[(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
-> [(Slot, (VKeyGenesis, VKey))]
forall s a. s -> Getting a s a -> a
^. Getting
[(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DSState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations
, _dIStateKeyEpochDelegations :: Set (Epoch, VKeyGenesis)
_dIStateKeyEpochDelegations = DSState
initSDelegsState DSState
-> Getting
(Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
-> Set (Epoch, VKeyGenesis)
forall s a. s -> Getting a s a -> a
^. Getting
(Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
forall s a. HasKeyEpochDelegations s a => Lens' s a
Lens' DSState (Set (Epoch, VKeyGenesis))
keyEpochDelegations
}
]
transitionRules :: [TransitionRule DELEG]
transitionRules =
[ do
TRC (Environment DELEG
env, State DELEG
st, Signal DELEG
sig) <- Rule DELEG 'Transition (RuleContext 'Transition DELEG)
F (Clause DELEG 'Transition) (TRC DELEG)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
DSState
sds <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEGS (RuleContext 'Transition SDELEGS
-> Rule DELEG 'Transition (State SDELEGS))
-> RuleContext 'Transition SDELEGS
-> Rule DELEG 'Transition (State SDELEGS)
forall a b. (a -> b) -> a -> b
$ (Environment SDELEGS, State SDELEGS, Signal SDELEGS) -> TRC SDELEGS
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment DELEG
Environment SDELEGS
env, State DELEG
DIState
st DIState -> Getting DSState DIState DSState -> DSState
forall s a. s -> Getting a s a -> a
^. Getting DSState DIState DSState
Lens' DIState DSState
dIStateDSState, Signal DELEG
Signal SDELEGS
sig)
let slots :: [(Slot, (VKeyGenesis, VKey))]
slots = ((Slot, (VKeyGenesis, VKey)) -> Bool)
-> [(Slot, (VKeyGenesis, VKey))] -> [(Slot, (VKeyGenesis, VKey))]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Slot -> Slot -> Bool
forall a. Ord a => a -> a -> Bool
<= (Environment DELEG
DSEnv
env DSEnv -> Getting Slot DSEnv Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot DSEnv Slot
forall s a. HasSlot s a => Lens' s a
Lens' DSEnv Slot
slot)) (Slot -> Bool)
-> ((Slot, (VKeyGenesis, VKey)) -> Slot)
-> (Slot, (VKeyGenesis, VKey))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Slot, (VKeyGenesis, VKey)) -> Slot
forall a b. (a, b) -> a
fst) ([(Slot, (VKeyGenesis, VKey))] -> [(Slot, (VKeyGenesis, VKey))])
-> [(Slot, (VKeyGenesis, VKey))] -> [(Slot, (VKeyGenesis, VKey))]
forall a b. (a -> b) -> a -> b
$ DSState
sds DSState
-> Getting
[(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
-> [(Slot, (VKeyGenesis, VKey))]
forall s a. s -> Getting a s a -> a
^. Getting
[(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DSState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations
DState
as <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @ADELEGS (RuleContext 'Transition ADELEGS
-> Rule DELEG 'Transition (State ADELEGS))
-> RuleContext 'Transition ADELEGS
-> Rule DELEG 'Transition (State ADELEGS)
forall a b. (a -> b) -> a -> b
$ (Environment ADELEGS, State ADELEGS, Signal ADELEGS) -> TRC ADELEGS
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment DELEG
DSEnv
env DSEnv
-> Getting (Set VKeyGenesis) DSEnv (Set VKeyGenesis)
-> Set VKeyGenesis
forall s a. s -> Getting a s a -> a
^. Getting (Set VKeyGenesis) DSEnv (Set VKeyGenesis)
forall s a. HasAllowedDelegators s a => Lens' s a
Lens' DSEnv (Set VKeyGenesis)
allowedDelegators, State DELEG
DIState
st DIState -> Getting DState DIState DState -> DState
forall s a. s -> Getting a s a -> a
^. Getting DState DIState DState
Lens' DIState DState
dIStateDState, [(Slot, (VKeyGenesis, VKey))]
Signal ADELEGS
slots)
DIState -> F (Clause DELEG 'Transition) DIState
forall a. a -> F (Clause DELEG 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return (DIState -> F (Clause DELEG 'Transition) DIState)
-> DIState -> F (Clause DELEG 'Transition) DIState
forall a b. (a -> b) -> a -> b
$
Bimap VKeyGenesis VKey
-> Map VKeyGenesis Slot
-> [(Slot, (VKeyGenesis, VKey))]
-> Set (Epoch, VKeyGenesis)
-> DIState
DIState
(DState
as DState
-> Getting (Bimap VKeyGenesis VKey) DState (Bimap VKeyGenesis VKey)
-> Bimap VKeyGenesis VKey
forall s a. s -> Getting a s a -> a
^. Getting (Bimap VKeyGenesis VKey) DState (Bimap VKeyGenesis VKey)
forall s a. HasDelegationMap s a => Lens' s a
Lens' DState (Bimap VKeyGenesis VKey)
delegationMap)
(DState
as DState
-> Getting (Map VKeyGenesis Slot) DState (Map VKeyGenesis Slot)
-> Map VKeyGenesis Slot
forall s a. s -> Getting a s a -> a
^. Getting (Map VKeyGenesis Slot) DState (Map VKeyGenesis Slot)
forall s a. HasLastDelegation s a => Lens' s a
Lens' DState (Map VKeyGenesis Slot)
lastDelegation)
( ((Slot, (VKeyGenesis, VKey)) -> Bool)
-> [(Slot, (VKeyGenesis, VKey))] -> [(Slot, (VKeyGenesis, VKey))]
forall a. (a -> Bool) -> [a] -> [a]
filter (((Environment DELEG
DSEnv
env DSEnv -> Getting Slot DSEnv Slot -> Slot
forall s a. s -> Getting a s a -> a
^. Getting Slot DSEnv Slot
forall s a. HasSlot s a => Lens' s a
Lens' DSEnv Slot
slot) Slot -> SlotCount -> Slot
`addSlot` SlotCount
1 Slot -> Slot -> Bool
forall a. Ord a => a -> a -> Bool
<=) (Slot -> Bool)
-> ((Slot, (VKeyGenesis, VKey)) -> Slot)
-> (Slot, (VKeyGenesis, VKey))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Slot, (VKeyGenesis, VKey)) -> Slot
forall a b. (a, b) -> a
fst) ([(Slot, (VKeyGenesis, VKey))] -> [(Slot, (VKeyGenesis, VKey))])
-> [(Slot, (VKeyGenesis, VKey))] -> [(Slot, (VKeyGenesis, VKey))]
forall a b. (a -> b) -> a -> b
$
DSState
sds DSState
-> Getting
[(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
-> [(Slot, (VKeyGenesis, VKey))]
forall s a. s -> Getting a s a -> a
^. Getting
[(Slot, (VKeyGenesis, VKey))] DSState [(Slot, (VKeyGenesis, VKey))]
forall s a. HasScheduledDelegations s a => Lens' s a
Lens' DSState [(Slot, (VKeyGenesis, VKey))]
scheduledDelegations
)
( ((Epoch, VKeyGenesis) -> Bool)
-> Set (Epoch, VKeyGenesis) -> Set (Epoch, VKeyGenesis)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((Environment DELEG
DSEnv
env DSEnv -> Getting Epoch DSEnv Epoch -> Epoch
forall s a. s -> Getting a s a -> a
^. Getting Epoch DSEnv Epoch
forall s a. HasEpoch s a => Lens' s a
Lens' DSEnv Epoch
epoch Epoch -> Epoch -> Bool
forall a. Ord a => a -> a -> Bool
<=) (Epoch -> Bool)
-> ((Epoch, VKeyGenesis) -> Epoch) -> (Epoch, VKeyGenesis) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Epoch, VKeyGenesis) -> Epoch
forall a b. (a, b) -> a
fst) (Set (Epoch, VKeyGenesis) -> Set (Epoch, VKeyGenesis))
-> Set (Epoch, VKeyGenesis) -> Set (Epoch, VKeyGenesis)
forall a b. (a -> b) -> a -> b
$
DSState
sds DSState
-> Getting
(Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
-> Set (Epoch, VKeyGenesis)
forall s a. s -> Getting a s a -> a
^. Getting
(Set (Epoch, VKeyGenesis)) DSState (Set (Epoch, VKeyGenesis))
forall s a. HasKeyEpochDelegations s a => Lens' s a
Lens' DSState (Set (Epoch, VKeyGenesis))
keyEpochDelegations
)
]
instance Embed SDELEGS DELEG where
wrapFailed :: PredicateFailure SDELEGS -> PredicateFailure DELEG
wrapFailed = PredicateFailure SDELEGS -> PredicateFailure DELEG
PredicateFailure SDELEGS -> DelegPredicateFailure
SDelegSFailure
instance Embed ADELEGS DELEG where
wrapFailed :: PredicateFailure ADELEGS -> PredicateFailure DELEG
wrapFailed = PredicateFailure ADELEGS -> PredicateFailure DELEG
PredicateFailure ADELEGS -> DelegPredicateFailure
ADelegSFailure
dcertGen :: DSEnv -> Set (Epoch, VKeyGenesis) -> Gen (Maybe DCert)
dcertGen :: DSEnv -> Set (Epoch, VKeyGenesis) -> Gen (Maybe DCert)
dcertGen DSEnv
env Set (Epoch, VKeyGenesis)
eks =
let allowed :: [VKeyGenesis]
allowed :: [VKeyGenesis]
allowed = Set VKeyGenesis -> [VKeyGenesis]
forall a. Set a -> [a]
Set.toList (DSEnv -> Set VKeyGenesis
_dSEnvAllowedDelegators DSEnv
env)
preCandidates :: Set (Epoch, VKeyGenesis)
preCandidates :: Set (Epoch, VKeyGenesis)
preCandidates =
[(Epoch, VKeyGenesis)] -> Set (Epoch, VKeyGenesis)
forall a. Ord a => [a] -> Set a
Set.fromList ([(Epoch, VKeyGenesis)] -> Set (Epoch, VKeyGenesis))
-> [(Epoch, VKeyGenesis)] -> Set (Epoch, VKeyGenesis)
forall a b. (a -> b) -> a -> b
$
[Epoch] -> [VKeyGenesis] -> [(Epoch, VKeyGenesis)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Epoch -> [Epoch]
forall a. a -> [a]
repeat (Epoch -> [Epoch]) -> Epoch -> [Epoch]
forall a b. (a -> b) -> a -> b
$ DSEnv -> Epoch
_dSEnvEpoch DSEnv
env) [VKeyGenesis]
allowed
[(Epoch, VKeyGenesis)]
-> [(Epoch, VKeyGenesis)] -> [(Epoch, VKeyGenesis)]
forall a. [a] -> [a] -> [a]
++ [Epoch] -> [VKeyGenesis] -> [(Epoch, VKeyGenesis)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Epoch -> [Epoch]
forall a. a -> [a]
repeat (Epoch -> [Epoch]) -> Epoch -> [Epoch]
forall a b. (a -> b) -> a -> b
$ DSEnv -> Epoch
_dSEnvEpoch DSEnv
env Epoch -> Epoch -> Epoch
forall a. Num a => a -> a -> a
+ Epoch
1) [VKeyGenesis]
allowed
candidates :: [(Epoch, VKeyGenesis)]
candidates :: [(Epoch, VKeyGenesis)]
candidates = Set (Epoch, VKeyGenesis) -> [(Epoch, VKeyGenesis)]
forall a. Set a -> [a]
Set.toList (Set (Epoch, VKeyGenesis) -> [(Epoch, VKeyGenesis)])
-> Set (Epoch, VKeyGenesis) -> [(Epoch, VKeyGenesis)]
forall a b. (a -> b) -> a -> b
$ Set (Epoch, VKeyGenesis)
preCandidates Set (Epoch, VKeyGenesis)
-> Set (Epoch, VKeyGenesis) -> Set (Epoch, VKeyGenesis)
forall a. Ord a => Set a -> Set a -> Set a
\\ Set (Epoch, VKeyGenesis)
eks
target :: [VKey]
target :: [VKey]
target = Owner -> VKey
VKey (Owner -> VKey) -> (Natural -> Owner) -> Natural -> VKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Owner
Owner (Natural -> VKey) -> [Natural] -> [VKey]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Natural
0 .. (Natural
2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([VKeyGenesis] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VKeyGenesis]
allowed))]
mkDCert' :: ((Epoch, VKeyGenesis), VKey) -> DCert
mkDCert' ((Epoch
e, VKeyGenesis
vkg), VKey
vk) = VKeyGenesis -> Sig (VKey, Epoch) -> VKey -> Epoch -> DCert
mkDCert VKeyGenesis
vkg (VKeyGenesis -> (VKey, Epoch) -> Sig (VKey, Epoch)
forall a. VKeyGenesis -> a -> Sig a
signWithGenesisKey VKeyGenesis
vkg (VKey
vk, Epoch
e)) VKey
vk Epoch
e
in if [(Epoch, VKeyGenesis)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Epoch, VKeyGenesis)]
candidates
then Maybe DCert -> Gen (Maybe DCert)
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe DCert
forall a. Maybe a
Nothing
else DCert -> Maybe DCert
forall a. a -> Maybe a
Just (DCert -> Maybe DCert) -> GenT Identity DCert -> Gen (Maybe DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DCert] -> GenT Identity DCert
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element (((Epoch, VKeyGenesis), VKey) -> DCert
mkDCert' (((Epoch, VKeyGenesis), VKey) -> DCert)
-> [((Epoch, VKeyGenesis), VKey)] -> [DCert]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Epoch, VKeyGenesis)] -> [VKey] -> [((Epoch, VKeyGenesis), VKey)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Epoch, VKeyGenesis)]
candidates [VKey]
target)
dcertsGen :: DSEnv -> DIState -> Gen [DCert]
dcertsGen :: DSEnv -> DIState -> Gen [DCert]
dcertsGen DSEnv
env DIState
st =
[Maybe DCert] -> [DCert]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe DCert] -> [DCert])
-> (Trace MSDELEG -> [Maybe DCert]) -> Trace MSDELEG -> [DCert]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TraceOrder -> Trace MSDELEG -> [Signal MSDELEG]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst (Trace MSDELEG -> [DCert])
-> GenT Identity (Trace MSDELEG) -> Gen [DCert]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s.
HasTrace s =>
BaseEnv s
-> Word64
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
genTrace @MSDELEG () Word64
n Environment MSDELEG
DSEnv
env State MSDELEG
DSState
subSt (forall s. HasTrace s => SignalGenerator s
sigGen @MSDELEG)
where
n :: Word64
n = DSEnv
env DSEnv -> Getting Word64 DSEnv Word64 -> Word64
forall s a. s -> Getting a s a -> a
^. (Set VKeyGenesis -> Const Word64 (Set VKeyGenesis))
-> DSEnv -> Const Word64 DSEnv
forall s a. HasAllowedDelegators s a => Lens' s a
Lens' DSEnv (Set VKeyGenesis)
allowedDelegators ((Set VKeyGenesis -> Const Word64 (Set VKeyGenesis))
-> DSEnv -> Const Word64 DSEnv)
-> ((Word64 -> Const Word64 Word64)
-> Set VKeyGenesis -> Const Word64 (Set VKeyGenesis))
-> Getting Word64 DSEnv Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set VKeyGenesis -> Int) -> SimpleGetter (Set VKeyGenesis) Int
forall s a. (s -> a) -> SimpleGetter s a
to Set VKeyGenesis -> Int
forall a. Set a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Getting Word64 (Set VKeyGenesis) Int
-> ((Word64 -> Const Word64 Word64) -> Int -> Const Word64 Int)
-> (Word64 -> Const Word64 Word64)
-> Set VKeyGenesis
-> Const Word64 (Set VKeyGenesis)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Word64) -> SimpleGetter Int Word64
forall s a. (s -> a) -> SimpleGetter s a
to Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral
subSt :: DSState
subSt =
DSState
{ _dSStateScheduledDelegations :: [(Slot, (VKeyGenesis, VKey))]
_dSStateScheduledDelegations = DIState -> [(Slot, (VKeyGenesis, VKey))]
_dIStateScheduledDelegations DIState
st
, _dSStateKeyEpochDelegations :: Set (Epoch, VKeyGenesis)
_dSStateKeyEpochDelegations = DIState -> Set (Epoch, VKeyGenesis)
_dIStateKeyEpochDelegations DIState
st
}
randomDCertGen :: Environment DELEG -> Gen DCert
randomDCertGen :: Environment DELEG -> GenT Identity DCert
randomDCertGen Environment DELEG
env = do
(VKeyGenesis
vkg, VKey
vk, Epoch
e) <- (,,) (VKeyGenesis -> VKey -> Epoch -> (VKeyGenesis, VKey, Epoch))
-> GenT Identity VKeyGenesis
-> GenT Identity (VKey -> Epoch -> (VKeyGenesis, VKey, Epoch))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenT Identity VKeyGenesis
vkgGen' GenT Identity (VKey -> Epoch -> (VKeyGenesis, VKey, Epoch))
-> GenT Identity VKey
-> GenT Identity (Epoch -> (VKeyGenesis, VKey, Epoch))
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GenT Identity VKey
vkGen' GenT Identity (Epoch -> (VKeyGenesis, VKey, Epoch))
-> GenT Identity Epoch -> GenT Identity (VKeyGenesis, VKey, Epoch)
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GenT Identity Epoch
epochGen'
DCert -> GenT Identity DCert
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DCert -> GenT Identity DCert) -> DCert -> GenT Identity DCert
forall a b. (a -> b) -> a -> b
$! VKeyGenesis -> Sig (VKey, Epoch) -> VKey -> Epoch -> DCert
mkDCert VKeyGenesis
vkg (VKeyGenesis -> (VKey, Epoch) -> Sig (VKey, Epoch)
forall a. VKeyGenesis -> a -> Sig a
signWithGenesisKey VKeyGenesis
vkg (VKey
vk, Epoch
e)) VKey
vk Epoch
e
where
vkgGen' :: GenT Identity VKeyGenesis
vkgGen' = [VKeyGenesis] -> GenT Identity VKeyGenesis
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element ([VKeyGenesis] -> GenT Identity VKeyGenesis)
-> [VKeyGenesis] -> GenT Identity VKeyGenesis
forall a b. (a -> b) -> a -> b
$ Set VKeyGenesis -> [VKeyGenesis]
forall a. Set a -> [a]
Set.toList Set VKeyGenesis
allowed
allowed :: Set VKeyGenesis
allowed = DSEnv -> Set VKeyGenesis
_dSEnvAllowedDelegators Environment DELEG
DSEnv
env
vkGen' :: GenT Identity VKey
vkGen' = [VKey] -> GenT Identity VKey
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element ([VKey] -> GenT Identity VKey) -> [VKey] -> GenT Identity VKey
forall a b. (a -> b) -> a -> b
$ Owner -> VKey
VKey (Owner -> VKey) -> (Natural -> Owner) -> Natural -> VKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Owner
Owner (Natural -> VKey) -> [Natural] -> [VKey]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Natural
0 .. (Natural
2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Set VKeyGenesis -> Int
forall a. Set a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Set VKeyGenesis
allowed))]
epochGen' :: GenT Identity Epoch
epochGen' =
Word64 -> Epoch
Epoch
(Word64 -> Epoch) -> (Int -> Word64) -> Int -> Epoch
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral
(Int -> Word64) -> (Int -> Int) -> Int -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+)
(Int -> Epoch) -> GenT Identity Int -> GenT Identity Epoch
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range Int -> GenT Identity Int
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Int -> Int -> Range Int
forall a. a -> a -> Range a
Range.constant (-Int
2 :: Int) Int
2)
where
Epoch Word64
n = DSEnv -> Epoch
_dSEnvEpoch Environment DELEG
DSEnv
env
data MSDELEG deriving (Typeable MSDELEG
Typeable MSDELEG =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MSDELEG -> c MSDELEG)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MSDELEG)
-> (MSDELEG -> Constr)
-> (MSDELEG -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MSDELEG))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MSDELEG))
-> ((forall b. Data b => b -> b) -> MSDELEG -> MSDELEG)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MSDELEG -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MSDELEG -> r)
-> (forall u. (forall d. Data d => d -> u) -> MSDELEG -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> MSDELEG -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> MSDELEG -> m MSDELEG)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MSDELEG -> m MSDELEG)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MSDELEG -> m MSDELEG)
-> Data MSDELEG
MSDELEG -> Constr
MSDELEG -> DataType
(forall b. Data b => b -> b) -> MSDELEG -> MSDELEG
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> MSDELEG -> u
forall u. (forall d. Data d => d -> u) -> MSDELEG -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MSDELEG -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MSDELEG -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> MSDELEG -> m MSDELEG
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MSDELEG -> m MSDELEG
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MSDELEG
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MSDELEG -> c MSDELEG
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MSDELEG)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MSDELEG)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MSDELEG -> c MSDELEG
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> MSDELEG -> c MSDELEG
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MSDELEG
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MSDELEG
$ctoConstr :: MSDELEG -> Constr
toConstr :: MSDELEG -> Constr
$cdataTypeOf :: MSDELEG -> DataType
dataTypeOf :: MSDELEG -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MSDELEG)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MSDELEG)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MSDELEG)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MSDELEG)
$cgmapT :: (forall b. Data b => b -> b) -> MSDELEG -> MSDELEG
gmapT :: (forall b. Data b => b -> b) -> MSDELEG -> MSDELEG
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MSDELEG -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MSDELEG -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MSDELEG -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MSDELEG -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> MSDELEG -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> MSDELEG -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> MSDELEG -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> MSDELEG -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> MSDELEG -> m MSDELEG
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> MSDELEG -> m MSDELEG
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MSDELEG -> m MSDELEG
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MSDELEG -> m MSDELEG
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MSDELEG -> m MSDELEG
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> MSDELEG -> m MSDELEG
Data)
data MsdelegPredicateFailure = SDELEGFailure (PredicateFailure SDELEG)
deriving (MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
(MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool)
-> (MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool)
-> Eq MsdelegPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
== :: MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
$c/= :: MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
/= :: MsdelegPredicateFailure -> MsdelegPredicateFailure -> Bool
Eq, Int -> MsdelegPredicateFailure -> ShowS
[MsdelegPredicateFailure] -> ShowS
MsdelegPredicateFailure -> String
(Int -> MsdelegPredicateFailure -> ShowS)
-> (MsdelegPredicateFailure -> String)
-> ([MsdelegPredicateFailure] -> ShowS)
-> Show MsdelegPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MsdelegPredicateFailure -> ShowS
showsPrec :: Int -> MsdelegPredicateFailure -> ShowS
$cshow :: MsdelegPredicateFailure -> String
show :: MsdelegPredicateFailure -> String
$cshowList :: [MsdelegPredicateFailure] -> ShowS
showList :: [MsdelegPredicateFailure] -> ShowS
Show, Typeable MsdelegPredicateFailure
Typeable MsdelegPredicateFailure =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> MsdelegPredicateFailure
-> c MsdelegPredicateFailure)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MsdelegPredicateFailure)
-> (MsdelegPredicateFailure -> Constr)
-> (MsdelegPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MsdelegPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c MsdelegPredicateFailure))
-> ((forall b. Data b => b -> b)
-> MsdelegPredicateFailure -> MsdelegPredicateFailure)
-> (forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r)
-> (forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r)
-> (forall u.
(forall d. Data d => d -> u) -> MsdelegPredicateFailure -> [u])
-> (forall u.
Int
-> (forall d. Data d => d -> u) -> MsdelegPredicateFailure -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure)
-> Data MsdelegPredicateFailure
MsdelegPredicateFailure -> Constr
MsdelegPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> MsdelegPredicateFailure -> MsdelegPredicateFailure
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> MsdelegPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> MsdelegPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MsdelegPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> MsdelegPredicateFailure
-> c MsdelegPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MsdelegPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c MsdelegPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> MsdelegPredicateFailure
-> c MsdelegPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> MsdelegPredicateFailure
-> c MsdelegPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MsdelegPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c MsdelegPredicateFailure
$ctoConstr :: MsdelegPredicateFailure -> Constr
toConstr :: MsdelegPredicateFailure -> Constr
$cdataTypeOf :: MsdelegPredicateFailure -> DataType
dataTypeOf :: MsdelegPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MsdelegPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c MsdelegPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c MsdelegPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c MsdelegPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> MsdelegPredicateFailure -> MsdelegPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> MsdelegPredicateFailure -> MsdelegPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> MsdelegPredicateFailure
-> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> MsdelegPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> MsdelegPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> MsdelegPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> MsdelegPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MsdelegPredicateFailure -> m MsdelegPredicateFailure
Data, (forall x.
MsdelegPredicateFailure -> Rep MsdelegPredicateFailure x)
-> (forall x.
Rep MsdelegPredicateFailure x -> MsdelegPredicateFailure)
-> Generic MsdelegPredicateFailure
forall x. Rep MsdelegPredicateFailure x -> MsdelegPredicateFailure
forall x. MsdelegPredicateFailure -> Rep MsdelegPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MsdelegPredicateFailure -> Rep MsdelegPredicateFailure x
from :: forall x. MsdelegPredicateFailure -> Rep MsdelegPredicateFailure x
$cto :: forall x. Rep MsdelegPredicateFailure x -> MsdelegPredicateFailure
to :: forall x. Rep MsdelegPredicateFailure x -> MsdelegPredicateFailure
Generic, Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
Proxy MsdelegPredicateFailure -> String
(Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy MsdelegPredicateFailure -> String)
-> NoThunks MsdelegPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> MsdelegPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy MsdelegPredicateFailure -> String
showTypeOf :: Proxy MsdelegPredicateFailure -> String
NoThunks)
instance STS MSDELEG where
type Environment MSDELEG = DSEnv
type State MSDELEG = DSState
type Signal MSDELEG = Maybe DCert
type PredicateFailure MSDELEG = MsdelegPredicateFailure
initialRules :: [InitialRule MSDELEG]
initialRules = []
transitionRules :: [TransitionRule MSDELEG]
transitionRules =
[ do
TRC (Environment MSDELEG
env, State MSDELEG
st, Signal MSDELEG
msig) <- Rule MSDELEG 'Transition (RuleContext 'Transition MSDELEG)
F (Clause MSDELEG 'Transition) (TRC MSDELEG)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
case Signal MSDELEG
msig of
Maybe DCert
Signal MSDELEG
Nothing -> DSState -> F (Clause MSDELEG 'Transition) DSState
forall a. a -> F (Clause MSDELEG 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure State MSDELEG
DSState
st
Just DCert
sig -> forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @SDELEG (RuleContext 'Transition SDELEG
-> Rule MSDELEG 'Transition (State SDELEG))
-> RuleContext 'Transition SDELEG
-> Rule MSDELEG 'Transition (State SDELEG)
forall a b. (a -> b) -> a -> b
$ (Environment SDELEG, State SDELEG, Signal SDELEG) -> TRC SDELEG
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment MSDELEG
Environment SDELEG
env, State MSDELEG
State SDELEG
st, Signal SDELEG
DCert
sig)
]
instance Embed SDELEG MSDELEG where
wrapFailed :: PredicateFailure SDELEG -> PredicateFailure MSDELEG
wrapFailed = PredicateFailure SDELEG -> PredicateFailure MSDELEG
PredicateFailure SDELEG -> MsdelegPredicateFailure
SDELEGFailure
instance HasTrace MSDELEG where
envGen :: Word64 -> Gen (Environment MSDELEG)
envGen = Word64 -> Gen (Environment MSDELEG)
Word64 -> Gen DSEnv
delegEnvGen
sigGen :: SignalGenerator MSDELEG
sigGen Environment MSDELEG
env State MSDELEG
st = DSEnv -> Set (Epoch, VKeyGenesis) -> Gen (Maybe DCert)
dcertGen Environment MSDELEG
DSEnv
env (DSState -> Set (Epoch, VKeyGenesis)
_dSStateKeyEpochDelegations State MSDELEG
DSState
st)
instance HasTrace DELEG where
envGen :: Word64 -> Gen (Environment DELEG)
envGen = Word64 -> Gen (Environment DELEG)
Word64 -> Gen DSEnv
delegEnvGen
sigGen :: SignalGenerator DELEG
sigGen = SignalGenerator DELEG
DSEnv -> DIState -> Gen [DCert]
dcertsGen
delegEnvGen :: Word64 -> Gen DSEnv
delegEnvGen :: Word64 -> Gen DSEnv
delegEnvGen Word64
chainLength = do
Word8
ngk <- Range Word8 -> GenT Identity Word8
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Word8 -> Word8 -> Range Word8
forall a. Integral a => a -> a -> Range a
Range.linear Word8
1 Word8
14)
Word8 -> Word64 -> Gen DSEnv
initialEnvFromGenesisKeys Word8
ngk Word64
chainLength
initialEnvFromGenesisKeys ::
Word8 ->
Word64 ->
Gen DSEnv
initialEnvFromGenesisKeys :: Word8 -> Word64 -> Gen DSEnv
initialEnvFromGenesisKeys Word8
ngk Word64
chainLength =
Set VKeyGenesis -> Epoch -> Slot -> BlockCount -> DSEnv
DSEnv
(Set VKeyGenesis -> Epoch -> Slot -> BlockCount -> DSEnv)
-> GenT Identity (Set VKeyGenesis)
-> GenT Identity (Epoch -> Slot -> BlockCount -> DSEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set VKeyGenesis -> GenT Identity (Set VKeyGenesis)
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Word8 -> Set VKeyGenesis
mkVkGenesisSet Word8
ngk)
GenT Identity (Epoch -> Slot -> BlockCount -> DSEnv)
-> GenT Identity Epoch
-> GenT Identity (Slot -> BlockCount -> DSEnv)
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> GenT Identity Epoch
epochGen Word64
0 Word64
10
GenT Identity (Slot -> BlockCount -> DSEnv)
-> GenT Identity Slot -> GenT Identity (BlockCount -> DSEnv)
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> GenT Identity Slot
slotGen Word64
0 Word64
100
GenT Identity (BlockCount -> DSEnv)
-> GenT Identity BlockCount -> Gen DSEnv
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> Word64 -> GenT Identity BlockCount
CoreGen.k Word64
chainLength (Word64
chainLength Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`div` Word64
10)
delegatorDelegate :: DCert -> (VKeyGenesis, VKey)
delegatorDelegate :: DCert -> (VKeyGenesis, VKey)
delegatorDelegate = DCert -> VKeyGenesis
delegator (DCert -> VKeyGenesis)
-> (DCert -> VKey) -> DCert -> (VKeyGenesis, VKey)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& DCert -> VKey
delegate
ratioInt :: Int -> Int -> Double
ratioInt :: Int -> Int -> Double
ratioInt Int
x Int
y =
Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
x Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
y
lenRatio :: ([a] -> [b]) -> [a] -> Double
lenRatio :: forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio [a] -> [b]
f [a]
xs =
Int -> Int -> Double
ratioInt
([b] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a] -> [b]
f [a]
xs))
([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs)
multiple :: (a, Int) -> Bool
multiple :: forall a. (a, Int) -> Bool
multiple = (Int
2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<=) (Int -> Bool) -> ((a, Int) -> Int) -> (a, Int) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Int) -> Int
forall a b. (a, b) -> b
snd
delegateCounter ::
Ord a =>
((VKeyGenesis, VKey) -> a) ->
[DCert] ->
[(a, Int)]
delegateCounter :: forall a.
Ord a =>
((VKeyGenesis, VKey) -> a) -> [DCert] -> [(a, Int)]
delegateCounter (VKeyGenesis, VKey) -> a
pick [DCert]
certs =
(DCert -> (VKeyGenesis, VKey)) -> [DCert] -> [(VKeyGenesis, VKey)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DCert -> (VKeyGenesis, VKey)
delegatorDelegate [DCert]
certs
[(VKeyGenesis, VKey)]
-> ([(VKeyGenesis, VKey)] -> [(VKeyGenesis, VKey)])
-> [(VKeyGenesis, VKey)]
forall a b. a -> (a -> b) -> b
& [(VKeyGenesis, VKey)] -> [(VKeyGenesis, VKey)]
forall a. Eq a => [a] -> [a]
List.nub
[(VKeyGenesis, VKey)] -> ([(VKeyGenesis, VKey)] -> [a]) -> [a]
forall a b. a -> (a -> b) -> b
& ((VKeyGenesis, VKey) -> a) -> [(VKeyGenesis, VKey)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VKeyGenesis, VKey) -> a
pick
[a] -> ([a] -> [(a, Int)]) -> [(a, Int)]
forall a b. a -> (a -> b) -> b
& [a] -> [(a, Int)]
forall a. Ord a => [a] -> [(a, Int)]
count
delegateCounts :: [DCert] -> [(VKey, Int)]
delegateCounts :: [DCert] -> [(VKey, Int)]
delegateCounts = ((VKeyGenesis, VKey) -> VKey) -> [DCert] -> [(VKey, Int)]
forall a.
Ord a =>
((VKeyGenesis, VKey) -> a) -> [DCert] -> [(a, Int)]
delegateCounter (VKeyGenesis, VKey) -> VKey
forall a b. (a, b) -> b
snd
delegatorCounts :: [DCert] -> [(VKeyGenesis, Int)]
delegatorCounts :: [DCert] -> [(VKeyGenesis, Int)]
delegatorCounts = ((VKeyGenesis, VKey) -> VKeyGenesis)
-> [DCert] -> [(VKeyGenesis, Int)]
forall a.
Ord a =>
((VKeyGenesis, VKey) -> a) -> [DCert] -> [(a, Int)]
delegateCounter (VKeyGenesis, VKey) -> VKeyGenesis
forall a b. (a, b) -> a
fst
emptyDelegationPayloadRatio :: [[DCert]] -> Double
emptyDelegationPayloadRatio :: [[DCert]] -> Double
emptyDelegationPayloadRatio =
([[DCert]] -> [[DCert]]) -> [[DCert]] -> Double
forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (([DCert] -> Bool) -> [[DCert]] -> [[DCert]]
forall a. (a -> Bool) -> [a] -> [a]
filter [DCert] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null)
thisEpochDelegationsRatio :: [(Epoch, Epoch)] -> Double
thisEpochDelegationsRatio :: [(Epoch, Epoch)] -> Double
thisEpochDelegationsRatio =
([(Epoch, Epoch)] -> [(Epoch, Epoch)])
-> [(Epoch, Epoch)] -> Double
forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (((Epoch, Epoch) -> Bool) -> [(Epoch, Epoch)] -> [(Epoch, Epoch)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Epoch, Epoch) -> Bool
thisEpoch)
where
thisEpoch :: (Epoch, Epoch) -> Bool
thisEpoch = (Epoch -> Epoch -> Bool) -> (Epoch, Epoch) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Epoch -> Epoch -> Bool
forall a. Eq a => a -> a -> Bool
(==)
nextEpochDelegationsRatio :: [(Epoch, Epoch)] -> Double
nextEpochDelegationsRatio :: [(Epoch, Epoch)] -> Double
nextEpochDelegationsRatio =
([(Epoch, Epoch)] -> [(Epoch, Epoch)])
-> [(Epoch, Epoch)] -> Double
forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (((Epoch, Epoch) -> Bool) -> [(Epoch, Epoch)] -> [(Epoch, Epoch)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Epoch, Epoch) -> Bool
forall {a}. (Eq a, Num a) => (a, a) -> Bool
nextEpoch)
where
nextEpoch :: (a, a) -> Bool
nextEpoch (a
e0, a
e1) = a
e0 a -> a -> a
forall a. Num a => a -> a -> a
+ a
1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
e1
selfDelegationsRatio :: [DCert] -> Double
selfDelegationsRatio :: [DCert] -> Double
selfDelegationsRatio =
([DCert] -> [(VKeyGenesis, VKey)]) -> [DCert] -> Double
forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (((VKeyGenesis, VKey) -> Bool)
-> [(VKeyGenesis, VKey)] -> [(VKeyGenesis, VKey)]
forall a. (a -> Bool) -> [a] -> [a]
filter (VKeyGenesis, VKey) -> Bool
forall {a} {a}. (HasOwner a, HasOwner a) => (a, a) -> Bool
selfDeleg ([(VKeyGenesis, VKey)] -> [(VKeyGenesis, VKey)])
-> ([DCert] -> [(VKeyGenesis, VKey)])
-> [DCert]
-> [(VKeyGenesis, VKey)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DCert -> (VKeyGenesis, VKey)) -> [DCert] -> [(VKeyGenesis, VKey)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DCert -> (VKeyGenesis, VKey)
delegatorDelegate)
where
selfDeleg :: (a, a) -> Bool
selfDeleg (a
vks, a
vk) = a -> Owner
forall a. HasOwner a => a -> Owner
owner a
vks Owner -> Owner -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Owner
forall a. HasOwner a => a -> Owner
owner a
vk
multipleDelegationsRatio :: [DCert] -> Double
multipleDelegationsRatio :: [DCert] -> Double
multipleDelegationsRatio [DCert]
dcerts =
([(VKey, Int)] -> [(VKey, Int)]) -> [(VKey, Int)] -> Double
forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (((VKey, Int) -> Bool) -> [(VKey, Int)] -> [(VKey, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (VKey, Int) -> Bool
forall a. (a, Int) -> Bool
multiple) ([DCert] -> [(VKey, Int)]
delegateCounts [DCert]
dcerts)
maxDelegationsTo :: [DCert] -> Int
maxDelegationsTo :: [DCert] -> Int
maxDelegationsTo [DCert]
dcerts =
case ((VKey, Int) -> Bool) -> [(VKey, Int)] -> [(VKey, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (VKey, Int) -> Bool
forall a. (a, Int) -> Bool
multiple ([DCert] -> [(VKey, Int)]
delegateCounts [DCert]
dcerts) of
[] -> Int
1
[(VKey, Int)]
xs -> [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum ((VKey, Int) -> Int
forall a b. (a, b) -> b
snd ((VKey, Int) -> Int) -> [(VKey, Int)] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(VKey, Int)]
xs)
changedDelegationsRatio :: [DCert] -> Double
changedDelegationsRatio :: [DCert] -> Double
changedDelegationsRatio [DCert]
dcerts =
([(VKeyGenesis, Int)] -> [(VKeyGenesis, Int)])
-> [(VKeyGenesis, Int)] -> Double
forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio (((VKeyGenesis, Int) -> Bool)
-> [(VKeyGenesis, Int)] -> [(VKeyGenesis, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (VKeyGenesis, Int) -> Bool
forall a. (a, Int) -> Bool
multiple) ([DCert] -> [(VKeyGenesis, Int)]
delegatorCounts [DCert]
dcerts)
maxChangedDelegations :: [DCert] -> Int
maxChangedDelegations :: [DCert] -> Int
maxChangedDelegations [DCert]
dcerts =
case ((VKey, Int) -> Bool) -> [(VKey, Int)] -> [(VKey, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (VKey, Int) -> Bool
forall a. (a, Int) -> Bool
multiple ([DCert] -> [(VKey, Int)]
delegateCounts [DCert]
dcerts) of
[] -> Int
1
[(VKey, Int)]
xs -> [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum ((VKey, Int) -> Int
forall a b. (a, b) -> b
snd ((VKey, Int) -> Int) -> [(VKey, Int)] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(VKey, Int)]
xs)
repeatedDelegationsRatio :: [DCert] -> Double
repeatedDelegationsRatio :: [DCert] -> Double
repeatedDelegationsRatio [DCert]
dcerts =
(DCert -> (VKeyGenesis, VKey)) -> [DCert] -> [(VKeyGenesis, VKey)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DCert -> (VKeyGenesis, VKey)
delegatorDelegate [DCert]
dcerts
[(VKeyGenesis, VKey)]
-> ([(VKeyGenesis, VKey)] -> [((VKeyGenesis, VKey), Int)])
-> [((VKeyGenesis, VKey), Int)]
forall a b. a -> (a -> b) -> b
& [(VKeyGenesis, VKey)] -> [((VKeyGenesis, VKey), Int)]
forall a. Ord a => [a] -> [(a, Int)]
count
[((VKeyGenesis, VKey), Int)]
-> ([((VKeyGenesis, VKey), Int)] -> Double) -> Double
forall a b. a -> (a -> b) -> b
& ([((VKeyGenesis, VKey), Int)] -> [((VKeyGenesis, VKey), Int)])
-> [((VKeyGenesis, VKey), Int)] -> Double
forall a b. ([a] -> [b]) -> [a] -> Double
lenRatio ((((VKeyGenesis, VKey), Int) -> Bool)
-> [((VKeyGenesis, VKey), Int)] -> [((VKeyGenesis, VKey), Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((VKeyGenesis, VKey), Int) -> Bool
forall a. (a, Int) -> Bool
multiple)
maxRepeatedDelegations :: [DCert] -> Int
maxRepeatedDelegations :: [DCert] -> Int
maxRepeatedDelegations [DCert]
dcerts =
case (((VKeyGenesis, VKey), Int) -> Bool)
-> [((VKeyGenesis, VKey), Int)] -> [((VKeyGenesis, VKey), Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((VKeyGenesis, VKey), Int) -> Bool
forall a. (a, Int) -> Bool
multiple [((VKeyGenesis, VKey), Int)]
ds of
[] -> Int
1
[((VKeyGenesis, VKey), Int)]
xs -> [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum (((VKeyGenesis, VKey), Int) -> Int
forall a b. (a, b) -> b
snd (((VKeyGenesis, VKey), Int) -> Int)
-> [((VKeyGenesis, VKey), Int)] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [((VKeyGenesis, VKey), Int)]
xs)
where
ds :: [((VKeyGenesis, VKey), Int)]
ds = [(VKeyGenesis, VKey)] -> [((VKeyGenesis, VKey), Int)]
forall a. Ord a => [a] -> [(a, Int)]
count ((DCert -> (VKeyGenesis, VKey)) -> [DCert] -> [(VKeyGenesis, VKey)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DCert -> (VKeyGenesis, VKey)
delegatorDelegate [DCert]
dcerts)
maxCertsPerBlock :: [[DCert]] -> Int
maxCertsPerBlock :: [[DCert]] -> Int
maxCertsPerBlock [[DCert]]
groupedCerts =
case [[DCert]]
groupedCerts of
[] -> Int
0
[[DCert]]
_ -> [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum ([DCert] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([DCert] -> Int) -> [[DCert]] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[DCert]]
groupedCerts)