{-# LANGUAGE UndecidableInstances #-}
module Test.QuickCheck.ContractModel.Internal.Model
  ( HasSymbolics(..)
  , BaseType(..)
  , GenericHasSymbolics(..)
  , ContractModel(..)
  , createsSymbolics
  , wait
  , waitUntil
  , contractAction
  , Actions(..)
  , pattern ContractAction
  , pattern WaitUntil
  , pattern Observation
  , pattern Actions
  , Act(..)
  , mapActions
  , isBind
  , toStateModelActions
  , fromStateModelActions
  , dummyModelState
  , stateAfter
  , annotatedStateAfter
  , asserts
  ) where

import Control.Lens
import Control.Monad.Reader
import Control.Monad.Writer as Writer
import Control.Monad.State as State

import Test.QuickCheck
import Test.QuickCheck.StateModel qualified as StateModel
import Test.QuickCheck.ContractModel.Internal.Symbolics
import Test.QuickCheck.ContractModel.Internal.Spec
import Test.QuickCheck.ContractModel.Internal.Common
import Test.QuickCheck.ContractModel.Internal.ChainIndex
import Data.Data
import Data.Maybe
import Data.Map (Map)
import Data.Map qualified as Map
import GHC.Generics as Generic

import Cardano.Api

type HasActions state = ( Eq (Action state)
                        , Show (Action state)
                        , HasSymbolics (Action state)
                        , StateModel.HasVariables state
                        , StateModel.HasVariables (Action state)
                        )

class HasSymbolics a where
  getAllSymbolics :: a -> SymCollectionIndex

  default getAllSymbolics :: (Generic a, GenericHasSymbolics (Rep a)) => a -> SymCollectionIndex
  getAllSymbolics = Rep a Any -> SymCollectionIndex
forall k (f :: k -> *) (k :: k).
GenericHasSymbolics f =>
f k -> SymCollectionIndex
genericGetAllSymbolics (Rep a Any -> SymCollectionIndex)
-> (a -> Rep a Any) -> a -> SymCollectionIndex
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall a x. Generic a => a -> Rep a x
Generic.from

newtype BaseType a = BaseType a

instance HasSymbolicRep t => HasSymbolics (Symbolic t) where
  getAllSymbolics :: Symbolic t -> SymCollectionIndex
getAllSymbolics = Symbolic t -> SymCollectionIndex
forall t. HasSymbolicRep t => Symbolic t -> SymCollectionIndex
symCollect

instance HasSymbolics (BaseType a) where
  getAllSymbolics :: BaseType a -> SymCollectionIndex
getAllSymbolics BaseType a
_ = SymCollectionIndex
forall a. Monoid a => a
mempty

deriving via BaseType Integer  instance HasSymbolics Integer
deriving via BaseType Int      instance HasSymbolics Int
deriving via BaseType Char     instance HasSymbolics Char
deriving via BaseType Value    instance HasSymbolics Value
deriving via BaseType Quantity instance HasSymbolics Quantity

deriving via StateModel.HasNoVariables (AddressInEra Era) instance StateModel.HasVariables (AddressInEra Era)
deriving via StateModel.HasNoVariables Quantity instance StateModel.HasVariables Quantity
deriving via StateModel.HasNoVariables Value instance StateModel.HasVariables Value

instance (HasSymbolics k, HasSymbolics v) => HasSymbolics (Map k v) where
  getAllSymbolics :: Map k v -> SymCollectionIndex
getAllSymbolics = [(k, v)] -> SymCollectionIndex
forall a. HasSymbolics a => a -> SymCollectionIndex
getAllSymbolics ([(k, v)] -> SymCollectionIndex)
-> (Map k v -> [(k, v)]) -> Map k v -> SymCollectionIndex
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList

instance {-# OVERLAPPABLE #-} (Generic a, GenericHasSymbolics (Rep a)) => HasSymbolics a

class GenericHasSymbolics f where
  genericGetAllSymbolics :: f k -> SymCollectionIndex

instance GenericHasSymbolics f => GenericHasSymbolics (M1 i c f) where
  genericGetAllSymbolics :: M1 i c f k -> SymCollectionIndex
genericGetAllSymbolics = f k -> SymCollectionIndex
forall k (f :: k -> *) (k :: k).
GenericHasSymbolics f =>
f k -> SymCollectionIndex
genericGetAllSymbolics (f k -> SymCollectionIndex)
-> (M1 i c f k -> f k) -> M1 i c f k -> SymCollectionIndex
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f k -> f k
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1

instance HasSymbolics c => GenericHasSymbolics (K1 i c) where
  genericGetAllSymbolics :: K1 i c k -> SymCollectionIndex
genericGetAllSymbolics = c -> SymCollectionIndex
forall a. HasSymbolics a => a -> SymCollectionIndex
getAllSymbolics (c -> SymCollectionIndex)
-> (K1 i c k -> c) -> K1 i c k -> SymCollectionIndex
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c k -> c
forall i c k (p :: k). K1 i c p -> c
unK1

instance GenericHasSymbolics U1 where
  genericGetAllSymbolics :: U1 k -> SymCollectionIndex
genericGetAllSymbolics U1 k
_ = SymCollectionIndex
forall a. Monoid a => a
mempty

instance (GenericHasSymbolics f, GenericHasSymbolics g) => GenericHasSymbolics (f :*: g) where
  genericGetAllSymbolics :: (:*:) f g k -> SymCollectionIndex
genericGetAllSymbolics (f k
x :*: g k
y) = f k -> SymCollectionIndex
forall k (f :: k -> *) (k :: k).
GenericHasSymbolics f =>
f k -> SymCollectionIndex
genericGetAllSymbolics f k
x SymCollectionIndex -> SymCollectionIndex -> SymCollectionIndex
forall a. Semigroup a => a -> a -> a
<> g k -> SymCollectionIndex
forall k (f :: k -> *) (k :: k).
GenericHasSymbolics f =>
f k -> SymCollectionIndex
genericGetAllSymbolics g k
y

instance (GenericHasSymbolics f, GenericHasSymbolics g) => GenericHasSymbolics (f :+: g) where
  genericGetAllSymbolics :: (:+:) f g k -> SymCollectionIndex
genericGetAllSymbolics (L1 f k
x) = f k -> SymCollectionIndex
forall k (f :: k -> *) (k :: k).
GenericHasSymbolics f =>
f k -> SymCollectionIndex
genericGetAllSymbolics f k
x
  genericGetAllSymbolics (R1 g k
x) = g k -> SymCollectionIndex
forall k (f :: k -> *) (k :: k).
GenericHasSymbolics f =>
f k -> SymCollectionIndex
genericGetAllSymbolics g k
x

-- | A `ContractModel` instance captures everything that is needed to generate and run tests of a
--   contract or set of contracts. It specifies among other things
--
--  * what operations are supported by the contract (`Action`),
--  * when they are valid (`precondition`),
--  * how to generate random actions (`arbitraryAction`),
--  * how the operations affect the state (`nextState`), and
--  * how to run the operations in the emulator (`perform`)
class ( Typeable state
      , Show state
      , HasActions state
      ) => ContractModel state where

    -- | The type of actions that are supported by the contract. An action usually represents a single
    --   `Plutus.Trace.Emulator.callEndpoint` or a transfer of tokens, but it can be anything
    --   that can be interpreted in the `EmulatorTrace` monad.
    data Action state

    -- | Given the current model state, provide a QuickCheck generator for a random next action.
    --   This is used in the `Arbitrary` instance for `Actions`s as well as by `anyAction` and
    --   `anyActions`.
    arbitraryAction :: ModelState state -> Gen (Action state)

    -- | The name of an Action, used to report statistics.
    actionName :: Action state -> String
    actionName = [String] -> String
forall a. [a] -> a
head ([String] -> String)
-> (Action state -> [String]) -> Action state -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
words (String -> [String])
-> (Action state -> String) -> Action state -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action state -> String
forall a. Show a => a -> String
show

    -- | The probability that we will generate a `WaitUntil` in a given state
    waitProbability :: ModelState state -> Double
    waitProbability ModelState state
_ = Double
0.1

    -- | Control the distribution of how long `WaitUntil` waits
    arbitraryWaitInterval :: ModelState state -> Gen SlotNo
    arbitraryWaitInterval ModelState state
s = Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> Gen Word64 -> Gen SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64 -> Word64 -> Word64
forall a. Ord a => a -> a -> a
max Word64
10 ([Word64] -> Word64
forall a. [a] -> a
head [ Word64
5Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
*(Word64
kWord64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
-Word64
1) | Word64
k <- [Word64
0..], Word64
2Word64 -> Word64 -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^Word64
k Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> Word64
n]))
      where
        SlotNo Word64
n = ModelState state -> SlotNo
forall state. ModelState state -> SlotNo
_currentSlot ModelState state
s

    -- | The initial state, before any actions have been performed.
    initialState :: state

    -- | The `precondition` function decides if a given action is valid in a given state. Typically
    --   actions generated by `arbitraryAction` will satisfy the precondition, but if they don't
    --   they will be discarded and another action will be generated. More importantly, the
    --   preconditions are used when shrinking (see `shrinkAction`) to ensure that shrunk test cases
    --   still make sense.
    --
    --   If an explicit `action` in a `DL` scenario violates the precondition an error is raised.
    precondition :: ModelState state -> Action state -> Bool
    precondition ModelState state
_ Action state
_ = Bool
True

    -- | `nextReactiveState` is run every time the model `wait`s for a slot to be reached. This
    --   can be used to model reactive components of off-chain code.
    nextReactiveState :: SlotNo -> Spec state ()
    nextReactiveState SlotNo
_ = () -> Spec state ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    -- | This is where the model logic is defined. Given an action, `nextState` specifies the
    --   effects running that action has on the model state. It runs in the `Spec` monad, which is a
    --   state monad over the `ModelState`.
    nextState :: Action state -> Spec state ()

    -- | When a test involving random sequences of actions fails, the framework tries to find a
    --   minimal failing test case by shrinking the original failure. Action sequences are shrunk by
    --   removing individual actions, or by replacing an action by one of the (simpler) actions
    --   returned by `shrinkAction`.
    --
    --   See `Test.QuickCheck.shrink` for more information on shrinking.
    shrinkAction :: ModelState state -> Action state -> [Action state]
    shrinkAction ModelState state
_ Action state
_ = []

    restricted :: Action state -> Bool
    restricted Action state
_ = Bool
False

-- | Check if a given action creates new symbolic tokens in a given `ModelState`
createsSymbolics :: ContractModel state
                 => ModelState state
                 -> Action state
                 -> Bool
createsSymbolics :: ModelState state -> Action state -> Bool
createsSymbolics ModelState state
s Action state
a = (SymCreationIndex
forall a. Monoid a => a
mempty SymCreationIndex -> SymCreationIndex -> Bool
forall a. Eq a => a -> a -> Bool
/=) (SymCreationIndex -> Bool) -> SymCreationIndex -> Bool
forall a b. (a -> b) -> a -> b
$ State (ModelState state) SymCreationIndex
-> ModelState state -> SymCreationIndex
forall s a. State s a -> s -> a
State.evalState (ReaderT (Var SymIndex) (State (ModelState state)) SymCreationIndex
-> Var SymIndex -> State (ModelState state) SymCreationIndex
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (((), SymCreationIndex) -> SymCreationIndex
forall a b. (a, b) -> b
snd (((), SymCreationIndex) -> SymCreationIndex)
-> ReaderT
     (Var SymIndex) (State (ModelState state)) ((), SymCreationIndex)
-> ReaderT
     (Var SymIndex) (State (ModelState state)) SymCreationIndex
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  ()
-> ReaderT
     (Var SymIndex) (State (ModelState state)) ((), SymCreationIndex)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
Writer.runWriterT (Spec state ()
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     ()
forall state a.
Spec state a
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     a
unSpec (Action state -> Spec state ()
forall state. ContractModel state => Action state -> Spec state ()
nextState Action state
a)))
                                                          (Int -> Var SymIndex
forall a. Int -> Var a
StateModel.mkVar Int
0)) ModelState state
s

-- | Wait the given number of slots. Updates the `currentSlot` of the model state.
wait :: ContractModel state => Integer -> Spec state ()
wait :: Integer -> Spec state ()
wait Integer
0 = () -> Spec state ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
wait Integer
n = do
  SlotNo
now <- Getting SlotNo (ModelState (StateType (Spec state))) SlotNo
-> Spec state SlotNo
forall (m :: * -> *) a.
GetModelState m =>
Getting a (ModelState (StateType m)) a -> m a
viewModelState Getting SlotNo (ModelState (StateType (Spec state))) SlotNo
forall state. Getter (ModelState state) SlotNo
currentSlot
  SlotNo -> Spec state ()
forall state. ContractModel state => SlotNo -> Spec state ()
nextReactiveState (SlotNo
now SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ Integer -> SlotNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n)
  Setter' (ModelState state) SlotNo
-> (SlotNo -> SlotNo) -> Spec state ()
forall state a.
Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState forall state. Lens' (ModelState state) SlotNo
Setter' (ModelState state) SlotNo
currentSlotL (SlotNo -> SlotNo -> SlotNo
forall a b. a -> b -> a
const (SlotNo
now SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ Integer -> SlotNo
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n))

-- | Wait until the given slot. Has no effect if `currentSlot` is greater than the given slot.
waitUntil :: ContractModel state => SlotNo -> Spec state ()
waitUntil :: SlotNo -> Spec state ()
waitUntil SlotNo
n = do
  SlotNo
now <- Getting SlotNo (ModelState (StateType (Spec state))) SlotNo
-> Spec state SlotNo
forall (m :: * -> *) a.
GetModelState m =>
Getting a (ModelState (StateType m)) a -> m a
viewModelState Getting SlotNo (ModelState (StateType (Spec state))) SlotNo
forall state. Getter (ModelState state) SlotNo
currentSlot
  Bool -> Spec state () -> Spec state ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SlotNo
now SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo
n) (Spec state () -> Spec state ()) -> Spec state () -> Spec state ()
forall a b. (a -> b) -> a -> b
$ do
    let SlotNo Word64
n' = SlotNo
n SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
- SlotNo
now
    Integer -> Spec state ()
forall state. ContractModel state => Integer -> Spec state ()
wait (Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n')

instance ContractModel state => Show (StateModel.Action (ModelState state) a) where
    showsPrec :: Int -> Action (ModelState state) a -> ShowS
showsPrec Int
p (ContractAction _ a) = Int -> Action state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Action state
a
    showsPrec Int
p (WaitUntil n)        = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"WaitUntil " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SlotNo -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 SlotNo
n
    showsPrec Int
_ o :: Action (ModelState state) a
o@Observation{}      = String -> ShowS
showString (String -> ShowS) -> String -> ShowS
forall a b. (a -> b) -> a -> b
$ Action (ModelState state) a -> String
forall state a. StateModel state => Action state a -> String
StateModel.actionName Action (ModelState state) a
o

instance ContractModel state => Eq (StateModel.Action (ModelState state) a) where
  ContractAction b a == :: Action (ModelState state) a -> Action (ModelState state) a -> Bool
== ContractAction b' a' = (Bool
b, Action state
a) (Bool, Action state) -> (Bool, Action state) -> Bool
forall a. Eq a => a -> a -> Bool
== (Bool
b', Action state
a')
  WaitUntil s == WaitUntil s'                = SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Eq a => a -> a -> Bool
== SlotNo
s'
  Observation o _ == Observation o' _        = String
o String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
o'
  Action (ModelState state) a
_ == Action (ModelState state) a
_                                     = Bool
False

contractAction :: ContractModel state
               => ModelState state
               -> Action state
               -> StateModel.Action (ModelState state) SymIndex
contractAction :: ModelState state
-> Action state -> Action (ModelState state) SymIndex
contractAction ModelState state
s Action state
a = Bool -> Action state -> Action (ModelState state) SymIndex
forall state.
Bool -> Action state -> Action (ModelState state) SymIndex
ContractAction (ModelState state -> Action state -> Bool
forall state.
ContractModel state =>
ModelState state -> Action state -> Bool
createsSymbolics ModelState state
s Action state
a) Action state
a

instance StateModel.HasVariables (Action state) =>
          StateModel.HasVariables (StateModel.Action (ModelState state) a) where
  getAllVariables :: Action (ModelState state) a -> Set (Any Var)
getAllVariables (ContractAction _ a) = Action state -> Set (Any Var)
forall a. HasVariables a => a -> Set (Any Var)
StateModel.getAllVariables Action state
a
  getAllVariables WaitUntil{}          = Set (Any Var)
forall a. Monoid a => a
mempty
  getAllVariables Observation{}        = Set (Any Var)
forall a. Monoid a => a
mempty

instance ContractModel state => StateModel.StateModel (ModelState state) where
  data Action (ModelState state) a where
    ContractAction :: Bool
                   -> Action state
                   -> StateModel.Action (ModelState state) SymIndex
    Observation :: String
                -- Note: the `Symbolic t -> t` argument is necessary because
                -- when the user calls `observe` in their DL property to issue one
                -- of these actions they are at _generation time_ so can't do symbolic
                -- resolution up-front, instead it has to happen in the `perform`
                -- for the `Observation` action.
                -> (SymbolicSemantics -> ChainState -> Bool)
                -> StateModel.Action (ModelState state) ()
    WaitUntil :: SlotNo
              -> StateModel.Action (ModelState state) ()

  actionName :: Action (ModelState state) a -> String
actionName (ContractAction _ act) = Action state -> String
forall state. ContractModel state => Action state -> String
actionName Action state
act
  actionName WaitUntil{}            = String
"WaitUntil"
  actionName (Observation n _)      = String
"Observation[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"

  arbitraryAction :: VarContext
-> ModelState state -> Gen (Any (Action (ModelState state)))
arbitraryAction VarContext
_ ModelState state
s =
    [(Int, Gen (Any (Action (ModelState state))))]
-> Gen (Any (Action (ModelState state)))
forall a. [(Int, Gen a)] -> Gen a
frequency [( Double -> Int
forall a b. (RealFrac a, Integral b) => a -> b
floor (Double -> Int) -> Double -> Int
forall a b. (a -> b) -> a -> b
$ Double
100.0Double -> Double -> Double
forall a. Num a => a -> a -> a
*(Double
1.0Double -> Double -> Double
forall a. Num a => a -> a -> a
-ModelState state -> Double
forall state. ContractModel state => ModelState state -> Double
waitProbability ModelState state
s)
               , do Action state
a <- ModelState state -> Gen (Action state)
forall state.
ContractModel state =>
ModelState state -> Gen (Action state)
arbitraryAction ModelState state
s
                    Any (Action (ModelState state))
-> Gen (Any (Action (ModelState state)))
forall (m :: * -> *) a. Monad m => a -> m a
return (Action (ModelState state) SymIndex
-> Any (Action (ModelState state))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
StateModel.Some (Bool -> Action state -> Action (ModelState state) SymIndex
forall state.
Bool -> Action state -> Action (ModelState state) SymIndex
ContractAction (ModelState state -> Action state -> Bool
forall state.
ContractModel state =>
ModelState state -> Action state -> Bool
createsSymbolics ModelState state
s Action state
a) Action state
a)))
              ,( Double -> Int
forall a b. (RealFrac a, Integral b) => a -> b
floor (Double -> Int) -> Double -> Int
forall a b. (a -> b) -> a -> b
$ Double
100.0Double -> Double -> Double
forall a. Num a => a -> a -> a
*ModelState state -> Double
forall state. ContractModel state => ModelState state -> Double
waitProbability ModelState state
s
               , Action (ModelState state) () -> Any (Action (ModelState state))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
StateModel.Some (Action (ModelState state) () -> Any (Action (ModelState state)))
-> (SlotNo -> Action (ModelState state) ())
-> SlotNo
-> Any (Action (ModelState state))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SlotNo -> Action (ModelState state) ()
forall state. SlotNo -> Action (ModelState state) ()
WaitUntil (SlotNo -> Action (ModelState state) ())
-> (SlotNo -> SlotNo) -> SlotNo -> Action (ModelState state) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SlotNo -> SlotNo
step (SlotNo -> Any (Action (ModelState state)))
-> Gen SlotNo -> Gen (Any (Action (ModelState state)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState state -> Gen SlotNo
forall state. ContractModel state => ModelState state -> Gen SlotNo
arbitraryWaitInterval ModelState state
s)]
        where
            slot :: SlotNo
slot = ModelState state
s ModelState state
-> Getting SlotNo (ModelState state) SlotNo -> SlotNo
forall s a. s -> Getting a s a -> a
^. Getting SlotNo (ModelState state) SlotNo
forall state. Getter (ModelState state) SlotNo
currentSlot
            step :: SlotNo -> SlotNo
step SlotNo
n = SlotNo
slot SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ SlotNo
n

  shrinkAction :: VarContext
-> ModelState state
-> Action (ModelState state) a
-> [Any (Action (ModelState state))]
shrinkAction VarContext
_ ModelState state
s (ContractAction _ a) =
    [ Action (ModelState state) () -> Any (Action (ModelState state))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
StateModel.Some (SlotNo -> Action (ModelState state) ()
forall state. SlotNo -> Action (ModelState state) ()
WaitUntil (Word64 -> SlotNo
SlotNo Word64
n'))
    | let SlotNo Word64
n = Spec state ()
-> Var SymIndex -> ModelState state -> ModelState state
forall state.
Spec state ()
-> Var SymIndex -> ModelState state -> ModelState state
runSpec (Action state -> Spec state ()
forall state. ContractModel state => Action state -> Spec state ()
nextState Action state
a) (Int -> Var SymIndex
forall a. Int -> Var a
StateModel.mkVar Int
0) ModelState state
s ModelState state
-> Getting SlotNo (ModelState state) SlotNo -> SlotNo
forall s a. s -> Getting a s a -> a
^. Getting SlotNo (ModelState state) SlotNo
forall state. Getter (ModelState state) SlotNo
currentSlot
    , Word64
n' <- Word64
n Word64 -> [Word64] -> [Word64]
forall a. a -> [a] -> [a]
: Word64 -> [Word64]
forall a. Arbitrary a => a -> [a]
shrink Word64
n
    , Word64 -> SlotNo
SlotNo Word64
n' SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
> ModelState state
s ModelState state
-> Getting SlotNo (ModelState state) SlotNo -> SlotNo
forall s a. s -> Getting a s a -> a
^. Getting SlotNo (ModelState state) SlotNo
forall state. Getter (ModelState state) SlotNo
currentSlot ] [Any (Action (ModelState state))]
-> [Any (Action (ModelState state))]
-> [Any (Action (ModelState state))]
forall a. [a] -> [a] -> [a]
++
    [ Action (ModelState state) SymIndex
-> Any (Action (ModelState state))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
StateModel.Some (ModelState state
-> Action state -> Action (ModelState state) SymIndex
forall state.
ContractModel state =>
ModelState state
-> Action state -> Action (ModelState state) SymIndex
contractAction ModelState state
s Action state
a')
    | Action state
a' <- ModelState state -> Action state -> [Action state]
forall state.
ContractModel state =>
ModelState state -> Action state -> [Action state]
shrinkAction ModelState state
s Action state
a ]
  shrinkAction VarContext
_ ModelState state
s (WaitUntil (SlotNo n)) =
    [ Action (ModelState state) () -> Any (Action (ModelState state))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
StateModel.Some (SlotNo -> Action (ModelState state) ()
forall state. SlotNo -> Action (ModelState state) ()
WaitUntil (Word64 -> SlotNo
SlotNo Word64
n'))
    | Word64
n' <- Word64 -> [Word64]
forall a. Arbitrary a => a -> [a]
shrink Word64
n
    , Word64 -> SlotNo
SlotNo Word64
n' SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
> ModelState state
s ModelState state
-> Getting SlotNo (ModelState state) SlotNo -> SlotNo
forall s a. s -> Getting a s a -> a
^. Getting SlotNo (ModelState state) SlotNo
forall state. Getter (ModelState state) SlotNo
currentSlot ]
  shrinkAction VarContext
_ ModelState state
_ Observation{} = []

  initialState :: ModelState state
initialState = ModelState :: forall state.
SlotNo
-> Map (AddressInEra Era) SymValue
-> SymValue
-> SymCollectionIndex
-> [(String, Bool)]
-> Bool
-> state
-> ModelState state
ModelState { _currentSlot :: SlotNo
_currentSlot      = SlotNo
1
                            , _balanceChanges :: Map (AddressInEra Era) SymValue
_balanceChanges   = Map (AddressInEra Era) SymValue
forall a. Monoid a => a
mempty
                            , _minted :: SymValue
_minted           = SymValue
forall a. Monoid a => a
mempty
                            , _assertions :: [(String, Bool)]
_assertions       = [(String, Bool)]
forall a. Monoid a => a
mempty
                            , _assertionsOk :: Bool
_assertionsOk     = Bool
True
                            , _symbolics :: SymCollectionIndex
_symbolics        = SymCollectionIndex
forall a. Monoid a => a
mempty
                            , _contractState :: state
_contractState    = state
forall state. ContractModel state => state
initialState
                            }

  nextState :: ModelState state
-> Action (ModelState state) a -> Var a -> ModelState state
nextState ModelState state
s (ContractAction _ cmd) Var a
v = Spec state ()
-> Var SymIndex -> ModelState state -> ModelState state
forall state.
Spec state ()
-> Var SymIndex -> ModelState state -> ModelState state
runSpec (Action state -> Spec state ()
forall state. ContractModel state => Action state -> Spec state ()
nextState Action state
cmd) Var a
Var SymIndex
v ModelState state
s
  nextState ModelState state
s (WaitUntil n) Var a
_          = Spec state ()
-> Var SymIndex -> ModelState state -> ModelState state
forall state.
Spec state ()
-> Var SymIndex -> ModelState state -> ModelState state
runSpec (() () -> Spec state () -> Spec state ()
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ SlotNo -> Spec state ()
forall state. ContractModel state => SlotNo -> Spec state ()
waitUntil SlotNo
n) (String -> Var SymIndex
forall a. HasCallStack => String -> a
error String
"unreachable") ModelState state
s
  nextState ModelState state
s (Observation _ _) Var a
_      = ModelState state
s

  -- Note that the order of the preconditions in this case matter - we want to run
  -- `getAllSymbolics` last because its likely to be stricter than the user precondition
  -- and so if the user relies on the lazyness of the Gen monad by using the precondition
  -- to avoid duplicate checks in the precondition and generator we don't screw that up.
  precondition :: ModelState state -> Action (ModelState state) a -> Bool
precondition ModelState state
s (ContractAction _ cmd) = ModelState state
s ModelState state -> Getting Bool (ModelState state) Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool (ModelState state) Bool
forall state. Lens' (ModelState state) Bool
assertionsOk
                                        Bool -> Bool -> Bool
&& ModelState state -> Action state -> Bool
forall state.
ContractModel state =>
ModelState state -> Action state -> Bool
precondition ModelState state
s Action state
cmd
                                        Bool -> Bool -> Bool
&& Action state -> SymCollectionIndex
forall a. HasSymbolics a => a -> SymCollectionIndex
getAllSymbolics Action state
cmd SymCollectionIndex -> SymCollectionIndex -> Bool
`symCollectionSubset` (ModelState state
s ModelState state
-> Getting SymCollectionIndex (ModelState state) SymCollectionIndex
-> SymCollectionIndex
forall s a. s -> Getting a s a -> a
^. Getting SymCollectionIndex (ModelState state) SymCollectionIndex
forall state. Lens' (ModelState state) SymCollectionIndex
symbolics)
  precondition ModelState state
s (WaitUntil n)          = SlotNo
n SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
> ModelState state
s ModelState state
-> Getting SlotNo (ModelState state) SlotNo -> SlotNo
forall s a. s -> Getting a s a -> a
^. Getting SlotNo (ModelState state) SlotNo
forall state. Getter (ModelState state) SlotNo
currentSlot
  precondition ModelState state
_ Observation{}          = Bool
True

-- We include a list of rejected action names.
data Actions s = Actions_ [String] (Smart [Act s])

{-# COMPLETE Actions #-}
pattern Actions :: [Act s] -> Actions s
pattern $bActions :: [Act s] -> Actions s
$mActions :: forall r s. Actions s -> ([Act s] -> r) -> (Void# -> r) -> r
Actions as <- Actions_ _ (Smart _ as) where
  Actions [Act s]
as = [String] -> Smart [Act s] -> Actions s
forall s. [String] -> Smart [Act s] -> Actions s
Actions_ [] (Int -> [Act s] -> Smart [Act s]
forall a. Int -> a -> Smart a
Smart Int
0 [Act s]
as)

data Act s = Bind   {Act s -> Var SymIndex
varOf :: StateModel.Var SymIndex, Act s -> Action s
actionOf :: Action s}
           | NoBind {varOf :: StateModel.Var SymIndex, actionOf :: Action s}
           | ActWaitUntil (StateModel.Var ()) SlotNo
           | ActObservation (StateModel.Var ()) String (SymbolicSemantics -> ChainState -> Bool)

mapActions :: (Action s -> Action s') -> Actions s -> Actions s'
mapActions :: (Action s -> Action s') -> Actions s -> Actions s'
mapActions Action s -> Action s'
f (Actions_ [String]
rej (Smart Int
n [Act s]
as)) = [String] -> Smart [Act s'] -> Actions s'
forall s. [String] -> Smart [Act s] -> Actions s
Actions_ [String]
rej (Smart [Act s'] -> Actions s') -> Smart [Act s'] -> Actions s'
forall a b. (a -> b) -> a -> b
$ Int -> [Act s'] -> Smart [Act s']
forall a. Int -> a -> Smart a
Smart Int
n ([Act s'] -> Smart [Act s']) -> [Act s'] -> Smart [Act s']
forall a b. (a -> b) -> a -> b
$ (Act s -> Act s') -> [Act s] -> [Act s']
forall a b. (a -> b) -> [a] -> [b]
map Act s -> Act s'
mapAct [Act s]
as
  where
    mapAct :: Act s -> Act s'
mapAct (Bind Var SymIndex
x Action s
a)             = Var SymIndex -> Action s' -> Act s'
forall s. Var SymIndex -> Action s -> Act s
Bind Var SymIndex
x (Action s -> Action s'
f Action s
a)
    mapAct (NoBind Var SymIndex
x Action s
a)           = Var SymIndex -> Action s' -> Act s'
forall s. Var SymIndex -> Action s -> Act s
NoBind Var SymIndex
x (Action s -> Action s'
f Action s
a)
    mapAct (ActWaitUntil Var ()
x SlotNo
n)     = Var () -> SlotNo -> Act s'
forall s. Var () -> SlotNo -> Act s
ActWaitUntil Var ()
x SlotNo
n
    mapAct (ActObservation Var ()
x String
n SymbolicSemantics -> ChainState -> Bool
p) = Var ()
-> String -> (SymbolicSemantics -> ChainState -> Bool) -> Act s'
forall s.
Var ()
-> String -> (SymbolicSemantics -> ChainState -> Bool) -> Act s
ActObservation Var ()
x String
n SymbolicSemantics -> ChainState -> Bool
p

instance ContractModel s => Eq (Act s) where
  Bind Var SymIndex
v Action s
a             == :: Act s -> Act s -> Bool
== Bind Var SymIndex
v' Action s
a'             = (Var SymIndex
v, Action s
a) (Var SymIndex, Action s) -> (Var SymIndex, Action s) -> Bool
forall a. Eq a => a -> a -> Bool
== (Var SymIndex
v', Action s
a')
  NoBind Var SymIndex
v Action s
a           == NoBind Var SymIndex
v' Action s
a'           = (Var SymIndex
v, Action s
a) (Var SymIndex, Action s) -> (Var SymIndex, Action s) -> Bool
forall a. Eq a => a -> a -> Bool
== (Var SymIndex
v', Action s
a')
  ActWaitUntil Var ()
v SlotNo
s     == ActWaitUntil Var ()
v' SlotNo
s'     = (Var ()
v, SlotNo
s) (Var (), SlotNo) -> (Var (), SlotNo) -> Bool
forall a. Eq a => a -> a -> Bool
== (Var ()
v', SlotNo
s')
  ActObservation Var ()
v String
n SymbolicSemantics -> ChainState -> Bool
_ == ActObservation Var ()
v' String
n' SymbolicSemantics -> ChainState -> Bool
_ = (Var ()
v, String
n) (Var (), String) -> (Var (), String) -> Bool
forall a. Eq a => a -> a -> Bool
== (Var ()
v', String
n')
  Act s
_                    == Act s
_                      = Bool
False

isBind :: Act s -> Bool
isBind :: Act s -> Bool
isBind Bind{} = Bool
True
isBind Act s
_      = Bool
False

instance ContractModel state => Show (Act state) where
  showsPrec :: Int -> Act state -> ShowS
showsPrec Int
d (Bind Var SymIndex
v Action state
a) =
    Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString (String
"tok." String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var SymIndex -> String
forall a. Show a => a -> String
show Var SymIndex
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" := ") ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Action state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 Action state
a
  showsPrec Int
d (ActWaitUntil Var ()
_ SlotNo
n) = Int -> Action (ModelState state) () -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d (SlotNo -> Action (ModelState state) ()
forall state. SlotNo -> Action (ModelState state) ()
WaitUntil @state SlotNo
n)
  showsPrec Int
d (ActObservation Var ()
_ String
n SymbolicSemantics -> ChainState -> Bool
p) = Int -> Action (ModelState state) () -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d (String
-> (SymbolicSemantics -> ChainState -> Bool)
-> Action (ModelState state) ()
forall state.
String
-> (SymbolicSemantics -> ChainState -> Bool)
-> Action (ModelState state) ()
Observation @state String
n SymbolicSemantics -> ChainState -> Bool
p)
  showsPrec Int
d (NoBind Var SymIndex
_ Action state
a) =
    Int -> Action state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d Action state
a

instance ContractModel state => Show (Actions state) where
  showsPrec :: Int -> Actions state -> ShowS
showsPrec Int
d (Actions [Act state]
as)
    | Int
dInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
10      = (String
"("String -> ShowS
forall a. [a] -> [a] -> [a]
++)ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Int -> Actions state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 ([Act state] -> Actions state
forall s. [Act s] -> Actions s
Actions [Act state]
as)ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(String
")"String -> ShowS
forall a. [a] -> [a] -> [a]
++)
    | [Act state] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Act state]
as   = (String
"Actions []"String -> ShowS
forall a. [a] -> [a] -> [a]
++)
    | Bool
otherwise = (String
"Actions \n [" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                  (ShowS -> ShowS -> ShowS) -> ShowS -> [ShowS] -> ShowS
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) (Int -> Act state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 ([Act state] -> Act state
forall a. [a] -> a
last [Act state]
as) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"]"String -> ShowS
forall a. [a] -> [a] -> [a]
++))
                    [Int -> Act state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 Act state
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
",\n  "String -> ShowS
forall a. [a] -> [a] -> [a]
++) | Act state
a <- [Act state] -> [Act state]
forall a. [a] -> [a]
init [Act state]
as]

instance ContractModel s => Arbitrary (Actions s) where
  arbitrary :: Gen (Actions s)
arbitrary = Actions (ModelState s) -> Actions s
forall s. Actions (ModelState s) -> Actions s
fromStateModelActions (Actions (ModelState s) -> Actions s)
-> Gen (Actions (ModelState s)) -> Gen (Actions s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Actions (ModelState s))
forall a. Arbitrary a => Gen a
arbitrary
  shrink :: Actions s -> [Actions s]
shrink = (Actions (ModelState s) -> Actions s)
-> [Actions (ModelState s)] -> [Actions s]
forall a b. (a -> b) -> [a] -> [b]
map Actions (ModelState s) -> Actions s
forall s. Actions (ModelState s) -> Actions s
fromStateModelActions ([Actions (ModelState s)] -> [Actions s])
-> (Actions s -> [Actions (ModelState s)])
-> Actions s
-> [Actions s]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions (ModelState s) -> [Actions (ModelState s)]
forall a. Arbitrary a => a -> [a]
shrink (Actions (ModelState s) -> [Actions (ModelState s)])
-> (Actions s -> Actions (ModelState s))
-> Actions s
-> [Actions (ModelState s)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions s -> Actions (ModelState s)
forall state.
ContractModel state =>
Actions state -> Actions (ModelState state)
toStateModelActions

toStateModelActions :: ContractModel state =>
                        Actions state -> StateModel.Actions (ModelState state)
toStateModelActions :: Actions state -> Actions (ModelState state)
toStateModelActions (Actions_ [String]
rs (Smart Int
k [Act state]
s)) =
  [String]
-> Smart [Step (ModelState state)] -> Actions (ModelState state)
forall state. [String] -> Smart [Step state] -> Actions state
StateModel.Actions_ [String]
rs (Int -> [Step (ModelState state)] -> Smart [Step (ModelState state)]
forall a. Int -> a -> Smart a
Smart Int
k ([Step (ModelState state)] -> Smart [Step (ModelState state)])
-> [Step (ModelState state)] -> Smart [Step (ModelState state)]
forall a b. (a -> b) -> a -> b
$ (Act state -> Step (ModelState state))
-> [Act state] -> [Step (ModelState state)]
forall a b. (a -> b) -> [a] -> [b]
map Act state -> Step (ModelState state)
forall state.
ContractModel state =>
Act state -> Step (ModelState state)
mkStep [Act state]
s)
    where mkStep :: Act state -> Step (ModelState state)
mkStep (ActWaitUntil Var ()
v SlotNo
n) = Var ()
v Var () -> Action (ModelState state) () -> Step (ModelState state)
forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
StateModel.:= SlotNo -> Action (ModelState state) ()
forall state. SlotNo -> Action (ModelState state) ()
WaitUntil SlotNo
n
          mkStep (ActObservation Var ()
v String
n SymbolicSemantics -> ChainState -> Bool
p) = Var ()
v Var () -> Action (ModelState state) () -> Step (ModelState state)
forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
StateModel.:= String
-> (SymbolicSemantics -> ChainState -> Bool)
-> Action (ModelState state) ()
forall state.
String
-> (SymbolicSemantics -> ChainState -> Bool)
-> Action (ModelState state) ()
Observation String
n SymbolicSemantics -> ChainState -> Bool
p
          mkStep Act state
act                = Act state -> Var SymIndex
forall s. Act s -> Var SymIndex
varOf Act state
act Var SymIndex
-> Action (ModelState state) SymIndex -> Step (ModelState state)
forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
StateModel.:= Bool -> Action state -> Action (ModelState state) SymIndex
forall state.
Bool -> Action state -> Action (ModelState state) SymIndex
ContractAction (Act state -> Bool
forall s. Act s -> Bool
isBind Act state
act) (Act state -> Action state
forall s. Act s -> Action s
actionOf Act state
act)

fromStateModelActions :: StateModel.Actions (ModelState s) -> Actions s
fromStateModelActions :: Actions (ModelState s) -> Actions s
fromStateModelActions (StateModel.Actions_ [String]
rs (Smart Int
k [Step (ModelState s)]
s)) =
  [String] -> Smart [Act s] -> Actions s
forall s. [String] -> Smart [Act s] -> Actions s
Actions_ [String]
rs (Int -> [Act s] -> Smart [Act s]
forall a. Int -> a -> Smart a
Smart Int
k ([Maybe (Act s)] -> [Act s]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Act s)] -> [Act s]) -> [Maybe (Act s)] -> [Act s]
forall a b. (a -> b) -> a -> b
$ (Step (ModelState s) -> Maybe (Act s))
-> [Step (ModelState s)] -> [Maybe (Act s)]
forall a b. (a -> b) -> [a] -> [b]
map Step (ModelState s) -> Maybe (Act s)
forall s. Step (ModelState s) -> Maybe (Act s)
mkAct [Step (ModelState s)]
s))
  where
    mkAct :: StateModel.Step (ModelState s) -> Maybe (Act s)
    mkAct :: Step (ModelState s) -> Maybe (Act s)
mkAct (Var a
v StateModel.:= ContractAction b act)
          | Bool
b         = Act s -> Maybe (Act s)
forall a. a -> Maybe a
Just (Act s -> Maybe (Act s)) -> Act s -> Maybe (Act s)
forall a b. (a -> b) -> a -> b
$ Var SymIndex -> Action s -> Act s
forall s. Var SymIndex -> Action s -> Act s
Bind   Var a
Var SymIndex
v Action s
act
          | Bool
otherwise = Act s -> Maybe (Act s)
forall a. a -> Maybe a
Just (Act s -> Maybe (Act s)) -> Act s -> Maybe (Act s)
forall a b. (a -> b) -> a -> b
$ Var SymIndex -> Action s -> Act s
forall s. Var SymIndex -> Action s -> Act s
NoBind Var a
Var SymIndex
v Action s
act
    mkAct (Var a
v StateModel.:= WaitUntil n) = Act s -> Maybe (Act s)
forall a. a -> Maybe a
Just (Act s -> Maybe (Act s)) -> Act s -> Maybe (Act s)
forall a b. (a -> b) -> a -> b
$ Var () -> SlotNo -> Act s
forall s. Var () -> SlotNo -> Act s
ActWaitUntil Var a
Var ()
v SlotNo
n
    mkAct (Var a
v StateModel.:= Observation n p) = Act s -> Maybe (Act s)
forall a. a -> Maybe a
Just (Act s -> Maybe (Act s)) -> Act s -> Maybe (Act s)
forall a b. (a -> b) -> a -> b
$ Var ()
-> String -> (SymbolicSemantics -> ChainState -> Bool) -> Act s
forall s.
Var ()
-> String -> (SymbolicSemantics -> ChainState -> Bool) -> Act s
ActObservation Var a
Var ()
v String
n SymbolicSemantics -> ChainState -> Bool
p

dummyModelState :: state -> ModelState state
dummyModelState :: state -> ModelState state
dummyModelState state
s = SlotNo
-> Map (AddressInEra Era) SymValue
-> SymValue
-> SymCollectionIndex
-> [(String, Bool)]
-> Bool
-> state
-> ModelState state
forall state.
SlotNo
-> Map (AddressInEra Era) SymValue
-> SymValue
-> SymCollectionIndex
-> [(String, Bool)]
-> Bool
-> state
-> ModelState state
ModelState SlotNo
1 Map (AddressInEra Era) SymValue
forall k a. Map k a
Map.empty SymValue
forall a. Monoid a => a
mempty SymCollectionIndex
forall a. Monoid a => a
mempty [(String, Bool)]
forall a. Monoid a => a
mempty Bool
True state
s

stateAfter :: ContractModel state => Actions state -> ModelState state
stateAfter :: Actions state -> ModelState state
stateAfter = Annotated (ModelState state) -> ModelState state
forall state. Annotated state -> state
StateModel.underlyingState (Annotated (ModelState state) -> ModelState state)
-> (Actions state -> Annotated (ModelState state))
-> Actions state
-> ModelState state
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions (ModelState state) -> Annotated (ModelState state)
forall state. StateModel state => Actions state -> Annotated state
StateModel.stateAfter (Actions (ModelState state) -> Annotated (ModelState state))
-> (Actions state -> Actions (ModelState state))
-> Actions state
-> Annotated (ModelState state)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions state -> Actions (ModelState state)
forall state.
ContractModel state =>
Actions state -> Actions (ModelState state)
toStateModelActions

annotatedStateAfter :: ContractModel state => Actions state -> StateModel.Annotated (ModelState state)
annotatedStateAfter :: Actions state -> Annotated (ModelState state)
annotatedStateAfter = Actions (ModelState state) -> Annotated (ModelState state)
forall state. StateModel state => Actions state -> Annotated state
StateModel.stateAfter (Actions (ModelState state) -> Annotated (ModelState state))
-> (Actions state -> Actions (ModelState state))
-> Actions state
-> Annotated (ModelState state)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions state -> Actions (ModelState state)
forall state.
ContractModel state =>
Actions state -> Actions (ModelState state)
toStateModelActions

-- TODO: this should probably have a better name.
-- Alternatively what we save in the
-- model state should just be a property.
asserts :: ModelState state -> Property
asserts :: ModelState state -> Property
asserts ModelState state
finalState = (Property -> Property -> Property)
-> Property -> [Property] -> Property
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
(.&&.) (Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True) [ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"assertSpec failed: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Bool
b
                                                  | (String
s, Bool
b) <- ModelState state
finalState ModelState state
-> Getting [(String, Bool)] (ModelState state) [(String, Bool)]
-> [(String, Bool)]
forall s a. s -> Getting a s a -> a
^. Getting [(String, Bool)] (ModelState state) [(String, Bool)]
forall state. Lens' (ModelState state) [(String, Bool)]
assertions ]