{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Byron.Spec.Ledger.STS.UTXOWS where
import NoThunks.Class (NoThunks(..))
import Data.Data (Data, Typeable)
import GHC.Generics (Generic)
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 Control.State.Transition.Generator (HasTrace, envGen, genTrace, sigGen)
import Control.State.Transition.Trace (TraceOrder (OldestFirst), traceSignals)
data UTXOWS deriving (Typeable UTXOWS
DataType
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 -> DataType
UTXOWS -> Constr
(forall b. Data b => b -> b) -> UTXOWS -> UTXOWS
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXOWS -> c UTXOWS
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$tUTXOWS :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d) -> UTXOWS -> m UTXOWS
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UTXOWS -> m UTXOWS
gmapQi :: Int -> (forall d. Data d => d -> u) -> UTXOWS -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UTXOWS -> u
gmapQ :: (forall d. Data d => d -> u) -> UTXOWS -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UTXOWS -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXOWS -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UTXOWS -> r
gmapT :: (forall b. Data b => b -> b) -> UTXOWS -> UTXOWS
$cgmapT :: (forall b. Data b => b -> b) -> UTXOWS -> UTXOWS
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXOWS)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UTXOWS)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c UTXOWS)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UTXOWS)
dataTypeOf :: UTXOWS -> DataType
$cdataTypeOf :: UTXOWS -> DataType
toConstr :: UTXOWS -> Constr
$ctoConstr :: UTXOWS -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXOWS
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UTXOWS
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXOWS -> c UTXOWS
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UTXOWS -> c UTXOWS
$cp1Data :: Typeable UTXOWS
Data, Typeable)
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
/= :: UtxowsPredicateFailure -> UtxowsPredicateFailure -> Bool
$c/= :: UtxowsPredicateFailure -> UtxowsPredicateFailure -> Bool
== :: UtxowsPredicateFailure -> UtxowsPredicateFailure -> Bool
$c== :: 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
showList :: [UtxowsPredicateFailure] -> ShowS
$cshowList :: [UtxowsPredicateFailure] -> ShowS
show :: UtxowsPredicateFailure -> String
$cshow :: UtxowsPredicateFailure -> String
showsPrec :: Int -> UtxowsPredicateFailure -> ShowS
$cshowsPrec :: Int -> UtxowsPredicateFailure -> ShowS
Show, Typeable UtxowsPredicateFailure
DataType
Constr
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 -> DataType
UtxowsPredicateFailure -> Constr
(forall b. Data b => b -> b)
-> UtxowsPredicateFailure -> UtxowsPredicateFailure
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxowsPredicateFailure
-> c UtxowsPredicateFailure
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cUtxowFailure :: Constr
$tUtxowsPredicateFailure :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d)
-> UtxowsPredicateFailure -> m UtxowsPredicateFailure
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UtxowsPredicateFailure -> m UtxowsPredicateFailure
gmapQi :: Int -> (forall d. Data d => d -> u) -> UtxowsPredicateFailure -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxowsPredicateFailure -> u
gmapQ :: (forall d. Data d => d -> u) -> UtxowsPredicateFailure -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxowsPredicateFailure -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> UtxowsPredicateFailure
-> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> UtxowsPredicateFailure
-> r
gmapT :: (forall b. Data b => b -> b)
-> UtxowsPredicateFailure -> UtxowsPredicateFailure
$cgmapT :: (forall b. Data b => b -> b)
-> UtxowsPredicateFailure -> UtxowsPredicateFailure
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxowsPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UtxowsPredicateFailure)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c UtxowsPredicateFailure)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UtxowsPredicateFailure)
dataTypeOf :: UtxowsPredicateFailure -> DataType
$cdataTypeOf :: UtxowsPredicateFailure -> DataType
toConstr :: UtxowsPredicateFailure -> Constr
$ctoConstr :: UtxowsPredicateFailure -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxowsPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UtxowsPredicateFailure
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxowsPredicateFailure
-> c UtxowsPredicateFailure
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UtxowsPredicateFailure
-> c UtxowsPredicateFailure
$cp1Data :: Typeable UtxowsPredicateFailure
Data, Typeable, (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
$cto :: forall x. Rep UtxowsPredicateFailure x -> UtxowsPredicateFailure
$cfrom :: forall x. UtxowsPredicateFailure -> Rep UtxowsPredicateFailure x
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
showTypeOf :: Proxy UtxowsPredicateFailure -> String
$cshowTypeOf :: Proxy UtxowsPredicateFailure -> String
wNoThunks :: Context -> UtxowsPredicateFailure -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> UtxowsPredicateFailure -> IO (Maybe ThunkInfo)
noThunks :: Context -> UtxowsPredicateFailure -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> UtxowsPredicateFailure -> IO (Maybe ThunkInfo)
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 <- 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)
forall super (rtype :: RuleType).
Embed UTXOW super =>
RuleContext rtype UTXOW -> Rule super rtype (State UTXOW)
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) <- 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 (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)
forall super (rtype :: RuleType).
Embed UTXOW super =>
RuleContext rtype UTXOW -> Rule super rtype (State UTXOW)
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)
forall super (rtype :: RuleType).
Embed UTXOWS super =>
RuleContext rtype UTXOWS -> Rule super rtype (State UTXOWS)
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 (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 = HasTrace UTXOW => Word64 -> Gen (Environment UTXOW)
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
<$> BaseEnv UTXOW
-> Word64
-> Environment UTXOW
-> State UTXOW
-> SignalGenerator UTXOW
-> GenT Identity (Trace UTXOW)
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 (HasTrace UTXOW => SignalGenerator UTXOW
forall s. HasTrace s => SignalGenerator s
sigGen @UTXOW)