{-# 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
UTXOWS -> DataType
UTXOWS -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> UTXOWS -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UTXOWS -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> UTXOWS -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UTXOWS -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data)

data UtxowsPredicateFailure
  = UtxowFailure (PredicateFailure UTXOW)
  deriving (UtxowsPredicateFailure -> UtxowsPredicateFailure -> Bool
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
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
UtxowsPredicateFailure -> DataType
UtxowsPredicateFailure -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(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 :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxowsPredicateFailure -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UtxowsPredicateFailure -> u
gmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxowsPredicateFailure -> [u]
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> UtxowsPredicateFailure -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, 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
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 <- 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 forall a b. (a -> b) -> a -> b
$ forall sts. Environment sts -> IRC sts
IRC Environment UTXOWS
env
    ]

  transitionRules :: [TransitionRule UTXOWS]
transitionRules =
    [ do
        TRC (Environment UTXOWS
env, State UTXOWS
utxo, Signal UTXOWS
txWits) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        case (Signal UTXOWS
txWits :: [Tx]) of
          [] -> forall (m :: * -> *) a. Monad m => a -> m a
return State UTXOWS
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 forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment UTXOWS
env, State UTXOWS
utxo, Tx
tx)
            UTxOState
utxo'' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UTXOWS forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment UTXOWS
env, UTxOState
utxo', [Tx]
gamma)
            forall (m :: * -> *) a. Monad m => a -> m a
return UTxOState
utxo''
    ]

instance Embed UTXOW UTXOWS where
  wrapFailed :: PredicateFailure UTXOW -> PredicateFailure UTXOWS
wrapFailed = 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 =
    forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst 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 UTXOWS
env State UTXOWS
st (forall s. HasTrace s => SignalGenerator s
sigGen @UTXOW)