-- 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 (..)
  , MichelsonFailed (..)
  , RemainingSteps (..)
  , SomeItStack (..)
  , MorleyLogs (..)
  , noMorleyLogs

  , interpret
  , interpretInstr
  , ContractReturn

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

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

import Prelude hiding (EQ, GT, LT)

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 Fmt (Buildable(build), Builder, genericF, pretty)

import Michelson.Interpret.Pack (packValue')
import Michelson.Interpret.Unpack (UnpackError, unpackValue')
import Michelson.TypeCheck
  (SomeContract(..), TCError, TcOriginatedContracts, matchTypes, runTypeCheck, typeCheckContract,
  typeCheckValue)
import Michelson.Typed
import qualified Michelson.Typed as T
import qualified Michelson.Untyped as U
import Tezos.Address (Address(..), 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.
  }

-- | 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
  MichelsonAmbigousEpRef :: EpName -> EpAddress -> 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
  MichelsonAmbigousEpRef ep1 :: EpName
ep1 epAddr1 :: EpAddress
epAddr1 == MichelsonAmbigousEpRef ep2 :: EpName
ep2 epAddr2 :: EpAddress
epAddr2 =
    EpName
ep1 EpName -> EpName -> Bool
forall a. Eq a => a -> a -> Bool
== EpName
ep2 Bool -> Bool -> Bool
&& EpAddress
epAddr1 EpAddress -> EpAddress -> Bool
forall a. Eq a => a -> a -> Bool
== EpAddress
epAddr2
  MichelsonAmbigousEpRef _ _ == _ = 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
      MichelsonAmbigousEpRef instrEp :: EpName
instrEp epAddr :: EpAddress
epAddr ->
        "Ambigous entrypoint reference. `CONTRACT %" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> EpName -> Builder
forall p. Buildable p => p -> Builder
build EpName
instrEp Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> "` \
        \called over address " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> EpAddress -> Builder
forall p. Buildable p => p -> Builder
build EpAddress
epAddr
    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)

data InterpretError
  = RuntimeFailure (MichelsonFailed, MorleyLogs)
  | IllTypedContract TCError
  | IllTypedParam TCError
  | IllTypedStorage TCError
  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 -> Builder
forall a. (Generic a, GBuildable (Rep a)) => a -> Builder
genericF

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.
newtype MorleyLogs = MorleyLogs
  { MorleyLogs -> [Text]
unMorleyLogs :: [Text]
    -- ^ Logs in reverse order.
  } 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, MorleyLogs -> Builder
(MorleyLogs -> Builder) -> Buildable MorleyLogs
forall p. (p -> Builder) -> Buildable p
build :: MorleyLogs -> Builder
$cbuild :: MorleyLogs -> Builder
Buildable)

instance NFData MorleyLogs

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

-- | Interpret a contract without performing any side effects.
-- This function uses untyped representation of contract, parameter and storage.
-- Mostly used for testing.
interpretUntyped
  :: U.Contract
  -> U.Value
  -> U.Value
  -> ContractEnv
  -> Either InterpretError InterpretResult
interpretUntyped :: Contract
-> Value
-> Value
-> ContractEnv
-> Either InterpretError InterpretResult
interpretUntyped uContract :: Contract
uContract@U.Contract{..} paramU :: Value
paramU initStU :: Value
initStU env :: ContractEnv
env = do
  SomeContract (Contract (ContractCode cp st
instr :: ContractCode cp st) _ _)
      <- (TCError -> InterpretError)
-> Either TCError SomeContract
-> Either InterpretError SomeContract
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first TCError -> InterpretError
IllTypedContract (Either TCError SomeContract -> Either InterpretError SomeContract)
-> Either TCError SomeContract
-> Either InterpretError SomeContract
forall a b. (a -> b) -> a -> b
$ TcOriginatedContracts -> Contract -> Either TCError SomeContract
typeCheckContract (ContractEnv -> TcOriginatedContracts
ceContracts ContractEnv
env) Contract
uContract
  -- Do creates dummy scope to somehow overcome this:
  -- GHC internal error: ‘st’ is not in scope during type checking, but it passed the renamer.
  do
    let
      runTC :: forall t. SingI t => U.Value -> Either TCError (Value t)
      runTC :: Value -> Either TCError (Value t)
runTC =
        ParameterType
-> TcOriginatedContracts
-> TypeCheck (Value t)
-> Either TCError (Value t)
forall a.
ParameterType
-> TcOriginatedContracts -> TypeCheck a -> Either TCError a
runTypeCheck ParameterType
contractParameter (ContractEnv -> TcOriginatedContracts
ceContracts ContractEnv
env) (TypeCheck (Value t) -> Either TCError (Value t))
-> (Value -> TypeCheck (Value t))
-> Value
-> Either TCError (Value t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        InstrCallStack
-> ReaderT InstrCallStack TypeCheck (Value t)
-> TypeCheck (Value t)
forall r (m :: * -> *) a. r -> ReaderT r m a -> m a
usingReaderT InstrCallStack
forall a. Default a => a
def (ReaderT InstrCallStack TypeCheck (Value t) -> TypeCheck (Value t))
-> (Value -> ReaderT InstrCallStack TypeCheck (Value t))
-> Value
-> TypeCheck (Value t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        SingI t => Value -> ReaderT InstrCallStack TypeCheck (Value t)
forall (t :: T). SingI t => Value -> TypeCheckInstr (Value t)
typeCheckValue @t

    Value cp
paramV <- (TCError -> InterpretError)
-> Either TCError (Value cp) -> Either InterpretError (Value cp)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first TCError -> InterpretError
IllTypedParam (Either TCError (Value cp) -> Either InterpretError (Value cp))
-> Either TCError (Value cp) -> Either InterpretError (Value cp)
forall a b. (a -> b) -> a -> b
$ Value -> Either TCError (Value cp)
forall (t :: T). SingI t => Value -> Either TCError (Value t)
runTC @cp Value
paramU
    Value st
initStV <- (TCError -> InterpretError)
-> Either TCError (Value st) -> Either InterpretError (Value st)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first TCError -> InterpretError
IllTypedStorage (Either TCError (Value st) -> Either InterpretError (Value st))
-> Either TCError (Value st) -> Either InterpretError (Value st)
forall a b. (a -> b) -> a -> b
$ Value -> Either TCError (Value st)
forall (t :: T). SingI t => Value -> Either TCError (Value t)
runTC @st Value
initStU
    ContractReturn st -> Either InterpretError InterpretResult
forall (st :: T).
StorageScope st =>
ContractReturn st -> Either InterpretError InterpretResult
handleContractReturn (ContractReturn st -> Either InterpretError InterpretResult)
-> ContractReturn st -> Either InterpretError InterpretResult
forall a b. (a -> b) -> a -> b
$
      ContractCode cp st
-> EntryPointCallT cp cp
-> Value cp
-> Value st
-> ContractEnv
-> ContractReturn st
forall (cp :: T) (st :: T) (arg :: T).
ContractCode cp st
-> EntryPointCallT cp arg
-> Value arg
-> Value st
-> ContractEnv
-> ContractReturn st
interpret ContractCode cp st
instr EntryPointCallT cp cp
forall (param :: T).
ParameterScope param =>
EntryPointCallT param param
epcCallRootUnsafe Value cp
paramV Value st
initStV ContractEnv
env

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
RuntimeFailure ((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

interpret'
  :: forall cp st arg.
     ContractCode cp st
  -> EntryPointCallT cp arg
  -> T.Value arg
  -> T.Value st
  -> ContractEnv
  -> InterpreterState
  -> ContractReturn st
interpret' :: ContractCode cp st
-> EntryPointCallT cp arg
-> Value arg
-> Value st
-> ContractEnv
-> InterpreterState
-> ContractReturn st
interpret' instr :: ContractCode cp st
instr epc :: EntryPointCallT cp arg
epc param :: Value arg
param initSt :: Value st
initSt env :: ContractEnv
env ist :: InterpreterState
ist = (Either MichelsonFailed (Rec Value (ContractOut st))
 -> Either MichelsonFailed ([Operation], Value st))
-> (Either MichelsonFailed (Rec Value (ContractOut st)),
    InterpreterState)
-> ContractReturn st
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Rec Value (ContractOut st) -> ([Operation], Value st))
-> Either MichelsonFailed (Rec Value (ContractOut st))
-> Either MichelsonFailed ([Operation], Value st)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rec Value (ContractOut st) -> ([Operation], Value st)
forall (st :: T).
Rec Value (ContractOut st) -> ([Operation], Value st)
fromFinalStack) ((Either MichelsonFailed (Rec Value (ContractOut st)),
  InterpreterState)
 -> ContractReturn st)
-> (Either MichelsonFailed (Rec Value (ContractOut st)),
    InterpreterState)
-> ContractReturn st
forall a b. (a -> b) -> a -> b
$
  EvalOp (Rec Value (ContractOut st))
-> ContractEnv
-> InterpreterState
-> (Either MichelsonFailed (Rec Value (ContractOut st)),
    InterpreterState)
forall a.
EvalOp a
-> ContractEnv
-> InterpreterState
-> (Either MichelsonFailed a, InterpreterState)
runEvalOp
    (ContractCode cp st
-> Rec Value (ContractInp cp st)
-> EvalOp (Rec Value (ContractOut st))
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr ContractCode cp st
instr (Rec Value (ContractInp cp st)
 -> EvalOp (Rec Value (ContractOut st)))
-> Rec Value (ContractInp cp st)
-> EvalOp (Rec Value (ContractOut st))
forall a b. (a -> b) -> a -> b
$ Value cp -> Value st -> Rec Value (ContractInp cp st)
forall (param :: T) (st :: T).
Value param -> Value st -> Rec Value (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) Value st
initSt)
    ContractEnv
env
    InterpreterState
ist

mkInitStack :: T.Value param -> T.Value st -> Rec T.Value (ContractInp param st)
mkInitStack :: Value param -> Value st -> Rec Value (ContractInp param st)
mkInitStack param :: Value param
param st :: Value st
st = (Value param, Value st) -> Value' Instr ('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) Value' Instr ('TPair param st)
-> Rec Value '[] -> Rec Value (ContractInp param st)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value '[]
forall u (a :: u -> *). Rec a '[]
RNil

fromFinalStack :: Rec T.Value (ContractOut st) -> ([T.Operation], T.Value st)
fromFinalStack :: Rec Value (ContractOut st) -> ([Operation], Value st)
fromFinalStack (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
  :: ContractCode cp st
  -> EntryPointCallT cp arg
  -> T.Value arg
  -> T.Value st
  -> ContractEnv
  -> ContractReturn st
interpret :: ContractCode cp st
-> EntryPointCallT cp arg
-> Value arg
-> Value st
-> ContractEnv
-> ContractReturn st
interpret instr :: ContractCode cp st
instr epc :: EntryPointCallT cp arg
epc param :: Value arg
param initSt :: Value st
initSt env :: ContractEnv
env =
  ContractCode cp st
-> EntryPointCallT cp arg
-> Value arg
-> Value st
-> ContractEnv
-> InterpreterState
-> ContractReturn st
forall (cp :: T) (st :: T) (arg :: T).
ContractCode cp st
-> EntryPointCallT cp arg
-> Value arg
-> Value st
-> ContractEnv
-> InterpreterState
-> ContractReturn st
interpret' ContractCode cp st
instr 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 env :: ContractEnv
env instr :: Instr inp out
instr inpSt :: Rec Value inp
inpSt =
  (Either MichelsonFailed (Rec Value out), InterpreterState)
-> Either MichelsonFailed (Rec Value out)
forall a b. (a, b) -> a
fst ((Either MichelsonFailed (Rec Value out), InterpreterState)
 -> Either MichelsonFailed (Rec Value out))
-> (Either MichelsonFailed (Rec Value out), InterpreterState)
-> Either MichelsonFailed (Rec Value out)
forall a b. (a -> b) -> a -> b
$
  EvalOp (Rec Value out)
-> ContractEnv
-> InterpreterState
-> (Either MichelsonFailed (Rec Value out), InterpreterState)
forall a.
EvalOp a
-> ContractEnv
-> InterpreterState
-> (Either MichelsonFailed a, InterpreterState)
runEvalOp
    (Instr inp out -> Rec Value inp -> EvalOp (Rec Value out)
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
instr 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 T.Value 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

type EvalM m =
  ( MonadReader ContractEnv m
  , MonadState InterpreterState m
  , MonadError MichelsonFailed m
  )

type InstrRunner m =
  forall inp out.
     Instr inp out
  -> Rec (T.Value) inp
  -> m (Rec (T.Value) 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 Value inp
r = InstrRunner m
-> Instr inp out -> Rec Value inp -> m (Rec Value out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
i Rec Value inp
r
runInstr i :: Instr inp out
i@(InstrWithNotes _ _i1 :: Instr inp out
_i1) r :: Rec Value inp
r = InstrRunner m
-> Instr inp out -> Rec Value inp -> m (Rec Value out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
i Rec Value inp
r
runInstr i :: Instr inp out
i@(InstrWithVarNotes _ _i1 :: Instr inp out
_i1) r :: Rec Value inp
r = InstrRunner m
-> Instr inp out -> Rec Value inp -> m (Rec Value out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
i Rec Value inp
r
runInstr i :: Instr inp out
i@Instr inp out
Nop r :: Rec Value inp
r = InstrRunner m
-> Instr inp out -> Rec Value inp -> m (Rec Value out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
i Rec Value inp
r
runInstr i :: Instr inp out
i@(Nested _) r :: Rec Value inp
r = InstrRunner m
-> Instr inp out -> Rec Value inp -> m (Rec Value out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
i Rec Value inp
r
runInstr i :: Instr inp out
i r :: Rec Value inp
r = do
  RemainingSteps
rs <- (InterpreterState -> RemainingSteps) -> m RemainingSteps
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets InterpreterState -> RemainingSteps
isRemainingSteps
  if RemainingSteps
rs RemainingSteps -> RemainingSteps -> Bool
forall a. Eq a => a -> a -> Bool
== 0
  then MichelsonFailed -> m (Rec Value out)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (MichelsonFailed -> m (Rec Value out))
-> MichelsonFailed -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ MichelsonFailed
MichelsonGasExhaustion
  else do
    (InterpreterState -> InterpreterState) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\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 Value inp -> m (Rec Value out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr Instr inp out
i Rec Value 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 Value inp
r = Instr inp b -> Rec Value inp -> m (Rec Value b)
InstrRunner m
runner Instr inp b
i1 Rec Value inp
r m (Rec Value b)
-> (Rec Value b -> m (Rec Value out)) -> m (Rec Value out)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \r' :: Rec Value b
r' -> Instr b out -> Rec Value b -> m (Rec Value out)
InstrRunner m
runner Instr b out
i2 Rec Value b
r'
runInstrImpl runner :: InstrRunner m
runner (InstrWithNotes _ i :: Instr inp out
i) r :: Rec Value inp
r = Instr inp out -> Rec Value inp -> m (Rec Value out)
InstrRunner m
runner Instr inp out
i Rec Value inp
r
runInstrImpl runner :: InstrRunner m
runner (InstrWithVarNotes _ i :: Instr inp out
i) r :: Rec Value inp
r = Instr inp out -> Rec Value inp -> m (Rec Value out)
InstrRunner m
runner Instr inp out
i Rec Value inp
r
runInstrImpl runner :: InstrRunner m
runner (FrameInstr (Proxy s
_ :: Proxy s) i :: Instr a b
i) r :: Rec Value inp
r = do
  let (inp :: Rec Value a
inp, end :: Rec Value s
end) = Rec Value (a ++ s) -> (Rec Value a, Rec Value 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 Value inp
Rec Value (a ++ s)
r
  Rec Value b
out <- InstrRunner m -> Instr a b -> Rec Value a -> m (Rec Value b)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner Instr a b
i Rec Value a
inp
  return (Rec Value b
out Rec Value b -> Rec Value s -> Rec Value (b ++ s)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Rec Value s
end)
runInstrImpl _ Nop r :: Rec Value inp
r = Rec Value inp -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value inp -> m (Rec Value out))
-> Rec Value inp -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Rec Value inp
r
runInstrImpl _ (Ext nop :: ExtInstr inp
nop) r :: Rec Value inp
r = Rec Value inp
r Rec Value inp -> m () -> m (Rec Value inp)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ SomeItStack -> m ()
forall (m :: * -> *). EvalM m => SomeItStack -> m ()
interpretExt (ExtInstr inp -> Rec Value inp -> SomeItStack
forall (inp :: [T]). ExtInstr inp -> Rec Value inp -> SomeItStack
SomeItStack ExtInstr inp
nop Rec Value inp
r)
runInstrImpl runner :: InstrRunner m
runner (Nested sq :: Instr inp out
sq) r :: Rec Value inp
r = InstrRunner m
-> Instr inp out -> Rec Value inp -> m (Rec Value out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner Instr inp out
sq Rec Value inp
r
runInstrImpl runner :: InstrRunner m
runner (DocGroup _ sq :: Instr inp out
sq) r :: Rec Value inp
r = InstrRunner m
-> Instr inp out -> Rec Value inp -> m (Rec Value out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner Instr inp out
sq Rec Value inp
r
runInstrImpl _ DROP (_ :& r :: Rec Value rs
r) = Rec Value rs -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value rs -> m (Rec Value out))
-> Rec Value rs -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Rec Value rs
r
runInstrImpl runner :: InstrRunner m
runner (DROPN s :: Sing n
s) stack :: Rec Value inp
stack =
  case Sing n
s of
    SZ -> Rec Value inp -> m (Rec Value inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec Value inp
stack
    SS s' -> case Rec Value 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 Value rs
r) -> InstrRunner m -> Instr rs out -> Rec Value rs -> m (Rec Value 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 Value rs
r
runInstrImpl _ DUP (a :: Value r
a :& r :: Rec Value rs
r) = Rec Value (r : r : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (r : r : rs) -> m (Rec Value out))
-> Rec Value (r : r : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Value r
a Value r -> Rec Value (r : rs) -> Rec Value (r : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Value r
a Value r -> Rec Value rs -> Rec Value (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ SWAP (a :: Value r
a :& b :: Value r
b :& r :: Rec Value rs
r) = Rec Value (r : r : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (r : r : rs) -> m (Rec Value out))
-> Rec Value (r : r : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Value r
b Value r -> Rec Value (r : rs) -> Rec Value (r : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Value r
a Value r -> Rec Value rs -> Rec Value (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ (DIG nSing0 :: Sing n
nSing0) input0 :: Rec Value inp
input0 =
  Rec Value out -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value out -> m (Rec Value out))
-> Rec Value out -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (Sing n, Rec Value inp) -> Rec Value out
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDIG n inp out a =>
(Sing n, Rec Value inp) -> Rec Value out
go (Sing n
nSing0, Rec Value inp
input0)
  where
    go :: forall (n :: Peano) inp out a. T.ConstraintDIG n inp out a =>
      (Sing n, Rec T.Value inp) -> Rec T.Value out
    go :: (Sing n, Rec Value inp) -> Rec Value out
go = \case
      (SZ, stack :: Rec Value inp
stack) ->  Rec Value inp
Rec Value out
stack
      (SS nSing, b :: Value r
b :& r :: Rec Value rs
r) -> case (Sing n, Rec Value rs)
-> Rec Value (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 Value inp) -> Rec Value out
go (Sing n
SingNat n
nSing, Rec Value rs
r) of
        (a :: Value r
a :& resTail :: Rec Value rs
resTail) -> Value r
a Value r -> Rec Value (r : rs) -> Rec Value (r : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Value r
b Value r -> Rec Value rs -> Rec Value (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
resTail
runInstrImpl _ (DUG nSing0 :: Sing n
nSing0) input0 :: Rec Value inp
input0 =
  Rec Value out -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value out -> m (Rec Value out))
-> Rec Value out -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (Sing n, Rec Value inp) -> Rec Value out
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDUG n inp out a =>
(Sing n, Rec Value inp) -> Rec Value out
go (Sing n
nSing0, Rec Value inp
input0)
  where
    go :: forall (n :: Peano) inp out a. T.ConstraintDUG n inp out a =>
      (Sing n, Rec T.Value inp) -> Rec T.Value out
    go :: (Sing n, Rec Value inp) -> Rec Value out
go = \case
      (SZ, stack :: Rec Value inp
stack) -> Rec Value inp
Rec Value out
stack
      (SS s', a :: Value r
a :& b :: Value r
b :& r :: Rec Value rs
r) -> Value r
b Value r
-> Rec Value (Take n rs ++ (a : Drop n (Drop ('S 'Z) inp)))
-> Rec Value (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 Value (r : rs))
-> Rec Value (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 Value inp) -> Rec Value out
go (Sing n
SingNat n
s', Value r
a Value r -> Rec Value rs -> Rec Value (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r)
runInstrImpl _ SOME (a :: Value r
a :& r :: Rec Value rs
r) =
  Value r -> (KnownT r => m (Rec Value out)) -> m (Rec Value out)
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (KnownT t => a) -> a
withValueTypeSanity Value r
a ((KnownT r => m (Rec Value out)) -> m (Rec Value out))
-> (KnownT r => m (Rec Value out)) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$
    Rec Value ('TOption r : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TOption r : rs) -> m (Rec Value out))
-> Rec Value ('TOption r : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Maybe (Value r) -> Value' Instr ('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) Value' Instr ('TOption r)
-> Rec Value rs -> Rec Value ('TOption r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ (PUSH v :: Value' Instr t
v) r :: Rec Value inp
r = Rec Value (t : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (t : inp) -> m (Rec Value out))
-> Rec Value (t : inp) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Value' Instr t
v Value' Instr t -> Rec Value inp -> Rec Value (t : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r
runInstrImpl _ NONE r :: Rec Value inp
r = Rec Value ('TOption a : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TOption a : inp) -> m (Rec Value out))
-> Rec Value ('TOption a : inp) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Maybe (Value' Instr a) -> Value' Instr ('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 Value' Instr ('TOption a)
-> Rec Value inp -> Rec Value ('TOption a : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r
runInstrImpl _ UNIT r :: Rec Value inp
r = Rec Value ('TUnit : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TUnit : inp) -> m (Rec Value out))
-> Rec Value ('TUnit : inp) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Value' Instr 'TUnit
forall (instr :: [T] -> [T] -> *). Value' instr 'TUnit
VUnit Value' Instr 'TUnit -> Rec Value inp -> Rec Value ('TUnit : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r
runInstrImpl runner :: InstrRunner m
runner (IF_NONE _bNone :: Instr s out
_bNone bJust :: Instr (a : s) out
bJust) (VOption (Just a :: Value' Instr t
a) :& r :: Rec Value rs
r) = Instr (a : s) out -> Rec Value (a : s) -> m (Rec Value out)
InstrRunner m
runner Instr (a : s) out
bJust (Value' Instr t
a Value' Instr t -> Rec Value rs -> Rec Value (t : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r)
runInstrImpl runner :: InstrRunner m
runner (IF_NONE bNone :: Instr s out
bNone _bJust :: Instr (a : s) out
_bJust) (VOption Nothing :& r :: Rec Value rs
r) = Instr s out -> Rec Value s -> m (Rec Value out)
InstrRunner m
runner Instr s out
bNone Rec Value s
Rec Value rs
r
runInstrImpl _ PAIR (a :: Value r
a :& b :: Value r
b :& r :: Rec Value rs
r) = Rec Value ('TPair r r : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TPair r r : rs) -> m (Rec Value out))
-> Rec Value ('TPair r r : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (Value r, Value r) -> Value' Instr ('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) Value' Instr ('TPair r r)
-> Rec Value rs -> Rec Value ('TPair r r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ (AnnCAR _) (VPair (a :: Value' Instr l
a, _b :: Value' Instr r
_b) :& r :: Rec Value rs
r) = Rec Value (l : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (l : rs) -> m (Rec Value out))
-> Rec Value (l : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Value' Instr l
a Value' Instr l -> Rec Value rs -> Rec Value (l : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ (AnnCDR _) (VPair (_a :: Value' Instr l
_a, b :: Value' Instr r
b) :& r :: Rec Value rs
r) = Rec Value (r : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (r : rs) -> m (Rec Value out))
-> Rec Value (r : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Value' Instr r
b Value' Instr r -> Rec Value rs -> Rec Value (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ LEFT (a :: Value r
a :& r :: Rec Value rs
r) =
  Value r -> (KnownT r => m (Rec Value out)) -> m (Rec Value out)
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (KnownT t => a) -> a
withValueTypeSanity Value r
a ((KnownT r => m (Rec Value out)) -> m (Rec Value out))
-> (KnownT r => m (Rec Value out)) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$
    Rec Value ('TOr r b : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TOr r b : rs) -> m (Rec Value out))
-> Rec Value ('TOr r b : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (Either (Value r) (Value' Instr b) -> Value' Instr ('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' Instr ('TOr r b))
-> Either (Value r) (Value' Instr b) -> Value' Instr ('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) Value' Instr ('TOr r b)
-> Rec Value rs -> Rec Value ('TOr r b : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ RIGHT (b :: Value r
b :& r :: Rec Value rs
r) =
  Value r -> (KnownT r => m (Rec Value out)) -> m (Rec Value out)
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (KnownT t => a) -> a
withValueTypeSanity Value r
b ((KnownT r => m (Rec Value out)) -> m (Rec Value out))
-> (KnownT r => m (Rec Value out)) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$
    Rec Value ('TOr a r : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TOr a r : rs) -> m (Rec Value out))
-> Rec Value ('TOr a r : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (Either (Value' Instr a) (Value r) -> Value' Instr ('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' Instr ('TOr a r))
-> Either (Value' Instr a) (Value r) -> Value' Instr ('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) Value' Instr ('TOr a r)
-> Rec Value rs -> Rec Value ('TOr a r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl runner :: InstrRunner m
runner (IF_LEFT bLeft :: Instr (a : s) out
bLeft _) (VOr (Left a :: Value' Instr l
a) :& r :: Rec Value rs
r) = Instr (a : s) out -> Rec Value (a : s) -> m (Rec Value out)
InstrRunner m
runner Instr (a : s) out
bLeft (Value' Instr l
a Value' Instr l -> Rec Value rs -> Rec Value (l : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r)
runInstrImpl runner :: InstrRunner m
runner (IF_LEFT _ bRight :: Instr (b : s) out
bRight) (VOr (Right a :: Value' Instr r
a) :& r :: Rec Value rs
r) = Instr (b : s) out -> Rec Value (b : s) -> m (Rec Value out)
InstrRunner m
runner Instr (b : s) out
bRight (Value' Instr r
a Value' Instr r -> Rec Value rs -> Rec Value (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r)
-- More here
runInstrImpl _ NIL r :: Rec Value inp
r = Rec Value ('TList p : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TList p : inp) -> m (Rec Value out))
-> Rec Value ('TList p : inp) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ [Value' Instr p] -> Value' Instr ('TList p)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
[Value' instr t] -> Value' instr ('TList t)
VList [] Value' Instr ('TList p)
-> Rec Value inp -> Rec Value ('TList p : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r
runInstrImpl _ CONS (a :: Value r
a :& VList l :: [Value' Instr t]
l :& r :: Rec Value rs
r) = Rec Value ('TList r : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TList r : rs) -> m (Rec Value out))
-> Rec Value ('TList r : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ [Value r] -> Value' Instr ('TList r)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
[Value' instr t] -> Value' instr ('TList t)
VList (Value r
a Value r -> [Value r] -> [Value r]
forall a. a -> [a] -> [a]
: [Value r]
[Value' Instr t]
l) Value' Instr ('TList r)
-> Rec Value rs -> Rec Value ('TList r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl runner :: InstrRunner m
runner (IF_CONS _ bNil :: Instr s out
bNil) (VList [] :& r :: Rec Value rs
r) = Instr s out -> Rec Value s -> m (Rec Value out)
InstrRunner m
runner Instr s out
bNil Rec Value s
Rec Value rs
r
runInstrImpl runner :: InstrRunner m
runner (IF_CONS bCons :: Instr (a : 'TList a : s) out
bCons _) (VList (lh :: Value' Instr t
lh : lr :: [Value' Instr t]
lr) :& r :: Rec Value rs
r) = Instr (a : 'TList a : s) out
-> Rec Value (a : 'TList a : s) -> m (Rec Value out)
InstrRunner m
runner Instr (a : 'TList a : s) out
bCons (Value' Instr t
lh Value' Instr t
-> Rec Value ('TList t : rs) -> Rec Value (t : 'TList t : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& [Value' Instr t] -> Value' Instr ('TList t)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
[Value' instr t] -> Value' instr ('TList t)
VList [Value' Instr t]
lr Value' Instr ('TList t)
-> Rec Value rs -> Rec Value ('TList t : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r)
runInstrImpl _ SIZE (a :: Value r
a :& r :: Rec Value rs
r) = Rec Value ('TNat : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TNat : rs) -> m (Rec Value out))
-> Rec Value ('TNat : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (Natural -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural -> Value' Instr 'TNat) -> Natural -> Value' Instr '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 r -> Int
forall (c :: T) (instr :: [T] -> [T] -> *).
SizeOp c =>
Value' instr c -> Int
evalSize Value r
a) Value' Instr 'TNat -> Rec Value rs -> Rec Value ('TNat : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ EMPTY_SET r :: Rec Value inp
r = Rec Value ('TSet e : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TSet e : inp) -> m (Rec Value out))
-> Rec Value ('TSet e : inp) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Set (Value' Instr e) -> Value' Instr ('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 Value' Instr ('TSet e)
-> Rec Value inp -> Rec Value ('TSet e : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r
runInstrImpl _ EMPTY_MAP r :: Rec Value inp
r = Rec Value ('TMap a b : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TMap a b : inp) -> m (Rec Value out))
-> Rec Value ('TMap a b : inp) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Map (Value' Instr a) (Value' Instr b) -> Value' Instr ('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 Value' Instr ('TMap a b)
-> Rec Value inp -> Rec Value ('TMap a b : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r
runInstrImpl _ EMPTY_BIG_MAP r :: Rec Value inp
r = Rec Value ('TBigMap a b : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TBigMap a b : inp) -> m (Rec Value out))
-> Rec Value ('TBigMap a b : inp) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Map (Value' Instr a) (Value' Instr b)
-> Value' Instr ('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 Value' Instr ('TBigMap a b)
-> Rec Value inp -> Rec Value ('TBigMap a b : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r
runInstrImpl runner :: InstrRunner m
runner (MAP ops :: Instr (MapOpInp c : s) (b : s)
ops) (a :: Value r
a :& r :: Rec Value 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 Value rs
newStack, newList :: [Value' Instr b]
newList) <- ((Rec Value rs, [Value' Instr b])
 -> Value (MapOpInp c) -> m (Rec Value rs, [Value' Instr b]))
-> (Rec Value rs, [Value' Instr b])
-> [Value (MapOpInp c)]
-> m (Rec Value 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 Value rs
curStack, curList :: [Value' Instr b]
curList) (val :: T.Value (MapOpInp c)) -> do
        Rec Value (b : s)
res <- Instr (MapOpInp c : rs) (b : s)
-> Rec Value (MapOpInp c : rs) -> m (Rec Value (b : s))
InstrRunner m
runner Instr (MapOpInp c : rs) (b : s)
Instr (MapOpInp r : s) (b : s)
code (Value (MapOpInp c)
Value (MapOpInp r)
val Value (MapOpInp c) -> Rec Value rs -> Rec Value (MapOpInp c : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
curStack)
        case Rec Value (b : s)
res of
          ((nextVal :: T.Value b) :& nextStack :: Rec Value rs
nextStack) -> (Rec Value rs, [Value' Instr b])
-> m (Rec Value rs, [Value' Instr b])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value 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 Value rs
r, []) (Value r -> [Value (MapOpInp r)]
forall (c :: T) (instr :: [T] -> [T] -> *).
MapOp c =>
Value' instr c -> [Value' instr (MapOpInp c)]
mapOpToList @c Value r
a)
      Rec Value (MapOpRes c b : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (MapOpRes c b : rs) -> m (Rec Value out))
-> Rec Value (MapOpRes c b : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ 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) Value' Instr (MapOpRes c b)
-> Rec Value rs -> Rec Value (MapOpRes c b : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
newStack
runInstrImpl runner :: InstrRunner m
runner (ITER ops :: Instr (IterOpEl c : out) out
ops) (a :: Value r
a :& r :: Rec Value rs
r) =
  case Instr (IterOpEl c : out) out
ops of
    (code :: Instr (IterOpEl c ': s) s) ->
      case Value r -> (Maybe (Value' Instr (IterOpEl r)), Value r)
forall (c :: T) (instr :: [T] -> [T] -> *).
IterOp c =>
Value' instr c
-> (Maybe (Value' instr (IterOpEl c)), Value' instr c)
iterOpDetachOne @c Value r
a of
        (Just x :: Value' Instr (IterOpEl r)
x, xs :: Value r
xs) -> do
          Rec Value out
res <- Instr (IterOpEl c : rs) out
-> Rec Value (IterOpEl c : rs) -> m (Rec Value out)
InstrRunner m
runner Instr (IterOpEl c : rs) out
Instr (IterOpEl r : out) out
code (Value' Instr (IterOpEl c)
Value' Instr (IterOpEl r)
x Value' Instr (IterOpEl c)
-> Rec Value rs -> Rec Value (IterOpEl c : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r)
          Instr (r : out) out -> Rec Value (r : out) -> m (Rec Value 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 r
xs Value r -> Rec Value out -> Rec Value (r : out)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value out
res)
        (Nothing, _) -> Rec Value rs -> m (Rec Value rs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec Value rs
r
runInstrImpl _ MEM (a :: Value r
a :& b :: Value r
b :& r :: Rec Value rs
r) = Rec Value ('TBool : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TBool : rs) -> m (Rec Value out))
-> Rec Value ('TBool : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (Bool -> Value' Instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Value' Instr (MemOpKey r) -> Value r -> Bool
forall (c :: T) (instr :: [T] -> [T] -> *).
MemOp c =>
Value' instr (MemOpKey c) -> Value' instr c -> Bool
evalMem Value r
Value' Instr (MemOpKey r)
a Value r
b)) Value' Instr 'TBool -> Rec Value rs -> Rec Value ('TBool : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ GET (a :: Value r
a :& b :: Value r
b :& r :: Rec Value rs
r) = Rec Value ('TOption (GetOpVal c) : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TOption (GetOpVal c) : rs) -> m (Rec Value out))
-> Rec Value ('TOption (GetOpVal c) : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Maybe (Value' Instr (GetOpVal c))
-> Value' Instr ('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 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 Value r
Value' Instr (GetOpKey r)
a Value r
b) Value' Instr ('TOption (GetOpVal c))
-> Rec Value rs -> Rec Value ('TOption (GetOpVal c) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ UPDATE (a :: Value r
a :& b :: Value r
b :& c :: Value r
c :& r :: Rec Value rs
r) = Rec Value (r : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (r : rs) -> m (Rec Value out))
-> Rec Value (r : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ 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 Value r
Value' Instr (UpdOpKey r)
a Value r
Value' Instr (UpdOpParams r)
b Value r
c Value r -> Rec Value rs -> Rec Value (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl runner :: InstrRunner m
runner (IF bTrue :: Instr s out
bTrue _) (VBool True :& r :: Rec Value rs
r) = Instr s out -> Rec Value s -> m (Rec Value out)
InstrRunner m
runner Instr s out
bTrue Rec Value s
Rec Value rs
r
runInstrImpl runner :: InstrRunner m
runner (IF _ bFalse :: Instr s out
bFalse) (VBool False :& r :: Rec Value rs
r) = Instr s out -> Rec Value s -> m (Rec Value out)
InstrRunner m
runner Instr s out
bFalse Rec Value s
Rec Value rs
r
runInstrImpl _ (LOOP _) (VBool False :& r :: Rec Value rs
r) = Rec Value rs -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value rs -> m (Rec Value out))
-> Rec Value rs -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Rec Value rs
r
runInstrImpl runner :: InstrRunner m
runner (LOOP ops :: Instr out ('TBool : out)
ops) (VBool True :& r :: Rec Value rs
r) = do
  Rec Value ('TBool : out)
res <- Instr out ('TBool : out)
-> Rec Value out -> m (Rec Value ('TBool : out))
InstrRunner m
runner Instr out ('TBool : out)
ops Rec Value out
Rec Value rs
r
  Instr ('TBool : out) out
-> Rec Value ('TBool : out) -> m (Rec Value 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 Value ('TBool : out)
res
runInstrImpl _ (LOOP_LEFT _) (VOr (Right a :: Value' Instr r
a) :&r :: Rec Value rs
r) = Rec Value (r : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (r : rs) -> m (Rec Value out))
-> Rec Value (r : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Value' Instr r
a Value' Instr r -> Rec Value rs -> Rec Value (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl runner :: InstrRunner m
runner (LOOP_LEFT ops :: Instr (a : s) ('TOr a b : s)
ops) (VOr (Left a :: Value' Instr l
a) :& r :: Rec Value rs
r) = do
  Rec Value ('TOr a b : s)
res <- Instr (a : s) ('TOr a b : s)
-> Rec Value (a : s) -> m (Rec Value ('TOr a b : s))
InstrRunner m
runner Instr (a : s) ('TOr a b : s)
ops (Value' Instr l
a Value' Instr l -> Rec Value rs -> Rec Value (l : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r)
  Instr ('TOr a b : s) (b : s)
-> Rec Value ('TOr a b : s) -> m (Rec Value (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 Value ('TOr a b : s)
res
runInstrImpl _ (LAMBDA lam :: Value' Instr ('TLambda i o)
lam) r :: Rec Value inp
r = Rec Value ('TLambda i o : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TLambda i o : inp) -> m (Rec Value out))
-> Rec Value ('TLambda i o : inp) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TLambda i o)
lam Value' Instr ('TLambda i o)
-> Rec Value inp -> Rec Value ('TLambda i o : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r
runInstrImpl runner :: InstrRunner m
runner EXEC (a :: Value r
a :& 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 Value rs
r) = do
  Rec Value '[out]
res <- Instr '[inp] '[out] -> Rec Value '[inp] -> m (Rec Value '[out])
InstrRunner m
runner Instr '[inp] '[out]
lBody (Value r
a Value r -> Rec Value '[] -> Rec Value '[r]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value '[]
forall u (a :: u -> *). Rec a '[]
RNil)
  pure $ Rec Value '[out]
res Rec Value '[out] -> Rec Value rs -> Rec Value ('[out] ++ rs)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Rec Value rs
r
runInstrImpl _ APPLY ((Value r
a :: T.Value a) :& VLam lBody :: RemFail Instr '[inp] '[out]
lBody :& r :: Rec Value rs
r) = do
  Rec Value ('TLambda b out : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TLambda b out : rs) -> m (Rec Value out))
-> Rec Value ('TLambda b out : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ RemFail Instr '[b] '[out] -> Value' Instr ('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) Value' Instr ('TLambda b out)
-> Rec Value rs -> Rec Value ('TLambda b out : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value 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 (a :: T) (b :: T) (s :: [T]).
Instr (a : b : s) ('TPair a b : s)
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 :: Value r
a :& r :: Rec Value rs
r) = do
  Rec Value c
res <- Instr a c -> Rec Value a -> m (Rec Value c)
InstrRunner m
runner Instr a c
i Rec Value a
Rec Value rs
r
  pure $ Value r
a Value r -> Rec Value c -> Rec Value (r : c)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value c
res
runInstrImpl runner :: InstrRunner m
runner (DIPN s :: Sing n
s i :: Instr s s'
i) stack :: Rec Value inp
stack =
  case Sing n
s of
    SZ -> Instr s s' -> Rec Value s -> m (Rec Value s')
InstrRunner m
runner Instr s s'
i Rec Value inp
Rec Value s
stack
    SS s' -> case Rec Value inp
stack of
      (a :: Value r
a :& r :: Rec Value rs
r) -> (Value r
a Value r
-> Rec Value (Take n rs ++ s') -> Rec Value (r : (Take n rs ++ s'))
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) (Rec Value (Take n rs ++ s') -> Rec Value (r : (Take n rs ++ s')))
-> m (Rec Value (Take n rs ++ s'))
-> m (Rec Value (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 Value rs
-> m (Rec Value (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 Value rs
r
runInstrImpl _ FAILWITH (a :: Value r
a :& _) = MichelsonFailed -> m (Rec Value out)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (MichelsonFailed -> m (Rec Value out))
-> MichelsonFailed -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Value r -> MichelsonFailed
forall (t :: T). KnownT t => Value t -> MichelsonFailed
MichelsonFailedWith Value r
a
runInstrImpl _ CAST (a :: Value r
a :& r :: Rec Value rs
r) = Rec Value (r : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (r : rs) -> m (Rec Value out))
-> Rec Value (r : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Value r
a Value r -> Rec Value rs -> Rec Value (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ RENAME (a :: Value r
a :& r :: Rec Value rs
r) = Rec Value (r : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (r : rs) -> m (Rec Value out))
-> Rec Value (r : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Value r
a Value r -> Rec Value rs -> Rec Value (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ PACK (a :: Value r
a :& r :: Rec Value rs
r) = Rec Value ('TBytes : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TBytes : rs) -> m (Rec Value out))
-> Rec Value ('TBytes : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (ByteString -> Value' Instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value' Instr 'TBytes)
-> ByteString -> Value' Instr 'TBytes
forall a b. (a -> b) -> a -> b
$ Value r -> ByteString
forall (t :: T). PackedValScope t => Value t -> ByteString
packValue' Value r
a) Value' Instr 'TBytes -> Rec Value rs -> Rec Value ('TBytes : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ UNPACK (VBytes a :: ByteString
a :& r :: Rec Value rs
r) =
  Rec Value ('TOption a : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TOption a : rs) -> m (Rec Value out))
-> Rec Value ('TOption a : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (Maybe (Value' Instr a) -> Value' Instr ('TOption a)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' Instr a) -> Value' Instr ('TOption a))
-> (Either UnpackError (Value' Instr a) -> Maybe (Value' Instr a))
-> Either UnpackError (Value' Instr a)
-> Value' Instr ('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' Instr ('TOption a))
-> Either UnpackError (Value' Instr a) -> Value' Instr ('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) Value' Instr ('TOption a)
-> Rec Value rs -> Rec Value ('TOption a : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ CONCAT (a :: Value r
a :& b :: Value r
b :& r :: Rec Value rs
r) = Rec Value (r : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (r : rs) -> m (Rec Value out))
-> Rec Value (r : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Value r -> Value r -> Value r
forall (c :: T) (instr :: [T] -> [T] -> *).
ConcatOp c =>
Value' instr c -> Value' instr c -> Value' instr c
evalConcat Value r
a Value r
Value r
b Value r -> Rec Value rs -> Rec Value (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ CONCAT' (VList a :: [Value' Instr t]
a :& r :: Rec Value rs
r) = Rec Value (t : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (t : rs) -> m (Rec Value out))
-> Rec Value (t : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ [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 Value' Instr t -> Rec Value rs -> Rec Value (t : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ SLICE (VNat o :: Natural
o :& VNat l :: Natural
l :& s :: Value r
s :& r :: Rec Value rs
r) =
  Rec Value ('TOption r : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TOption r : rs) -> m (Rec Value out))
-> Rec Value ('TOption r : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Maybe (Value r) -> Value' Instr ('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) Value' Instr ('TOption r)
-> Rec Value rs -> Rec Value ('TOption r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ ISNAT (VInt i :: Integer
i :& r :: Rec Value rs
r) =
  if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0
  then Rec Value ('TOption 'TNat : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TOption 'TNat : rs) -> m (Rec Value out))
-> Rec Value ('TOption 'TNat : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Maybe (Value' Instr 'TNat) -> Value' Instr ('TOption 'TNat)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption Maybe (Value' Instr 'TNat)
forall a. Maybe a
Nothing Value' Instr ('TOption 'TNat)
-> Rec Value rs -> Rec Value ('TOption 'TNat : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
  else Rec Value ('TOption 'TNat : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TOption 'TNat : rs) -> m (Rec Value out))
-> Rec Value ('TOption 'TNat : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Maybe (Value' Instr 'TNat) -> Value' Instr ('TOption 'TNat)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Value' Instr 'TNat -> Maybe (Value' Instr 'TNat)
forall a. a -> Maybe a
Just (Natural -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural -> Value' Instr 'TNat) -> Natural -> Value' Instr 'TNat
forall a b. (a -> b) -> a -> b
$ Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i)) Value' Instr ('TOption 'TNat)
-> Rec Value rs -> Rec Value ('TOption 'TNat : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ ADD (l :: Value r
l :& r :: Value r
r :& rest :: Rec Value rs
rest) =
  (Value (ArithRes Add n m)
-> Rec Value rs -> Rec Value (ArithRes Add n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest) (Value (ArithRes Add n m) -> Rec Value (ArithRes Add n m : rs))
-> m (Value (ArithRes Add n m))
-> m (Rec Value (ArithRes Add n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Add -> Value r -> Value r -> m (Value (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 -> Value n -> Value m -> monad (Value (ArithRes aop n m))
runArithOp (Proxy Add
forall k (t :: k). Proxy t
Proxy @Add) Value r
l Value r
r
runInstrImpl _ SUB (l :: Value r
l :& r :: Value r
r :& rest :: Rec Value rs
rest) = (Value (ArithRes Sub n m)
-> Rec Value rs -> Rec Value (ArithRes Sub n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest) (Value (ArithRes Sub n m) -> Rec Value (ArithRes Sub n m : rs))
-> m (Value (ArithRes Sub n m))
-> m (Rec Value (ArithRes Sub n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Sub -> Value r -> Value r -> m (Value (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 -> Value n -> Value m -> monad (Value (ArithRes aop n m))
runArithOp (Proxy Sub
forall k (t :: k). Proxy t
Proxy @Sub) Value r
l Value r
r
runInstrImpl _ MUL (l :: Value r
l :& r :: Value r
r :& rest :: Rec Value rs
rest) = (Value (ArithRes Mul n m)
-> Rec Value rs -> Rec Value (ArithRes Mul n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest) (Value (ArithRes Mul n m) -> Rec Value (ArithRes Mul n m : rs))
-> m (Value (ArithRes Mul n m))
-> m (Rec Value (ArithRes Mul n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Mul -> Value r -> Value r -> m (Value (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 -> Value n -> Value m -> monad (Value (ArithRes aop n m))
runArithOp (Proxy Mul
forall k (t :: k). Proxy t
Proxy @Mul) Value r
l Value r
r
runInstrImpl _ EDIV (l :: Value r
l :& r :: Value r
r :& rest :: Rec Value rs
rest) = Rec Value ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : rs)
-> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : rs)
 -> m (Rec Value out))
-> Rec
     Value ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : rs)
-> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Value r
-> Value 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 Value r
l Value r
r Value' Instr ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
-> Rec Value rs
-> Rec
     Value ('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 Value rs
rest
runInstrImpl _ ABS (a :: Value r
a :& rest :: Rec Value rs
rest) = Rec Value (UnaryArithRes Abs n : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (UnaryArithRes Abs n : rs) -> m (Rec Value out))
-> Rec Value (UnaryArithRes Abs n : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (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) Value' Instr (UnaryArithRes Abs n)
-> Rec Value rs -> Rec Value (UnaryArithRes Abs n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest
runInstrImpl _ NEG (a :: Value r
a :& rest :: Rec Value rs
rest) = Rec Value (UnaryArithRes Neg n : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (UnaryArithRes Neg n : rs) -> m (Rec Value out))
-> Rec Value (UnaryArithRes Neg n : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (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) Value' Instr (UnaryArithRes Neg n)
-> Rec Value rs -> Rec Value (UnaryArithRes Neg n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest
runInstrImpl _ LSL (x :: Value r
x :& s :: Value r
s :& rest :: Rec Value rs
rest) = (Value (ArithRes Lsl n m)
-> Rec Value rs -> Rec Value (ArithRes Lsl n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest) (Value (ArithRes Lsl n m) -> Rec Value (ArithRes Lsl n m : rs))
-> m (Value (ArithRes Lsl n m))
-> m (Rec Value (ArithRes Lsl n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Lsl -> Value r -> Value r -> m (Value (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 -> Value n -> Value m -> monad (Value (ArithRes aop n m))
runArithOp (Proxy Lsl
forall k (t :: k). Proxy t
Proxy @Lsl) Value r
x Value r
s
runInstrImpl _ LSR (x :: Value r
x :& s :: Value r
s :& rest :: Rec Value rs
rest) = (Value (ArithRes Lsr n m)
-> Rec Value rs -> Rec Value (ArithRes Lsr n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest) (Value (ArithRes Lsr n m) -> Rec Value (ArithRes Lsr n m : rs))
-> m (Value (ArithRes Lsr n m))
-> m (Rec Value (ArithRes Lsr n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Lsr -> Value r -> Value r -> m (Value (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 -> Value n -> Value m -> monad (Value (ArithRes aop n m))
runArithOp (Proxy Lsr
forall k (t :: k). Proxy t
Proxy @Lsr) Value r
x Value r
s
runInstrImpl _ OR (l :: Value r
l :& r :: Value r
r :& rest :: Rec Value rs
rest) = (Value (ArithRes Or n m)
-> Rec Value rs -> Rec Value (ArithRes Or n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest) (Value (ArithRes Or n m) -> Rec Value (ArithRes Or n m : rs))
-> m (Value (ArithRes Or n m))
-> m (Rec Value (ArithRes Or n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Or -> Value r -> Value r -> m (Value (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 -> Value n -> Value m -> monad (Value (ArithRes aop n m))
runArithOp (Proxy Or
forall k (t :: k). Proxy t
Proxy @Or) Value r
l Value r
r
runInstrImpl _ AND (l :: Value r
l :& r :: Value r
r :& rest :: Rec Value rs
rest) = (Value (ArithRes And n m)
-> Rec Value rs -> Rec Value (ArithRes And n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest) (Value (ArithRes And n m) -> Rec Value (ArithRes And n m : rs))
-> m (Value (ArithRes And n m))
-> m (Rec Value (ArithRes And n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy And -> Value r -> Value r -> m (Value (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 -> Value n -> Value m -> monad (Value (ArithRes aop n m))
runArithOp (Proxy And
forall k (t :: k). Proxy t
Proxy @And) Value r
l Value r
r
runInstrImpl _ XOR (l :: Value r
l :& r :: Value r
r :& rest :: Rec Value rs
rest) = (Value (ArithRes Xor n m)
-> Rec Value rs -> Rec Value (ArithRes Xor n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest) (Value (ArithRes Xor n m) -> Rec Value (ArithRes Xor n m : rs))
-> m (Value (ArithRes Xor n m))
-> m (Rec Value (ArithRes Xor n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Xor -> Value r -> Value r -> m (Value (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 -> Value n -> Value m -> monad (Value (ArithRes aop n m))
runArithOp (Proxy Xor
forall k (t :: k). Proxy t
Proxy @Xor) Value r
l Value r
r
runInstrImpl _ NOT (a :: Value r
a :& rest :: Rec Value rs
rest) = Rec Value (UnaryArithRes Not n : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (UnaryArithRes Not n : rs) -> m (Rec Value out))
-> Rec Value (UnaryArithRes Not n : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (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) Value' Instr (UnaryArithRes Not n)
-> Rec Value rs -> Rec Value (UnaryArithRes Not n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest
runInstrImpl _ COMPARE (l :: Value r
l :& r :: Value r
r :& rest :: Rec Value rs
rest) = Rec Value ('TInt : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TInt : rs) -> m (Rec Value out))
-> Rec Value ('TInt : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (Integer -> Value' Instr '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)) Value' Instr 'TInt -> Rec Value rs -> Rec Value ('TInt : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest
runInstrImpl _ EQ (a :: Value r
a :& rest :: Rec Value rs
rest) = Rec Value (UnaryArithRes Eq' n : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (UnaryArithRes Eq' n : rs) -> m (Rec Value out))
-> Rec Value (UnaryArithRes Eq' n : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (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) Value' Instr (UnaryArithRes Eq' n)
-> Rec Value rs -> Rec Value (UnaryArithRes Eq' n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest
runInstrImpl _ NEQ (a :: Value r
a :& rest :: Rec Value rs
rest) = Rec Value (UnaryArithRes Neq n : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (UnaryArithRes Neq n : rs) -> m (Rec Value out))
-> Rec Value (UnaryArithRes Neq n : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (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) Value' Instr (UnaryArithRes Neq n)
-> Rec Value rs -> Rec Value (UnaryArithRes Neq n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest
runInstrImpl _ LT (a :: Value r
a :& rest :: Rec Value rs
rest) = Rec Value (UnaryArithRes Lt n : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (UnaryArithRes Lt n : rs) -> m (Rec Value out))
-> Rec Value (UnaryArithRes Lt n : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (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) Value' Instr (UnaryArithRes Lt n)
-> Rec Value rs -> Rec Value (UnaryArithRes Lt n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest
runInstrImpl _ GT (a :: Value r
a :& rest :: Rec Value rs
rest) = Rec Value (UnaryArithRes Gt n : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (UnaryArithRes Gt n : rs) -> m (Rec Value out))
-> Rec Value (UnaryArithRes Gt n : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (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) Value' Instr (UnaryArithRes Gt n)
-> Rec Value rs -> Rec Value (UnaryArithRes Gt n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest
runInstrImpl _ LE (a :: Value r
a :& rest :: Rec Value rs
rest) = Rec Value (UnaryArithRes Le n : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (UnaryArithRes Le n : rs) -> m (Rec Value out))
-> Rec Value (UnaryArithRes Le n : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (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) Value' Instr (UnaryArithRes Le n)
-> Rec Value rs -> Rec Value (UnaryArithRes Le n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest
runInstrImpl _ GE (a :: Value r
a :& rest :: Rec Value rs
rest) = Rec Value (UnaryArithRes Ge n : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value (UnaryArithRes Ge n : rs) -> m (Rec Value out))
-> Rec Value (UnaryArithRes Ge n : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (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) Value' Instr (UnaryArithRes Ge n)
-> Rec Value rs -> Rec Value (UnaryArithRes Ge n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
rest
runInstrImpl _ INT (VNat n :: Natural
n :& r :: Rec Value rs
r) = Rec Value ('TInt : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TInt : rs) -> m (Rec Value out))
-> Rec Value ('TInt : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (Integer -> Value' Instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer -> Value' Instr 'TInt) -> Integer -> Value' Instr 'TInt
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n) Value' Instr 'TInt -> Rec Value rs -> Rec Value ('TInt : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ (SELF sepc :: SomeEntryPointCallT arg
sepc :: Instr inp out) r :: Rec Value 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 Value ('TContract arg : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TContract arg : inp) -> m (Rec Value out))
-> Rec Value ('TContract arg : inp) -> m (Rec Value out)
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
ceSelf SomeEntryPointCallT arg
sepc Value' Instr ('TContract arg)
-> Rec Value inp -> Rec Value ('TContract arg : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r
runInstrImpl _ (CONTRACT (Notes p
nt :: T.Notes a) instrEpName :: EpName
instrEpName) (VAddress epAddr :: EpAddress
epAddr :& r :: Rec Value 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
  EpName
epName <- case (EpName
instrEpName, EpName
addrEpName) of
    (DefEpName, DefEpName) -> EpName -> m EpName
forall (f :: * -> *) a. Applicative f => a -> f a
pure EpName
DefEpName
    (DefEpName, en :: EpName
en) -> EpName -> m EpName
forall (f :: * -> *) a. Applicative f => a -> f a
pure EpName
en
    (en :: EpName
en, DefEpName) -> EpName -> m EpName
forall (f :: * -> *) a. Applicative f => a -> f a
pure EpName
en
    _ -> MichelsonFailed -> m EpName
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (MichelsonFailed -> m EpName) -> MichelsonFailed -> m EpName
forall a b. (a -> b) -> a -> b
$ EpName -> EpAddress -> MichelsonFailed
MichelsonAmbigousEpRef EpName
instrEpName EpAddress
epAddr

  pure $ 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 Value ('TOption ('TContract p))
-> Rec Value rs -> Rec Value ('TOption ('TContract p) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
    ContractAddress ca :: ContractHash
ca ->
      case ContractHash -> TcOriginatedContracts -> Maybe ParameterType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ContractHash
ca TcOriginatedContracts
ceContracts of
        -- Wrapping into 'ParamNotesUnsafe' is safe because originated contract has
        -- valid parameter type. Should be not necessary after [#36].
        Just tc :: ParameterType
tc@(U.ParameterType (AsUTypeExt (_ :: Sing tc) tcNotes :: Notes t
tcNotes) rootAnn :: RootAnn
rootAnn) ->
          let paramNotes :: ParamNotes t
paramNotes = Notes t -> RootAnn -> ParamNotes t
forall (t :: T). Notes t -> RootAnn -> ParamNotes t
ParamNotesUnsafe Notes t
tcNotes RootAnn
rootAnn in
          case CheckScope (ParameterScope t) =>
Either BadTypeForScope (Dict (ParameterScope t))
forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
T.checkScope @(T.ParameterScope tc) of
            Right Dict -> 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 Value ('TOption ('TContract p))
-> Rec Value rs -> Rec Value ('TOption ('TContract p) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
            _ -> Text -> Rec Value out
forall a. HasCallStack => Text -> a
error (Text -> Rec Value out) -> Text -> Rec Value out
forall a b. (a -> b) -> a -> b
$ "Illegal type in parameter of env contract: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> ParameterType -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty ParameterType
tc
            -- TODO [#36]: we can do this safely once 'TcOriginatedContracts' stores
            -- typed stuff.
        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 Value ('TOption ('TContract p))
-> Rec Value rs -> Rec Value ('TOption ('TContract p) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
  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 (p :: Value r
p :& VMutez mutez :: Mutez
mutez :& contract :: Value r
contract :& r :: Rec Value rs
r) =
  Rec Value ('TOperation : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TOperation : rs) -> m (Rec Value out))
-> Rec Value ('TOperation : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Operation -> Value' Instr '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) Value' Instr 'TOperation
-> Rec Value rs -> Rec Value ('TOperation : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ SET_DELEGATE (VOption mbKeyHash :: Maybe (Value' Instr t)
mbKeyHash :& r :: Rec Value rs
r) =
  case Maybe (Value' Instr t)
mbKeyHash of
    Just (VKeyHash k :: KeyHash
k) -> Rec Value ('TOperation : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TOperation : rs) -> m (Rec Value out))
-> Rec Value ('TOperation : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Operation -> Value' Instr '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) Value' Instr 'TOperation
-> Rec Value rs -> Rec Value ('TOperation : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
    Nothing -> Rec Value ('TOperation : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TOperation : rs) -> m (Rec Value out))
-> Rec Value ('TOperation : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Operation -> Value' Instr '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) Value' Instr 'TOperation
-> Rec Value rs -> Rec Value ('TOperation : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ (CREATE_CONTRACT contract :: Contract p g
contract)
  (VOption mbKeyHash :: Maybe (Value' Instr t)
mbKeyHash :& VMutez m :: Mutez
m :& g :: Value r
g :& r :: Rec Value 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 s (m :: * -> *). MonadState s m => m s
get
  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 s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((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 -> Address
mkContractAddress OperationHash
hash OriginationIndex
originationNonce
          Nothing ->
            OperationHash -> OriginationIndex -> Address
mkContractAddress
              (OriginationOperation -> GlobalCounter -> OperationHash
U.mkOriginationOperationHash (Address
-> Maybe (Value 'TKeyHash)
-> Mutez
-> ContractCode p g
-> Value' Instr g
-> OriginationOperation
forall (param :: T) (store :: T).
(SingI param, StorageScope store) =>
Address
-> Maybe (Value 'TKeyHash)
-> Mutez
-> ContractCode param store
-> Value' Instr store
-> OriginationOperation
createOrigOp Address
originator Maybe (Value' Instr t)
Maybe (Value 'TKeyHash)
mbKeyHash Mutez
m ContractCode p g
ops Value' Instr g
Value r
g) (Word64 -> GlobalCounter
U.GlobalCounter 0))
              -- 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 and counter set to 0.
              OriginationIndex
originationNonce
  let resEpAddr :: EpAddress
resEpAddr = Address -> EpName -> EpAddress
EpAddress Address
resAddr EpName
forall a. Default a => a
def
  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 Value ('TOperation : 'TAddress : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TOperation : 'TAddress : rs) -> m (Rec Value out))
-> Rec Value ('TOperation : 'TAddress : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Operation -> Value' Instr '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)
      Value' Instr 'TOperation
-> Rec Value ('TAddress : rs)
-> Rec Value ('TOperation : 'TAddress : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& (EpAddress -> Value' Instr 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress EpAddress
resEpAddr)
      Value' Instr 'TAddress
-> Rec Value rs -> Rec Value ('TAddress : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ IMPLICIT_ACCOUNT (VKeyHash k :: KeyHash
k :& r :: Rec Value rs
r) =
  Rec Value ('TContract 'TUnit : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TContract 'TUnit : rs) -> m (Rec Value out))
-> Rec Value ('TContract 'TUnit : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ Address
-> SomeEntryPointCallT 'TUnit -> Value' Instr ('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 Value' Instr ('TContract 'TUnit)
-> Rec Value rs -> Rec Value ('TContract 'TUnit : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ NOW r :: Rec Value inp
r = do
  ContractEnv{..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec Value ('TTimestamp : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TTimestamp : inp) -> m (Rec Value out))
-> Rec Value ('TTimestamp : inp) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (Timestamp -> Value' Instr 'TTimestamp
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp Timestamp
ceNow) Value' Instr 'TTimestamp
-> Rec Value inp -> Rec Value ('TTimestamp : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r
runInstrImpl _ AMOUNT r :: Rec Value inp
r = do
  ContractEnv{..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec Value ('TMutez : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TMutez : inp) -> m (Rec Value out))
-> Rec Value ('TMutez : inp) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (Mutez -> Value' Instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez Mutez
ceAmount) Value' Instr 'TMutez -> Rec Value inp -> Rec Value ('TMutez : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r
runInstrImpl _ BALANCE r :: Rec Value inp
r = do
  ContractEnv{..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec Value ('TMutez : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TMutez : inp) -> m (Rec Value out))
-> Rec Value ('TMutez : inp) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (Mutez -> Value' Instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez Mutez
ceBalance) Value' Instr 'TMutez -> Rec Value inp -> Rec Value ('TMutez : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r
runInstrImpl _ CHECK_SIGNATURE (VKey k :: PublicKey
k :& VSignature v :: Signature
v :&
  VBytes b :: ByteString
b :& r :: Rec Value rs
r) = Rec Value ('TBool : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TBool : rs) -> m (Rec Value out))
-> Rec Value ('TBool : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (Bool -> Value' Instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Bool -> Value' Instr 'TBool) -> Bool -> Value' Instr 'TBool
forall a b. (a -> b) -> a -> b
$ PublicKey -> Signature -> ByteString -> Bool
checkSignature PublicKey
k Signature
v ByteString
b) Value' Instr 'TBool -> Rec Value rs -> Rec Value ('TBool : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ SHA256 (VBytes b :: ByteString
b :& r :: Rec Value rs
r) = Rec Value ('TBytes : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TBytes : rs) -> m (Rec Value out))
-> Rec Value ('TBytes : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (ByteString -> Value' Instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value' Instr 'TBytes)
-> ByteString -> Value' Instr 'TBytes
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
sha256 ByteString
b) Value' Instr 'TBytes -> Rec Value rs -> Rec Value ('TBytes : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ SHA512 (VBytes b :: ByteString
b :& r :: Rec Value rs
r) = Rec Value ('TBytes : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TBytes : rs) -> m (Rec Value out))
-> Rec Value ('TBytes : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (ByteString -> Value' Instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value' Instr 'TBytes)
-> ByteString -> Value' Instr 'TBytes
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
sha512 ByteString
b) Value' Instr 'TBytes -> Rec Value rs -> Rec Value ('TBytes : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ BLAKE2B (VBytes b :: ByteString
b :& r :: Rec Value rs
r) = Rec Value ('TBytes : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TBytes : rs) -> m (Rec Value out))
-> Rec Value ('TBytes : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (ByteString -> Value' Instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value' Instr 'TBytes)
-> ByteString -> Value' Instr 'TBytes
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
blake2b ByteString
b) Value' Instr 'TBytes -> Rec Value rs -> Rec Value ('TBytes : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ HASH_KEY (VKey k :: PublicKey
k :& r :: Rec Value rs
r) = Rec Value ('TKeyHash : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TKeyHash : rs) -> m (Rec Value out))
-> Rec Value ('TKeyHash : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (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) Value 'TKeyHash -> Rec Value rs -> Rec Value ('TKeyHash : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ SOURCE r :: Rec Value inp
r = do
  ContractEnv{..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec Value ('TAddress : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TAddress : inp) -> m (Rec Value out))
-> Rec Value ('TAddress : inp) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (EpAddress -> Value' Instr 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (EpAddress -> Value' Instr 'TAddress)
-> EpAddress -> Value' Instr 'TAddress
forall a b. (a -> b) -> a -> b
$ Address -> EpName -> EpAddress
EpAddress Address
ceSource EpName
forall a. Default a => a
def) Value' Instr 'TAddress
-> Rec Value inp -> Rec Value ('TAddress : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r
runInstrImpl _ SENDER r :: Rec Value inp
r = do
  ContractEnv{..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec Value ('TAddress : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TAddress : inp) -> m (Rec Value out))
-> Rec Value ('TAddress : inp) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (EpAddress -> Value' Instr 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (EpAddress -> Value' Instr 'TAddress)
-> EpAddress -> Value' Instr 'TAddress
forall a b. (a -> b) -> a -> b
$ Address -> EpName -> EpAddress
EpAddress Address
ceSender EpName
forall a. Default a => a
def) Value' Instr 'TAddress
-> Rec Value inp -> Rec Value ('TAddress : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r
runInstrImpl _ ADDRESS (VContract a :: Address
a sepc :: SomeEntryPointCallT arg
sepc :& r :: Rec Value rs
r) =
  Rec Value ('TAddress : rs) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TAddress : rs) -> m (Rec Value out))
-> Rec Value ('TAddress : rs) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ (EpAddress -> Value' Instr 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (EpAddress -> Value' Instr 'TAddress)
-> EpAddress -> Value' Instr '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)) Value' Instr 'TAddress
-> Rec Value rs -> Rec Value ('TAddress : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value rs
r
runInstrImpl _ CHAIN_ID r :: Rec Value inp
r = do
  ContractEnv{..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec Value ('TChainId : inp) -> m (Rec Value out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec Value ('TChainId : inp) -> m (Rec Value out))
-> Rec Value ('TChainId : inp) -> m (Rec Value out)
forall a b. (a -> b) -> a -> b
$ ChainId -> Value' Instr 'TChainId
forall (instr :: [T] -> [T] -> *).
ChainId -> Value' instr 'TChainId
VChainId ChainId
ceChainId Value' Instr 'TChainId
-> Rec Value inp -> Rec Value ('TChainId : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value inp
r

-- | Evaluates an arithmetic operation and either fails or proceeds.
runArithOp
  :: (ArithOp aop n m, Typeable n, Typeable m, EvalM monad)
  => proxy aop
  -> Value n
  -> Value m
  -> monad (Value (ArithRes aop n m))
runArithOp :: proxy aop -> Value n -> Value m -> monad (Value (ArithRes aop n m))
runArithOp op :: proxy aop
op l :: Value n
l r :: Value m
r = case proxy aop
-> Value n
-> Value m
-> Either
     (ArithError (Value n) (Value m)) (Value (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 Value n
l Value m
r of
  Left  err :: ArithError (Value n) (Value m)
err -> MichelsonFailed -> monad (Value (ArithRes aop n m))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (ArithError (Value n) (Value 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 n) (Value m)
err)
  Right res :: Value (ArithRes aop n m)
res -> Value (ArithRes aop n m) -> monad (Value (ArithRes aop n m))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value (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
  :: (SingI param, StorageScope store)
  => Address
  -> Maybe (T.Value 'T.TKeyHash)
  -> Mutez
  -> ContractCode param store
  -> Value' Instr store
  -> U.OriginationOperation
createOrigOp :: Address
-> Maybe (Value 'TKeyHash)
-> Mutez
-> ContractCode param store
-> Value' Instr store
-> OriginationOperation
createOrigOp originator :: Address
originator mbDelegate :: Maybe (Value 'TKeyHash)
mbDelegate bal :: Mutez
bal contract :: ContractCode param store
contract g :: Value' Instr store
g =
  $WOriginationOperation :: Address
-> Maybe KeyHash
-> Mutez
-> Value
-> Contract
-> OriginationOperation
U.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
ooStorage = Value' Instr store -> Value
forall (t :: T). (SingI t, HasNoOp t) => Value' Instr t -> Value
untypeValue Value' Instr store
g
    , ooContract :: Contract
ooContract = ContractCode param store -> Contract
forall (param :: T) (store :: T).
(SingI param, SingI store) =>
ContractCode param store -> Contract
convertContractCode ContractCode 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 => SomeItStack -> m ()
interpretExt :: SomeItStack -> m ()
interpretExt (SomeItStack (T.PRINT (T.PrintComment pc :: [Either Text (StackRef inp)]
pc)) st :: Rec Value 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 Value inp -> (forall (t :: T). Value t -> Text) -> Text
forall (st :: [T]) a.
StackRef st -> Rec Value st -> (forall (t :: T). Value t -> a) -> a
withStackElem StackRef inp
str Rec Value inp
st forall b a. (Show a, IsString b) => a -> b
forall (t :: T). Value t -> Text
show
  (InterpreterState -> InterpreterState) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\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]
unMorleyLogs (InterpreterState -> MorleyLogs
isMorleyLogs InterpreterState
s)})

interpretExt (SomeItStack (T.TEST_ASSERT (T.TestAssert nm :: Text
nm pc :: PrintComment inp
pc instr :: Instr inp ('TBool : out)
instr)) st :: Rec Value inp
st) = do
  Rec Value ('TBool : out)
ost <- Instr inp ('TBool : out)
-> Rec Value inp -> m (Rec Value ('TBool : out))
forall (m :: * -> *). EvalM m => InstrRunner m
runInstrNoGas Instr inp ('TBool : out)
instr Rec Value inp
st
  let ((Value r -> Bool
forall a. IsoValue a => Value (ToT a) -> a
T.fromVal -> Bool
succeeded) :& _) = Rec Value ('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
    SomeItStack -> m ()
forall (m :: * -> *). EvalM m => SomeItStack -> m ()
interpretExt (ExtInstr inp -> Rec Value inp -> SomeItStack
forall (inp :: [T]). ExtInstr inp -> Rec Value inp -> SomeItStack
SomeItStack (PrintComment inp -> ExtInstr inp
forall (s :: [T]). PrintComment s -> ExtInstr s
T.PRINT PrintComment inp
pc) Rec Value 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 T.Value st
  -> (forall t. T.Value t -> a)
  -> a
withStackElem :: StackRef st -> Rec Value st -> (forall (t :: T). Value t -> a) -> a
withStackElem (T.StackRef sn :: Sing idx
sn) vals :: Rec Value st
vals cont :: forall (t :: T). Value t -> a
cont =
  (Rec Value st, Sing idx) -> a
forall (s :: [T]) (n :: Peano).
LongerThan s n =>
(Rec Value s, Sing n) -> a
loop (Rec Value st
vals, Sing idx
sn)
  where
    loop
      :: forall s (n :: Peano). (LongerThan s n)
      => (Rec T.Value s, Sing n) -> a
    loop :: (Rec Value s, Sing n) -> a
loop = \case
      (e :: Value r
e :& _, SZ) -> Value r -> a
forall (t :: T). Value t -> a
cont Value r
e
      (_ :& es :: Rec Value rs
es, SS n) -> (Rec Value rs, Sing n) -> a
forall (s :: [T]) (n :: Peano).
LongerThan s n =>
(Rec Value s, Sing n) -> a
loop (Rec Value rs
es, Sing n
SingNat n
n)

(deriveGADTNFData ''MichelsonFailed)