-- 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
  , 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)

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

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

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

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

deriving stock instance Show InterpretError

instance Buildable InterpretError where
  build :: InterpretError -> Builder
build = InterpretError -> 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 []

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

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

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 (WithLoc _ i :: Instr inp out
i) 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
i Rec Value inp
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 _ (AnnPAIR{}) (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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
Instr i o
PAIR Instr (i : s) ('TPair r i : s)
-> Instr ('TPair r i : s) o -> Instr (i : s) o
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr ('TPair r i : s) o -> Instr ('TPair r i : s) o
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
Nested Instr ('TPair r i : s) o
b
runInstrImpl runner :: InstrRunner m
runner (DIP i :: Instr a c
i) (a :: 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 SomeParamType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ContractHash
ca TcOriginatedContracts
ceContracts of
        Just (SomeParamType _ paramNotes :: ParamNotes t
paramNotes) ->
          Address
-> EpName -> ParamNotes t -> Value ('TOption ('TContract p))
forall (p :: T).
ParameterScope p =>
Address
-> EpName -> ParamNotes p -> Value ('TOption ('TContract p))
castContract Address
addr EpName
epName ParamNotes t
paramNotes 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
        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) -> m OriginationIndex
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets InterpreterState -> OriginationIndex
isOriginationNonce
  GlobalCounter
globalCounter <- (ContractEnv -> GlobalCounter) -> m GlobalCounter
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ContractEnv -> GlobalCounter
ceGlobalCounter
  Maybe OperationHash
opHash <- ContractEnv -> Maybe OperationHash
ceOperationHash (ContractEnv -> Maybe OperationHash)
-> m ContractEnv -> m (Maybe OperationHash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  (InterpreterState -> InterpreterState) -> m ()
forall 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 -> GlobalCounter -> Address
mkContractAddress OperationHash
hash OriginationIndex
originationNonce GlobalCounter
globalCounter
          Nothing ->
            OperationHash -> OriginationIndex -> GlobalCounter -> Address
mkContractAddress
              (OriginationOperation -> OperationHash
mkOriginationOperationHash (Address
-> Maybe (Value 'TKeyHash)
-> Mutez
-> Contract p g
-> Value' Instr g
-> OriginationOperation
forall (param :: T) (store :: T).
(ParameterScope param, StorageScope store) =>
Address
-> Maybe (Value 'TKeyHash)
-> Mutez
-> Contract param store
-> Value' Instr store
-> OriginationOperation
createOrigOp Address
originator Maybe (Value' Instr t)
Maybe (Value 'TKeyHash)
mbKeyHash Mutez
m Contract p g
contract Value' Instr g
Value r
g))
              -- If opHash is Nothing it means that interpreter is running in some kind of test
              -- context, therefore we generate dummy contract address with its own origination
              -- operation.
              OriginationIndex
originationNonce
              GlobalCounter
globalCounter
  let resEpAddr :: EpAddress
resEpAddr = Address -> EpName -> EpAddress
EpAddress Address
resAddr EpName
DefEpName
  let resOp :: CreateContract Instr p r
resOp = Address
-> Maybe KeyHash
-> Mutez
-> Value r
-> Instr (ContractInp p r) (ContractOut r)
-> CreateContract Instr p r
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
(Show (instr (ContractInp cp st) (ContractOut st)),
 Eq (instr (ContractInp cp st) (ContractOut st))) =>
Address
-> Maybe KeyHash
-> Mutez
-> Value' instr st
-> instr (ContractInp cp st) (ContractOut st)
-> CreateContract instr cp st
CreateContract Address
originator (Maybe (Value 'TKeyHash) -> Maybe KeyHash
unwrapMbKeyHash Maybe (Value' Instr t)
Maybe (Value 'TKeyHash)
mbKeyHash) Mutez
m Value r
g ContractCode p g
Instr (ContractInp p r) (ContractOut r)
ops
  Rec 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
DefEpName) 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
DefEpName) 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
  :: (ParameterScope param, StorageScope store)
  => Address
  -> Maybe (T.Value 'T.TKeyHash)
  -> Mutez
  -> Contract param store
  -> Value' Instr store
  -> OriginationOperation
createOrigOp :: Address
-> Maybe (Value 'TKeyHash)
-> Mutez
-> Contract param store
-> Value' Instr store
-> OriginationOperation
createOrigOp originator :: Address
originator mbDelegate :: Maybe (Value 'TKeyHash)
mbDelegate bal :: Mutez
bal contract :: Contract param store
contract storage :: Value' Instr store
storage =
  $WOriginationOperation :: forall (cp :: T) (st :: T).
(StorageScope st, ParameterScope cp) =>
Address
-> Maybe KeyHash
-> Mutez
-> Value st
-> Contract cp st
-> OriginationOperation
OriginationOperation
    { ooOriginator :: Address
ooOriginator = Address
originator
    , ooDelegate :: Maybe KeyHash
ooDelegate = Maybe (Value 'TKeyHash) -> Maybe KeyHash
unwrapMbKeyHash Maybe (Value 'TKeyHash)
mbDelegate
    , ooBalance :: Mutez
ooBalance = Mutez
bal
    , ooStorage :: Value' Instr store
ooStorage = Value' Instr store
storage
    , ooContract :: Contract param store
ooContract = Contract param store
contract
    }

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

interpretExt :: EvalM m => 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)