module Test.QuickCheck.ContractModel.Internal.Spec where

import Control.Monad.Morph
import Control.Monad.State as State
import Control.Monad.Reader
import Control.Monad.Writer as Writer
import Test.QuickCheck.StateModel
import Data.Map (Map)
import Cardano.Api
import Test.QuickCheck.ContractModel.Internal.Symbolics
import Test.QuickCheck.ContractModel.Internal.Common
import Control.Lens
import Data.Foldable
import Data.Coerce

-- | The `ModelState` models the state of the blockchain. It contains,
--
--   * the contract-specific state (`contractState`)
--   * the current slot (`currentSlot`)
--   * the wallet balances (`balances`)
--   * the amount that has been minted (`minted`)
data ModelState state = ModelState
        { ModelState state -> SlotNo
_currentSlot    :: SlotNo
        , ModelState state -> Map (AddressInEra Era) SymValue
_balanceChanges :: Map (AddressInEra Era) SymValue
        , ModelState state -> SymValue
_minted         :: SymValue
        , ModelState state -> SymCollectionIndex
_symbolics      :: SymCollectionIndex
        , ModelState state -> [(String, Bool)]
_assertions     :: [(String, Bool)]
        , ModelState state -> Bool
_assertionsOk   :: Bool
        , ModelState state -> state
_contractState  :: state
        }
  deriving stock (Int -> ModelState state -> ShowS
[ModelState state] -> ShowS
ModelState state -> String
(Int -> ModelState state -> ShowS)
-> (ModelState state -> String)
-> ([ModelState state] -> ShowS)
-> Show (ModelState state)
forall state. Show state => Int -> ModelState state -> ShowS
forall state. Show state => [ModelState state] -> ShowS
forall state. Show state => ModelState state -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModelState state] -> ShowS
$cshowList :: forall state. Show state => [ModelState state] -> ShowS
show :: ModelState state -> String
$cshow :: forall state. Show state => ModelState state -> String
showsPrec :: Int -> ModelState state -> ShowS
$cshowsPrec :: forall state. Show state => Int -> ModelState state -> ShowS
Show, (forall x. ModelState state -> Rep (ModelState state) x)
-> (forall x. Rep (ModelState state) x -> ModelState state)
-> Generic (ModelState state)
forall x. Rep (ModelState state) x -> ModelState state
forall x. ModelState state -> Rep (ModelState state) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall state x. Rep (ModelState state) x -> ModelState state
forall state x. ModelState state -> Rep (ModelState state) x
$cto :: forall state x. Rep (ModelState state) x -> ModelState state
$cfrom :: forall state x. ModelState state -> Rep (ModelState state) x
Generic)

instance Functor ModelState where
  fmap :: (a -> b) -> ModelState a -> ModelState b
fmap a -> b
f ModelState a
m = ModelState a
m { _contractState :: b
_contractState = a -> b
f (ModelState a -> a
forall state. ModelState state -> state
_contractState ModelState a
m) }

-- | The `Spec` monad is a state monad over the `ModelState` with reader and writer components to keep track
--   of newly created symbolic tokens. It is used exclusively by the `nextState` function to model the effects
--   of an action on the blockchain.
newtype Spec state a = Spec { Spec state a
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     a
unSpec :: WriterT SymCreationIndex (ReaderT (Var SymIndex) (State (ModelState state))) a }
    deriving newtype (a -> Spec state b -> Spec state a
(a -> b) -> Spec state a -> Spec state b
(forall a b. (a -> b) -> Spec state a -> Spec state b)
-> (forall a b. a -> Spec state b -> Spec state a)
-> Functor (Spec state)
forall a b. a -> Spec state b -> Spec state a
forall a b. (a -> b) -> Spec state a -> Spec state b
forall state a b. a -> Spec state b -> Spec state a
forall state a b. (a -> b) -> Spec state a -> Spec state b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Spec state b -> Spec state a
$c<$ :: forall state a b. a -> Spec state b -> Spec state a
fmap :: (a -> b) -> Spec state a -> Spec state b
$cfmap :: forall state a b. (a -> b) -> Spec state a -> Spec state b
Functor, Functor (Spec state)
a -> Spec state a
Functor (Spec state)
-> (forall a. a -> Spec state a)
-> (forall a b.
    Spec state (a -> b) -> Spec state a -> Spec state b)
-> (forall a b c.
    (a -> b -> c) -> Spec state a -> Spec state b -> Spec state c)
-> (forall a b. Spec state a -> Spec state b -> Spec state b)
-> (forall a b. Spec state a -> Spec state b -> Spec state a)
-> Applicative (Spec state)
Spec state a -> Spec state b -> Spec state b
Spec state a -> Spec state b -> Spec state a
Spec state (a -> b) -> Spec state a -> Spec state b
(a -> b -> c) -> Spec state a -> Spec state b -> Spec state c
forall state. Functor (Spec state)
forall a. a -> Spec state a
forall state a. a -> Spec state a
forall a b. Spec state a -> Spec state b -> Spec state a
forall a b. Spec state a -> Spec state b -> Spec state b
forall a b. Spec state (a -> b) -> Spec state a -> Spec state b
forall state a b. Spec state a -> Spec state b -> Spec state a
forall state a b. Spec state a -> Spec state b -> Spec state b
forall state a b.
Spec state (a -> b) -> Spec state a -> Spec state b
forall a b c.
(a -> b -> c) -> Spec state a -> Spec state b -> Spec state c
forall state a b c.
(a -> b -> c) -> Spec state a -> Spec state b -> Spec state c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: Spec state a -> Spec state b -> Spec state a
$c<* :: forall state a b. Spec state a -> Spec state b -> Spec state a
*> :: Spec state a -> Spec state b -> Spec state b
$c*> :: forall state a b. Spec state a -> Spec state b -> Spec state b
liftA2 :: (a -> b -> c) -> Spec state a -> Spec state b -> Spec state c
$cliftA2 :: forall state a b c.
(a -> b -> c) -> Spec state a -> Spec state b -> Spec state c
<*> :: Spec state (a -> b) -> Spec state a -> Spec state b
$c<*> :: forall state a b.
Spec state (a -> b) -> Spec state a -> Spec state b
pure :: a -> Spec state a
$cpure :: forall state a. a -> Spec state a
$cp1Applicative :: forall state. Functor (Spec state)
Applicative, Applicative (Spec state)
a -> Spec state a
Applicative (Spec state)
-> (forall a b.
    Spec state a -> (a -> Spec state b) -> Spec state b)
-> (forall a b. Spec state a -> Spec state b -> Spec state b)
-> (forall a. a -> Spec state a)
-> Monad (Spec state)
Spec state a -> (a -> Spec state b) -> Spec state b
Spec state a -> Spec state b -> Spec state b
forall state. Applicative (Spec state)
forall a. a -> Spec state a
forall state a. a -> Spec state a
forall a b. Spec state a -> Spec state b -> Spec state b
forall a b. Spec state a -> (a -> Spec state b) -> Spec state b
forall state a b. Spec state a -> Spec state b -> Spec state b
forall state a b.
Spec state a -> (a -> Spec state b) -> Spec state b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> Spec state a
$creturn :: forall state a. a -> Spec state a
>> :: Spec state a -> Spec state b -> Spec state b
$c>> :: forall state a b. Spec state a -> Spec state b -> Spec state b
>>= :: Spec state a -> (a -> Spec state b) -> Spec state b
$c>>= :: forall state a b.
Spec state a -> (a -> Spec state b) -> Spec state b
$cp1Monad :: forall state. Applicative (Spec state)
Monad)

coerceSpec :: forall s s' a. Coercible s s' => Spec s a -> Spec s' a
coerceSpec :: Spec s a -> Spec s' a
coerceSpec (Spec WriterT
  SymCreationIndex (ReaderT (Var SymIndex) (State (ModelState s))) a
spec) = do
  ModelState s'
s' <- WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState s')))
  (ModelState s')
-> Spec s' (ModelState s')
forall state a.
WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  a
-> Spec state a
Spec (WriterT
   SymCreationIndex
   (ReaderT (Var SymIndex) (State (ModelState s')))
   (ModelState s')
 -> Spec s' (ModelState s'))
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState s')))
     (ModelState s')
-> Spec s' (ModelState s')
forall a b. (a -> b) -> a -> b
$ WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState s')))
  (ModelState s')
forall s (m :: * -> *). MonadState s m => m s
get
  WriterT
  SymCreationIndex (ReaderT (Var SymIndex) (State (ModelState s'))) a
-> Spec s' a
forall state a.
WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  a
-> Spec state a
Spec (WriterT
   SymCreationIndex (ReaderT (Var SymIndex) (State (ModelState s'))) a
 -> Spec s' a)
-> WriterT
     SymCreationIndex (ReaderT (Var SymIndex) (State (ModelState s'))) a
-> Spec s' a
forall a b. (a -> b) -> a -> b
$ (forall a.
 ReaderT (Var SymIndex) (State (ModelState s)) a
 -> ReaderT (Var SymIndex) (State (ModelState s')) a)
-> WriterT
     SymCreationIndex (ReaderT (Var SymIndex) (State (ModelState s))) a
-> WriterT
     SymCreationIndex (ReaderT (Var SymIndex) (State (ModelState s'))) a
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist ((forall a. State (ModelState s) a -> State (ModelState s') a)
-> ReaderT (Var SymIndex) (State (ModelState s)) a
-> ReaderT (Var SymIndex) (State (ModelState s')) a
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist ((forall a. State (ModelState s) a -> State (ModelState s') a)
 -> ReaderT (Var SymIndex) (State (ModelState s)) a
 -> ReaderT (Var SymIndex) (State (ModelState s')) a)
-> (forall a. State (ModelState s) a -> State (ModelState s') a)
-> ReaderT (Var SymIndex) (State (ModelState s)) a
-> ReaderT (Var SymIndex) (State (ModelState s')) a
forall a b. (a -> b) -> a -> b
$ \ State (ModelState s) a
stateful -> let (a
a, ModelState s
s) = State (ModelState s) a -> ModelState s -> (a, ModelState s)
forall s a. State s a -> s -> (a, s)
runState State (ModelState s) a
stateful (ModelState s' -> ModelState s
coerce ModelState s'
s') in ModelState s' -> State (ModelState s') ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ModelState s -> ModelState s'
coerce ModelState s
s) State (ModelState s') ()
-> State (ModelState s') a -> State (ModelState s') a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> State (ModelState s') a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a) WriterT
  SymCreationIndex (ReaderT (Var SymIndex) (State (ModelState s))) a
spec

instance MonadState state (Spec state) where
  state :: (state -> (a, state)) -> Spec state a
state state -> (a, state)
f = WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  a
-> Spec state a
forall state a.
WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  a
-> Spec state a
Spec (WriterT
   SymCreationIndex
   (ReaderT (Var SymIndex) (State (ModelState state)))
   a
 -> Spec state a)
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     a
-> Spec state a
forall a b. (a -> b) -> a -> b
$ (ModelState state -> (a, ModelState state))
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
State.state ((ModelState state -> (a, ModelState state))
 -> WriterT
      SymCreationIndex
      (ReaderT (Var SymIndex) (State (ModelState state)))
      a)
-> (ModelState state -> (a, ModelState state))
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     a
forall a b. (a -> b) -> a -> b
$ \ModelState state
s -> case state -> (a, state)
f (ModelState state -> state
forall state. ModelState state -> state
_contractState ModelState state
s) of
      (a
a, state
cs) -> (a
a, ModelState state
s { _contractState :: state
_contractState = state
cs })
  {-# INLINE state #-}

  get :: Spec state state
get = WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  state
-> Spec state state
forall state a.
WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  a
-> Spec state a
Spec (WriterT
   SymCreationIndex
   (ReaderT (Var SymIndex) (State (ModelState state)))
   state
 -> Spec state state)
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     state
-> Spec state state
forall a b. (a -> b) -> a -> b
$ (ModelState state -> state)
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     (ModelState state)
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModelState state -> state
forall state. ModelState state -> state
_contractState WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  (ModelState state)
forall s (m :: * -> *). MonadState s m => m s
State.get
  {-# INLINE get #-}

  put :: state -> Spec state ()
put state
cs = WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  ()
-> Spec state ()
forall state a.
WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  a
-> Spec state a
Spec (WriterT
   SymCreationIndex
   (ReaderT (Var SymIndex) (State (ModelState state)))
   ()
 -> Spec state ())
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     ()
-> Spec state ()
forall a b. (a -> b) -> a -> b
$ (ModelState state -> ModelState state)
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
State.modify' ((ModelState state -> ModelState state)
 -> WriterT
      SymCreationIndex
      (ReaderT (Var SymIndex) (State (ModelState state)))
      ())
-> (ModelState state -> ModelState state)
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     ()
forall a b. (a -> b) -> a -> b
$ \ModelState state
s -> ModelState state
s { _contractState :: state
_contractState = state
cs }
  {-# INLINE put #-}

-- | Lens for the contract-specific part of the model state.
makeLensesFor [("_contractState",  "contractState")]   'ModelState
makeLensesFor [("_currentSlot",    "currentSlotL")]    'ModelState
makeLensesFor [("_lastSlot",       "lastSlotL")]       'ModelState
makeLensesFor [("_balanceChanges", "balanceChangesL")] 'ModelState
makeLensesFor [("_minted",         "mintedL")]         'ModelState
makeLensesFor [("_assertions", "assertions")]          'ModelState
makeLensesFor [("_assertionsOk", "assertionsOk")]      'ModelState
makeLensesFor [("_symbolics", "symbolics")]            'ModelState

-- | Get the current slot.
--
--   `Spec` monad update functions: `wait` and `waitUntil`.
currentSlot :: Getter (ModelState state) SlotNo
currentSlot :: (SlotNo -> f SlotNo) -> ModelState state -> f (ModelState state)
currentSlot = (SlotNo -> f SlotNo) -> ModelState state -> f (ModelState state)
forall state. Lens' (ModelState state) SlotNo
currentSlotL

-- | Get the current wallet balance changes. These are delta balances, so they start out at zero and
--   can be negative. The absolute balances used by the emulator can be set in the `CheckOptions`
--   argument to `propRunActionsWithOptions`.
--
--   `Spec` monad update functions: `withdraw`, `deposit`, `transfer`.
balanceChanges :: Getter (ModelState state) (Map (AddressInEra Era) SymValue)
balanceChanges :: (Map (AddressInEra Era) SymValue
 -> f (Map (AddressInEra Era) SymValue))
-> ModelState state -> f (ModelState state)
balanceChanges = (Map (AddressInEra Era) SymValue
 -> f (Map (AddressInEra Era) SymValue))
-> ModelState state -> f (ModelState state)
forall state.
Lens' (ModelState state) (Map (AddressInEra Era) SymValue)
balanceChangesL

-- | Get the current balance change for a wallet. This is the delta balance, so it starts out at zero and
--   can be negative. The absolute balance used by the emulator can be set in the `CheckOptions`
--   argument to `propRunActionsWithOptions`.
--
--   `Spec` monad update functions: `withdraw`, `deposit`, `transfer`.
balanceChange :: Ord (AddressInEra Era) => AddressInEra Era -> Getter (ModelState state) SymValue
balanceChange :: AddressInEra Era -> Getter (ModelState state) SymValue
balanceChange AddressInEra Era
w = (Map (AddressInEra Era) SymValue
 -> f (Map (AddressInEra Era) SymValue))
-> ModelState state -> f (ModelState state)
forall state.
Lens' (ModelState state) (Map (AddressInEra Era) SymValue)
balanceChangesL ((Map (AddressInEra Era) SymValue
  -> f (Map (AddressInEra Era) SymValue))
 -> ModelState state -> f (ModelState state))
-> ((SymValue -> f SymValue)
    -> Map (AddressInEra Era) SymValue
    -> f (Map (AddressInEra Era) SymValue))
-> (SymValue -> f SymValue)
-> ModelState state
-> f (ModelState state)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map (AddressInEra Era) SymValue)
-> Lens'
     (Map (AddressInEra Era) SymValue)
     (Maybe (IxValue (Map (AddressInEra Era) SymValue)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at AddressInEra Era
Index (Map (AddressInEra Era) SymValue)
w ((Maybe SymValue -> f (Maybe SymValue))
 -> Map (AddressInEra Era) SymValue
 -> f (Map (AddressInEra Era) SymValue))
-> ((SymValue -> f SymValue)
    -> Maybe SymValue -> f (Maybe SymValue))
-> (SymValue -> f SymValue)
-> Map (AddressInEra Era) SymValue
-> f (Map (AddressInEra Era) SymValue)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymValue -> Iso' (Maybe SymValue) SymValue
forall a. Eq a => a -> Iso' (Maybe a) a
non SymValue
forall a. Monoid a => a
mempty

-- | Get the amount of tokens minted so far. This is used to compute `lockedValue`.
--
--   `Spec` monad update functions: `mint` and `burn`.
minted :: Getter (ModelState state) SymValue
minted :: (SymValue -> f SymValue)
-> ModelState state -> f (ModelState state)
minted = (SymValue -> f SymValue)
-> ModelState state -> f (ModelState state)
forall state. Lens' (ModelState state) SymValue
mintedL

-- | How much value is currently locked by contracts. This computed by subtracting the wallet
--   `balances` from the `minted` value.
lockedValue :: ModelState s -> SymValue
lockedValue :: ModelState s -> SymValue
lockedValue ModelState s
s = ModelState s
s ModelState s
-> Getting SymValue (ModelState s) SymValue -> SymValue
forall s a. s -> Getting a s a -> a
^. Getting SymValue (ModelState s) SymValue
forall state. Getter (ModelState state) SymValue
minted SymValue -> SymValue -> SymValue
forall a. Semigroup a => a -> a -> a
<> SymValue -> SymValue
inv (Map (AddressInEra Era) SymValue -> SymValue
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Map (AddressInEra Era) SymValue -> SymValue)
-> Map (AddressInEra Era) SymValue -> SymValue
forall a b. (a -> b) -> a -> b
$ ModelState s
s ModelState s
-> Getting
     (Map (AddressInEra Era) SymValue)
     (ModelState s)
     (Map (AddressInEra Era) SymValue)
-> Map (AddressInEra Era) SymValue
forall s a. s -> Getting a s a -> a
^. Getting
  (Map (AddressInEra Era) SymValue)
  (ModelState s)
  (Map (AddressInEra Era) SymValue)
forall state.
Getter (ModelState state) (Map (AddressInEra Era) SymValue)
balanceChanges)

-- | Modify a field in the `ModelState`
modState :: forall state a. Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState :: Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState Setter' (ModelState state) a
l a -> a
f = WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  ()
-> Spec state ()
forall state a.
WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  a
-> Spec state a
Spec (WriterT
   SymCreationIndex
   (ReaderT (Var SymIndex) (State (ModelState state)))
   ()
 -> Spec state ())
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     ()
-> Spec state ()
forall a b. (a -> b) -> a -> b
$ (ModelState state -> ModelState state)
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
State.modify ((ModelState state -> ModelState state)
 -> WriterT
      SymCreationIndex
      (ReaderT (Var SymIndex) (State (ModelState state)))
      ())
-> (ModelState state -> ModelState state)
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     ()
forall a b. (a -> b) -> a -> b
$ ASetter (ModelState state) (ModelState state) a a
-> (a -> a) -> ModelState state -> ModelState state
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter (ModelState state) (ModelState state) a a
Setter' (ModelState state) a
l a -> a
f

-- | Monads with read access to the model state: the `Spec` monad used in `nextState`, and the `DL`
--   monad used to construct test scenarios.
class Monad m => GetModelState m where
    -- | The contract state type of the monad. For both `Spec` and `DL` this is simply the @state@
    --   parameter of the respective monad.
    type StateType m :: *

    -- | Get the current model state.
    getModelState :: m (ModelState (StateType m))

-- | Get the contract state part of the model state.
getContractState :: GetModelState m => m (StateType m)
getContractState :: m (StateType m)
getContractState = ModelState (StateType m) -> StateType m
forall state. ModelState state -> state
_contractState (ModelState (StateType m) -> StateType m)
-> m (ModelState (StateType m)) -> m (StateType m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ModelState (StateType m))
forall (m :: * -> *).
GetModelState m =>
m (ModelState (StateType m))
getModelState

-- | Get a component of the model state.
askModelState :: GetModelState m => (ModelState (StateType m) -> a) -> m a
askModelState :: (ModelState (StateType m) -> a) -> m a
askModelState ModelState (StateType m) -> a
f = ModelState (StateType m) -> a
f (ModelState (StateType m) -> a)
-> m (ModelState (StateType m)) -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ModelState (StateType m))
forall (m :: * -> *).
GetModelState m =>
m (ModelState (StateType m))
getModelState

-- | Get a component of the contract state.
askContractState :: GetModelState m => (StateType m -> a) -> m a
askContractState :: (StateType m -> a) -> m a
askContractState StateType m -> a
f = (ModelState (StateType m) -> a) -> m a
forall (m :: * -> *) a.
GetModelState m =>
(ModelState (StateType m) -> a) -> m a
askModelState (StateType m -> a
f (StateType m -> a)
-> (ModelState (StateType m) -> StateType m)
-> ModelState (StateType m)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelState (StateType m) -> StateType m
forall state. ModelState state -> state
_contractState)

-- | Get a component of the model state using a lens.
viewModelState :: GetModelState m => Getting a (ModelState (StateType m)) a -> m a
viewModelState :: Getting a (ModelState (StateType m)) a -> m a
viewModelState Getting a (ModelState (StateType m)) a
l = (ModelState (StateType m) -> a) -> m a
forall (m :: * -> *) a.
GetModelState m =>
(ModelState (StateType m) -> a) -> m a
askModelState (ModelState (StateType m)
-> Getting a (ModelState (StateType m)) a -> a
forall s a. s -> Getting a s a -> a
^. Getting a (ModelState (StateType m)) a
l)

-- | Get a component of the contract state using a lens.
viewContractState :: GetModelState m => Getting a (StateType m) a -> m a
viewContractState :: Getting a (StateType m) a -> m a
viewContractState Getting a (StateType m) a
l = Getting a (ModelState (StateType m)) a -> m a
forall (m :: * -> *) a.
GetModelState m =>
Getting a (ModelState (StateType m)) a -> m a
viewModelState ((StateType m -> Const a (StateType m))
-> ModelState (StateType m) -> Const a (ModelState (StateType m))
forall state state.
Lens (ModelState state) (ModelState state) state state
contractState ((StateType m -> Const a (StateType m))
 -> ModelState (StateType m) -> Const a (ModelState (StateType m)))
-> Getting a (StateType m) a
-> Getting a (ModelState (StateType m)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting a (StateType m) a
l)

instance GetModelState (Spec state) where
  type StateType (Spec state) = state
  getModelState :: Spec state (ModelState (StateType (Spec state)))
getModelState = WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  (ModelState state)
-> Spec state (ModelState state)
forall state a.
WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  a
-> Spec state a
Spec WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  (ModelState state)
forall s (m :: * -> *). MonadState s m => m s
State.get

runSpec :: Spec state ()
        -> Var SymIndex
        -> ModelState state
        -> ModelState state
runSpec :: Spec state ()
-> Var SymIndex -> ModelState state -> ModelState state
runSpec (Spec WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  ()
spec) Var SymIndex
v ModelState state
s = (State (ModelState state) ()
 -> ModelState state -> ModelState state)
-> ModelState state
-> State (ModelState state) ()
-> ModelState state
forall a b c. (a -> b -> c) -> b -> a -> c
flip State (ModelState state) () -> ModelState state -> ModelState state
forall s a. State s a -> s -> s
State.execState ModelState state
s (State (ModelState state) () -> ModelState state)
-> State (ModelState state) () -> ModelState state
forall a b. (a -> b) -> a -> b
$ do
  SymCreationIndex
ci <- 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 WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  ()
spec) Var SymIndex
v
  (SymCollectionIndex -> Identity SymCollectionIndex)
-> ModelState state -> Identity (ModelState state)
forall state. Lens' (ModelState state) SymCollectionIndex
symbolics ((SymCollectionIndex -> Identity SymCollectionIndex)
 -> ModelState state -> Identity (ModelState state))
-> SymCollectionIndex -> State (ModelState state) ()
forall s (m :: * -> *) a.
(MonadState s m, Semigroup a) =>
ASetter' s a -> a -> m ()
<>= SymCreationIndex -> Var SymIndex -> SymCollectionIndex
makeSymCollection SymCreationIndex
ci Var SymIndex
v

symbolicsCreatedBy :: Spec state ()
                   -> Var SymIndex
                   -> ModelState state
                   -> SymCreationIndex
symbolicsCreatedBy :: Spec state ()
-> Var SymIndex -> ModelState state -> SymCreationIndex
symbolicsCreatedBy (Spec WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  ()
spec) Var SymIndex
v ModelState state
s = (State (ModelState state) SymCreationIndex
 -> ModelState state -> SymCreationIndex)
-> ModelState state
-> State (ModelState state) SymCreationIndex
-> SymCreationIndex
forall a b c. (a -> b -> c) -> b -> a -> c
flip State (ModelState state) SymCreationIndex
-> ModelState state -> SymCreationIndex
forall s a. State s a -> s -> a
State.evalState ModelState state
s (State (ModelState state) SymCreationIndex -> SymCreationIndex)
-> State (ModelState state) SymCreationIndex -> SymCreationIndex
forall a b. (a -> b) -> a -> b
$ 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 WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  ()
spec) Var SymIndex
v

createSymbolic :: forall t state. HasSymbolicRep t => String -> Spec state (Symbolic t)
createSymbolic :: String -> Spec state (Symbolic t)
createSymbolic String
key = WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  (Symbolic t)
-> Spec state (Symbolic t)
forall state a.
WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  a
-> Spec state a
Spec (WriterT
   SymCreationIndex
   (ReaderT (Var SymIndex) (State (ModelState state)))
   (Symbolic t)
 -> Spec state (Symbolic t))
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     (Symbolic t)
-> Spec state (Symbolic t)
forall a b. (a -> b) -> a -> b
$ do
  Var SymIndex
var <- WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  (Var SymIndex)
forall r (m :: * -> *). MonadReader r m => m r
ask
  SymCreationIndex
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
Writer.tell (SymCreationIndex
 -> WriterT
      SymCreationIndex
      (ReaderT (Var SymIndex) (State (ModelState state)))
      ())
-> SymCreationIndex
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     ()
forall a b. (a -> b) -> a -> b
$ String -> SymCreationIndex
forall t. HasSymbolicRep t => String -> SymCreationIndex
createIndex @t String
key
  Symbolic t
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     (Symbolic t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Symbolic t
 -> WriterT
      SymCreationIndex
      (ReaderT (Var SymIndex) (State (ModelState state)))
      (Symbolic t))
-> Symbolic t
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     (Symbolic t)
forall a b. (a -> b) -> a -> b
$ Var SymIndex -> String -> Symbolic t
forall k (t :: k). Var SymIndex -> String -> Symbolic t
Symbolic Var SymIndex
var String
key

-- | Create a new symbolic token in `nextState` - must have a
-- corresponding `registerToken` call in `perform`
createToken :: String -> Spec state SymToken
createToken :: String -> Spec state SymToken
createToken = String -> Spec state SymToken
forall t state.
HasSymbolicRep t =>
String -> Spec state (Symbolic t)
createSymbolic

-- | Create a new symbolic TxOut in `nextState` - must have a
-- corresponding `registerTxOut` call in `perform`
createTxOut :: String -> Spec state SymTxOut
createTxOut :: String -> Spec state SymTxOut
createTxOut = String -> Spec state SymTxOut
forall t state.
HasSymbolicRep t =>
String -> Spec state (Symbolic t)
createSymbolic

-- | Create a new symbolic TxIn in `nextState` - must have a
-- corresponding `registerTxIn` call in `perform`
createTxIn :: String -> Spec state SymTxIn
createTxIn :: String -> Spec state SymTxIn
createTxIn = String -> Spec state SymTxIn
forall t state.
HasSymbolicRep t =>
String -> Spec state (Symbolic t)
createSymbolic

-- | Mint tokens. Minted tokens start out as `lockedValue` (i.e. owned by the contract) and can be
--   transferred to wallets using `deposit`.
mint :: SymValueLike v => v -> Spec state ()
mint :: v -> Spec state ()
mint v
v = Setter' (ModelState state) SymValue
-> (SymValue -> SymValue) -> Spec state ()
forall state a.
Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState forall state. Lens' (ModelState state) SymValue
Setter' (ModelState state) SymValue
mintedL (SymValue -> SymValue -> SymValue
forall a. Semigroup a => a -> a -> a
<> v -> SymValue
forall v. SymValueLike v => v -> SymValue
toSymValue v
v)

-- | Burn tokens. Equivalent to @`mint` . `inv`@.
burn :: SymValueLike v => v -> Spec state ()
burn :: v -> Spec state ()
burn = SymValue -> Spec state ()
forall v state. SymValueLike v => v -> Spec state ()
mint (SymValue -> Spec state ())
-> (v -> SymValue) -> v -> Spec state ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymValue -> SymValue
inv (SymValue -> SymValue) -> (v -> SymValue) -> v -> SymValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> SymValue
forall v. SymValueLike v => v -> SymValue
toSymValue

-- | Add tokens to the `balanceChange` of an address. The added tokens are subtracted from the
--   `lockedValue` of tokens held by contracts.
deposit :: SymValueLike v => AddressInEra Era -> v -> Spec state ()
deposit :: AddressInEra Era -> v -> Spec state ()
deposit AddressInEra Era
w v
val = Setter' (ModelState state) (Maybe SymValue)
-> (Maybe SymValue -> Maybe SymValue) -> Spec state ()
forall state a.
Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState ((Map (AddressInEra Era) SymValue
 -> f (Map (AddressInEra Era) SymValue))
-> ModelState state -> f (ModelState state)
forall state.
Lens' (ModelState state) (Map (AddressInEra Era) SymValue)
balanceChangesL ((Map (AddressInEra Era) SymValue
  -> f (Map (AddressInEra Era) SymValue))
 -> ModelState state -> f (ModelState state))
-> ((Maybe SymValue -> f (Maybe SymValue))
    -> Map (AddressInEra Era) SymValue
    -> f (Map (AddressInEra Era) SymValue))
-> (Maybe SymValue -> f (Maybe SymValue))
-> ModelState state
-> f (ModelState state)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map (AddressInEra Era) SymValue)
-> Lens'
     (Map (AddressInEra Era) SymValue)
     (Maybe (IxValue (Map (AddressInEra Era) SymValue)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at AddressInEra Era
Index (Map (AddressInEra Era) SymValue)
w) (SymValue -> Maybe SymValue
forall a. a -> Maybe a
Just (SymValue -> Maybe SymValue)
-> (Maybe SymValue -> SymValue) -> Maybe SymValue -> Maybe SymValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymValue -> (SymValue -> SymValue) -> Maybe SymValue -> SymValue
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (v -> SymValue
forall v. SymValueLike v => v -> SymValue
toSymValue v
val) (SymValue -> SymValue -> SymValue
forall a. Semigroup a => a -> a -> a
<> v -> SymValue
forall v. SymValueLike v => v -> SymValue
toSymValue v
val))

-- | Withdraw tokens from an address. The withdrawn tokens are added to the `lockedValue` of tokens
--   held by contracts.
withdraw :: SymValueLike v => AddressInEra Era -> v -> Spec state ()
withdraw :: AddressInEra Era -> v -> Spec state ()
withdraw AddressInEra Era
w v
val = AddressInEra Era -> SymValue -> Spec state ()
forall v state.
SymValueLike v =>
AddressInEra Era -> v -> Spec state ()
deposit AddressInEra Era
w (SymValue -> SymValue
inv (SymValue -> SymValue) -> (v -> SymValue) -> v -> SymValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> SymValue
forall v. SymValueLike v => v -> SymValue
toSymValue (v -> SymValue) -> v -> SymValue
forall a b. (a -> b) -> a -> b
$ v
val)

-- | Transfer tokens between wallets, updating their `balances`.
transfer :: SymValueLike v
         => AddressInEra Era  -- ^ Transfer from this address
         -> AddressInEra Era  -- ^ to this address
         -> v                 -- ^ this much value
         -> Spec state ()
transfer :: AddressInEra Era -> AddressInEra Era -> v -> Spec state ()
transfer AddressInEra Era
fromW AddressInEra Era
toW v
val = AddressInEra Era -> v -> Spec state ()
forall v state.
SymValueLike v =>
AddressInEra Era -> v -> Spec state ()
withdraw AddressInEra Era
fromW v
val Spec state () -> Spec state () -> Spec state ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AddressInEra Era -> v -> Spec state ()
forall v state.
SymValueLike v =>
AddressInEra Era -> v -> Spec state ()
deposit AddressInEra Era
toW v
val

-- | Assert that a particular predicate holds at a point in the specification
assertSpec :: String -> Bool -> Spec state ()
assertSpec :: String -> Bool -> Spec state ()
assertSpec String
s Bool
b = do
  Setter' (ModelState state) [(String, Bool)]
-> ([(String, Bool)] -> [(String, Bool)]) -> Spec state ()
forall state a.
Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState forall state. Lens' (ModelState state) [(String, Bool)]
Setter' (ModelState state) [(String, Bool)]
assertions ((String
s, Bool
b)(String, Bool) -> [(String, Bool)] -> [(String, Bool)]
forall a. a -> [a] -> [a]
:)
  Setter' (ModelState state) Bool -> (Bool -> Bool) -> Spec state ()
forall state a.
Setter' (ModelState state) a -> (a -> a) -> Spec state ()
modState forall state. Lens' (ModelState state) Bool
Setter' (ModelState state) Bool
assertionsOk (Bool -> Bool -> Bool
&&Bool
b)