-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- | Module, containing function to interpret Michelson
-- instructions against given context and input stack.
module Michelson.Interpret
  ( ContractEnv (..)
  , InterpreterState (..)
  , isMorleyLogsL
  , MichelsonFailed (..)
  , RemainingSteps (..)
  , SomeItStack (..)
  , MorleyLogs (..)
  , noMorleyLogs
  , pickMorleyLogs

  , interpret
  , interpretInstr
  , interpretInstrAnnotated
  , ContractReturn

  , mkInitStack
  , fromFinalStack
  , InterpretError (..)
  , InterpretResult (..)
  , EvalM
  , InterpreterStateMonad (..)
  , StkEl (..)
  , InstrRunner
  , runInstr
  , runInstrNoGas
  , runUnpack

    -- * Internals
  , initInterpreterState
  , handleContractReturn
  , runInstrImpl
  ) where

import Prelude hiding (EQ, GT, LT)

import Control.Lens (makeLensesFor)
import Control.Monad.Except (MonadError, throwError)
import Data.Default (Default(..))
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Singletons (Sing)
import Data.Vinyl (Rec(..), (<+>))
import Data.Vinyl.Recursive (rmap)
import Fmt (Buildable(build), Builder, blockListF, prettyLn)

import Michelson.Interpret.Pack (packValue')
import Michelson.Interpret.Unpack (UnpackError, unpackValue')
import Michelson.TypeCheck (SomeParamType(..), TcOriginatedContracts, matchTypes)
import Michelson.Typed
import qualified Michelson.Typed as T
import Michelson.Typed.Origination (OriginationOperation(..), mkOriginationOperationHash)
import qualified Michelson.Untyped as U
import Tezos.Address (Address(..), GlobalCounter(..), OriginationIndex(..), mkContractAddress)
import Tezos.Core (ChainId, Mutez, Timestamp)
import Tezos.Crypto (KeyHash, blake2b, checkSignature, hashKey, sha256, sha512)
import Util.Peano (LongerThan, Peano, SingNat(SS, SZ))
import Util.TH
import Util.Type
import Util.Typeable

-- | Environment for contract execution.
data ContractEnv = ContractEnv
  { ContractEnv -> Timestamp
ceNow :: Timestamp
  -- ^ Timestamp returned by the 'NOW' instruction.
  , ContractEnv -> RemainingSteps
ceMaxSteps :: RemainingSteps
  -- ^ Number of steps after which execution unconditionally terminates.
  , ContractEnv -> Mutez
ceBalance :: Mutez
  -- ^ Current amount of mutez of the current contract.
  , ContractEnv -> TcOriginatedContracts
ceContracts :: TcOriginatedContracts
  -- ^ Mapping from existing contracts' addresses to their executable
  -- representation.
  , ContractEnv -> Address
ceSelf :: Address
  -- ^ Address of the interpreted contract.
  , ContractEnv -> Address
ceSource :: Address
  -- ^ The contract that initiated the current transaction.
  , ContractEnv -> Address
ceSender :: Address
  -- ^ The contract that initiated the current internal transaction.
  , ContractEnv -> Mutez
ceAmount :: Mutez
  -- ^ Amount of the current transaction.
  , ContractEnv -> ChainId
ceChainId :: ChainId
  -- ^ Identifier of the current chain.
  , ContractEnv -> Maybe OperationHash
ceOperationHash :: Maybe U.OperationHash
  -- ^ Hash of the currently executed operation, required for
  -- correct contract address computation in 'CREATE_CONTRACT' instruction.
  , ContractEnv -> GlobalCounter
ceGlobalCounter :: GlobalCounter
  -- ^ A global counter that is used to ensure newly created
  -- contracts have unique addresses.
  }

-- | Represents @[FAILED]@ state of a Michelson program. Contains
-- value that was on top of the stack when @FAILWITH@ was called.
data MichelsonFailed where
  MichelsonFailedWith :: (KnownT t) => T.Value t -> MichelsonFailed
  MichelsonArithError
    :: (Typeable n, Typeable m, Typeable instr)
    => ArithError (Value' instr n) (Value' instr m) -> MichelsonFailed
  MichelsonGasExhaustion :: MichelsonFailed
  MichelsonFailedTestAssert :: Text -> MichelsonFailed

deriving stock instance Show MichelsonFailed

instance Eq MichelsonFailed where
  MichelsonFailedWith v1 :: Value t
v1 == :: MichelsonFailed -> MichelsonFailed -> Bool
== MichelsonFailedWith v2 :: Value t
v2 = Value t
v1 Value t -> Value t -> Bool
forall k (a1 :: k) (a2 :: k) (t :: k -> *).
(Typeable a1, Typeable a2, Eq (t a1)) =>
t a1 -> t a2 -> Bool
`eqParam1` Value t
v2
  MichelsonFailedWith _ == _ = Bool
False
  MichelsonArithError ae1 :: ArithError (Value' instr n) (Value' instr m)
ae1 == MichelsonArithError ae2 :: ArithError (Value' instr n) (Value' instr m)
ae2 = ArithError (Value' instr n) (Value' instr m)
ae1 ArithError (Value' instr n) (Value' instr m)
-> ArithError (Value' instr n) (Value' instr m) -> Bool
forall k1 k2 (a1 :: k1) (a2 :: k1) (b1 :: k2) (b2 :: k2)
       (t :: k1 -> k2 -> *).
(Typeable a1, Typeable a2, Typeable b1, Typeable b2,
 Eq (t a1 b2)) =>
t a1 b1 -> t a2 b2 -> Bool
`eqParam2` ArithError (Value' instr n) (Value' instr m)
ae2
  MichelsonArithError _ == _ = Bool
False
  MichelsonGasExhaustion == MichelsonGasExhaustion = Bool
True
  MichelsonGasExhaustion == _ = Bool
False
  MichelsonFailedTestAssert t1 :: Text
t1 == MichelsonFailedTestAssert t2 :: Text
t2 = Text
t1 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
t2
  MichelsonFailedTestAssert _ == _ = Bool
False

instance Buildable MichelsonFailed where
  build :: MichelsonFailed -> Builder
build =
    \case
      MichelsonFailedWith (Value t
v :: T.Value t) ->
        "Reached FAILWITH instruction with " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Value t -> Builder
forall (t :: T). SingI t => Value t -> Builder
formatValue Value t
v
      MichelsonArithError v :: ArithError (Value' instr n) (Value' instr m)
v -> ArithError (Value' instr n) (Value' instr m) -> Builder
forall p. Buildable p => p -> Builder
build ArithError (Value' instr n) (Value' instr m)
v
      MichelsonGasExhaustion ->
        "Gas limit exceeded on contract execution"
      MichelsonFailedTestAssert t :: Text
t -> Text -> Builder
forall p. Buildable p => p -> Builder
build Text
t
    where
      formatValue :: forall t . SingI t => Value t -> Builder
      formatValue :: Value t -> Builder
formatValue v :: Value t
v =
        case Sing t -> OpPresence t
forall (ty :: T). Sing ty -> OpPresence ty
T.checkOpPresence (SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t) of
          OpPresent -> "<value with operations>"
          OpAbsent -> Value -> Builder
forall p. Buildable p => p -> Builder
build (Value t -> Value
forall (t :: T). (SingI t, HasNoOp t) => Value' Instr t -> Value
untypeValue Value t
v)

newtype InterpretError = InterpretError (MichelsonFailed, MorleyLogs)
  deriving stock ((forall x. InterpretError -> Rep InterpretError x)
-> (forall x. Rep InterpretError x -> InterpretError)
-> Generic InterpretError
forall x. Rep InterpretError x -> InterpretError
forall x. InterpretError -> Rep InterpretError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep InterpretError x -> InterpretError
$cfrom :: forall x. InterpretError -> Rep InterpretError x
Generic)

deriving stock instance Show InterpretError

instance Buildable InterpretError where
  build :: InterpretError -> Builder
build (InterpretError (mf :: MichelsonFailed
mf, _)) = MichelsonFailed -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> b
prettyLn MichelsonFailed
mf

data InterpretResult where
  InterpretResult
    :: ( StorageScope st )
    => { InterpretResult -> [Operation]
iurOps :: [Operation]
       , ()
iurNewStorage :: T.Value st
       , InterpretResult -> InterpreterState
iurNewState   :: InterpreterState
       }
    -> InterpretResult

deriving stock instance Show InterpretResult

constructIR ::
  (StorageScope st) =>
  (([Operation], Value' Instr st), InterpreterState) ->
  InterpretResult
constructIR :: (([Operation], Value' Instr st), InterpreterState)
-> InterpretResult
constructIR ((ops :: [Operation]
ops, val :: Value' Instr st
val), st :: InterpreterState
st) =
  $WInterpretResult :: forall (st :: T).
StorageScope st =>
[Operation] -> Value st -> InterpreterState -> InterpretResult
InterpretResult
  { iurOps :: [Operation]
iurOps = [Operation]
ops
  , iurNewStorage :: Value' Instr st
iurNewStorage = Value' Instr st
val
  , iurNewState :: InterpreterState
iurNewState = InterpreterState
st
  }

-- | Morley logs for interpreter state that are stored in reverse order.
newtype MorleyLogs = MorleyLogs [Text]
  deriving stock (MorleyLogs -> MorleyLogs -> Bool
(MorleyLogs -> MorleyLogs -> Bool)
-> (MorleyLogs -> MorleyLogs -> Bool) -> Eq MorleyLogs
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MorleyLogs -> MorleyLogs -> Bool
$c/= :: MorleyLogs -> MorleyLogs -> Bool
== :: MorleyLogs -> MorleyLogs -> Bool
$c== :: MorleyLogs -> MorleyLogs -> Bool
Eq, Int -> MorleyLogs -> ShowS
[MorleyLogs] -> ShowS
MorleyLogs -> String
(Int -> MorleyLogs -> ShowS)
-> (MorleyLogs -> String)
-> ([MorleyLogs] -> ShowS)
-> Show MorleyLogs
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MorleyLogs] -> ShowS
$cshowList :: [MorleyLogs] -> ShowS
show :: MorleyLogs -> String
$cshow :: MorleyLogs -> String
showsPrec :: Int -> MorleyLogs -> ShowS
$cshowsPrec :: Int -> MorleyLogs -> ShowS
Show, (forall x. MorleyLogs -> Rep MorleyLogs x)
-> (forall x. Rep MorleyLogs x -> MorleyLogs) -> Generic MorleyLogs
forall x. Rep MorleyLogs x -> MorleyLogs
forall x. MorleyLogs -> Rep MorleyLogs x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MorleyLogs x -> MorleyLogs
$cfrom :: forall x. MorleyLogs -> Rep MorleyLogs x
Generic)
  deriving newtype MorleyLogs
MorleyLogs -> Default MorleyLogs
forall a. a -> Default a
def :: MorleyLogs
$cdef :: MorleyLogs
Default

pickMorleyLogs :: MorleyLogs -> [Text]
pickMorleyLogs :: MorleyLogs -> [Text]
pickMorleyLogs (MorleyLogs logs :: [Text]
logs) = [Text] -> [Text]
forall a. [a] -> [a]
reverse [Text]
logs

instance Buildable MorleyLogs where
  build :: MorleyLogs -> Builder
build = [Text] -> Builder
forall (f :: * -> *) a. (Foldable f, Buildable a) => f a -> Builder
blockListF ([Text] -> Builder)
-> (MorleyLogs -> [Text]) -> MorleyLogs -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MorleyLogs -> [Text]
pickMorleyLogs

instance NFData MorleyLogs

noMorleyLogs :: MorleyLogs
noMorleyLogs :: MorleyLogs
noMorleyLogs = [Text] -> MorleyLogs
MorleyLogs []

type ContractReturn st =
  (Either MichelsonFailed ([Operation], T.Value st), InterpreterState)

handleContractReturn
  :: (StorageScope st)
  => ContractReturn st -> Either InterpretError InterpretResult
handleContractReturn :: ContractReturn st -> Either InterpretError InterpretResult
handleContractReturn (ei :: Either MichelsonFailed ([Operation], Value st)
ei, s :: InterpreterState
s) =
  (MichelsonFailed -> InterpretError)
-> (([Operation], Value st) -> InterpretResult)
-> Either MichelsonFailed ([Operation], Value st)
-> Either InterpretError InterpretResult
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((MichelsonFailed, MorleyLogs) -> InterpretError
InterpretError ((MichelsonFailed, MorleyLogs) -> InterpretError)
-> (MichelsonFailed -> (MichelsonFailed, MorleyLogs))
-> MichelsonFailed
-> InterpretError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, InterpreterState -> MorleyLogs
isMorleyLogs InterpreterState
s)) ((([Operation], Value st), InterpreterState) -> InterpretResult
forall (st :: T).
StorageScope st =>
(([Operation], Value' Instr st), InterpreterState)
-> InterpretResult
constructIR ((([Operation], Value st), InterpreterState) -> InterpretResult)
-> (([Operation], Value st)
    -> (([Operation], Value st), InterpreterState))
-> ([Operation], Value st)
-> InterpretResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, InterpreterState
s)) Either MichelsonFailed ([Operation], Value st)
ei

-- | Function to change amount of remaining steps stored in State monad
-- | Helper function to convert a record of @Value@ to @StkEl@. These will be
-- created with @starNotes@.
mapToStkEl :: Rec T.Value inp -> Rec StkEl inp
mapToStkEl :: Rec Value inp -> Rec StkEl inp
mapToStkEl = (forall (x :: T). Value x -> StkEl x)
-> Rec Value inp -> Rec StkEl inp
forall u (f :: u -> *) (g :: u -> *) (rs :: [u]).
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap forall (x :: T). Value x -> StkEl x
starNotesStkEl

-- | Helper function to convert a record of @StkEl@ to @Value@. Any present
-- notes will be discarded.
mapToValue :: Rec StkEl inp -> Rec T.Value inp
mapToValue :: Rec StkEl inp -> Rec Value inp
mapToValue = (forall (x :: T). StkEl x -> Value x)
-> Rec StkEl inp -> Rec Value inp
forall u (f :: u -> *) (g :: u -> *) (rs :: [u]).
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap forall (x :: T). StkEl x -> Value x
seValue

interpret'
  :: forall cp st arg.
     Contract cp st
  -> EntrypointCallT cp arg
  -> T.Value arg
  -> T.Value st
  -> ContractEnv
  -> InterpreterState
  -> ContractReturn st
interpret' :: Contract cp st
-> EntrypointCallT cp arg
-> Value arg
-> Value st
-> ContractEnv
-> InterpreterState
-> ContractReturn st
interpret' Contract{..} epc :: EntrypointCallT cp arg
epc param :: Value arg
param initSt :: Value st
initSt env :: ContractEnv
env ist :: InterpreterState
ist = (Either MichelsonFailed (Rec StkEl (ContractOut st))
 -> Either MichelsonFailed ([Operation], Value st))
-> (Either MichelsonFailed (Rec StkEl (ContractOut st)),
    InterpreterState)
-> ContractReturn st
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Rec StkEl (ContractOut st) -> ([Operation], Value st))
-> Either MichelsonFailed (Rec StkEl (ContractOut st))
-> Either MichelsonFailed ([Operation], Value st)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rec StkEl (ContractOut st) -> ([Operation], Value st)
forall (st :: T).
Rec StkEl (ContractOut st) -> ([Operation], Value st)
fromFinalStack) ((Either MichelsonFailed (Rec StkEl (ContractOut st)),
  InterpreterState)
 -> ContractReturn st)
-> (Either MichelsonFailed (Rec StkEl (ContractOut st)),
    InterpreterState)
-> ContractReturn st
forall a b. (a -> b) -> a -> b
$
  EvalOp (Rec StkEl (ContractOut st))
-> ContractEnv
-> InterpreterState
-> (Either MichelsonFailed (Rec StkEl (ContractOut st)),
    InterpreterState)
forall a.
EvalOp a
-> ContractEnv
-> InterpreterState
-> (Either MichelsonFailed a, InterpreterState)
runEvalOp
    (ContractCode cp st
-> Rec StkEl (ContractInp cp st)
-> EvalOp (Rec StkEl (ContractOut st))
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr ContractCode cp st
cCode (Rec StkEl (ContractInp cp st)
 -> EvalOp (Rec StkEl (ContractOut st)))
-> Rec StkEl (ContractInp cp st)
-> EvalOp (Rec StkEl (ContractOut st))
forall a b. (a -> b) -> a -> b
$ Value cp
-> ParamNotes cp
-> Value st
-> Notes st
-> Rec StkEl (ContractInp cp st)
forall (param :: T) (st :: T).
Value param
-> ParamNotes param
-> Value st
-> Notes st
-> Rec StkEl (ContractInp param st)
mkInitStack (EntrypointCallT cp arg -> Value arg -> Value cp
forall (param :: T) (arg :: T) (instr :: [T] -> [T] -> *).
EntrypointCallT param arg -> Value' instr arg -> Value' instr param
liftCallArg EntrypointCallT cp arg
epc Value arg
param) ParamNotes cp
cParamNotes Value st
initSt Notes st
cStoreNotes)
    ContractEnv
env
    InterpreterState
ist

mkInitStack
  :: T.Value param
  -> T.ParamNotes param
  -> T.Value st
  -> T.Notes st
  -> Rec StkEl (ContractInp param st)
mkInitStack :: Value param
-> ParamNotes param
-> Value st
-> Notes st
-> Rec StkEl (ContractInp param st)
mkInitStack param :: Value param
param T.ParamNotesUnsafe{..} st :: Value st
st stNotes :: Notes st
stNotes = Value ('TPair param st)
-> VarAnn -> Notes ('TPair param st) -> StkEl ('TPair param st)
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl
  ((Value param, Value st) -> Value ('TPair param st)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
T.VPair (Value param
param, Value st
st))
  VarAnn
forall k (a :: k). Annotation a
U.noAnn
  (TypeAnn
-> RootAnn
-> RootAnn
-> Notes param
-> Notes st
-> Notes ('TPair param st)
forall (p :: T) (q :: T).
TypeAnn
-> RootAnn -> RootAnn -> Notes p -> Notes q -> Notes ('TPair p q)
T.NTPair TypeAnn
forall k (a :: k). Annotation a
U.noAnn (RootAnn -> RootAnn
forall k1 k2 (tag1 :: k1) (tag2 :: k2).
Annotation tag1 -> Annotation tag2
U.convAnn RootAnn
pnRootAnn) RootAnn
forall k (a :: k). Annotation a
U.noAnn Notes param
pnNotes Notes st
stNotes)
    StkEl ('TPair param st)
-> Rec StkEl '[] -> Rec StkEl (ContractInp param st)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl '[]
forall u (a :: u -> *). Rec a '[]
RNil

fromFinalStack :: Rec StkEl (ContractOut st) -> ([T.Operation], T.Value st)
fromFinalStack :: Rec StkEl (ContractOut st) -> ([Operation], Value st)
fromFinalStack (StkEl (T.VPair (T.VList ops :: [Value' Instr t]
ops, st :: Value' Instr r
st)) _ _ :& RNil) =
  ((Value' Instr t -> Operation) -> [Value' Instr t] -> [Operation]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (\(T.VOp op :: Operation
op) -> Operation
op) [Value' Instr t]
ops, Value st
Value' Instr r
st)

interpret
  :: Contract cp st
  -> EntrypointCallT cp arg
  -> T.Value arg
  -> T.Value st
  -> ContractEnv
  -> ContractReturn st
interpret :: Contract cp st
-> EntrypointCallT cp arg
-> Value arg
-> Value st
-> ContractEnv
-> ContractReturn st
interpret contract :: Contract cp st
contract epc :: EntrypointCallT cp arg
epc param :: Value arg
param initSt :: Value st
initSt env :: ContractEnv
env =
  Contract cp st
-> EntrypointCallT cp arg
-> Value arg
-> Value st
-> ContractEnv
-> InterpreterState
-> ContractReturn st
forall (cp :: T) (st :: T) (arg :: T).
Contract cp st
-> EntrypointCallT cp arg
-> Value arg
-> Value st
-> ContractEnv
-> InterpreterState
-> ContractReturn st
interpret' Contract cp st
contract EntrypointCallT cp arg
epc Value arg
param Value st
initSt ContractEnv
env (ContractEnv -> InterpreterState
initInterpreterState ContractEnv
env)

initInterpreterState :: ContractEnv -> InterpreterState
initInterpreterState :: ContractEnv -> InterpreterState
initInterpreterState env :: ContractEnv
env = MorleyLogs
-> RemainingSteps -> OriginationIndex -> InterpreterState
InterpreterState MorleyLogs
forall a. Default a => a
def (ContractEnv -> RemainingSteps
ceMaxSteps ContractEnv
env) (Int32 -> OriginationIndex
OriginationIndex 0)

-- | Interpret an instruction in vacuum, putting no extra contraints on
-- its execution.
--
-- Mostly for testing purposes.
interpretInstr
  :: ContractEnv
  -> Instr inp out
  -> Rec T.Value inp
  -> Either MichelsonFailed (Rec T.Value out)
interpretInstr :: ContractEnv
-> Instr inp out
-> Rec Value inp
-> Either MichelsonFailed (Rec Value out)
interpretInstr = (Rec StkEl out -> Rec Value out)
-> Either MichelsonFailed (Rec StkEl out)
-> Either MichelsonFailed (Rec Value out)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rec StkEl out -> Rec Value out
forall (inp :: [T]). Rec StkEl inp -> Rec Value inp
mapToValue (Either MichelsonFailed (Rec StkEl out)
 -> Either MichelsonFailed (Rec Value out))
-> (ContractEnv
    -> Instr inp out
    -> Rec Value inp
    -> Either MichelsonFailed (Rec StkEl out))
-> ContractEnv
-> Instr inp out
-> Rec Value inp
-> Either MichelsonFailed (Rec Value out)
forall a b c. SuperComposition a b c => a -> b -> c
... ContractEnv
-> Instr inp out
-> Rec Value inp
-> Either MichelsonFailed (Rec StkEl out)
forall (inp :: [T]) (out :: [T]).
ContractEnv
-> Instr inp out
-> Rec Value inp
-> Either MichelsonFailed (Rec StkEl out)
interpretInstrAnnotated

-- | Interpret an instruction in vacuum, putting no extra contraints on
-- its execution while preserving its annotations.
--
-- Mostly for testing purposes.
interpretInstrAnnotated
  :: ContractEnv
  -> Instr inp out
  -> Rec T.Value inp
  -> Either MichelsonFailed (Rec StkEl out)
interpretInstrAnnotated :: ContractEnv
-> Instr inp out
-> Rec Value inp
-> Either MichelsonFailed (Rec StkEl out)
interpretInstrAnnotated env :: ContractEnv
env instr :: Instr inp out
instr inpSt :: Rec Value inp
inpSt =
  (Either MichelsonFailed (Rec StkEl out), InterpreterState)
-> Either MichelsonFailed (Rec StkEl out)
forall a b. (a, b) -> a
fst ((Either MichelsonFailed (Rec StkEl out), InterpreterState)
 -> Either MichelsonFailed (Rec StkEl out))
-> (Either MichelsonFailed (Rec StkEl out), InterpreterState)
-> Either MichelsonFailed (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$
  EvalOp (Rec StkEl out)
-> ContractEnv
-> InterpreterState
-> (Either MichelsonFailed (Rec StkEl out), InterpreterState)
forall a.
EvalOp a
-> ContractEnv
-> InterpreterState
-> (Either MichelsonFailed a, InterpreterState)
runEvalOp
    (Instr inp out -> Rec StkEl inp -> EvalOp (Rec StkEl out)
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
instr (Rec StkEl inp -> EvalOp (Rec StkEl out))
-> Rec StkEl inp -> EvalOp (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Rec Value inp -> Rec StkEl inp
forall (inp :: [T]). Rec Value inp -> Rec StkEl inp
mapToStkEl Rec Value inp
inpSt)
    ContractEnv
env
    $WInterpreterState :: MorleyLogs
-> RemainingSteps -> OriginationIndex -> InterpreterState
InterpreterState
      { isMorleyLogs :: MorleyLogs
isMorleyLogs = [Text] -> MorleyLogs
MorleyLogs []
      , isRemainingSteps :: RemainingSteps
isRemainingSteps = 9999999999
      , isOriginationNonce :: OriginationIndex
isOriginationNonce = Int32 -> OriginationIndex
OriginationIndex 0
      }

data SomeItStack where
  SomeItStack :: T.ExtInstr inp -> Rec StkEl inp -> SomeItStack

newtype RemainingSteps = RemainingSteps Word64
  deriving stock (Int -> RemainingSteps -> ShowS
[RemainingSteps] -> ShowS
RemainingSteps -> String
(Int -> RemainingSteps -> ShowS)
-> (RemainingSteps -> String)
-> ([RemainingSteps] -> ShowS)
-> Show RemainingSteps
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RemainingSteps] -> ShowS
$cshowList :: [RemainingSteps] -> ShowS
show :: RemainingSteps -> String
$cshow :: RemainingSteps -> String
showsPrec :: Int -> RemainingSteps -> ShowS
$cshowsPrec :: Int -> RemainingSteps -> ShowS
Show, (forall x. RemainingSteps -> Rep RemainingSteps x)
-> (forall x. Rep RemainingSteps x -> RemainingSteps)
-> Generic RemainingSteps
forall x. Rep RemainingSteps x -> RemainingSteps
forall x. RemainingSteps -> Rep RemainingSteps x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep RemainingSteps x -> RemainingSteps
$cfrom :: forall x. RemainingSteps -> Rep RemainingSteps x
Generic)
  deriving newtype (RemainingSteps -> RemainingSteps -> Bool
(RemainingSteps -> RemainingSteps -> Bool)
-> (RemainingSteps -> RemainingSteps -> Bool) -> Eq RemainingSteps
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RemainingSteps -> RemainingSteps -> Bool
$c/= :: RemainingSteps -> RemainingSteps -> Bool
== :: RemainingSteps -> RemainingSteps -> Bool
$c== :: RemainingSteps -> RemainingSteps -> Bool
Eq, Eq RemainingSteps
Eq RemainingSteps =>
(RemainingSteps -> RemainingSteps -> Ordering)
-> (RemainingSteps -> RemainingSteps -> Bool)
-> (RemainingSteps -> RemainingSteps -> Bool)
-> (RemainingSteps -> RemainingSteps -> Bool)
-> (RemainingSteps -> RemainingSteps -> Bool)
-> (RemainingSteps -> RemainingSteps -> RemainingSteps)
-> (RemainingSteps -> RemainingSteps -> RemainingSteps)
-> Ord RemainingSteps
RemainingSteps -> RemainingSteps -> Bool
RemainingSteps -> RemainingSteps -> Ordering
RemainingSteps -> RemainingSteps -> RemainingSteps
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RemainingSteps -> RemainingSteps -> RemainingSteps
$cmin :: RemainingSteps -> RemainingSteps -> RemainingSteps
max :: RemainingSteps -> RemainingSteps -> RemainingSteps
$cmax :: RemainingSteps -> RemainingSteps -> RemainingSteps
>= :: RemainingSteps -> RemainingSteps -> Bool
$c>= :: RemainingSteps -> RemainingSteps -> Bool
> :: RemainingSteps -> RemainingSteps -> Bool
$c> :: RemainingSteps -> RemainingSteps -> Bool
<= :: RemainingSteps -> RemainingSteps -> Bool
$c<= :: RemainingSteps -> RemainingSteps -> Bool
< :: RemainingSteps -> RemainingSteps -> Bool
$c< :: RemainingSteps -> RemainingSteps -> Bool
compare :: RemainingSteps -> RemainingSteps -> Ordering
$ccompare :: RemainingSteps -> RemainingSteps -> Ordering
$cp1Ord :: Eq RemainingSteps
Ord, RemainingSteps -> Builder
(RemainingSteps -> Builder) -> Buildable RemainingSteps
forall p. (p -> Builder) -> Buildable p
build :: RemainingSteps -> Builder
$cbuild :: RemainingSteps -> Builder
Buildable, Integer -> RemainingSteps
RemainingSteps -> RemainingSteps
RemainingSteps -> RemainingSteps -> RemainingSteps
(RemainingSteps -> RemainingSteps -> RemainingSteps)
-> (RemainingSteps -> RemainingSteps -> RemainingSteps)
-> (RemainingSteps -> RemainingSteps -> RemainingSteps)
-> (RemainingSteps -> RemainingSteps)
-> (RemainingSteps -> RemainingSteps)
-> (RemainingSteps -> RemainingSteps)
-> (Integer -> RemainingSteps)
-> Num RemainingSteps
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> RemainingSteps
$cfromInteger :: Integer -> RemainingSteps
signum :: RemainingSteps -> RemainingSteps
$csignum :: RemainingSteps -> RemainingSteps
abs :: RemainingSteps -> RemainingSteps
$cabs :: RemainingSteps -> RemainingSteps
negate :: RemainingSteps -> RemainingSteps
$cnegate :: RemainingSteps -> RemainingSteps
* :: RemainingSteps -> RemainingSteps -> RemainingSteps
$c* :: RemainingSteps -> RemainingSteps -> RemainingSteps
- :: RemainingSteps -> RemainingSteps -> RemainingSteps
$c- :: RemainingSteps -> RemainingSteps -> RemainingSteps
+ :: RemainingSteps -> RemainingSteps -> RemainingSteps
$c+ :: RemainingSteps -> RemainingSteps -> RemainingSteps
Num)

instance NFData RemainingSteps

data InterpreterState = InterpreterState
  { InterpreterState -> MorleyLogs
isMorleyLogs :: MorleyLogs
  , InterpreterState -> RemainingSteps
isRemainingSteps :: RemainingSteps
  , InterpreterState -> OriginationIndex
isOriginationNonce :: OriginationIndex
  } deriving stock (Int -> InterpreterState -> ShowS
[InterpreterState] -> ShowS
InterpreterState -> String
(Int -> InterpreterState -> ShowS)
-> (InterpreterState -> String)
-> ([InterpreterState] -> ShowS)
-> Show InterpreterState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [InterpreterState] -> ShowS
$cshowList :: [InterpreterState] -> ShowS
show :: InterpreterState -> String
$cshow :: InterpreterState -> String
showsPrec :: Int -> InterpreterState -> ShowS
$cshowsPrec :: Int -> InterpreterState -> ShowS
Show, (forall x. InterpreterState -> Rep InterpreterState x)
-> (forall x. Rep InterpreterState x -> InterpreterState)
-> Generic InterpreterState
forall x. Rep InterpreterState x -> InterpreterState
forall x. InterpreterState -> Rep InterpreterState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep InterpreterState x -> InterpreterState
$cfrom :: forall x. InterpreterState -> Rep InterpreterState x
Generic)

instance NFData InterpreterState

type EvalOp a =
  ExceptT MichelsonFailed
    (ReaderT ContractEnv
       (State InterpreterState)) a

runEvalOp
  :: EvalOp a
  -> ContractEnv
  -> InterpreterState
  -> (Either MichelsonFailed a, InterpreterState)
runEvalOp :: EvalOp a
-> ContractEnv
-> InterpreterState
-> (Either MichelsonFailed a, InterpreterState)
runEvalOp act :: EvalOp a
act env :: ContractEnv
env initSt :: InterpreterState
initSt =
  (State InterpreterState (Either MichelsonFailed a)
 -> InterpreterState
 -> (Either MichelsonFailed a, InterpreterState))
-> InterpreterState
-> State InterpreterState (Either MichelsonFailed a)
-> (Either MichelsonFailed a, InterpreterState)
forall a b c. (a -> b -> c) -> b -> a -> c
flip State InterpreterState (Either MichelsonFailed a)
-> InterpreterState -> (Either MichelsonFailed a, InterpreterState)
forall s a. State s a -> s -> (a, s)
runState InterpreterState
initSt (State InterpreterState (Either MichelsonFailed a)
 -> (Either MichelsonFailed a, InterpreterState))
-> State InterpreterState (Either MichelsonFailed a)
-> (Either MichelsonFailed a, InterpreterState)
forall a b. (a -> b) -> a -> b
$ ContractEnv
-> ReaderT
     ContractEnv (State InterpreterState) (Either MichelsonFailed a)
-> State InterpreterState (Either MichelsonFailed a)
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT ContractEnv
env (ReaderT
   ContractEnv (State InterpreterState) (Either MichelsonFailed a)
 -> State InterpreterState (Either MichelsonFailed a))
-> ReaderT
     ContractEnv (State InterpreterState) (Either MichelsonFailed a)
-> State InterpreterState (Either MichelsonFailed a)
forall a b. (a -> b) -> a -> b
$ EvalOp a
-> ReaderT
     ContractEnv (State InterpreterState) (Either MichelsonFailed a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT EvalOp a
act

class Monad m => InterpreterStateMonad m where
  getInterpreterState :: m InterpreterState
  getInterpreterState = (InterpreterState -> (InterpreterState, InterpreterState))
-> m InterpreterState
forall (m :: * -> *) a.
InterpreterStateMonad m =>
(InterpreterState -> (a, InterpreterState)) -> m a
stateInterpreterState (\s :: InterpreterState
s -> (InterpreterState
s, InterpreterState
s))

  putInterpreterState :: InterpreterState -> m ()
  putInterpreterState s :: InterpreterState
s = (InterpreterState -> ((), InterpreterState)) -> m ()
forall (m :: * -> *) a.
InterpreterStateMonad m =>
(InterpreterState -> (a, InterpreterState)) -> m a
stateInterpreterState (\_ -> ((), InterpreterState
s))

  stateInterpreterState :: (InterpreterState -> (a, InterpreterState)) -> m a
  stateInterpreterState f :: InterpreterState -> (a, InterpreterState)
f = do
    InterpreterState
s <- m InterpreterState
forall (m :: * -> *). InterpreterStateMonad m => m InterpreterState
getInterpreterState
    let (a :: a
a, s' :: InterpreterState
s') = InterpreterState -> (a, InterpreterState)
f InterpreterState
s
    a
a a -> m () -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ InterpreterState -> m ()
forall (m :: * -> *).
InterpreterStateMonad m =>
InterpreterState -> m ()
putInterpreterState InterpreterState
s'

  modifyInterpreterState :: (InterpreterState -> InterpreterState) -> m ()
  modifyInterpreterState f :: InterpreterState -> InterpreterState
f = (InterpreterState -> ((), InterpreterState)) -> m ()
forall (m :: * -> *) a.
InterpreterStateMonad m =>
(InterpreterState -> (a, InterpreterState)) -> m a
stateInterpreterState (((), ) (InterpreterState -> ((), InterpreterState))
-> (InterpreterState -> InterpreterState)
-> InterpreterState
-> ((), InterpreterState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InterpreterState -> InterpreterState
f)

instance InterpreterStateMonad (ExceptT MichelsonFailed $
                              ReaderT ContractEnv $
                                 State InterpreterState) where
  stateInterpreterState :: (InterpreterState -> (a, InterpreterState))
-> ($)
     (ExceptT MichelsonFailed)
     (ReaderT ContractEnv $ State InterpreterState)
     a
stateInterpreterState f :: InterpreterState -> (a, InterpreterState)
f = ReaderT ContractEnv (State InterpreterState) a
-> ($)
     (ExceptT MichelsonFailed)
     (ReaderT ContractEnv $ State InterpreterState)
     a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ReaderT ContractEnv (State InterpreterState) a
 -> ($)
      (ExceptT MichelsonFailed)
      (ReaderT ContractEnv $ State InterpreterState)
      a)
-> ReaderT ContractEnv (State InterpreterState) a
-> ($)
     (ExceptT MichelsonFailed)
     (ReaderT ContractEnv $ State InterpreterState)
     a
forall a b. (a -> b) -> a -> b
$ State InterpreterState a
-> ReaderT ContractEnv (State InterpreterState) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (State InterpreterState a
 -> ReaderT ContractEnv (State InterpreterState) a)
-> State InterpreterState a
-> ReaderT ContractEnv (State InterpreterState) a
forall a b. (a -> b) -> a -> b
$ (InterpreterState -> (a, InterpreterState))
-> State InterpreterState a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state InterpreterState -> (a, InterpreterState)
f

type EvalM m =
  ( MonadReader ContractEnv m
  , InterpreterStateMonad m
  , MonadError MichelsonFailed m
  )

data StkEl t = StkEl
  { StkEl t -> Value t
seValue :: Value t
  , StkEl t -> VarAnn
seVarAnn :: U.VarAnn
  , StkEl t -> Notes t
seNotes :: Notes t
  } deriving stock (StkEl t -> StkEl t -> Bool
(StkEl t -> StkEl t -> Bool)
-> (StkEl t -> StkEl t -> Bool) -> Eq (StkEl t)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (t :: T). StkEl t -> StkEl t -> Bool
/= :: StkEl t -> StkEl t -> Bool
$c/= :: forall (t :: T). StkEl t -> StkEl t -> Bool
== :: StkEl t -> StkEl t -> Bool
$c== :: forall (t :: T). StkEl t -> StkEl t -> Bool
Eq, Int -> StkEl t -> ShowS
[StkEl t] -> ShowS
StkEl t -> String
(Int -> StkEl t -> ShowS)
-> (StkEl t -> String) -> ([StkEl t] -> ShowS) -> Show (StkEl t)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (t :: T). Int -> StkEl t -> ShowS
forall (t :: T). [StkEl t] -> ShowS
forall (t :: T). StkEl t -> String
showList :: [StkEl t] -> ShowS
$cshowList :: forall (t :: T). [StkEl t] -> ShowS
show :: StkEl t -> String
$cshow :: forall (t :: T). StkEl t -> String
showsPrec :: Int -> StkEl t -> ShowS
$cshowsPrec :: forall (t :: T). Int -> StkEl t -> ShowS
Show)

starNotesStkEl :: forall t. Value t -> StkEl t
starNotesStkEl :: Value t -> StkEl t
starNotesStkEl v :: Value t
v = Value t -> VarAnn -> Notes t -> StkEl t
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value t
v VarAnn
forall k (a :: k). Annotation a
U.noAnn (Notes t -> StkEl t) -> Notes t -> StkEl t
forall a b. (a -> b) -> a -> b
$ Value t -> (KnownT t => Notes t) -> Notes t
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (KnownT t => a) -> a
withValueTypeSanity Value t
v ((KnownT t => Notes t) -> Notes t)
-> (KnownT t => Notes t) -> Notes t
forall a b. (a -> b) -> a -> b
$ SingI t => Notes t
forall (t :: T). SingI t => Notes t
starNotes @t

type InstrRunner m =
  forall inp out.
     Instr inp out
  -> Rec StkEl inp
  -> m (Rec StkEl out)

-- | Function to change amount of remaining steps stored in State monad.
runInstr :: EvalM m => InstrRunner m
runInstr :: InstrRunner m
runInstr i :: Instr inp out
i@(Seq _i1 :: Instr inp b
_i1 _i2 :: Instr b out
_i2) r :: Rec StkEl inp
r = InstrRunner m
-> Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
i Rec StkEl inp
r
runInstr i :: Instr inp out
i@(WithLoc _ _) r :: Rec StkEl inp
r = InstrRunner m
-> Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
i Rec StkEl inp
r
runInstr i :: Instr inp out
i@(InstrWithNotes _ _i1 :: Instr inp out
_i1) r :: Rec StkEl inp
r = InstrRunner m
-> Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
i Rec StkEl inp
r
runInstr i :: Instr inp out
i@(InstrWithVarNotes _ _i1 :: Instr inp out
_i1) r :: Rec StkEl inp
r = InstrRunner m
-> Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
i Rec StkEl inp
r
runInstr i :: Instr inp out
i@Instr inp out
Nop r :: Rec StkEl inp
r = InstrRunner m
-> Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
i Rec StkEl inp
r
runInstr i :: Instr inp out
i@(Nested _) r :: Rec StkEl inp
r = InstrRunner m
-> Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
i Rec StkEl inp
r
runInstr i :: Instr inp out
i r :: Rec StkEl inp
r = do
  RemainingSteps
rs <- InterpreterState -> RemainingSteps
isRemainingSteps (InterpreterState -> RemainingSteps)
-> m InterpreterState -> m RemainingSteps
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m InterpreterState
forall (m :: * -> *). InterpreterStateMonad m => m InterpreterState
getInterpreterState
  if RemainingSteps
rs RemainingSteps -> RemainingSteps -> Bool
forall a. Eq a => a -> a -> Bool
== 0
  then MichelsonFailed -> m (Rec StkEl out)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError MichelsonFailed
MichelsonGasExhaustion
  else do
    (InterpreterState -> InterpreterState) -> m ()
forall (m :: * -> *).
InterpreterStateMonad m =>
(InterpreterState -> InterpreterState) -> m ()
modifyInterpreterState (\s :: InterpreterState
s -> InterpreterState
s {isRemainingSteps :: RemainingSteps
isRemainingSteps = RemainingSteps
rs RemainingSteps -> RemainingSteps -> RemainingSteps
forall a. Num a => a -> a -> a
- 1})
    InstrRunner m
-> Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
i Rec StkEl inp
r

runInstrNoGas :: EvalM m => InstrRunner m
runInstrNoGas :: InstrRunner m
runInstrNoGas = InstrRunner m -> InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstrNoGas

-- | Function to interpret Michelson instruction(s) against given stack.
runInstrImpl :: EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl :: InstrRunner m -> InstrRunner m
runInstrImpl runner :: InstrRunner m
runner (Seq i1 :: Instr inp b
i1 i2 :: Instr b out
i2) r :: Rec StkEl inp
r = Instr inp b -> Rec StkEl inp -> m (Rec StkEl b)
InstrRunner m
runner Instr inp b
i1 Rec StkEl inp
r m (Rec StkEl b)
-> (Rec StkEl b -> m (Rec StkEl out)) -> m (Rec StkEl out)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \r' :: Rec StkEl b
r' -> Instr b out -> Rec StkEl b -> m (Rec StkEl out)
InstrRunner m
runner Instr b out
i2 Rec StkEl b
r'
runInstrImpl runner :: InstrRunner m
runner (WithLoc _ i :: Instr inp out
i) r :: Rec StkEl inp
r = Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
InstrRunner m
runner Instr inp out
i Rec StkEl inp
r
runInstrImpl runner :: InstrRunner m
runner (InstrWithNotes (PackedNotes n :: Notes a
n) i :: Instr inp out
i) inp :: Rec StkEl inp
inp =
  Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
InstrRunner m
runner Instr inp out
i Rec StkEl inp
inp m (Rec StkEl out)
-> (Rec StkEl out -> Rec StkEl out) -> m (Rec StkEl out)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    StkEl v :: Value r
v vn :: VarAnn
vn _ :& r :: Rec StkEl rs
r -> Value r -> VarAnn -> Notes r -> StkEl r
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value r
v VarAnn
vn Notes a
Notes r
n StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl runner :: InstrRunner m
runner (InstrWithVarNotes (NonEmpty VarAnn -> [Element (NonEmpty VarAnn)]
forall t. Container t => t -> [Element t]
toList -> [Element (NonEmpty VarAnn)]
vns) i :: Instr inp out
i) inp :: Rec StkEl inp
inp = do
  Rec StkEl out
out <- Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
InstrRunner m
runner Instr inp out
i Rec StkEl inp
inp
  let zipRec :: [U.VarAnn] -> Rec StkEl rs -> Rec StkEl rs
      zipRec :: [VarAnn] -> Rec StkEl rs -> Rec StkEl rs
zipRec [] RNil = Rec StkEl rs
forall u (a :: u -> *). Rec a '[]
RNil
      zipRec (vn :: VarAnn
vn : rs :: [VarAnn]
rs) stk :: Rec StkEl rs
stk = case Rec StkEl rs
stk of
        StkEl v :: Value r
v _ n :: Notes r
n :& r :: Rec StkEl rs
r -> Value r -> VarAnn -> Notes r -> StkEl r
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value r
v VarAnn
vn Notes r
n StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& [VarAnn] -> Rec StkEl rs -> Rec StkEl rs
forall (rs :: [T]). [VarAnn] -> Rec StkEl rs -> Rec StkEl rs
zipRec [VarAnn]
rs Rec StkEl rs
r
        RNil -> Text -> Rec StkEl rs
forall a. HasCallStack => Text -> a
error "Output stack is exhausted but there are still var annotations"
      zipRec [] sm :: Rec StkEl rs
sm = Rec StkEl rs
sm
  Rec StkEl out -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl out -> m (Rec StkEl out))
-> Rec StkEl out -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ [VarAnn] -> Rec StkEl out -> Rec StkEl out
forall (rs :: [T]). [VarAnn] -> Rec StkEl rs -> Rec StkEl rs
zipRec [Element (NonEmpty VarAnn)]
[VarAnn]
vns Rec StkEl out
out
runInstrImpl runner :: InstrRunner m
runner (FrameInstr (Proxy s
_ :: Proxy s) i :: Instr a b
i) r :: Rec StkEl inp
r = do
  let (inp :: Rec StkEl a
inp, end :: Rec StkEl s
end) = Rec StkEl (a ++ s) -> (Rec StkEl a, Rec StkEl s)
forall k (l :: [k]) (r :: [k]) (f :: k -> *).
RSplit l r =>
Rec f (l ++ r) -> (Rec f l, Rec f r)
rsplit @_ @_ @s Rec StkEl inp
Rec StkEl (a ++ s)
r
  Rec StkEl b
out <- InstrRunner m -> Instr a b -> Rec StkEl a -> m (Rec StkEl b)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner Instr a b
i Rec StkEl a
inp
  return (Rec StkEl b
out Rec StkEl b -> Rec StkEl s -> Rec StkEl (b ++ s)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Rec StkEl s
end)
runInstrImpl _ Nop r :: Rec StkEl inp
r = Rec StkEl inp -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl inp -> m (Rec StkEl out))
-> Rec StkEl inp -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Rec StkEl inp
r
runInstrImpl runner :: InstrRunner m
runner (Ext nop :: ExtInstr inp
nop) r :: Rec StkEl inp
r = Rec StkEl inp
r Rec StkEl inp -> m () -> m (Rec StkEl inp)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ InstrRunner m -> SomeItStack -> m ()
forall (m :: * -> *).
EvalM m =>
InstrRunner m -> SomeItStack -> m ()
interpretExt InstrRunner m
runner (ExtInstr inp -> Rec StkEl inp -> SomeItStack
forall (inp :: [T]). ExtInstr inp -> Rec StkEl inp -> SomeItStack
SomeItStack ExtInstr inp
nop Rec StkEl inp
r)
runInstrImpl runner :: InstrRunner m
runner (Nested sq :: Instr inp out
sq) r :: Rec StkEl inp
r = Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
InstrRunner m
runner Instr inp out
sq Rec StkEl inp
r
runInstrImpl runner :: InstrRunner m
runner (DocGroup _ sq :: Instr inp out
sq) r :: Rec StkEl inp
r = InstrRunner m
-> Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner Instr inp out
sq Rec StkEl inp
r
runInstrImpl _ DROP (_ :& r :: Rec StkEl rs
r) = Rec StkEl rs -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl rs -> m (Rec StkEl out))
-> Rec StkEl rs -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Rec StkEl rs
r
runInstrImpl runner :: InstrRunner m
runner (DROPN s :: Sing n
s) stack :: Rec StkEl inp
stack =
  case Sing n
s of
    SZ -> Rec StkEl inp -> m (Rec StkEl inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec StkEl inp
stack
    SS s' -> case Rec StkEl inp
stack of
      -- Note: we intentionally do not use `runner` to recursively
      -- interpret `DROPN` here.
      -- All these recursive calls together correspond to a single
      -- Michelson instruction call.
      -- This recursion is implementation detail of `DROPN`.
      -- The same reasoning applies to other instructions parameterized
      -- by a natural number like 'DIPN'.
      (_ :& r :: Rec StkEl rs
r) -> InstrRunner m -> Instr rs out -> Rec StkEl rs -> m (Rec StkEl out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner (Sing n -> Instr rs (Drop n rs)
forall (n :: Peano) (s :: [T]).
(SingI n, KnownPeano n, RequireLongerOrSameLength s n,
 NFData (Sing n)) =>
Sing n -> Instr s (Drop n s)
DROPN Sing n
SingNat n
s') Rec StkEl rs
r
runInstrImpl _ DUP (a :: StkEl r
a :& r :: Rec StkEl rs
r) = Rec StkEl (r : r : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : r : rs) -> m (Rec StkEl out))
-> Rec StkEl (r : r : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ StkEl r
a StkEl r -> Rec StkEl (r : rs) -> Rec StkEl (r : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StkEl r
a StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ SWAP (a :: StkEl r
a :& b :: StkEl r
b :& r :: Rec StkEl rs
r) = Rec StkEl (r : r : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : r : rs) -> m (Rec StkEl out))
-> Rec StkEl (r : r : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ StkEl r
b StkEl r -> Rec StkEl (r : rs) -> Rec StkEl (r : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StkEl r
a StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ (DIG nSing0 :: Sing n
nSing0) input0 :: Rec StkEl inp
input0 =
  Rec StkEl out -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl out -> m (Rec StkEl out))
-> Rec StkEl out -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ (Sing n, Rec StkEl inp) -> Rec StkEl out
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDIG n inp out a =>
(Sing n, Rec StkEl inp) -> Rec StkEl out
go (Sing n
nSing0, Rec StkEl inp
input0)
  where
    go :: forall (n :: Peano) inp out a. T.ConstraintDIG n inp out a =>
      (Sing n, Rec StkEl inp) -> Rec StkEl out
    go :: (Sing n, Rec StkEl inp) -> Rec StkEl out
go = \case
      (SZ, stack :: Rec StkEl inp
stack) ->  Rec StkEl inp
Rec StkEl out
stack
      (SS nSing, b :: StkEl r
b :& r :: Rec StkEl rs
r) -> case (Sing n, Rec StkEl rs)
-> Rec StkEl (a : (Take n rs ++ Drop ('S n) inp))
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDIG n inp out a =>
(Sing n, Rec StkEl inp) -> Rec StkEl out
go (Sing n
SingNat n
nSing, Rec StkEl rs
r) of
        (a :: StkEl r
a :& resTail :: Rec StkEl rs
resTail) -> StkEl r
a StkEl r -> Rec StkEl (r : rs) -> Rec StkEl (r : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StkEl r
b StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
resTail
runInstrImpl _ (DUG nSing0 :: Sing n
nSing0) input0 :: Rec StkEl inp
input0 =
  Rec StkEl out -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl out -> m (Rec StkEl out))
-> Rec StkEl out -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ (Sing n, Rec StkEl inp) -> Rec StkEl out
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDUG n inp out a =>
(Sing n, Rec StkEl inp) -> Rec StkEl out
go (Sing n
nSing0, Rec StkEl inp
input0)
  where
    go :: forall (n :: Peano) inp out a. T.ConstraintDUG n inp out a =>
      (Sing n, Rec StkEl inp) -> Rec StkEl out
    go :: (Sing n, Rec StkEl inp) -> Rec StkEl out
go = \case
      (SZ, stack :: Rec StkEl inp
stack) -> Rec StkEl inp
Rec StkEl out
stack
      (SS s', a :: StkEl r
a :& b :: StkEl r
b :& r :: Rec StkEl rs
r) -> StkEl r
b StkEl r
-> Rec StkEl (Take n rs ++ (a : Drop n (Drop ('S 'Z) inp)))
-> Rec StkEl (r : (Take n rs ++ (a : Drop n (Drop ('S 'Z) inp))))
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& (Sing n, Rec StkEl (r : rs))
-> Rec StkEl (Take n rs ++ (a : Drop n (Drop ('S 'Z) inp)))
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDUG n inp out a =>
(Sing n, Rec StkEl inp) -> Rec StkEl out
go (Sing n
SingNat n
s', StkEl r
a StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
runInstrImpl _ SOME ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& r :: Rec StkEl rs
r) =
  Value r -> (KnownT r => m (Rec StkEl out)) -> m (Rec StkEl out)
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (KnownT t => a) -> a
withValueTypeSanity Value r
a ((KnownT r => m (Rec StkEl out)) -> m (Rec StkEl out))
-> (KnownT r => m (Rec StkEl out)) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$
    Rec StkEl ('TOption r : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption r : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TOption r : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TOption r) -> StkEl ('TOption r)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value r) -> Value ('TOption r)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Value r -> Maybe (Value r)
forall a. a -> Maybe a
Just Value r
a)) StkEl ('TOption r) -> Rec StkEl rs -> Rec StkEl ('TOption r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ (PUSH v :: Value' Instr t
v) r :: Rec StkEl inp
r = Rec StkEl (t : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (t : inp) -> m (Rec StkEl out))
-> Rec StkEl (t : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value' Instr t -> StkEl t
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr t
v StkEl t -> Rec StkEl inp -> Rec StkEl (t : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl _ NONE r :: Rec StkEl inp
r = Rec StkEl ('TOption a : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption a : inp) -> m (Rec StkEl out))
-> Rec StkEl ('TOption a : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TOption a) -> StkEl ('TOption a)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value' Instr a) -> Value ('TOption a)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption Maybe (Value' Instr a)
forall a. Maybe a
Nothing) StkEl ('TOption a) -> Rec StkEl inp -> Rec StkEl ('TOption a : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl _ UNIT r :: Rec StkEl inp
r = Rec StkEl ('TUnit : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TUnit : inp) -> m (Rec StkEl out))
-> Rec StkEl ('TUnit : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TUnit -> StkEl 'TUnit
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value 'TUnit
forall (instr :: [T] -> [T] -> *). Value' instr 'TUnit
VUnit StkEl 'TUnit -> Rec StkEl inp -> Rec StkEl ('TUnit : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl runner :: InstrRunner m
runner (IF_NONE _bNone :: Instr s out
_bNone bJust :: Instr (a : s) out
bJust) (StkEl (VOption (Just a :: Value' Instr t
a)) _ _ :& r :: Rec StkEl rs
r) =
  Instr (a : s) out -> Rec StkEl (a : s) -> m (Rec StkEl out)
InstrRunner m
runner Instr (a : s) out
bJust (Value' Instr t -> StkEl t
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr t
a StkEl t -> Rec StkEl rs -> Rec StkEl (t : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
runInstrImpl runner :: InstrRunner m
runner (IF_NONE bNone :: Instr s out
bNone _bJust :: Instr (a : s) out
_bJust) (StkEl (VOption Nothing) _ _ :& r :: Rec StkEl rs
r) =
  Instr s out -> Rec StkEl s -> m (Rec StkEl out)
InstrRunner m
runner Instr s out
bNone Rec StkEl s
Rec StkEl rs
r
runInstrImpl _ (AnnPAIR nt :: TypeAnn
nt nf1 :: RootAnn
nf1 nf2 :: RootAnn
nf2) ((StkEl a :: Value r
a _ na :: Notes r
na) :& (StkEl b :: Value r
b _ nb :: Notes r
nb) :& r :: Rec StkEl rs
r) =
  Rec StkEl ('TPair r r : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TPair r r : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TPair r r : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TPair r r)
-> VarAnn -> Notes ('TPair r r) -> StkEl ('TPair r r)
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl ((Value r, Value r) -> Value ('TPair r r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value r
a, Value r
b)) VarAnn
forall k (a :: k). Annotation a
U.noAnn (TypeAnn
-> RootAnn -> RootAnn -> Notes r -> Notes r -> Notes ('TPair r r)
forall (p :: T) (q :: T).
TypeAnn
-> RootAnn -> RootAnn -> Notes p -> Notes q -> Notes ('TPair p q)
NTPair TypeAnn
nt RootAnn
nf1 RootAnn
nf2 Notes r
na Notes r
nb) StkEl ('TPair r r) -> Rec StkEl rs -> Rec StkEl ('TPair r r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ (AnnCAR _) (StkEl (VPair (a :: Value' Instr l
a, _b :: Value' Instr r
_b)) _ _ :& r :: Rec StkEl rs
r) = Rec StkEl (l : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (l : rs) -> m (Rec StkEl out))
-> Rec StkEl (l : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value' Instr l -> StkEl l
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr l
a StkEl l -> Rec StkEl rs -> Rec StkEl (l : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ (AnnCDR _) (StkEl (VPair (_a :: Value' Instr l
_a, b :: Value' Instr r
b)) _ _ :& r :: Rec StkEl rs
r) = Rec StkEl (r : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : rs) -> m (Rec StkEl out))
-> Rec StkEl (r : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value' Instr r -> StkEl r
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr r
b StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ LEFT ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& r :: Rec StkEl rs
r) =
  Value r -> (KnownT r => m (Rec StkEl out)) -> m (Rec StkEl out)
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (KnownT t => a) -> a
withValueTypeSanity Value r
a ((KnownT r => m (Rec StkEl out)) -> m (Rec StkEl out))
-> (KnownT r => m (Rec StkEl out)) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$
    Rec StkEl ('TOr r b : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOr r b : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TOr r b : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TOr r b) -> StkEl ('TOr r b)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Either (Value r) (Value' Instr b) -> Value ('TOr r b)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(KnownT l, KnownT r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Either (Value r) (Value' Instr b) -> Value ('TOr r b))
-> Either (Value r) (Value' Instr b) -> Value ('TOr r b)
forall a b. (a -> b) -> a -> b
$ Value r -> Either (Value r) (Value' Instr b)
forall a b. a -> Either a b
Left Value r
a) StkEl ('TOr r b) -> Rec StkEl rs -> Rec StkEl ('TOr r b : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ RIGHT ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
b) :& r :: Rec StkEl rs
r) =
  Value r -> (KnownT r => m (Rec StkEl out)) -> m (Rec StkEl out)
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (KnownT t => a) -> a
withValueTypeSanity Value r
b ((KnownT r => m (Rec StkEl out)) -> m (Rec StkEl out))
-> (KnownT r => m (Rec StkEl out)) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$
    Rec StkEl ('TOr a r : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOr a r : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TOr a r : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TOr a r) -> StkEl ('TOr a r)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Either (Value' Instr a) (Value r) -> Value ('TOr a r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(KnownT l, KnownT r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Either (Value' Instr a) (Value r) -> Value ('TOr a r))
-> Either (Value' Instr a) (Value r) -> Value ('TOr a r)
forall a b. (a -> b) -> a -> b
$ Value r -> Either (Value' Instr a) (Value r)
forall a b. b -> Either a b
Right Value r
b) StkEl ('TOr a r) -> Rec StkEl rs -> Rec StkEl ('TOr a r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl runner :: InstrRunner m
runner (IF_LEFT bLeft :: Instr (a : s) out
bLeft _) (StkEl (VOr (Left a :: Value' Instr l
a)) _ _ :& r :: Rec StkEl rs
r) =
  Instr (a : s) out -> Rec StkEl (a : s) -> m (Rec StkEl out)
InstrRunner m
runner Instr (a : s) out
bLeft (Value' Instr l -> StkEl l
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr l
a StkEl l -> Rec StkEl rs -> Rec StkEl (l : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
runInstrImpl runner :: InstrRunner m
runner (IF_LEFT _ bRight :: Instr (b : s) out
bRight) (StkEl (VOr (Right a :: Value' Instr r
a)) _ _ :& r :: Rec StkEl rs
r) =
  Instr (b : s) out -> Rec StkEl (b : s) -> m (Rec StkEl out)
InstrRunner m
runner Instr (b : s) out
bRight (Value' Instr r -> StkEl r
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr r
a StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
-- More here
runInstrImpl _ NIL r :: Rec StkEl inp
r = Rec StkEl ('TList p : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TList p : inp) -> m (Rec StkEl out))
-> Rec StkEl ('TList p : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TList p) -> StkEl ('TList p)
forall (x :: T). Value x -> StkEl x
starNotesStkEl ([Value' Instr p] -> Value ('TList p)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
[Value' instr t] -> Value' instr ('TList t)
VList []) StkEl ('TList p) -> Rec StkEl inp -> Rec StkEl ('TList p : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl _ CONS (a :: StkEl r
a :& StkEl (VList l :: [Value' Instr t]
l) _ _ :& r :: Rec StkEl rs
r) = Rec StkEl ('TList r : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TList r : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TList r : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TList r) -> StkEl ('TList r)
forall (x :: T). Value x -> StkEl x
starNotesStkEl ([Value' Instr r] -> Value ('TList r)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
[Value' instr t] -> Value' instr ('TList t)
VList (StkEl r -> Value' Instr r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a Value' Instr r -> [Value' Instr r] -> [Value' Instr r]
forall a. a -> [a] -> [a]
: [Value' Instr r]
[Value' Instr t]
l)) StkEl ('TList r) -> Rec StkEl rs -> Rec StkEl ('TList r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl runner :: InstrRunner m
runner (IF_CONS _ bNil :: Instr s out
bNil) (StkEl (VList []) _ _ :& r :: Rec StkEl rs
r) = Instr s out -> Rec StkEl s -> m (Rec StkEl out)
InstrRunner m
runner Instr s out
bNil Rec StkEl s
Rec StkEl rs
r
runInstrImpl runner :: InstrRunner m
runner (IF_CONS bCons :: Instr (a : 'TList a : s) out
bCons _) (StkEl (VList (lh :: Value' Instr t
lh : lr :: [Value' Instr t]
lr)) _ _ :& r :: Rec StkEl rs
r) =
  Instr (a : 'TList a : s) out
-> Rec StkEl (a : 'TList a : s) -> m (Rec StkEl out)
InstrRunner m
runner Instr (a : 'TList a : s) out
bCons (Value' Instr t -> StkEl t
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr t
lh StkEl t
-> Rec StkEl ('TList t : rs) -> Rec StkEl (t : 'TList t : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Value ('TList t) -> StkEl ('TList t)
forall (x :: T). Value x -> StkEl x
starNotesStkEl ([Value' Instr t] -> Value ('TList t)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
[Value' instr t] -> Value' instr ('TList t)
VList [Value' Instr t]
lr) StkEl ('TList t) -> Rec StkEl rs -> Rec StkEl ('TList t : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
runInstrImpl _ SIZE (a :: StkEl r
a :& r :: Rec StkEl rs
r) = Rec StkEl ('TNat : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TNat : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TNat : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TNat -> StkEl 'TNat
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Natural -> Value 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural -> Value 'TNat) -> Natural -> Value 'TNat
forall a b. (a -> b) -> a -> b
$ (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> (Int -> Integer) -> Int -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger) (Int -> Natural) -> Int -> Natural
forall a b. (a -> b) -> a -> b
$ Value' Instr r -> Int
forall (c :: T) (instr :: [T] -> [T] -> *).
SizeOp c =>
Value' instr c -> Int
evalSize (Value' Instr r -> Int) -> Value' Instr r -> Int
forall a b. (a -> b) -> a -> b
$ StkEl r -> Value' Instr r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a) StkEl 'TNat -> Rec StkEl rs -> Rec StkEl ('TNat : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ EMPTY_SET r :: Rec StkEl inp
r = Rec StkEl ('TSet e : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TSet e : inp) -> m (Rec StkEl out))
-> Rec StkEl ('TSet e : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TSet e) -> StkEl ('TSet e)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Set (Value' Instr e) -> Value ('TSet e)
forall (t :: T) (instr :: [T] -> [T] -> *).
(KnownT t, Comparable t) =>
Set (Value' instr t) -> Value' instr ('TSet t)
VSet Set (Value' Instr e)
forall a. Set a
Set.empty) StkEl ('TSet e) -> Rec StkEl inp -> Rec StkEl ('TSet e : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl _ EMPTY_MAP r :: Rec StkEl inp
r = Rec StkEl ('TMap a b : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TMap a b : inp) -> m (Rec StkEl out))
-> Rec StkEl ('TMap a b : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TMap a b) -> StkEl ('TMap a b)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Map (Value' Instr a) (Value' Instr b) -> Value ('TMap a b)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
VMap Map (Value' Instr a) (Value' Instr b)
forall k a. Map k a
Map.empty) StkEl ('TMap a b) -> Rec StkEl inp -> Rec StkEl ('TMap a b : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl _ EMPTY_BIG_MAP r :: Rec StkEl inp
r = Rec StkEl ('TBigMap a b : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBigMap a b : inp) -> m (Rec StkEl out))
-> Rec StkEl ('TBigMap a b : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TBigMap a b) -> StkEl ('TBigMap a b)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Map (Value' Instr a) (Value' Instr b) -> Value ('TBigMap a b)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VBigMap Map (Value' Instr a) (Value' Instr b)
forall k a. Map k a
Map.empty) StkEl ('TBigMap a b)
-> Rec StkEl inp -> Rec StkEl ('TBigMap a b : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl runner :: InstrRunner m
runner (MAP ops :: Instr (MapOpInp c : s) (b : s)
ops) ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& r :: Rec StkEl rs
r) =
  case Instr (MapOpInp c : s) (b : s)
ops of
    (code :: Instr (MapOpInp c ': s) (b ': s)) -> do
      -- Evaluation must preserve all stack modifications that @MAP@'s does.
      (newStack :: Rec StkEl rs
newStack, newList :: [Value' Instr b]
newList) <- ((Rec StkEl rs, [Value' Instr b])
 -> StkEl (MapOpInp c) -> m (Rec StkEl rs, [Value' Instr b]))
-> (Rec StkEl rs, [Value' Instr b])
-> [StkEl (MapOpInp c)]
-> m (Rec StkEl rs, [Value' Instr b])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (\(curStack :: Rec StkEl rs
curStack, curList :: [Value' Instr b]
curList) (val :: StkEl (MapOpInp c)) -> do
        Rec StkEl (b : s)
res <- Instr (MapOpInp c : rs) (b : s)
-> Rec StkEl (MapOpInp c : rs) -> m (Rec StkEl (b : s))
InstrRunner m
runner Instr (MapOpInp c : rs) (b : s)
Instr (MapOpInp r : s) (b : s)
code (StkEl (MapOpInp c)
StkEl (MapOpInp r)
val StkEl (MapOpInp c) -> Rec StkEl rs -> Rec StkEl (MapOpInp c : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
curStack)
        case Rec StkEl (b : s)
res of
          ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> nextVal :: T.Value b) :& nextStack :: Rec StkEl rs
nextStack) -> (Rec StkEl rs, [Value' Instr b])
-> m (Rec StkEl rs, [Value' Instr b])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl rs
nextStack, Value' Instr b
nextVal Value' Instr b -> [Value' Instr b] -> [Value' Instr b]
forall a. a -> [a] -> [a]
: [Value' Instr b]
curList))
        (Rec StkEl rs
r, []) (Value (MapOpInp c) -> StkEl (MapOpInp c)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Value (MapOpInp c) -> StkEl (MapOpInp c))
-> [Value (MapOpInp c)] -> [StkEl (MapOpInp c)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value r -> [Value' Instr (MapOpInp r)]
forall (c :: T) (instr :: [T] -> [T] -> *).
MapOp c =>
Value' instr c -> [Value' instr (MapOpInp c)]
mapOpToList @c Value r
a)
      Rec StkEl (MapOpRes c b : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (MapOpRes c b : rs) -> m (Rec StkEl out))
-> Rec StkEl (MapOpRes c b : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value (MapOpRes c b) -> StkEl (MapOpRes c b)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Value r -> [Value' Instr b] -> Value' Instr (MapOpRes r b)
forall (c :: T) (b :: T) (instr :: [T] -> [T] -> *).
(MapOp c, KnownT b) =>
Value' instr c -> [Value' instr b] -> Value' instr (MapOpRes c b)
mapOpFromList Value r
a ([Value' Instr b] -> [Value' Instr b]
forall a. [a] -> [a]
reverse [Value' Instr b]
newList)) StkEl (MapOpRes c b)
-> Rec StkEl rs -> Rec StkEl (MapOpRes c b : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
newStack
runInstrImpl runner :: InstrRunner m
runner (ITER ops :: Instr (IterOpEl c : out) out
ops) (a :: StkEl r
a :& r :: Rec StkEl rs
r) =
  case Instr (IterOpEl c : out) out
ops of
    (code :: Instr (IterOpEl c ': s) s) ->
      case Value' Instr r
-> (Maybe (Value' Instr (IterOpEl r)), Value' Instr r)
forall (c :: T) (instr :: [T] -> [T] -> *).
IterOp c =>
Value' instr c
-> (Maybe (Value' instr (IterOpEl c)), Value' instr c)
iterOpDetachOne @c (StkEl r -> Value' Instr r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a) of
        (Just x :: Value' Instr (IterOpEl r)
x, xs :: Value' Instr r
xs) -> do
          Rec StkEl out
res <- Instr (IterOpEl c : rs) out
-> Rec StkEl (IterOpEl c : rs) -> m (Rec StkEl out)
InstrRunner m
runner Instr (IterOpEl c : rs) out
Instr (IterOpEl r : out) out
code (Value (IterOpEl c) -> StkEl (IterOpEl c)
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value (IterOpEl c)
Value' Instr (IterOpEl r)
x StkEl (IterOpEl c) -> Rec StkEl rs -> Rec StkEl (IterOpEl c : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
          Instr (r : out) out -> Rec StkEl (r : out) -> m (Rec StkEl out)
InstrRunner m
runner (Instr (IterOpEl r : out) out -> Instr (r : out) out
forall (c :: T) (s :: [T]).
IterOp c =>
Instr (IterOpEl c : s) s -> Instr (c : s) s
ITER Instr (IterOpEl r : out) out
code) (Value' Instr r -> StkEl r
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr r
xs StkEl r -> Rec StkEl out -> Rec StkEl (r : out)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl out
res)
        (Nothing, _) -> Rec StkEl rs -> m (Rec StkEl rs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec StkEl rs
r
runInstrImpl _ MEM (a :: StkEl r
a :& b :: StkEl r
b :& r :: Rec StkEl rs
r) = Rec StkEl ('TBool : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBool : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TBool : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TBool -> StkEl 'TBool
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Bool -> Value 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Value' Instr (MemOpKey r) -> Value' Instr r -> Bool
forall (c :: T) (instr :: [T] -> [T] -> *).
MemOp c =>
Value' instr (MemOpKey c) -> Value' instr c -> Bool
evalMem (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a) (StkEl r -> Value' Instr r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
b))) StkEl 'TBool -> Rec StkEl rs -> Rec StkEl ('TBool : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ GET (a :: StkEl r
a :& b :: StkEl r
b :& r :: Rec StkEl rs
r) = Rec StkEl ('TOption (GetOpVal c) : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption (GetOpVal c) : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TOption (GetOpVal c) : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TOption (GetOpVal c)) -> StkEl ('TOption (GetOpVal c))
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value' Instr (GetOpVal c)) -> Value ('TOption (GetOpVal c))
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Value' Instr (GetOpKey r)
-> Value' Instr r -> Maybe (Value' Instr (GetOpVal r))
forall (c :: T) (instr :: [T] -> [T] -> *).
GetOp c =>
Value' instr (GetOpKey c)
-> Value' instr c -> Maybe (Value' instr (GetOpVal c))
evalGet (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a) (StkEl r -> Value' Instr r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
b))) StkEl ('TOption (GetOpVal c))
-> Rec StkEl rs -> Rec StkEl ('TOption (GetOpVal c) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ UPDATE (a :: StkEl r
a :& b :: StkEl r
b :& c :: StkEl r
c :& r :: Rec StkEl rs
r) =
    Rec StkEl (r : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : rs) -> m (Rec StkEl out))
-> Rec StkEl (r : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value r -> StkEl r
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Value' Instr (UpdOpKey r)
-> Value' Instr (UpdOpParams r) -> Value r -> Value r
forall (c :: T) (instr :: [T] -> [T] -> *).
UpdOp c =>
Value' instr (UpdOpKey c)
-> Value' instr (UpdOpParams c) -> Value' instr c -> Value' instr c
evalUpd (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a) (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
b) (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
c)) StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl runner :: InstrRunner m
runner (IF bTrue :: Instr s out
bTrue _) (StkEl (VBool True) _ _ :& r :: Rec StkEl rs
r) = Instr s out -> Rec StkEl s -> m (Rec StkEl out)
InstrRunner m
runner Instr s out
bTrue Rec StkEl s
Rec StkEl rs
r
runInstrImpl runner :: InstrRunner m
runner (IF _ bFalse :: Instr s out
bFalse) (StkEl (VBool False) _ _ :& r :: Rec StkEl rs
r) = Instr s out -> Rec StkEl s -> m (Rec StkEl out)
InstrRunner m
runner Instr s out
bFalse Rec StkEl s
Rec StkEl rs
r
runInstrImpl _ (LOOP _) (StkEl (VBool False) _ _ :& r :: Rec StkEl rs
r) = Rec StkEl rs -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl rs -> m (Rec StkEl out))
-> Rec StkEl rs -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Rec StkEl rs
r
runInstrImpl runner :: InstrRunner m
runner (LOOP ops :: Instr out ('TBool : out)
ops) (StkEl (VBool True) _ _ :& r :: Rec StkEl rs
r) = do
  Rec StkEl ('TBool : out)
res <- Instr out ('TBool : out)
-> Rec StkEl out -> m (Rec StkEl ('TBool : out))
InstrRunner m
runner Instr out ('TBool : out)
ops Rec StkEl out
Rec StkEl rs
r
  Instr ('TBool : out) out
-> Rec StkEl ('TBool : out) -> m (Rec StkEl out)
InstrRunner m
runner (Instr out ('TBool : out) -> Instr ('TBool : out) out
forall (s :: [T]). Instr s ('TBool : s) -> Instr ('TBool : s) s
LOOP Instr out ('TBool : out)
ops) Rec StkEl ('TBool : out)
res
runInstrImpl _ (LOOP_LEFT _) (StkEl (VOr (Right a :: Value' Instr r
a)) _ _ :& r :: Rec StkEl rs
r) = Rec StkEl (r : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : rs) -> m (Rec StkEl out))
-> Rec StkEl (r : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value' Instr r -> StkEl r
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr r
a StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl runner :: InstrRunner m
runner (LOOP_LEFT ops :: Instr (a : s) ('TOr a b : s)
ops) (StkEl (VOr (Left a :: Value' Instr l
a)) _ _ :& r :: Rec StkEl rs
r) = do
  Rec StkEl ('TOr a b : s)
res <- Instr (a : s) ('TOr a b : s)
-> Rec StkEl (a : s) -> m (Rec StkEl ('TOr a b : s))
InstrRunner m
runner Instr (a : s) ('TOr a b : s)
ops (Value' Instr l -> StkEl l
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr l
a StkEl l -> Rec StkEl rs -> Rec StkEl (l : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
  Instr ('TOr a b : s) (b : s)
-> Rec StkEl ('TOr a b : s) -> m (Rec StkEl (b : s))
InstrRunner m
runner (Instr (a : s) ('TOr a b : s) -> Instr ('TOr a b : s) (b : s)
forall (a :: T) (s :: [T]) (b :: T).
Instr (a : s) ('TOr a b : s) -> Instr ('TOr a b : s) (b : s)
LOOP_LEFT Instr (a : s) ('TOr a b : s)
ops) Rec StkEl ('TOr a b : s)
res
runInstrImpl _ (LAMBDA lam :: Value' Instr ('TLambda i o)
lam) r :: Rec StkEl inp
r = Rec StkEl ('TLambda i o : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TLambda i o : inp) -> m (Rec StkEl out))
-> Rec StkEl ('TLambda i o : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TLambda i o) -> StkEl ('TLambda i o)
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr ('TLambda i o)
lam StkEl ('TLambda i o)
-> Rec StkEl inp -> Rec StkEl ('TLambda i o : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl runner :: InstrRunner m
runner EXEC (a :: StkEl r
a :& StkEl (VLam (RemFail Instr '[inp] '[out] -> Instr '[inp] '[out]
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
T.rfAnyInstr -> Instr '[inp] '[out]
lBody)) _ _ :& r :: Rec StkEl rs
r) = do
  Rec StkEl '[out]
res <- Instr '[inp] '[out] -> Rec StkEl '[inp] -> m (Rec StkEl '[out])
InstrRunner m
runner Instr '[inp] '[out]
lBody (StkEl r
a StkEl r -> Rec StkEl '[] -> Rec StkEl '[r]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl '[]
forall u (a :: u -> *). Rec a '[]
RNil)
  pure $ Rec StkEl '[out]
res Rec StkEl '[out] -> Rec StkEl rs -> Rec StkEl ('[out] ++ rs)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Rec StkEl rs
r
runInstrImpl _ APPLY (StkEl (Value r
a :: T.Value a) _ _ :& StkEl (VLam lBody :: RemFail Instr '[inp] '[out]
lBody) _ _ :& r :: Rec StkEl rs
r) = do
  Rec StkEl ('TLambda b out : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TLambda b out : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TLambda b out : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TLambda b out) -> StkEl ('TLambda b out)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (RemFail Instr '[b] '[out] -> Value ('TLambda b out)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(KnownT inp, KnownT out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
RemFail instr '[inp] '[out] -> Value' instr ('TLambda inp out)
VLam ((forall (o' :: [T]). Instr '[inp] o' -> Instr '[b] o')
-> RemFail Instr '[inp] '[out] -> RemFail Instr '[b] '[out]
forall k (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (o :: k).
(forall (o' :: k). instr i1 o' -> instr i2 o')
-> RemFail instr i1 o -> RemFail instr i2 o
T.rfMapAnyInstr forall (o' :: [T]). Instr '[inp] o' -> Instr '[b] o'
forall (i :: T) (s :: [T]) (o :: [T]).
Instr ('TPair r i : s) o -> Instr (i : s) o
doApply RemFail Instr '[inp] '[out]
lBody)) StkEl ('TLambda b out)
-> Rec StkEl rs -> Rec StkEl ('TLambda b out : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
  where
    doApply :: Instr ('TPair a i ': s) o -> Instr (i ': s) o
    doApply :: Instr ('TPair r i : s) o -> Instr (i : s) o
doApply b :: Instr ('TPair r i : s) o
b = Value r -> Instr (i : s) (r : i : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value r
a Instr (i : s) (r : i : s)
-> Instr (r : i : s) ('TPair r i : s)
-> Instr (i : s) ('TPair r i : s)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr (r : i : s) ('TPair r i : s)
forall (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR Instr (i : s) ('TPair r i : s)
-> Instr ('TPair r i : s) o -> Instr (i : s) o
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr ('TPair r i : s) o -> Instr ('TPair r i : s) o
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
Nested Instr ('TPair r i : s) o
b
runInstrImpl runner :: InstrRunner m
runner (DIP i :: Instr a c
i) (a :: StkEl r
a :& r :: Rec StkEl rs
r) = do
  Rec StkEl c
res <- Instr a c -> Rec StkEl a -> m (Rec StkEl c)
InstrRunner m
runner Instr a c
i Rec StkEl a
Rec StkEl rs
r
  pure $ StkEl r
a StkEl r -> Rec StkEl c -> Rec StkEl (r : c)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl c
res
runInstrImpl runner :: InstrRunner m
runner (DIPN s :: Sing n
s i :: Instr s s'
i) stack :: Rec StkEl inp
stack =
  case Sing n
s of
    SZ -> Instr s s' -> Rec StkEl s -> m (Rec StkEl s')
InstrRunner m
runner Instr s s'
i Rec StkEl inp
Rec StkEl s
stack
    SS s' -> case Rec StkEl inp
stack of
      (a :: StkEl r
a :& r :: Rec StkEl rs
r) -> (StkEl r
a StkEl r
-> Rec StkEl (Take n rs ++ s') -> Rec StkEl (r : (Take n rs ++ s'))
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) (Rec StkEl (Take n rs ++ s') -> Rec StkEl (r : (Take n rs ++ s')))
-> m (Rec StkEl (Take n rs ++ s'))
-> m (Rec StkEl (r : (Take n rs ++ s')))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InstrRunner m
-> Instr rs (Take n rs ++ s')
-> Rec StkEl rs
-> m (Rec StkEl (Take n rs ++ s'))
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner (Sing n -> Instr s s' -> Instr rs (Take n rs ++ s')
forall (n :: Peano) (inp :: [T]) (out :: [T]) (s :: [T])
       (s' :: [T]).
(ConstraintDIPN n inp out s s', NFData (Sing n)) =>
Sing n -> Instr s s' -> Instr inp out
DIPN Sing n
SingNat n
s' Instr s s'
i) Rec StkEl rs
r
runInstrImpl _ FAILWITH (a :: StkEl r
a :& _) = MichelsonFailed -> m (Rec StkEl out)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (MichelsonFailed -> m (Rec StkEl out))
-> MichelsonFailed -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value r -> MichelsonFailed
forall (t :: T). KnownT t => Value t -> MichelsonFailed
MichelsonFailedWith (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a)
runInstrImpl _ CAST (StkEl a :: Value r
a vn :: VarAnn
vn _ :& r :: Rec StkEl rs
r) = Rec StkEl (r : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : rs) -> m (Rec StkEl out))
-> Rec StkEl (r : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value r -> VarAnn -> Notes r -> StkEl r
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value r
a VarAnn
vn Notes r
forall (t :: T). SingI t => Notes t
starNotes StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ RENAME (StkEl a :: Value r
a _ n :: Notes r
n :& r :: Rec StkEl rs
r) = Rec StkEl (r : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : rs) -> m (Rec StkEl out))
-> Rec StkEl (r : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value r -> VarAnn -> Notes r -> StkEl r
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value r
a VarAnn
forall k (a :: k). Annotation a
U.noAnn Notes r
n StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ PACK ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& r :: Rec StkEl rs
r) = Rec StkEl ('TBytes : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBytes : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TBytes : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TBytes -> StkEl 'TBytes
forall (x :: T). Value x -> StkEl x
starNotesStkEl (ByteString -> Value 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value 'TBytes) -> ByteString -> Value 'TBytes
forall a b. (a -> b) -> a -> b
$ Value r -> ByteString
forall (t :: T). PackedValScope t => Value t -> ByteString
packValue' Value r
a) StkEl 'TBytes -> Rec StkEl rs -> Rec StkEl ('TBytes : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ UNPACK (StkEl (VBytes a :: ByteString
a) _ _ :& r :: Rec StkEl rs
r) =
  Rec StkEl ('TOption a : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption a : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TOption a : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TOption a) -> StkEl ('TOption a)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value' Instr a) -> Value ('TOption a)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' Instr a) -> Value ('TOption a))
-> (Either UnpackError (Value' Instr a) -> Maybe (Value' Instr a))
-> Either UnpackError (Value' Instr a)
-> Value ('TOption a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either UnpackError (Value' Instr a) -> Maybe (Value' Instr a)
forall l r. Either l r -> Maybe r
rightToMaybe (Either UnpackError (Value' Instr a) -> Value ('TOption a))
-> Either UnpackError (Value' Instr a) -> Value ('TOption a)
forall a b. (a -> b) -> a -> b
$ ByteString -> Either UnpackError (Value' Instr a)
forall (t :: T).
UnpackedValScope t =>
ByteString -> Either UnpackError (Value t)
runUnpack ByteString
a) StkEl ('TOption a) -> Rec StkEl rs -> Rec StkEl ('TOption a : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ CONCAT (a :: StkEl r
a :& b :: StkEl r
b :& r :: Rec StkEl rs
r) = Rec StkEl (r : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : rs) -> m (Rec StkEl out))
-> Rec StkEl (r : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value r -> StkEl r
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Value r -> Value r -> Value r
forall (c :: T) (instr :: [T] -> [T] -> *).
ConcatOp c =>
Value' instr c -> Value' instr c -> Value' instr c
evalConcat (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a) (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
b)) StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ CONCAT' (StkEl (VList a :: [Value' Instr t]
a) _ _ :& r :: Rec StkEl rs
r) = Rec StkEl (t : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (t : rs) -> m (Rec StkEl out))
-> Rec StkEl (t : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value' Instr t -> StkEl t
forall (x :: T). Value x -> StkEl x
starNotesStkEl ([Value' Instr t] -> Value' Instr t
forall (c :: T) (instr :: [T] -> [T] -> *).
ConcatOp c =>
[Value' instr c] -> Value' instr c
evalConcat' [Value' Instr t]
a) StkEl t -> Rec StkEl rs -> Rec StkEl (t : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ SLICE (StkEl (VNat o :: Natural
o) _ _ :& StkEl (VNat l :: Natural
l) _ _ :& StkEl s :: Value r
s _ _ :& r :: Rec StkEl rs
r) =
  Rec StkEl ('TOption r : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption r : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TOption r : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TOption r) -> StkEl ('TOption r)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value r) -> Value ('TOption r)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Natural -> Natural -> Value r -> Maybe (Value r)
forall (c :: T) (instr :: [T] -> [T] -> *).
SliceOp c =>
Natural -> Natural -> Value' instr c -> Maybe (Value' instr c)
evalSlice Natural
o Natural
l Value r
s)) StkEl ('TOption r) -> Rec StkEl rs -> Rec StkEl ('TOption r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ ISNAT (StkEl (VInt i :: Integer
i) _ _ :& r :: Rec StkEl rs
r) =
  if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0
  then Rec StkEl ('TOption 'TNat : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption 'TNat : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TOption 'TNat : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TOption 'TNat) -> StkEl ('TOption 'TNat)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value 'TNat) -> Value ('TOption 'TNat)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption Maybe (Value 'TNat)
forall a. Maybe a
Nothing) StkEl ('TOption 'TNat)
-> Rec StkEl rs -> Rec StkEl ('TOption 'TNat : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
  else Rec StkEl ('TOption 'TNat : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption 'TNat : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TOption 'TNat : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TOption 'TNat) -> StkEl ('TOption 'TNat)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value 'TNat) -> Value ('TOption 'TNat)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Value 'TNat -> Maybe (Value 'TNat)
forall a. a -> Maybe a
Just (Natural -> Value 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural -> Value 'TNat) -> Natural -> Value 'TNat
forall a b. (a -> b) -> a -> b
$ Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i))) StkEl ('TOption 'TNat)
-> Rec StkEl rs -> Rec StkEl ('TOption 'TNat : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ ADD (l :: StkEl r
l :& r :: StkEl r
r :& rest :: Rec StkEl rs
rest) = (StkEl (ArithRes Add n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes Add n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes Add n m) -> Rec StkEl (ArithRes Add n m : rs))
-> m (StkEl (ArithRes Add n m))
-> m (Rec StkEl (ArithRes Add n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Add -> StkEl r -> StkEl r -> m (StkEl (ArithRes Add r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, Typeable n, Typeable m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy Add
forall k (t :: k). Proxy t
Proxy @Add) StkEl r
l StkEl r
r
runInstrImpl _ SUB (l :: StkEl r
l :& r :: StkEl r
r :& rest :: Rec StkEl rs
rest) = (StkEl (ArithRes Sub n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes Sub n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes Sub n m) -> Rec StkEl (ArithRes Sub n m : rs))
-> m (StkEl (ArithRes Sub n m))
-> m (Rec StkEl (ArithRes Sub n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Sub -> StkEl r -> StkEl r -> m (StkEl (ArithRes Sub r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, Typeable n, Typeable m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy Sub
forall k (t :: k). Proxy t
Proxy @Sub) StkEl r
l StkEl r
r
runInstrImpl _ MUL (l :: StkEl r
l :& r :: StkEl r
r :& rest :: Rec StkEl rs
rest) = (StkEl (ArithRes Mul n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes Mul n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes Mul n m) -> Rec StkEl (ArithRes Mul n m : rs))
-> m (StkEl (ArithRes Mul n m))
-> m (Rec StkEl (ArithRes Mul n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Mul -> StkEl r -> StkEl r -> m (StkEl (ArithRes Mul r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, Typeable n, Typeable m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy Mul
forall k (t :: k). Proxy t
Proxy @Mul) StkEl r
l StkEl r
r
runInstrImpl _ EDIV (l :: StkEl r
l :& r :: StkEl r
r :& rest :: Rec StkEl rs
rest) = Rec StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : rs)
-> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : rs)
 -> m (Rec StkEl out))
-> Rec
     StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : rs)
-> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
-> StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Value' Instr r
-> Value' Instr r
-> Value' Instr ('TOption ('TPair (EDivOpRes r r) (EModOpRes r r)))
forall (n :: T) (m :: T) (instr :: [T] -> [T] -> *).
EDivOp n m =>
Value' instr n
-> Value' instr m
-> Value' instr ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
evalEDivOp (StkEl r -> Value' Instr r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
l) (StkEl r -> Value' Instr r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
r)) StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
-> Rec StkEl rs
-> Rec
     StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl _ ABS ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& rest :: Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Abs n : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Abs n : rs) -> m (Rec StkEl out))
-> Rec StkEl (UnaryArithRes Abs n : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Abs n) -> StkEl (UnaryArithRes Abs n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Abs -> Value r -> Value' Instr (UnaryArithRes Abs r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Abs
forall k (t :: k). Proxy t
Proxy @Abs) Value r
a) StkEl (UnaryArithRes Abs n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Abs n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl _ NEG ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& rest :: Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Neg n : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Neg n : rs) -> m (Rec StkEl out))
-> Rec StkEl (UnaryArithRes Neg n : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Neg n) -> StkEl (UnaryArithRes Neg n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Neg -> Value r -> Value' Instr (UnaryArithRes Neg r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Neg
forall k (t :: k). Proxy t
Proxy @Neg) Value r
a) StkEl (UnaryArithRes Neg n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Neg n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl _ LSL (x :: StkEl r
x :& s :: StkEl r
s :& rest :: Rec StkEl rs
rest) = (StkEl (ArithRes Lsl n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes Lsl n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes Lsl n m) -> Rec StkEl (ArithRes Lsl n m : rs))
-> m (StkEl (ArithRes Lsl n m))
-> m (Rec StkEl (ArithRes Lsl n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Lsl -> StkEl r -> StkEl r -> m (StkEl (ArithRes Lsl r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, Typeable n, Typeable m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy Lsl
forall k (t :: k). Proxy t
Proxy @Lsl) StkEl r
x StkEl r
s
runInstrImpl _ LSR (x :: StkEl r
x :& s :: StkEl r
s :& rest :: Rec StkEl rs
rest) = (StkEl (ArithRes Lsr n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes Lsr n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes Lsr n m) -> Rec StkEl (ArithRes Lsr n m : rs))
-> m (StkEl (ArithRes Lsr n m))
-> m (Rec StkEl (ArithRes Lsr n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Lsr -> StkEl r -> StkEl r -> m (StkEl (ArithRes Lsr r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, Typeable n, Typeable m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy Lsr
forall k (t :: k). Proxy t
Proxy @Lsr) StkEl r
x StkEl r
s
runInstrImpl _ OR (l :: StkEl r
l :& r :: StkEl r
r :& rest :: Rec StkEl rs
rest) = (StkEl (ArithRes Or n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes Or n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes Or n m) -> Rec StkEl (ArithRes Or n m : rs))
-> m (StkEl (ArithRes Or n m))
-> m (Rec StkEl (ArithRes Or n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Or -> StkEl r -> StkEl r -> m (StkEl (ArithRes Or r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, Typeable n, Typeable m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy Or
forall k (t :: k). Proxy t
Proxy @Or) StkEl r
l StkEl r
r
runInstrImpl _ AND (l :: StkEl r
l :& r :: StkEl r
r :& rest :: Rec StkEl rs
rest) = (StkEl (ArithRes And n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes And n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes And n m) -> Rec StkEl (ArithRes And n m : rs))
-> m (StkEl (ArithRes And n m))
-> m (Rec StkEl (ArithRes And n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy And -> StkEl r -> StkEl r -> m (StkEl (ArithRes And r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, Typeable n, Typeable m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy And
forall k (t :: k). Proxy t
Proxy @And) StkEl r
l StkEl r
r
runInstrImpl _ XOR (l :: StkEl r
l :& r :: StkEl r
r :& rest :: Rec StkEl rs
rest) = (StkEl (ArithRes Xor n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes Xor n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes Xor n m) -> Rec StkEl (ArithRes Xor n m : rs))
-> m (StkEl (ArithRes Xor n m))
-> m (Rec StkEl (ArithRes Xor n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Xor -> StkEl r -> StkEl r -> m (StkEl (ArithRes Xor r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, Typeable n, Typeable m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy Xor
forall k (t :: k). Proxy t
Proxy @Xor) StkEl r
l StkEl r
r
runInstrImpl _ NOT ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& rest :: Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Not n : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Not n : rs) -> m (Rec StkEl out))
-> Rec StkEl (UnaryArithRes Not n : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Not n) -> StkEl (UnaryArithRes Not n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Not -> Value r -> Value' Instr (UnaryArithRes Not r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Not
forall k (t :: k). Proxy t
Proxy @Not) Value r
a) StkEl (UnaryArithRes Not n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Not n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl _ COMPARE ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
l) :& (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
r) :& rest :: Rec StkEl rs
rest) =
  Rec StkEl ('TInt : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TInt : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TInt : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TInt -> StkEl 'TInt
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Integer -> Value 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
T.VInt (Value r -> Value r -> Integer
forall (t :: T) (i :: [T] -> [T] -> *).
(Comparable t, SingI t) =>
Value' i t -> Value' i t -> Integer
compareOp Value r
l Value r
Value r
r)) StkEl 'TInt -> Rec StkEl rs -> Rec StkEl ('TInt : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl _ EQ ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& rest :: Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Eq' n : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Eq' n : rs) -> m (Rec StkEl out))
-> Rec StkEl (UnaryArithRes Eq' n : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Eq' n) -> StkEl (UnaryArithRes Eq' n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Eq' -> Value r -> Value' Instr (UnaryArithRes Eq' r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Eq'
forall k (t :: k). Proxy t
Proxy @Eq') Value r
a) StkEl (UnaryArithRes Eq' n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Eq' n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl _ NEQ ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& rest :: Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Neq n : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Neq n : rs) -> m (Rec StkEl out))
-> Rec StkEl (UnaryArithRes Neq n : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Neq n) -> StkEl (UnaryArithRes Neq n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Neq -> Value r -> Value' Instr (UnaryArithRes Neq r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Neq
forall k (t :: k). Proxy t
Proxy @Neq) Value r
a) StkEl (UnaryArithRes Neq n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Neq n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl _ LT ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& rest :: Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Lt n : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Lt n : rs) -> m (Rec StkEl out))
-> Rec StkEl (UnaryArithRes Lt n : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Lt n) -> StkEl (UnaryArithRes Lt n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Lt -> Value r -> Value' Instr (UnaryArithRes Lt r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Lt
forall k (t :: k). Proxy t
Proxy @Lt) Value r
a) StkEl (UnaryArithRes Lt n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Lt n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl _ GT ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& rest :: Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Gt n : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Gt n : rs) -> m (Rec StkEl out))
-> Rec StkEl (UnaryArithRes Gt n : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Gt n) -> StkEl (UnaryArithRes Gt n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Gt -> Value r -> Value' Instr (UnaryArithRes Gt r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Gt
forall k (t :: k). Proxy t
Proxy @Gt) Value r
a) StkEl (UnaryArithRes Gt n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Gt n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl _ LE ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& rest :: Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Le n : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Le n : rs) -> m (Rec StkEl out))
-> Rec StkEl (UnaryArithRes Le n : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Le n) -> StkEl (UnaryArithRes Le n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Le -> Value r -> Value' Instr (UnaryArithRes Le r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Le
forall k (t :: k). Proxy t
Proxy @Le) Value r
a) StkEl (UnaryArithRes Le n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Le n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl _ GE ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& rest :: Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Ge n : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Ge n : rs) -> m (Rec StkEl out))
-> Rec StkEl (UnaryArithRes Ge n : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Ge n) -> StkEl (UnaryArithRes Ge n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Ge -> Value r -> Value' Instr (UnaryArithRes Ge r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Ge
forall k (t :: k). Proxy t
Proxy @Ge) Value r
a) StkEl (UnaryArithRes Ge n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Ge n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl _ INT (StkEl (VNat n :: Natural
n) _ _ :& r :: Rec StkEl rs
r) = Rec StkEl ('TInt : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TInt : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TInt : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TInt -> StkEl 'TInt
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Integer -> Value 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer -> Value 'TInt) -> Integer -> Value 'TInt
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n) StkEl 'TInt -> Rec StkEl rs -> Rec StkEl ('TInt : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ (SELF sepc :: SomeEntrypointCallT arg
sepc :: Instr inp out) r :: Rec StkEl inp
r = do
  ContractEnv{..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  case Proxy out
forall k (t :: k). Proxy t
Proxy @out of
    (_ :: Proxy ('TContract cp ': s)) -> do
      Rec StkEl ('TContract arg : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TContract arg : inp) -> m (Rec StkEl out))
-> Rec StkEl ('TContract arg : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TContract arg) -> StkEl ('TContract arg)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Address -> SomeEntrypointCallT arg -> Value ('TContract arg)
forall (arg :: T) (instr :: [T] -> [T] -> *).
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract Address
ceSelf SomeEntrypointCallT arg
sepc) StkEl ('TContract arg)
-> Rec StkEl inp -> Rec StkEl ('TContract arg : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl _ (CONTRACT (Notes p
nt :: T.Notes a) instrEpName :: EpName
instrEpName) (StkEl (VAddress epAddr :: EpAddress
epAddr) _ _ :& r :: Rec StkEl rs
r) = do
  ContractEnv{..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  let T.EpAddress addr :: Address
addr addrEpName :: EpName
addrEpName = EpAddress
epAddr
  let mepName :: Maybe EpName
mepName =
        case (EpName
instrEpName, EpName
addrEpName) of
          (DefEpName, DefEpName) -> EpName -> Maybe EpName
forall a. a -> Maybe a
Just EpName
DefEpName
          (DefEpName, en :: EpName
en) -> EpName -> Maybe EpName
forall a. a -> Maybe a
Just EpName
en
          (en :: EpName
en, DefEpName) -> EpName -> Maybe EpName
forall a. a -> Maybe a
Just EpName
en
          _ -> Maybe EpName
forall a. Maybe a
Nothing

  let withNotes :: Value ('TOption ('TContract p))
-> Rec StkEl ('TOption ('TContract p) : rs)
withNotes v :: Value ('TOption ('TContract p))
v = Value ('TOption ('TContract p))
-> VarAnn
-> Notes ('TOption ('TContract p))
-> StkEl ('TOption ('TContract p))
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value ('TOption ('TContract p))
v VarAnn
forall k (a :: k). Annotation a
U.noAnn (TypeAnn -> Notes ('TContract p) -> Notes ('TOption ('TContract p))
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
forall k (a :: k). Annotation a
U.noAnn (Notes ('TContract p) -> Notes ('TOption ('TContract p)))
-> Notes ('TContract p) -> Notes ('TOption ('TContract p))
forall a b. (a -> b) -> a -> b
$ TypeAnn -> Notes p -> Notes ('TContract p)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TContract t)
NTContract TypeAnn
forall k (a :: k). Annotation a
U.noAnn Notes p
nt) StkEl ('TOption ('TContract p))
-> Rec StkEl rs -> Rec StkEl ('TOption ('TContract p) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
  Rec StkEl ('TOption ('TContract p) : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption ('TContract p) : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TOption ('TContract p) : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value ('TOption ('TContract p))
-> Rec StkEl ('TOption ('TContract p) : rs)
withNotes (Value ('TOption ('TContract p))
 -> Rec StkEl ('TOption ('TContract p) : rs))
-> Value ('TOption ('TContract p))
-> Rec StkEl ('TOption ('TContract p) : rs)
forall a b. (a -> b) -> a -> b
$ case Maybe EpName
mepName of
    Nothing -> Maybe (Value' Instr ('TContract p))
-> Value ('TOption ('TContract p))
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption Maybe (Value' Instr ('TContract p))
forall a. Maybe a
Nothing
    Just epName :: EpName
epName ->
      case Address
addr of
        KeyAddress _ -> Address
-> EpName -> ParamNotes 'TUnit -> Value ('TOption ('TContract p))
forall (p :: T).
ParameterScope p =>
Address
-> EpName -> ParamNotes p -> Value ('TOption ('TContract p))
castContract Address
addr EpName
epName ParamNotes 'TUnit
T.tyImplicitAccountParam
        ContractAddress ca :: ContractHash
ca ->
          case ContractHash -> TcOriginatedContracts -> Maybe SomeParamType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ContractHash
ca TcOriginatedContracts
ceContracts of
            Just (SomeParamType _ paramNotes :: ParamNotes t
paramNotes) -> Address
-> EpName -> ParamNotes t -> Value ('TOption ('TContract p))
forall (p :: T).
ParameterScope p =>
Address
-> EpName -> ParamNotes p -> Value ('TOption ('TContract p))
castContract Address
addr EpName
epName ParamNotes t
paramNotes
            Nothing -> Maybe (Value' Instr ('TContract p))
-> Value ('TOption ('TContract p))
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption Maybe (Value' Instr ('TContract p))
forall a. Maybe a
Nothing
  where
  castContract
    :: forall p. T.ParameterScope p
    => Address -> EpName -> T.ParamNotes p -> T.Value ('TOption ('TContract a))
  castContract :: Address
-> EpName -> ParamNotes p -> Value ('TOption ('TContract p))
castContract addr :: Address
addr epName :: EpName
epName param :: ParamNotes p
param = Maybe (Value' Instr ('TContract p))
-> Value ('TOption ('TContract p))
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' Instr ('TContract p))
 -> Value ('TOption ('TContract p)))
-> Maybe (Value' Instr ('TContract p))
-> Value ('TOption ('TContract p))
forall a b. (a -> b) -> a -> b
$ do
    -- As we are within Maybe monad, pattern-match failure results in Nothing
    MkEntrypointCallRes na :: Notes arg
na epc :: EntrypointCallT p arg
epc <- EpName -> ParamNotes p -> Maybe (MkEntrypointCallRes p)
forall (param :: T).
ParameterScope param =>
EpName -> ParamNotes param -> Maybe (MkEntrypointCallRes param)
T.mkEntrypointCall EpName
epName ParamNotes p
param
    Right (Refl, _) <- Either TCTypeError (p :~: arg, Notes p)
-> Maybe (Either TCTypeError (p :~: arg, Notes p))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either TCTypeError (p :~: arg, Notes p)
 -> Maybe (Either TCTypeError (p :~: arg, Notes p)))
-> Either TCTypeError (p :~: arg, Notes p)
-> Maybe (Either TCTypeError (p :~: arg, Notes p))
forall a b. (a -> b) -> a -> b
$ Notes p -> Notes arg -> Either TCTypeError (p :~: arg, Notes p)
forall (t1 :: T) (t2 :: T).
Each '[KnownT] '[t1, t2] =>
Notes t1 -> Notes t2 -> Either TCTypeError (t1 :~: t2, Notes t1)
matchTypes Notes p
nt Notes arg
na
    Value' Instr ('TContract arg)
-> Maybe (Value' Instr ('TContract p))
forall (m :: * -> *) a. Monad m => a -> m a
return (Value' Instr ('TContract arg)
 -> Maybe (Value' Instr ('TContract p)))
-> Value' Instr ('TContract arg)
-> Maybe (Value' Instr ('TContract p))
forall a b. (a -> b) -> a -> b
$ Address -> SomeEntrypointCallT arg -> Value' Instr ('TContract arg)
forall (arg :: T) (instr :: [T] -> [T] -> *).
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract Address
addr (EntrypointCallT p arg -> SomeEntrypointCallT arg
forall (arg :: T) (param :: T).
ParameterScope param =>
EntrypointCallT param arg -> SomeEntrypointCallT arg
T.SomeEpc EntrypointCallT p arg
epc)

runInstrImpl _ TRANSFER_TOKENS
  (StkEl p :: Value r
p _ _ :& StkEl (VMutez mutez :: Mutez
mutez) _ _ :& StkEl contract :: Value r
contract _ _ :& r :: Rec StkEl rs
r) =
  Rec StkEl ('TOperation : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOperation : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TOperation : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TOperation -> StkEl 'TOperation
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Operation -> Value 'TOperation
forall (instr :: [T] -> [T] -> *).
Operation' instr -> Value' instr 'TOperation
VOp (TransferTokens Instr r -> Operation
forall (p :: T) (instr :: [T] -> [T] -> *).
ParameterScope p =>
TransferTokens instr p -> Operation' instr
OpTransferTokens (TransferTokens Instr r -> Operation)
-> TransferTokens Instr r -> Operation
forall a b. (a -> b) -> a -> b
$ Value r
-> Mutez -> Value' Instr ('TContract r) -> TransferTokens Instr r
forall (instr :: [T] -> [T] -> *) (p :: T).
Value' instr p
-> Mutez -> Value' instr ('TContract p) -> TransferTokens instr p
TransferTokens Value r
p Mutez
mutez Value r
Value' Instr ('TContract r)
contract)) StkEl 'TOperation -> Rec StkEl rs -> Rec StkEl ('TOperation : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ SET_DELEGATE (StkEl (VOption mbKeyHash :: Maybe (Value' Instr t)
mbKeyHash) _ _ :& r :: Rec StkEl rs
r) =
  case Maybe (Value' Instr t)
mbKeyHash of
    Just (VKeyHash k :: KeyHash
k) -> Rec StkEl ('TOperation : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOperation : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TOperation : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TOperation -> StkEl 'TOperation
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Operation -> Value 'TOperation
forall (instr :: [T] -> [T] -> *).
Operation' instr -> Value' instr 'TOperation
VOp (SetDelegate -> Operation
forall (instr :: [T] -> [T] -> *). SetDelegate -> Operation' instr
OpSetDelegate (SetDelegate -> Operation) -> SetDelegate -> Operation
forall a b. (a -> b) -> a -> b
$ Maybe KeyHash -> SetDelegate
SetDelegate (Maybe KeyHash -> SetDelegate) -> Maybe KeyHash -> SetDelegate
forall a b. (a -> b) -> a -> b
$ KeyHash -> Maybe KeyHash
forall a. a -> Maybe a
Just KeyHash
k)) StkEl 'TOperation -> Rec StkEl rs -> Rec StkEl ('TOperation : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
    Nothing -> Rec StkEl ('TOperation : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOperation : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TOperation : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TOperation -> StkEl 'TOperation
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Operation -> Value 'TOperation
forall (instr :: [T] -> [T] -> *).
Operation' instr -> Value' instr 'TOperation
VOp (SetDelegate -> Operation
forall (instr :: [T] -> [T] -> *). SetDelegate -> Operation' instr
OpSetDelegate (SetDelegate -> Operation) -> SetDelegate -> Operation
forall a b. (a -> b) -> a -> b
$ Maybe KeyHash -> SetDelegate
SetDelegate (Maybe KeyHash -> SetDelegate) -> Maybe KeyHash -> SetDelegate
forall a b. (a -> b) -> a -> b
$ Maybe KeyHash
forall a. Maybe a
Nothing)) StkEl 'TOperation -> Rec StkEl rs -> Rec StkEl ('TOperation : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ (CREATE_CONTRACT contract :: Contract p g
contract)
  (StkEl (VOption mbKeyHash :: Maybe (Value' Instr t)
mbKeyHash) _ _ :& StkEl (VMutez m :: Mutez
m) _ _ :& StkEl g :: Value r
g _ _ :& r :: Rec StkEl rs
r) = do
  Address
originator <- ContractEnv -> Address
ceSelf (ContractEnv -> Address) -> m ContractEnv -> m Address
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask

  OriginationIndex
originationNonce <- InterpreterState -> OriginationIndex
isOriginationNonce (InterpreterState -> OriginationIndex)
-> m InterpreterState -> m OriginationIndex
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m InterpreterState
forall (m :: * -> *). InterpreterStateMonad m => m InterpreterState
getInterpreterState
  GlobalCounter
globalCounter <- (ContractEnv -> GlobalCounter) -> m GlobalCounter
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ContractEnv -> GlobalCounter
ceGlobalCounter
  Maybe OperationHash
opHash <- ContractEnv -> Maybe OperationHash
ceOperationHash (ContractEnv -> Maybe OperationHash)
-> m ContractEnv -> m (Maybe OperationHash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  (InterpreterState -> InterpreterState) -> m ()
forall (m :: * -> *).
InterpreterStateMonad m =>
(InterpreterState -> InterpreterState) -> m ()
modifyInterpreterState ((InterpreterState -> InterpreterState) -> m ())
-> (InterpreterState -> InterpreterState) -> m ()
forall a b. (a -> b) -> a -> b
$ \iState :: InterpreterState
iState ->
    InterpreterState
iState { isOriginationNonce :: OriginationIndex
isOriginationNonce = Int32 -> OriginationIndex
OriginationIndex (Int32 -> OriginationIndex) -> Int32 -> OriginationIndex
forall a b. (a -> b) -> a -> b
$ (OriginationIndex -> Int32
unOriginationIndex (OriginationIndex -> Int32) -> OriginationIndex -> Int32
forall a b. (a -> b) -> a -> b
$ InterpreterState -> OriginationIndex
isOriginationNonce InterpreterState
iState) Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+ 1 }
  let ops :: ContractCode p g
ops = Contract p g -> ContractCode p g
forall (cp :: T) (st :: T). Contract cp st -> ContractCode cp st
cCode Contract p g
contract
  let resAddr :: Address
resAddr =
        case Maybe OperationHash
opHash of
          Just hash :: OperationHash
hash -> OperationHash -> OriginationIndex -> GlobalCounter -> Address
mkContractAddress OperationHash
hash OriginationIndex
originationNonce GlobalCounter
globalCounter
          Nothing ->
            OperationHash -> OriginationIndex -> GlobalCounter -> Address
mkContractAddress
              (OriginationOperation -> OperationHash
mkOriginationOperationHash (Address
-> Maybe (Value 'TKeyHash)
-> Mutez
-> Contract p g
-> Value' Instr g
-> OriginationOperation
forall (param :: T) (store :: T).
(ParameterScope param, StorageScope store) =>
Address
-> Maybe (Value 'TKeyHash)
-> Mutez
-> Contract param store
-> Value' Instr store
-> OriginationOperation
createOrigOp Address
originator Maybe (Value' Instr t)
Maybe (Value 'TKeyHash)
mbKeyHash Mutez
m Contract p g
contract Value' Instr g
Value r
g))
              -- If opHash is Nothing it means that interpreter is running in some kind of test
              -- context, therefore we generate dummy contract address with its own origination
              -- operation.
              OriginationIndex
originationNonce
              GlobalCounter
globalCounter
  let resEpAddr :: EpAddress
resEpAddr = Address -> EpName -> EpAddress
EpAddress Address
resAddr EpName
DefEpName
  let resOp :: CreateContract Instr p r
resOp = Address
-> Maybe KeyHash
-> Mutez
-> Value r
-> Instr (ContractInp p r) (ContractOut r)
-> CreateContract Instr p r
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
(Show (instr (ContractInp cp st) (ContractOut st)),
 Eq (instr (ContractInp cp st) (ContractOut st))) =>
Address
-> Maybe KeyHash
-> Mutez
-> Value' instr st
-> instr (ContractInp cp st) (ContractOut st)
-> CreateContract instr cp st
CreateContract Address
originator (Maybe (Value 'TKeyHash) -> Maybe KeyHash
unwrapMbKeyHash Maybe (Value' Instr t)
Maybe (Value 'TKeyHash)
mbKeyHash) Mutez
m Value r
g ContractCode p g
Instr (ContractInp p r) (ContractOut r)
ops
  Rec StkEl ('TOperation : 'TAddress : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOperation : 'TAddress : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TOperation : 'TAddress : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TOperation -> StkEl 'TOperation
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Operation -> Value 'TOperation
forall (instr :: [T] -> [T] -> *).
Operation' instr -> Value' instr 'TOperation
VOp (CreateContract Instr p r -> Operation
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
(Show (instr (ContractInp cp st) (ContractOut st)),
 NFData (instr (ContractInp cp st) (ContractOut st)),
 Typeable instr, ParameterScope cp, StorageScope st) =>
CreateContract instr cp st -> Operation' instr
OpCreateContract CreateContract Instr p r
resOp))
      StkEl 'TOperation
-> Rec StkEl ('TAddress : rs)
-> Rec StkEl ('TOperation : 'TAddress : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Value 'TAddress -> StkEl 'TAddress
forall (x :: T). Value x -> StkEl x
starNotesStkEl (EpAddress -> Value 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress EpAddress
resEpAddr)
      StkEl 'TAddress -> Rec StkEl rs -> Rec StkEl ('TAddress : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ IMPLICIT_ACCOUNT (StkEl (VKeyHash k :: KeyHash
k) _ _ :& r :: Rec StkEl rs
r) =
  Rec StkEl ('TContract 'TUnit : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TContract 'TUnit : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TContract 'TUnit : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ (Value ('TContract 'TUnit) -> StkEl ('TContract 'TUnit)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Address -> SomeEntrypointCallT 'TUnit -> Value ('TContract 'TUnit)
forall (arg :: T) (instr :: [T] -> [T] -> *).
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract (KeyHash -> Address
KeyAddress KeyHash
k) SomeEntrypointCallT 'TUnit
forall (t :: T).
(ParameterScope t, ForbidOr t) =>
SomeEntrypointCallT t
sepcPrimitive)) StkEl ('TContract 'TUnit)
-> Rec StkEl rs -> Rec StkEl ('TContract 'TUnit : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ NOW r :: Rec StkEl inp
r = do
  ContractEnv{..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TTimestamp : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TTimestamp : inp) -> m (Rec StkEl out))
-> Rec StkEl ('TTimestamp : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TTimestamp -> StkEl 'TTimestamp
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Timestamp -> Value 'TTimestamp
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp Timestamp
ceNow) StkEl 'TTimestamp -> Rec StkEl inp -> Rec StkEl ('TTimestamp : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl _ AMOUNT r :: Rec StkEl inp
r = do
  ContractEnv{..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TMutez : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TMutez : inp) -> m (Rec StkEl out))
-> Rec StkEl ('TMutez : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TMutez -> StkEl 'TMutez
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Mutez -> Value 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez Mutez
ceAmount) StkEl 'TMutez -> Rec StkEl inp -> Rec StkEl ('TMutez : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl _ BALANCE r :: Rec StkEl inp
r = do
  ContractEnv{..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TMutez : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TMutez : inp) -> m (Rec StkEl out))
-> Rec StkEl ('TMutez : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TMutez -> StkEl 'TMutez
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Mutez -> Value 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez Mutez
ceBalance) StkEl 'TMutez -> Rec StkEl inp -> Rec StkEl ('TMutez : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl _ CHECK_SIGNATURE
  (StkEl (VKey k :: PublicKey
k) _ _ :& StkEl (VSignature v :: Signature
v) _ _ :& StkEl (VBytes b :: ByteString
b) _ _ :& r :: Rec StkEl rs
r) =
  Rec StkEl ('TBool : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBool : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TBool : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TBool -> StkEl 'TBool
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Bool -> Value 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Bool -> Value 'TBool) -> Bool -> Value 'TBool
forall a b. (a -> b) -> a -> b
$ PublicKey -> Signature -> ByteString -> Bool
checkSignature PublicKey
k Signature
v ByteString
b) StkEl 'TBool -> Rec StkEl rs -> Rec StkEl ('TBool : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ SHA256 (StkEl (VBytes b :: ByteString
b) _ _ :& r :: Rec StkEl rs
r) =
  Rec StkEl ('TBytes : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBytes : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TBytes : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TBytes -> StkEl 'TBytes
forall (x :: T). Value x -> StkEl x
starNotesStkEl (ByteString -> Value 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value 'TBytes) -> ByteString -> Value 'TBytes
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
sha256 ByteString
b) StkEl 'TBytes -> Rec StkEl rs -> Rec StkEl ('TBytes : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ SHA512 (StkEl (VBytes b :: ByteString
b) _ _ :& r :: Rec StkEl rs
r) =
  Rec StkEl ('TBytes : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBytes : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TBytes : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TBytes -> StkEl 'TBytes
forall (x :: T). Value x -> StkEl x
starNotesStkEl (ByteString -> Value 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value 'TBytes) -> ByteString -> Value 'TBytes
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
sha512 ByteString
b) StkEl 'TBytes -> Rec StkEl rs -> Rec StkEl ('TBytes : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ BLAKE2B (StkEl (VBytes b :: ByteString
b) _ _ :& r :: Rec StkEl rs
r) =
  Rec StkEl ('TBytes : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBytes : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TBytes : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TBytes -> StkEl 'TBytes
forall (x :: T). Value x -> StkEl x
starNotesStkEl (ByteString -> Value 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value 'TBytes) -> ByteString -> Value 'TBytes
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
blake2b ByteString
b) StkEl 'TBytes -> Rec StkEl rs -> Rec StkEl ('TBytes : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ HASH_KEY (StkEl (VKey k :: PublicKey
k) _ _ :& r :: Rec StkEl rs
r) =
  Rec StkEl ('TKeyHash : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TKeyHash : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TKeyHash : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TKeyHash -> StkEl 'TKeyHash
forall (x :: T). Value x -> StkEl x
starNotesStkEl (KeyHash -> Value 'TKeyHash
forall (instr :: [T] -> [T] -> *).
KeyHash -> Value' instr 'TKeyHash
VKeyHash (KeyHash -> Value 'TKeyHash) -> KeyHash -> Value 'TKeyHash
forall a b. (a -> b) -> a -> b
$ PublicKey -> KeyHash
hashKey PublicKey
k) StkEl 'TKeyHash -> Rec StkEl rs -> Rec StkEl ('TKeyHash : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ SOURCE r :: Rec StkEl inp
r = do
  ContractEnv{..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TAddress : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TAddress : inp) -> m (Rec StkEl out))
-> Rec StkEl ('TAddress : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TAddress -> StkEl 'TAddress
forall (x :: T). Value x -> StkEl x
starNotesStkEl (EpAddress -> Value 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (EpAddress -> Value 'TAddress) -> EpAddress -> Value 'TAddress
forall a b. (a -> b) -> a -> b
$ Address -> EpName -> EpAddress
EpAddress Address
ceSource EpName
DefEpName) StkEl 'TAddress -> Rec StkEl inp -> Rec StkEl ('TAddress : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl _ SENDER r :: Rec StkEl inp
r = do
  ContractEnv{..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TAddress : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TAddress : inp) -> m (Rec StkEl out))
-> Rec StkEl ('TAddress : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TAddress -> StkEl 'TAddress
forall (x :: T). Value x -> StkEl x
starNotesStkEl (EpAddress -> Value 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (EpAddress -> Value 'TAddress) -> EpAddress -> Value 'TAddress
forall a b. (a -> b) -> a -> b
$ Address -> EpName -> EpAddress
EpAddress Address
ceSender EpName
DefEpName) StkEl 'TAddress -> Rec StkEl inp -> Rec StkEl ('TAddress : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl _ ADDRESS (StkEl (VContract a :: Address
a sepc :: SomeEntrypointCallT arg
sepc) _ _ :& r :: Rec StkEl rs
r) =
  Rec StkEl ('TAddress : rs) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TAddress : rs) -> m (Rec StkEl out))
-> Rec StkEl ('TAddress : rs) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TAddress -> StkEl 'TAddress
forall (x :: T). Value x -> StkEl x
starNotesStkEl (EpAddress -> Value 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (EpAddress -> Value 'TAddress) -> EpAddress -> Value 'TAddress
forall a b. (a -> b) -> a -> b
$ Address -> EpName -> EpAddress
EpAddress Address
a (SomeEntrypointCallT arg -> EpName
forall (arg :: T). SomeEntrypointCallT arg -> EpName
sepcName SomeEntrypointCallT arg
sepc)) StkEl 'TAddress -> Rec StkEl rs -> Rec StkEl ('TAddress : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl _ CHAIN_ID r :: Rec StkEl inp
r = do
  ContractEnv{..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TChainId : inp) -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TChainId : inp) -> m (Rec StkEl out))
-> Rec StkEl ('TChainId : inp) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value 'TChainId -> StkEl 'TChainId
forall (x :: T). Value x -> StkEl x
starNotesStkEl (ChainId -> Value 'TChainId
forall (instr :: [T] -> [T] -> *).
ChainId -> Value' instr 'TChainId
VChainId ChainId
ceChainId) StkEl 'TChainId -> Rec StkEl inp -> Rec StkEl ('TChainId : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r

-- | Evaluates an arithmetic operation and either fails or proceeds.
runArithOp
  :: (ArithOp aop n m, Typeable n, Typeable m, EvalM monad)
  => proxy aop
  -> StkEl n
  -> StkEl m
  -> monad (StkEl (ArithRes aop n m))
runArithOp :: proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp op :: proxy aop
op l :: StkEl n
l r :: StkEl m
r = case proxy aop
-> Value' Instr n
-> Value' Instr m
-> Either
     (ArithError (Value' Instr n) (Value' Instr m))
     (Value' Instr (ArithRes aop n m))
forall k (aop :: k) (n :: T) (m :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
ArithOp aop n m =>
proxy aop
-> Value' instr n
-> Value' instr m
-> Either
     (ArithError (Value' instr n) (Value' instr m))
     (Value' instr (ArithRes aop n m))
evalOp proxy aop
op (StkEl n -> Value' Instr n
forall (x :: T). StkEl x -> Value x
seValue StkEl n
l) (StkEl m -> Value' Instr m
forall (x :: T). StkEl x -> Value x
seValue StkEl m
r) of
  Left  err :: ArithError (Value' Instr n) (Value' Instr m)
err -> MichelsonFailed -> monad (StkEl (ArithRes aop n m))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (ArithError (Value' Instr n) (Value' Instr m) -> MichelsonFailed
forall (n :: T) (m :: T) (instr :: [T] -> [T] -> *).
(Typeable n, Typeable m, Typeable instr) =>
ArithError (Value' instr n) (Value' instr m) -> MichelsonFailed
MichelsonArithError ArithError (Value' Instr n) (Value' Instr m)
err)
  Right res :: Value' Instr (ArithRes aop n m)
res -> StkEl (ArithRes aop n m) -> monad (StkEl (ArithRes aop n m))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StkEl (ArithRes aop n m) -> monad (StkEl (ArithRes aop n m)))
-> StkEl (ArithRes aop n m) -> monad (StkEl (ArithRes aop n m))
forall a b. (a -> b) -> a -> b
$ Value' Instr (ArithRes aop n m) -> StkEl (ArithRes aop n m)
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr (ArithRes aop n m)
res

-- | Unpacks given raw data into a typed value.
runUnpack
  :: forall t. (UnpackedValScope t)
  => ByteString
  -> Either UnpackError (T.Value t)
runUnpack :: ByteString -> Either UnpackError (Value t)
runUnpack bs :: ByteString
bs =
  -- TODO [TM-80] Gas consumption here should depend on unpacked data size
  -- and size of resulting expression, errors would also spend some (all equally).
  -- Fortunatelly, the inner decoding logic does not need to know anything about gas use.
  ByteString -> Either UnpackError (Value t)
forall (t :: T).
UnpackedValScope t =>
ByteString -> Either UnpackError (Value t)
unpackValue' ByteString
bs

createOrigOp
  :: (ParameterScope param, StorageScope store)
  => Address
  -> Maybe (T.Value 'T.TKeyHash)
  -> Mutez
  -> Contract param store
  -> Value' Instr store
  -> OriginationOperation
createOrigOp :: Address
-> Maybe (Value 'TKeyHash)
-> Mutez
-> Contract param store
-> Value' Instr store
-> OriginationOperation
createOrigOp originator :: Address
originator mbDelegate :: Maybe (Value 'TKeyHash)
mbDelegate bal :: Mutez
bal contract :: Contract param store
contract storage :: Value' Instr store
storage =
  $WOriginationOperation :: forall (cp :: T) (st :: T).
(StorageScope st, ParameterScope cp) =>
Address
-> Maybe KeyHash
-> Mutez
-> Value st
-> Contract cp st
-> OriginationOperation
OriginationOperation
    { ooOriginator :: Address
ooOriginator = Address
originator
    , ooDelegate :: Maybe KeyHash
ooDelegate = Maybe (Value 'TKeyHash) -> Maybe KeyHash
unwrapMbKeyHash Maybe (Value 'TKeyHash)
mbDelegate
    , ooBalance :: Mutez
ooBalance = Mutez
bal
    , ooStorage :: Value' Instr store
ooStorage = Value' Instr store
storage
    , ooContract :: Contract param store
ooContract = Contract param store
contract
    }

unwrapMbKeyHash :: Maybe (T.Value 'T.TKeyHash) -> Maybe KeyHash
unwrapMbKeyHash :: Maybe (Value 'TKeyHash) -> Maybe KeyHash
unwrapMbKeyHash mbKeyHash :: Maybe (Value 'TKeyHash)
mbKeyHash = Maybe (Value 'TKeyHash)
mbKeyHash Maybe (Value 'TKeyHash)
-> (Value 'TKeyHash -> KeyHash) -> Maybe KeyHash
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(VKeyHash keyHash :: KeyHash
keyHash) -> KeyHash
keyHash

interpretExt :: EvalM m => InstrRunner m -> SomeItStack -> m ()
interpretExt :: InstrRunner m -> SomeItStack -> m ()
interpretExt _ (SomeItStack (T.PRINT (T.PrintComment pc :: [Either Text (StackRef inp)]
pc)) st :: Rec StkEl inp
st) = do
  let getEl :: Either Text (StackRef inp) -> Text
getEl (Left l :: Text
l) = Text
l
      getEl (Right str :: StackRef inp
str) = StackRef inp
-> Rec StkEl inp -> (forall (t :: T). StkEl t -> Text) -> Text
forall (st :: [T]) a.
StackRef st -> Rec StkEl st -> (forall (t :: T). StkEl t -> a) -> a
withStackElem StackRef inp
str Rec StkEl inp
st (Value t -> Text
forall b a. (Show a, IsString b) => a -> b
show (Value t -> Text) -> (StkEl t -> Value t) -> StkEl t -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StkEl t -> Value t
forall (x :: T). StkEl x -> Value x
seValue)
      getMorleyLogs :: MorleyLogs -> [Text]
getMorleyLogs (MorleyLogs logs :: [Text]
logs) = [Text]
logs
  (InterpreterState -> InterpreterState) -> m ()
forall (m :: * -> *).
InterpreterStateMonad m =>
(InterpreterState -> InterpreterState) -> m ()
modifyInterpreterState (\s :: InterpreterState
s -> InterpreterState
s {isMorleyLogs :: MorleyLogs
isMorleyLogs = [Text] -> MorleyLogs
MorleyLogs ([Text] -> MorleyLogs) -> [Text] -> MorleyLogs
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat ((Either Text (StackRef inp) -> Text)
-> [Either Text (StackRef inp)] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map Either Text (StackRef inp) -> Text
getEl [Either Text (StackRef inp)]
pc) Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: MorleyLogs -> [Text]
getMorleyLogs (InterpreterState -> MorleyLogs
isMorleyLogs InterpreterState
s)})

interpretExt runner :: InstrRunner m
runner (SomeItStack (T.TEST_ASSERT (T.TestAssert nm :: Text
nm pc :: PrintComment inp
pc instr :: Instr inp ('TBool : out)
instr)) st :: Rec StkEl inp
st) = do
  Rec StkEl ('TBool : out)
ost <- InstrRunner m
-> Instr inp ('TBool : out)
-> Rec StkEl inp
-> m (Rec StkEl ('TBool : out))
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner Instr inp ('TBool : out)
instr Rec StkEl inp
st
  let ((StkEl r -> Value 'TBool
forall (x :: T). StkEl x -> Value x
seValue -> Value 'TBool -> Bool
forall a. IsoValue a => Value (ToT a) -> a
T.fromVal -> Bool
succeeded) :& _) = Rec StkEl ('TBool : out)
ost
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
succeeded (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    InstrRunner m -> SomeItStack -> m ()
forall (m :: * -> *).
EvalM m =>
InstrRunner m -> SomeItStack -> m ()
interpretExt InstrRunner m
runner (ExtInstr inp -> Rec StkEl inp -> SomeItStack
forall (inp :: [T]). ExtInstr inp -> Rec StkEl inp -> SomeItStack
SomeItStack (PrintComment inp -> ExtInstr inp
forall (s :: [T]). PrintComment s -> ExtInstr s
T.PRINT PrintComment inp
pc) Rec StkEl inp
st)
    MichelsonFailed -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (MichelsonFailed -> m ()) -> MichelsonFailed -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> MichelsonFailed
MichelsonFailedTestAssert (Text -> MichelsonFailed) -> Text -> MichelsonFailed
forall a b. (a -> b) -> a -> b
$ "TEST_ASSERT " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> " failed"

interpretExt _ (SomeItStack T.DOC_ITEM{} _) = m ()
forall (f :: * -> *). Applicative f => f ()
pass
interpretExt _ (SomeItStack T.COMMENT_ITEM{} _) = m ()
forall (f :: * -> *). Applicative f => f ()
pass

-- | Access given stack reference (in CPS style).
withStackElem
  :: forall st a.
     T.StackRef st
  -> Rec StkEl st
  -> (forall t. StkEl t -> a)
  -> a
withStackElem :: StackRef st -> Rec StkEl st -> (forall (t :: T). StkEl t -> a) -> a
withStackElem (T.StackRef sn :: Sing idx
sn) vals :: Rec StkEl st
vals cont :: forall (t :: T). StkEl t -> a
cont =
  (Rec StkEl st, Sing idx) -> a
forall (s :: [T]) (n :: Peano).
LongerThan s n =>
(Rec StkEl s, Sing n) -> a
loop (Rec StkEl st
vals, Sing idx
sn)
  where
    loop
      :: forall s (n :: Peano). (LongerThan s n)
      => (Rec StkEl s, Sing n) -> a
    loop :: (Rec StkEl s, Sing n) -> a
loop = \case
      (e :: StkEl r
e :& _, SZ) -> StkEl r -> a
forall (t :: T). StkEl t -> a
cont StkEl r
e
      (_ :& es :: Rec StkEl rs
es, SS n) -> (Rec StkEl rs, Sing n) -> a
forall (s :: [T]) (n :: Peano).
LongerThan s n =>
(Rec StkEl s, Sing n) -> a
loop (Rec StkEl rs
es, Sing n
SingNat n
n)

(deriveGADTNFData ''MichelsonFailed)
makeLensesFor [("isMorleyLogs", "isMorleyLogsL")] ''InterpreterState