{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Byron.Spec.Ledger.STS.UTXOWS where
import Byron.Spec.Ledger.STS.UTXO (UTxOEnv, UTxOState)
import Byron.Spec.Ledger.STS.UTXOW (UTXOW)
import Byron.Spec.Ledger.UTxO (Tx)
import Control.State.Transition (
Embed,
Environment,
IRC (IRC),
PredicateFailure,
STS (..),
Signal,
State,
TRC (TRC),
initialRules,
judgmentContext,
trans,
transitionRules,
wrapFailed,
)
import Data.Data (Data)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks (..))
import Test.Control.State.Transition.Generator (HasTrace, envGen, genTrace, sigGen)
import Test.Control.State.Transition.Trace (TraceOrder (OldestFirst), traceSignals)
data UTXOWS deriving (Typeable UTXOWS
Typeable UTXOWS =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXOWS -> c UTXOWS)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXOWS)
-> (UTXOWS -> Constr)
-> (UTXOWS -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXOWS))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXOWS))
-> ((forall b. Data b => b -> b) -> UTXOWS -> UTXOWS)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> UTXOWS -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> UTXOWS -> r)
-> (forall u. (forall d. Data d => d -> u) -> UTXOWS -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> UTXOWS -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UTXOWS -> m UTXOWS)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXOWS -> m UTXOWS)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXOWS -> m UTXOWS)
-> Data UTXOWS
UTXOWS -> Constr
UTXOWS -> DataType
(forall b. Data b => b -> b) -> UTXOWS -> UTXOWS
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) -> UTXOWS -> u
forall u. (forall d. Data d => d -> u) -> UTXOWS -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXOWS -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UTXOWS -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UTXOWS -> m UTXOWS
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXOWS -> m UTXOWS
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXOWS
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXOWS -> c UTXOWS
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXOWS)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXOWS)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXOWS -> c UTXOWS
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXOWS -> c UTXOWS
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXOWS
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXOWS
$ctoConstr :: UTXOWS -> Constr
toConstr :: UTXOWS -> Constr
$cdataTypeOf :: UTXOWS -> DataType
dataTypeOf :: UTXOWS -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXOWS)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXOWS)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXOWS)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXOWS)
$cgmapT :: (forall b. Data b => b -> b) -> UTXOWS -> UTXOWS
gmapT :: (forall b. Data b => b -> b) -> UTXOWS -> UTXOWS
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXOWS -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXOWS -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UTXOWS -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UTXOWS -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UTXOWS -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> UTXOWS -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UTXOWS -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UTXOWS -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UTXOWS -> m UTXOWS
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UTXOWS -> m UTXOWS
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXOWS -> m UTXOWS
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXOWS -> m UTXOWS
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXOWS -> m UTXOWS
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UTXOWS -> m UTXOWS
Data)
data UtxowsPredicateFailure
= UtxowFailure (PredicateFailure UTXOW)
deriving (UtxowsPredicateFailure -> UtxowsPredicateFailure -> Bool
(UtxowsPredicateFailure -> UtxowsPredicateFailure -> Bool)
-> (UtxowsPredicateFailure -> UtxowsPredicateFailure -> Bool)
-> Eq UtxowsPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UtxowsPredicateFailure -> UtxowsPredicateFailure -> Bool
== :: UtxowsPredicateFailure -> UtxowsPredicateFailure -> Bool
$c/= :: UtxowsPredicateFailure -> UtxowsPredicateFailure -> Bool
/= :: UtxowsPredicateFailure -> UtxowsPredicateFailure -> Bool
Eq, Int -> UtxowsPredicateFailure -> ShowS
[UtxowsPredicateFailure] -> ShowS
UtxowsPredicateFailure -> String
(Int -> UtxowsPredicateFailure -> ShowS)
-> (UtxowsPredicateFailure -> String)
-> ([UtxowsPredicateFailure] -> ShowS)
-> Show UtxowsPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UtxowsPredicateFailure -> ShowS
showsPrec :: Int -> UtxowsPredicateFailure -> ShowS
$cshow :: UtxowsPredicateFailure -> String
show :: UtxowsPredicateFailure -> String
$cshowList :: [UtxowsPredicateFailure] -> ShowS
showList :: [UtxowsPredicateFailure] -> ShowS
Show, Typeable UtxowsPredicateFailure
Typeable UtxowsPredicateFailure =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxowsPredicateFailure
-> c UtxowsPredicateFailure)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxowsPredicateFailure)
-> (UtxowsPredicateFailure -> Constr)
-> (UtxowsPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxowsPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxowsPredicateFailure))
-> ((forall b. Data b => b -> b)
-> UtxowsPredicateFailure -> UtxowsPredicateFailure)
-> (forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> UtxowsPredicateFailure
-> r)
-> (forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> UtxowsPredicateFailure
-> r)
-> (forall u.
(forall d. Data d => d -> u) -> UtxowsPredicateFailure -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> UtxowsPredicateFailure -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UtxowsPredicateFailure -> m UtxowsPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxowsPredicateFailure -> m UtxowsPredicateFailure)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxowsPredicateFailure -> m UtxowsPredicateFailure)
-> Data UtxowsPredicateFailure
UtxowsPredicateFailure -> Constr
UtxowsPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> UtxowsPredicateFailure -> UtxowsPredicateFailure
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) -> UtxowsPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> UtxowsPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> UtxowsPredicateFailure
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> UtxowsPredicateFailure
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UtxowsPredicateFailure -> m UtxowsPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxowsPredicateFailure -> m UtxowsPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxowsPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxowsPredicateFailure
-> c UtxowsPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxowsPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxowsPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxowsPredicateFailure
-> c UtxowsPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxowsPredicateFailure
-> c UtxowsPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxowsPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxowsPredicateFailure
$ctoConstr :: UtxowsPredicateFailure -> Constr
toConstr :: UtxowsPredicateFailure -> Constr
$cdataTypeOf :: UtxowsPredicateFailure -> DataType
dataTypeOf :: UtxowsPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxowsPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxowsPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxowsPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxowsPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> UtxowsPredicateFailure -> UtxowsPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> UtxowsPredicateFailure -> UtxowsPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> UtxowsPredicateFailure
-> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> UtxowsPredicateFailure
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> UtxowsPredicateFailure
-> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> UtxowsPredicateFailure
-> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxowsPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxowsPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxowsPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxowsPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UtxowsPredicateFailure -> m UtxowsPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UtxowsPredicateFailure -> m UtxowsPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxowsPredicateFailure -> m UtxowsPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxowsPredicateFailure -> m UtxowsPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxowsPredicateFailure -> m UtxowsPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UtxowsPredicateFailure -> m UtxowsPredicateFailure
Data, (forall x. UtxowsPredicateFailure -> Rep UtxowsPredicateFailure x)
-> (forall x.
Rep UtxowsPredicateFailure x -> UtxowsPredicateFailure)
-> Generic UtxowsPredicateFailure
forall x. Rep UtxowsPredicateFailure x -> UtxowsPredicateFailure
forall x. UtxowsPredicateFailure -> Rep UtxowsPredicateFailure x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. UtxowsPredicateFailure -> Rep UtxowsPredicateFailure x
from :: forall x. UtxowsPredicateFailure -> Rep UtxowsPredicateFailure x
$cto :: forall x. Rep UtxowsPredicateFailure x -> UtxowsPredicateFailure
to :: forall x. Rep UtxowsPredicateFailure x -> UtxowsPredicateFailure
Generic, Context -> UtxowsPredicateFailure -> IO (Maybe ThunkInfo)
Proxy UtxowsPredicateFailure -> String
(Context -> UtxowsPredicateFailure -> IO (Maybe ThunkInfo))
-> (Context -> UtxowsPredicateFailure -> IO (Maybe ThunkInfo))
-> (Proxy UtxowsPredicateFailure -> String)
-> NoThunks UtxowsPredicateFailure
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> UtxowsPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> UtxowsPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> UtxowsPredicateFailure -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> UtxowsPredicateFailure -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy UtxowsPredicateFailure -> String
showTypeOf :: Proxy UtxowsPredicateFailure -> String
NoThunks)
instance STS UTXOWS where
type State UTXOWS = UTxOState
type Signal UTXOWS = [Tx]
type Environment UTXOWS = UTxOEnv
type PredicateFailure UTXOWS = UtxowsPredicateFailure
initialRules :: [InitialRule UTXOWS]
initialRules =
[ do
IRC Environment UTXOWS
env <- Rule UTXOWS 'Initial (RuleContext 'Initial UTXOWS)
F (Clause UTXOWS 'Initial) (IRC UTXOWS)
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 @UTXOW (RuleContext 'Initial UTXOW -> Rule UTXOWS 'Initial (State UTXOW))
-> RuleContext 'Initial UTXOW -> Rule UTXOWS 'Initial (State UTXOW)
forall a b. (a -> b) -> a -> b
$ Environment UTXOW -> IRC UTXOW
forall sts. Environment sts -> IRC sts
IRC Environment UTXOW
Environment UTXOWS
env
]
transitionRules :: [TransitionRule UTXOWS]
transitionRules =
[ do
TRC (Environment UTXOWS
env, State UTXOWS
utxo, Signal UTXOWS
txWits) <- Rule UTXOWS 'Transition (RuleContext 'Transition UTXOWS)
F (Clause UTXOWS 'Transition) (TRC UTXOWS)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
case ([Tx]
Signal UTXOWS
txWits :: [Tx]) of
[] -> UTxOState -> F (Clause UTXOWS 'Transition) UTxOState
forall a. a -> F (Clause UTXOWS 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return State UTXOWS
UTxOState
utxo
(Tx
tx : [Tx]
gamma) -> do
UTxOState
utxo' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UTXOW (RuleContext 'Transition UTXOW
-> Rule UTXOWS 'Transition (State UTXOW))
-> RuleContext 'Transition UTXOW
-> Rule UTXOWS 'Transition (State UTXOW)
forall a b. (a -> b) -> a -> b
$ (Environment UTXOW, State UTXOW, Signal UTXOW) -> TRC UTXOW
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment UTXOW
Environment UTXOWS
env, State UTXOW
State UTXOWS
utxo, Signal UTXOW
Tx
tx)
UTxOState
utxo'' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UTXOWS (RuleContext 'Transition UTXOWS -> TransitionRule UTXOWS)
-> RuleContext 'Transition UTXOWS -> TransitionRule UTXOWS
forall a b. (a -> b) -> a -> b
$ (Environment UTXOWS, State UTXOWS, Signal UTXOWS) -> TRC UTXOWS
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment UTXOWS
env, State UTXOWS
UTxOState
utxo', [Tx]
Signal UTXOWS
gamma)
UTxOState -> F (Clause UTXOWS 'Transition) UTxOState
forall a. a -> F (Clause UTXOWS 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return UTxOState
utxo''
]
instance Embed UTXOW UTXOWS where
wrapFailed :: PredicateFailure UTXOW -> PredicateFailure UTXOWS
wrapFailed = PredicateFailure UTXOW -> PredicateFailure UTXOWS
PredicateFailure UTXOW -> UtxowsPredicateFailure
UtxowFailure
instance HasTrace UTXOWS where
envGen :: Word64 -> Gen (Environment UTXOWS)
envGen = forall s. HasTrace s => Word64 -> Gen (Environment s)
envGen @UTXOW
sigGen :: SignalGenerator UTXOWS
sigGen Environment UTXOWS
env State UTXOWS
st =
TraceOrder -> Trace UTXOW -> [Signal UTXOW]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst (Trace UTXOW -> [Tx])
-> GenT Identity (Trace UTXOW) -> GenT Identity [Tx]
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 @UTXOW () Word64
20 Environment UTXOW
Environment UTXOWS
env State UTXOW
State UTXOWS
st (forall s. HasTrace s => SignalGenerator s
sigGen @UTXOW)