{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

-- | Transition system that models the application of multiple transactions to
-- the UTxO part of the ledger state.
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

  -- We generate signal for UTXOWS as a list of signals from 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)