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

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

  , interpret
  , interpretInstr
  , interpretInstrAnnotated
  , ContractReturn

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

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

import Prelude hiding (EQ, GT, LT)

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

import Michelson.Interpret.Pack (packValue')
import Michelson.Interpret.Unpack (UnpackError, unpackValue')
import Michelson.Runtime.GState
import Michelson.TypeCheck (SomeParamType(..), TcOriginatedContracts, matchTypes)
import Michelson.Typed hiding (Branch(..))
import qualified Michelson.Typed as T
import Michelson.Typed.Origination
  (OperationHash(..), OriginationOperation(..), mkContractAddress, mkOriginationOperationHash)
import qualified Michelson.Untyped as U
import Michelson.Untyped.Annotation (annQ)
import Tezos.Address (Address(..), GlobalCounter(..), OriginationIndex(..))
import Tezos.Core (ChainId, Mutez, Timestamp)
import Tezos.Crypto (KeyHash, blake2b, checkSignature, hashKey, keccak, sha256, sha3, sha512)
import Tezos.Crypto.BLS12381 (checkPairing)
import Util.Peano (LongerThan, Peano)
import Util.PeanoNatural (PeanoNatural(..))
import Util.Sing (eqParamSing)
import Util.TH
import Util.Type
import Util.Typeable

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

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

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

instance NFData MorleyLogs

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

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
  , InterpreterState -> BigMapCounter
isBigMapCounter :: BigMapCounter
  } 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
makeLensesFor
  [ ("isMorleyLogs", "isMorleyLogsL")
  , ("isBigMapCounter", "isBigMapCounterL")
  ]
  ''InterpreterState

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

makeLensesFor
  [ ("seValue", "seValueL")
  , ("seVarAnn", "seVarAnnL")
  ]
  ''StkEl

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

-- | 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 -> VotingPowers
ceVotingPowers :: VotingPowers
  -- ^ Distribution of voting power.
  , ContractEnv -> ChainId
ceChainId :: ChainId
  -- ^ Identifier of the current chain.
  , ContractEnv -> Maybe OperationHash
ceOperationHash :: Maybe 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.
  , ContractEnv -> Natural
ceLevel :: Natural
  -- ^ Number of blocks before the given one in the chain
  }

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

deriving stock instance Show MichelsonFailed

instance Eq MichelsonFailed where
  MichelsonFailedWith Value t
v1 == :: MichelsonFailed -> MichelsonFailed -> Bool
== MichelsonFailedWith Value t
v2 = Value t
v1 Value t -> Value t -> Bool
forall k (a1 :: k) (a2 :: k) (t :: k -> *).
(SingI a1, SingI a2, SDecide k, Eq (t a1)) =>
t a1 -> t a2 -> Bool
`eqParamSing` Value t
v2
  MichelsonFailedWith Value t
_ == MichelsonFailed
_ = Bool
False
  MichelsonArithError ArithError (Value' instr n) (Value' instr m)
ae1 == MichelsonArithError 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 ArithError (Value' instr n) (Value' instr m)
_ == MichelsonFailed
_ = Bool
False
  MichelsonFailed
MichelsonGasExhaustion == MichelsonFailed
MichelsonGasExhaustion = Bool
True
  MichelsonFailed
MichelsonGasExhaustion == MichelsonFailed
_ = Bool
False
  MichelsonFailedTestAssert Text
t1 == MichelsonFailedTestAssert Text
t2 = Text
t1 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
t2
  MichelsonFailedTestAssert Text
_ == MichelsonFailed
_ = Bool
False

instance Buildable MichelsonFailed where
  build :: MichelsonFailed -> Builder
build =
    \case
      MichelsonFailedWith (Value t
v :: T.Value t) ->
        Builder
"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 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
      MichelsonFailed
MichelsonGasExhaustion ->
        Builder
"Gas limit exceeded on contract execution"
      MichelsonFailedTestAssert Text
t -> Text -> Builder
forall p. Buildable p => p -> Builder
build Text
t
    where
      formatValue :: forall t . SingI t => Value t -> Builder
      formatValue :: Value t -> Builder
formatValue 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
          OpPresence t
OpPresent -> Builder
"<value with operations>"
          OpPresence t
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 (MichelsonFailed
mf, MorleyLogs
_)) = MichelsonFailed -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> b
prettyLn MichelsonFailed
mf

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

deriving stock instance Show InterpretResult

constructIR ::
  (StorageScope st) =>
  (([Operation], Value' Instr st), InterpreterState) ->
  InterpretResult
constructIR :: (([Operation], Value' Instr st), InterpreterState)
-> InterpretResult
constructIR (([Operation]
ops, Value' Instr st
val), InterpreterState
st) =
  InterpretResult :: 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
  }

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 (Either MichelsonFailed ([Operation], Value st)
ei, 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Function to interpret Michelson instruction(s) against given stack.
runInstrImpl :: forall m. EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl :: InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner (Seq Instr inp b
i1 Instr b out
i2) Rec StkEl inp
r = Instr inp b -> Rec StkEl inp -> m (Rec StkEl b)
InstrRunner m
runner Instr inp b
i1 Rec StkEl inp
r m (Rec StkEl b)
-> (Rec StkEl b -> m (Rec StkEl out)) -> m (Rec StkEl out)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Rec StkEl b
r' -> Instr b out -> Rec StkEl b -> m (Rec StkEl out)
InstrRunner m
runner Instr b out
i2 Rec StkEl b
r'
runInstrImpl InstrRunner m
runner (WithLoc InstrCallStack
_ Instr inp out
i) Rec StkEl inp
r = Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
InstrRunner m
runner Instr inp out
i Rec StkEl inp
r
runInstrImpl InstrRunner m
runner (InstrWithNotes (Proxy s
_ :: Proxy rest) Rec Notes topElems
notes Instr inp (topElems ++ s)
instr) Rec StkEl inp
inp = do
  Rec StkEl out
out <- Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
InstrRunner m
runner Instr inp out
Instr inp (topElems ++ s)
instr Rec StkEl inp
inp
  let zipRec :: Rec Notes topElems -> Rec StkEl (topElems ++ rest) -> Rec StkEl (topElems ++ rest)
      zipRec :: Rec Notes topElems
-> Rec StkEl (topElems ++ s) -> Rec StkEl (topElems ++ s)
zipRec Rec Notes topElems
RNil Rec StkEl (topElems ++ s)
stkElems = Rec StkEl (topElems ++ s)
stkElems
      zipRec (Notes r
stkElemNotes :& Rec Notes rs
xs) (StkEl r
stkElem :& Rec StkEl rs
ys) =
        StkEl r
stkElem { seNotes :: Notes r
seNotes = Notes r
Notes r
stkElemNotes } StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Notes rs -> Rec StkEl (rs ++ s) -> Rec StkEl (rs ++ s)
forall (topElems :: [T]).
Rec Notes topElems
-> Rec StkEl (topElems ++ s) -> Rec StkEl (topElems ++ s)
zipRec Rec Notes rs
xs Rec StkEl rs
Rec StkEl (rs ++ s)
ys
  Rec StkEl out -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl out -> m (Rec StkEl out))
-> Rec StkEl out -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Rec Notes topElems
-> Rec StkEl (topElems ++ s) -> Rec StkEl (topElems ++ s)
forall (topElems :: [T]).
Rec Notes topElems
-> Rec StkEl (topElems ++ s) -> Rec StkEl (topElems ++ s)
zipRec Rec Notes topElems
notes Rec StkEl out
Rec StkEl (topElems ++ s)
out
runInstrImpl InstrRunner m
runner (InstrWithVarNotes NonEmpty VarAnn
_vns Instr inp out
i) Rec StkEl inp
inp = Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
InstrRunner m
runner Instr inp out
i Rec StkEl inp
inp
runInstrImpl InstrRunner m
runner (InstrWithVarAnns VarAnns
vns Instr inp out
i) Rec StkEl inp
inp = do
  Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
InstrRunner m
runner Instr inp out
i Rec StkEl inp
inp m (Rec StkEl out)
-> (Rec StkEl out -> Rec StkEl out) -> m (Rec StkEl out)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    StkEl Value r
v1 VarAnn
_ Notes r
n1 :& StkEl Value r
v2 VarAnn
vn2 Notes r
n2 :& Rec StkEl rs
r -> case VarAnns
vns of
      U.OneVarAnn VarAnn
vn      -> Value r -> VarAnn -> Notes r -> StkEl r
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value r
v1 VarAnn
vn Notes r
n1 StkEl r -> Rec StkEl (r : rs) -> Rec StkEl (r : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Value r -> VarAnn -> Notes r -> StkEl r
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value r
v2 VarAnn
vn2 Notes r
n2 StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
      U.TwoVarAnns VarAnn
vn VarAnn
vn' -> Value r -> VarAnn -> Notes r -> StkEl r
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value r
v1 VarAnn
vn Notes r
n1 StkEl r -> Rec StkEl (r : rs) -> Rec StkEl (r : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Value r -> VarAnn -> Notes r -> StkEl r
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value r
v2 VarAnn
vn' Notes r
n2 StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
    StkEl Value r
v VarAnn
_ Notes r
n :& Rec StkEl rs
r -> case VarAnns
vns of
      U.OneVarAnn VarAnn
vn   -> Value r -> VarAnn -> Notes r -> StkEl r
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value r
v VarAnn
vn Notes r
n StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
      U.TwoVarAnns VarAnn
_ VarAnn
_ -> Text -> Rec StkEl out
forall a. HasCallStack => Text -> a
error Text
"Input stack is exhausted but there is still a variable annotation."
    Rec StkEl out
RNil -> Text -> Rec StkEl out
forall a. HasCallStack => Text -> a
error Text
"Input stack is exhausted but there is still variables annotations."
runInstrImpl InstrRunner m
runner (FrameInstr (Proxy s
_ :: Proxy s) Instr a b
i) Rec StkEl inp
r = do
  let (Rec StkEl a
inp, Rec StkEl s
end) = Rec StkEl (a ++ s) -> (Rec StkEl a, Rec StkEl s)
forall k (l :: [k]) (r :: [k]) (f :: k -> *).
RSplit l r =>
Rec f (l ++ r) -> (Rec f l, Rec f r)
rsplit @_ @_ @s Rec StkEl inp
Rec StkEl (a ++ s)
r
  Rec StkEl b
out <- InstrRunner m -> Instr a b -> Rec StkEl a -> m (Rec StkEl b)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner Instr a b
i Rec StkEl a
inp
  return (Rec StkEl b
out Rec StkEl b -> Rec StkEl s -> Rec StkEl (b ++ s)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Rec StkEl s
end)
runInstrImpl InstrRunner m
_ Instr inp out
Nop Rec StkEl inp
r = Rec StkEl inp -> m (Rec StkEl inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl inp -> m (Rec StkEl inp))
-> Rec StkEl inp -> m (Rec StkEl inp)
forall a b. (a -> b) -> a -> b
$ Rec StkEl inp
r
runInstrImpl InstrRunner m
runner (Ext ExtInstr inp
nop) Rec StkEl inp
r = Rec StkEl inp
r Rec StkEl inp -> m () -> m (Rec StkEl inp)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ InstrRunner m -> SomeItStack -> m ()
forall (m :: * -> *).
EvalM m =>
InstrRunner m -> SomeItStack -> m ()
interpretExt InstrRunner m
runner (ExtInstr inp -> Rec StkEl inp -> SomeItStack
forall (inp :: [T]). ExtInstr inp -> Rec StkEl inp -> SomeItStack
SomeItStack ExtInstr inp
nop Rec StkEl inp
r)
runInstrImpl InstrRunner m
runner (Nested Instr inp out
sq) Rec StkEl inp
r = Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
InstrRunner m
runner Instr inp out
sq Rec StkEl inp
r
runInstrImpl InstrRunner m
runner (DocGroup DocGrouping
_ Instr inp out
sq) Rec StkEl inp
r = InstrRunner m
-> Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner Instr inp out
sq Rec StkEl inp
r
runInstrImpl InstrRunner m
runner (Fn Text
_ StackFn
_ Instr inp out
i) Rec StkEl inp
r = Instr inp out -> Rec StkEl inp -> m (Rec StkEl out)
InstrRunner m
runner Instr inp out
i Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
DROP (StkEl r
_ :& Rec StkEl rs
r) = Rec StkEl rs -> m (Rec StkEl rs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl rs -> m (Rec StkEl rs))
-> Rec StkEl rs -> m (Rec StkEl rs)
forall a b. (a -> b) -> a -> b
$ Rec StkEl rs
r
runInstrImpl InstrRunner m
runner (DROPN PeanoNatural n
n) Rec StkEl inp
stack =
  case PeanoNatural n
n of
    PeanoNatural n
Zero    -> Rec StkEl inp -> m (Rec StkEl inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec StkEl inp
stack
    Succ PeanoNatural m
s' -> case Rec StkEl inp
stack of
      (StkEl r
_ :& Rec StkEl rs
r) -> InstrRunner m -> Instr rs out -> Rec StkEl rs -> m (Rec StkEl out)
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner (PeanoNatural m -> Instr rs (Drop m rs)
forall (n :: Peano) (s :: [T]).
(RequireLongerOrSameLength s n, NFData (Sing n)) =>
PeanoNatural n -> Instr s (Drop n s)
DROPN PeanoNatural m
s') Rec StkEl rs
r
      -- 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'.
runInstrImpl InstrRunner m
_ Instr inp out
DUP (StkEl r
stkEl :& Rec StkEl rs
r) = do
  -- If we're duplicating a big_map, or a value containing big_map(s), we need to generate new big_map ID(s).
  StkEl r
duplicateStkEl <- LensLike m (StkEl r) (StkEl r) (Value r) (Value r)
-> LensLike m (StkEl r) (StkEl r) (Value r) (Value r)
forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf LensLike m (StkEl r) (StkEl r) (Value r) (Value r)
forall (t :: T). Lens' (StkEl t) (Value t)
seValueL Value r -> m (Value r)
forall (m :: * -> *) (t :: T). EvalM m => Value t -> m (Value t)
assignBigMapIds' StkEl r
stkEl
  pure $ StkEl r
duplicateStkEl StkEl r -> Rec StkEl (r : rs) -> Rec StkEl (r : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StkEl r
stkEl StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ (DUPN PeanoNatural n
s) Rec StkEl inp
stack = PeanoNatural n -> Rec StkEl inp -> m (Rec StkEl out)
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDUPN n inp out a =>
PeanoNatural n -> Rec StkEl inp -> m (Rec StkEl out)
go PeanoNatural n
s Rec StkEl inp
stack
  where
    go :: forall (n :: Peano) inp out a. ConstraintDUPN n inp out a
       => PeanoNatural n -> Rec StkEl inp -> m (Rec StkEl out)
    go :: PeanoNatural n -> Rec StkEl inp -> m (Rec StkEl out)
go (Succ PeanoNatural m
Zero) stk :: Rec StkEl inp
stk@(StkEl r
stkEl :& Rec StkEl rs
_) = do
        -- If we're duplicating a big_map, or a value containing big_map(s), we need to generate new big_map ID(s).
        StkEl r
duplicateStkEl <- LensLike m (StkEl r) (StkEl r) (Value r) (Value r)
-> LensLike m (StkEl r) (StkEl r) (Value r) (Value r)
forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf LensLike m (StkEl r) (StkEl r) (Value r) (Value r)
forall (t :: T). Lens' (StkEl t) (Value t)
seValueL Value r -> m (Value r)
forall (m :: * -> *) (t :: T). EvalM m => Value t -> m (Value t)
assignBigMapIds' StkEl r
stkEl
        -- Discard variable annotations. This is consistent with tezos-client.
        pure $ (StkEl r
duplicateStkEl StkEl r -> (StkEl r -> StkEl r) -> StkEl r
forall a b. a -> (a -> b) -> b
& (VarAnn -> Identity VarAnn) -> StkEl r -> Identity (StkEl r)
forall (t :: T). Lens' (StkEl t) VarAnn
seVarAnnL ((VarAnn -> Identity VarAnn) -> StkEl r -> Identity (StkEl r))
-> VarAnn -> StkEl r -> StkEl r
forall s t a b. ASetter s t a b -> b -> s -> t
.~ VarAnn
forall k (a :: k). Annotation a
U.noAnn) StkEl r -> Rec StkEl inp -> Rec StkEl (r : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
stk
    go (Succ n :: PeanoNatural m
n@(Succ PeanoNatural m
_)) (StkEl r
b :& Rec StkEl rs
r) =
      PeanoNatural m -> Rec StkEl rs -> m (Rec StkEl (a : rs))
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDUPN n inp out a =>
PeanoNatural n -> Rec StkEl inp -> m (Rec StkEl out)
go PeanoNatural m
n Rec StkEl rs
r m (Rec StkEl (a : rs))
-> (Rec StkEl (a : rs) -> Rec StkEl out) -> m (Rec StkEl out)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
        (StkEl r
a :& Rec StkEl rs
resTail) -> StkEl r
a StkEl r -> Rec StkEl (r : rs) -> Rec StkEl (r : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StkEl r
b StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
resTail
runInstrImpl InstrRunner m
_ Instr inp out
SWAP (StkEl r
a :& StkEl r
b :& Rec StkEl rs
r) = Rec StkEl (r : r : rs) -> m (Rec StkEl (r : r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : r : rs) -> m (Rec StkEl (r : r : rs)))
-> Rec StkEl (r : r : rs) -> m (Rec StkEl (r : r : rs))
forall a b. (a -> b) -> a -> b
$ StkEl r
b StkEl r -> Rec StkEl (r : rs) -> Rec StkEl (r : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StkEl r
a StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ (DIG PeanoNatural n
s) Rec StkEl inp
input0 =
  Rec StkEl out -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl out -> m (Rec StkEl out))
-> Rec StkEl out -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ PeanoNatural n -> Rec StkEl inp -> Rec StkEl out
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDIG n inp out a =>
PeanoNatural n -> Rec StkEl inp -> Rec StkEl out
go PeanoNatural n
s Rec StkEl inp
input0
  where
    go :: forall (n :: Peano) inp out a. ConstraintDIG n inp out a
       => PeanoNatural n -> Rec StkEl inp -> Rec StkEl out
    go :: PeanoNatural n -> Rec StkEl inp -> Rec StkEl out
go PeanoNatural n
Zero Rec StkEl inp
stack = Rec StkEl inp
Rec StkEl out
stack
    go (Succ PeanoNatural m
n') (StkEl r
b :& Rec StkEl rs
r) = case PeanoNatural m
-> Rec StkEl rs -> Rec StkEl (a : (Take m rs ++ Drop ('S n) inp))
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDIG n inp out a =>
PeanoNatural n -> Rec StkEl inp -> Rec StkEl out
go PeanoNatural m
n' Rec StkEl rs
r of
      (StkEl r
a :& Rec StkEl rs
resTail) -> StkEl r
a StkEl r -> Rec StkEl (r : rs) -> Rec StkEl (r : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StkEl r
b StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
resTail
runInstrImpl InstrRunner m
_ (DUG PeanoNatural n
s) Rec StkEl inp
input0 =
  Rec StkEl out -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl out -> m (Rec StkEl out))
-> Rec StkEl out -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ PeanoNatural n -> Rec StkEl inp -> Rec StkEl out
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDUG n inp out a =>
PeanoNatural n -> Rec StkEl inp -> Rec StkEl out
go PeanoNatural n
s Rec StkEl inp
input0
  where
    go :: forall (n :: Peano) inp out a. ConstraintDUG n inp out a
       => PeanoNatural n -> Rec StkEl inp -> Rec StkEl out
    go :: PeanoNatural n -> Rec StkEl inp -> Rec StkEl out
go PeanoNatural n
Zero Rec StkEl inp
stack = Rec StkEl inp
Rec StkEl out
stack
    go (Succ PeanoNatural m
n') (StkEl r
a :& StkEl r
b :& Rec StkEl rs
r) = StkEl r
b StkEl r
-> Rec StkEl (Take m rs ++ (a : Drop n (Drop ('S 'Z) inp)))
-> Rec StkEl (r : (Take m 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)
:& PeanoNatural m
-> Rec StkEl (r : rs)
-> Rec StkEl (Take m rs ++ (a : Drop n (Drop ('S 'Z) inp)))
forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDUG n inp out a =>
PeanoNatural n -> Rec StkEl inp -> Rec StkEl out
go PeanoNatural m
n' (StkEl r
a StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
runInstrImpl InstrRunner m
_ Instr inp out
SOME ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& Rec StkEl rs
r) =
  Value r -> (SingI r => m (Rec StkEl out)) -> m (Rec StkEl out)
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value r
a ((SingI r => m (Rec StkEl out)) -> m (Rec StkEl out))
-> (SingI r => m (Rec StkEl out)) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$
    Rec StkEl ('TOption r : rs) -> m (Rec StkEl ('TOption r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption r : rs) -> m (Rec StkEl ('TOption r : rs)))
-> Rec StkEl ('TOption r : rs) -> m (Rec StkEl ('TOption r : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TOption r) -> StkEl ('TOption r)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value r) -> Value ('TOption r)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Value r -> Maybe (Value r)
forall a. a -> Maybe a
Just Value r
a)) StkEl ('TOption r) -> Rec StkEl rs -> Rec StkEl ('TOption r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ (PUSH Value' Instr t
v) Rec StkEl inp
r = Rec StkEl (t : inp) -> m (Rec StkEl (t : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (t : inp) -> m (Rec StkEl (t : inp)))
-> Rec StkEl (t : inp) -> m (Rec StkEl (t : inp))
forall a b. (a -> b) -> a -> b
$ Value' Instr t -> StkEl t
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr t
v StkEl t -> Rec StkEl inp -> Rec StkEl (t : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
NONE Rec StkEl inp
r = Rec StkEl ('TOption a : inp) -> m (Rec StkEl ('TOption a : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption a : inp) -> m (Rec StkEl ('TOption a : inp)))
-> Rec StkEl ('TOption a : inp) -> m (Rec StkEl ('TOption a : inp))
forall a b. (a -> b) -> a -> b
$ Value ('TOption a) -> StkEl ('TOption a)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value' Instr a) -> Value ('TOption a)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption Maybe (Value' Instr a)
forall a. Maybe a
Nothing) StkEl ('TOption a) -> Rec StkEl inp -> Rec StkEl ('TOption a : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
UNIT Rec StkEl inp
r = Rec StkEl ('TUnit : inp) -> m (Rec StkEl ('TUnit : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TUnit : inp) -> m (Rec StkEl ('TUnit : inp)))
-> Rec StkEl ('TUnit : inp) -> m (Rec StkEl ('TUnit : inp))
forall a b. (a -> b) -> a -> b
$ Value 'TUnit -> StkEl 'TUnit
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value 'TUnit
forall (instr :: [T] -> [T] -> *). Value' instr 'TUnit
VUnit StkEl 'TUnit -> Rec StkEl inp -> Rec StkEl ('TUnit : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
runner (IF_NONE Instr s out
_bNone Instr (a : s) out
bJust) (StkEl (VOption (Just Value' Instr t
a)) VarAnn
vn (NTOption TypeAnn
_ Notes t
n) :& Rec StkEl rs
r) =
  Instr (a : s) out -> Rec StkEl (a : s) -> m (Rec StkEl out)
InstrRunner m
runner Instr (a : s) out
bJust (Value' Instr t -> VarAnn -> Notes t -> StkEl t
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value' Instr t
a VarAnn
vn Notes t
Notes t
n StkEl t -> Rec StkEl rs -> Rec StkEl (t : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
runInstrImpl InstrRunner m
runner (IF_NONE Instr s out
bNone Instr (a : s) out
_bJust) (StkEl (VOption Maybe (Value' Instr t)
Nothing) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Instr s out -> Rec StkEl s -> m (Rec StkEl out)
InstrRunner m
runner Instr s out
bNone Rec StkEl s
Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
NEVER Rec StkEl inp
inp = case Rec StkEl inp
inp of {}
runInstrImpl InstrRunner m
_ (AnnPAIR{}) ((StkEl Value r
a VarAnn
_ Notes r
_) :& (StkEl Value r
b VarAnn
_ Notes r
_) :& Rec StkEl rs
r) =
  Rec StkEl ('TPair r r : rs) -> m (Rec StkEl ('TPair r r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TPair r r : rs) -> m (Rec StkEl ('TPair r r : rs)))
-> Rec StkEl ('TPair r r : rs) -> m (Rec StkEl ('TPair r r : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TPair r r) -> StkEl ('TPair r r)
forall (x :: T). Value x -> StkEl x
starNotesStkEl ((Value r, Value r) -> Value ('TPair r r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value r
a, Value r
b)) StkEl ('TPair r r) -> Rec StkEl rs -> Rec StkEl ('TPair r r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ (AnnUNPAIR{}) ((StkEl (VPair (Value' Instr l
a, Value' Instr r
b)) VarAnn
_ Notes r
_) :& Rec StkEl rs
r) =
  Rec StkEl (l : r : rs) -> m (Rec StkEl (l : r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (l : r : rs) -> m (Rec StkEl (l : r : rs)))
-> Rec StkEl (l : r : rs) -> m (Rec StkEl (l : r : rs))
forall a b. (a -> b) -> a -> b
$ Value' Instr l -> StkEl l
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr l
a StkEl l -> Rec StkEl (r : rs) -> Rec StkEl (l : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Value' Instr r -> StkEl r
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr r
b StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ (PAIRN PeanoNatural n
s) Rec StkEl inp
stack = Rec StkEl out -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl out -> m (Rec StkEl out))
-> Rec StkEl out -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ PeanoNatural n -> Rec StkEl inp -> Rec StkEl (PairN n inp)
forall (n :: Peano) (inp :: [T]).
ConstraintPairN n inp =>
PeanoNatural n -> Rec StkEl inp -> Rec StkEl (PairN n inp)
go PeanoNatural n
s Rec StkEl inp
stack
  where
    go :: forall n inp. ConstraintPairN n inp => PeanoNatural n -> Rec StkEl inp -> Rec StkEl (PairN n inp)
    go :: PeanoNatural n -> Rec StkEl inp -> Rec StkEl (PairN n inp)
go (Succ (Succ PeanoNatural m
Zero)) (StkEl Value r
a VarAnn
_ Notes r
_ :& StkEl Value r
b VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
      -- if n=2
      Value ('TPair r r) -> StkEl ('TPair r r)
forall (x :: T). Value x -> StkEl x
starNotesStkEl ((Value r, Value r) -> Value ('TPair r r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value r
a, Value r
b)) StkEl ('TPair r r) -> Rec StkEl rs -> Rec StkEl ('TPair r r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
    go (Succ n :: PeanoNatural m
n@(Succ (Succ PeanoNatural m
_))) (StkEl Value r
a VarAnn
_ Notes r
_ :& r :: Rec StkEl rs
r@(StkEl r
_ :& StkEl r
_ :& Rec StkEl rs
_)) =
      -- if n>2
      case PeanoNatural m -> Rec StkEl rs -> Rec StkEl (PairN m rs)
forall (n :: Peano) (inp :: [T]).
ConstraintPairN n inp =>
PeanoNatural n -> Rec StkEl inp -> Rec StkEl (PairN n inp)
go PeanoNatural m
n Rec StkEl rs
r of
        StkEl Value r
combed VarAnn
_ Notes r
_ :& Rec StkEl rs
r' ->
            Value ('TPair r r) -> StkEl ('TPair r r)
forall (x :: T). Value x -> StkEl x
starNotesStkEl ((Value r, Value r) -> Value ('TPair r r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value r
a, Value r
combed)) StkEl ('TPair r r) -> Rec StkEl rs -> Rec StkEl ('TPair r r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r'
runInstrImpl InstrRunner m
_ (UNPAIRN PeanoNatural n
s) (StkEl Value r
pair0 VarAnn
_ Notes r
pairNotes0 :& Rec StkEl rs
r) = do
  Rec StkEl out -> m (Rec StkEl out)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl out -> m (Rec StkEl out))
-> Rec StkEl out -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ PeanoNatural n -> Value r -> Notes r -> Rec StkEl (UnpairN n r)
forall (n :: Peano) (pair :: T).
ConstraintUnpairN n pair =>
PeanoNatural n
-> Value pair -> Notes pair -> Rec StkEl (UnpairN n pair)
go PeanoNatural n
s Value r
pair0 Notes r
pairNotes0 Rec StkEl (UnpairN n pair)
-> Rec StkEl rs -> Rec StkEl (UnpairN n pair ++ rs)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Rec StkEl rs
r
  where
    go
      :: forall n pair. ConstraintUnpairN n pair
      => PeanoNatural n -> Value pair -> Notes pair
      -> Rec StkEl (UnpairN n pair)
    go :: PeanoNatural n
-> Value pair -> Notes pair -> Rec StkEl (UnpairN n pair)
go PeanoNatural n
n Value pair
pair Notes pair
pairNotes =
      case (PeanoNatural n
n, Value pair
pair, Notes pair
pairNotes) of
        -- if n=2
        (Succ (Succ PeanoNatural m
Zero), VPair (Value' Instr l
a, Value' Instr r
b), NTPair TypeAnn
_ RootAnn
aFieldAnn RootAnn
bFieldAnn VarAnn
_ VarAnn
_ Notes p
aNotes Notes q
bNotes) ->
          -- @UNPAIR n@ converts field annotations into var annotations.
          --
          -- > /* [ @pair pair (int %aa) (int %bb) (int %cc) (int %dd) ] */ ;
          -- > UNPAIR 3
          -- > /* [ @aa int : @bb int : pair (int %cc) (int %dd) ] */ ;
          --
          -- Nested var annotations will be discarded.
          --
          -- > /* [ pair (int @c) (int @a) (int @b) ] */ ;
          -- UNPAIR 3
          -- /* [ int : int : int ] */ ;
          Value' Instr l -> VarAnn -> Notes l -> StkEl l
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value' Instr l
a (RootAnn -> VarAnn
forall k1 k2 (tag1 :: k1) (tag2 :: k2).
Annotation tag1 -> Annotation tag2
U.convAnn @U.FieldTag @U.VarTag RootAnn
aFieldAnn) Notes l
Notes p
aNotes
            StkEl l -> Rec StkEl '[r] -> Rec StkEl '[l, r]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Value' Instr r -> VarAnn -> Notes r -> StkEl r
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value' Instr r
b (RootAnn -> VarAnn
forall k1 k2 (tag1 :: k1) (tag2 :: k2).
Annotation tag1 -> Annotation tag2
U.convAnn @U.FieldTag @U.VarTag RootAnn
bFieldAnn) Notes r
Notes q
bNotes
            StkEl r -> Rec StkEl '[] -> Rec StkEl '[r]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl '[]
forall u (a :: u -> *). Rec a '[]
RNil
        -- if n>2
        (Succ n' :: PeanoNatural m
n'@(Succ (Succ PeanoNatural m
_)), VPair (Value' Instr l
a, b :: Value' Instr r
b@(VPair (Value' Instr l, Value' Instr r)
_)), NTPair TypeAnn
_ RootAnn
aFieldAnn RootAnn
_ VarAnn
_ VarAnn
_ Notes p
aNotes Notes q
bNotes) ->
          Value' Instr l -> VarAnn -> Notes l -> StkEl l
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value' Instr l
a (RootAnn -> VarAnn
forall k1 k2 (tag1 :: k1) (tag2 :: k2).
Annotation tag1 -> Annotation tag2
U.convAnn @U.FieldTag @U.VarTag RootAnn
aFieldAnn) Notes l
Notes p
aNotes
            StkEl l
-> Rec StkEl (UnpairN ('S ('S m)) ('TPair l r))
-> Rec StkEl (l : UnpairN ('S ('S m)) ('TPair l r))
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& PeanoNatural m
-> Value' Instr r -> Notes r -> Rec StkEl (UnpairN m r)
forall (n :: Peano) (pair :: T).
ConstraintUnpairN n pair =>
PeanoNatural n
-> Value pair -> Notes pair -> Rec StkEl (UnpairN n pair)
go PeanoNatural m
n' Value' Instr r
b Notes r
Notes q
bNotes
runInstrImpl InstrRunner m
_ (AnnCAR VarAnn
_ RootAnn
_) (StkEl (VPair (Value' Instr l
a, Value' Instr r
_b)) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = Rec StkEl (l : rs) -> m (Rec StkEl (l : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (l : rs) -> m (Rec StkEl (l : rs)))
-> Rec StkEl (l : rs) -> m (Rec StkEl (l : rs))
forall a b. (a -> b) -> a -> b
$ Value' Instr l -> StkEl l
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr l
a StkEl l -> Rec StkEl rs -> Rec StkEl (l : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ (AnnCDR VarAnn
_ RootAnn
_) (StkEl (VPair (Value' Instr l
_a, Value' Instr r
b)) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = Rec StkEl (r : rs) -> m (Rec StkEl (r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : rs) -> m (Rec StkEl (r : rs)))
-> Rec StkEl (r : rs) -> m (Rec StkEl (r : rs))
forall a b. (a -> b) -> a -> b
$ Value' Instr r -> StkEl r
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr r
b StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ (AnnLEFT TypeAnn
nt RootAnn
nf1 RootAnn
nf2) ((StkEl Value r
a VarAnn
_ Notes r
na) :& Rec StkEl rs
r) =
  Value r -> (SingI r => m (Rec StkEl out)) -> m (Rec StkEl out)
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value r
a ((SingI r => m (Rec StkEl out)) -> m (Rec StkEl out))
-> (SingI r => m (Rec StkEl out)) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$
    Rec StkEl ('TOr r b : rs) -> m (Rec StkEl ('TOr r b : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOr r b : rs) -> m (Rec StkEl ('TOr r b : rs)))
-> Rec StkEl ('TOr r b : rs) -> m (Rec StkEl ('TOr r b : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TOr r b) -> VarAnn -> Notes ('TOr r b) -> StkEl ('TOr r b)
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl (Either (Value r) (Value' Instr b) -> Value ('TOr r b)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(SingI l, SingI r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Either (Value r) (Value' Instr b) -> Value ('TOr r b))
-> Either (Value r) (Value' Instr b) -> Value ('TOr r b)
forall a b. (a -> b) -> a -> b
$ Value r -> Either (Value r) (Value' Instr b)
forall a b. a -> Either a b
Left Value r
a) VarAnn
forall k (a :: k). Annotation a
U.noAnn (TypeAnn
-> RootAnn -> RootAnn -> Notes r -> Notes b -> Notes ('TOr r b)
forall (p :: T) (q :: T).
TypeAnn
-> RootAnn -> RootAnn -> Notes p -> Notes q -> Notes ('TOr p q)
NTOr TypeAnn
nt RootAnn
nf1 RootAnn
nf2 Notes r
na Notes b
forall (t :: T). SingI t => Notes t
starNotes) StkEl ('TOr r b) -> Rec StkEl rs -> Rec StkEl ('TOr r b : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ (AnnRIGHT TypeAnn
nt RootAnn
nf1 RootAnn
nf2) ((StkEl Value r
b VarAnn
_ Notes r
nb) :& Rec StkEl rs
r) =
  Value r -> (SingI r => m (Rec StkEl out)) -> m (Rec StkEl out)
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value r
b ((SingI r => m (Rec StkEl out)) -> m (Rec StkEl out))
-> (SingI r => m (Rec StkEl out)) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$
    Rec StkEl ('TOr a r : rs) -> m (Rec StkEl ('TOr a r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOr a r : rs) -> m (Rec StkEl ('TOr a r : rs)))
-> Rec StkEl ('TOr a r : rs) -> m (Rec StkEl ('TOr a r : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TOr a r) -> VarAnn -> Notes ('TOr a r) -> StkEl ('TOr a r)
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl (Either (Value' Instr a) (Value r) -> Value ('TOr a r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(SingI l, SingI r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Either (Value' Instr a) (Value r) -> Value ('TOr a r))
-> Either (Value' Instr a) (Value r) -> Value ('TOr a r)
forall a b. (a -> b) -> a -> b
$ Value r -> Either (Value' Instr a) (Value r)
forall a b. b -> Either a b
Right Value r
b) VarAnn
forall k (a :: k). Annotation a
U.noAnn (TypeAnn
-> RootAnn -> RootAnn -> Notes a -> Notes r -> Notes ('TOr a r)
forall (p :: T) (q :: T).
TypeAnn
-> RootAnn -> RootAnn -> Notes p -> Notes q -> Notes ('TOr p q)
NTOr TypeAnn
nt RootAnn
nf1 RootAnn
nf2 Notes a
forall (t :: T). SingI t => Notes t
starNotes Notes r
nb) StkEl ('TOr a r) -> Rec StkEl rs -> Rec StkEl ('TOr a r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
runner (IF_LEFT Instr (a : s) out
bLeft Instr (b : s) out
_) (StkEl (VOr (Left Value' Instr l
a)) VarAnn
vn (NTOr TypeAnn
_ RootAnn
_ RootAnn
_ Notes p
nl Notes q
_) :& Rec StkEl rs
r) =
  Instr (a : s) out -> Rec StkEl (a : s) -> m (Rec StkEl out)
InstrRunner m
runner Instr (a : s) out
bLeft (Value' Instr l -> VarAnn -> Notes l -> StkEl l
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value' Instr l
a VarAnn
vn Notes l
Notes p
nl StkEl l -> Rec StkEl rs -> Rec StkEl (l : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
runInstrImpl InstrRunner m
runner (IF_LEFT Instr (a : s) out
_ Instr (b : s) out
bRight) (StkEl (VOr (Right Value' Instr r
a)) VarAnn
vn (NTOr TypeAnn
_ RootAnn
_ RootAnn
_ Notes p
_ Notes q
nr) :& Rec StkEl rs
r) =
  Instr (b : s) out -> Rec StkEl (b : s) -> m (Rec StkEl out)
InstrRunner m
runner Instr (b : s) out
bRight (Value' Instr r -> VarAnn -> Notes r -> StkEl r
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value' Instr r
a VarAnn
vn Notes r
Notes q
nr StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
runInstrImpl InstrRunner m
_ Instr inp out
NIL Rec StkEl inp
r = Rec StkEl ('TList p : inp) -> m (Rec StkEl ('TList p : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TList p : inp) -> m (Rec StkEl ('TList p : inp)))
-> Rec StkEl ('TList p : inp) -> m (Rec StkEl ('TList p : inp))
forall a b. (a -> b) -> a -> b
$ Value ('TList p) -> StkEl ('TList p)
forall (x :: T). Value x -> StkEl x
starNotesStkEl ([Value' Instr p] -> Value ('TList p)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
[Value' instr t] -> Value' instr ('TList t)
VList []) StkEl ('TList p) -> Rec StkEl inp -> Rec StkEl ('TList p : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
CONS (StkEl r
a :& StkEl (VList [Value' Instr t]
l) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = Rec StkEl ('TList r : rs) -> m (Rec StkEl ('TList r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TList r : rs) -> m (Rec StkEl ('TList r : rs)))
-> Rec StkEl ('TList r : rs) -> m (Rec StkEl ('TList r : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TList r) -> StkEl ('TList r)
forall (x :: T). Value x -> StkEl x
starNotesStkEl ([Value' Instr r] -> Value ('TList r)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
[Value' instr t] -> Value' instr ('TList t)
VList (StkEl r -> Value' Instr r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a Value' Instr r -> [Value' Instr r] -> [Value' Instr r]
forall a. a -> [a] -> [a]
: [Value' Instr r]
[Value' Instr t]
l)) StkEl ('TList r) -> Rec StkEl rs -> Rec StkEl ('TList r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
runner (IF_CONS Instr (a : 'TList a : s) out
_ Instr s out
bNil) (StkEl (VList []) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = Instr s out -> Rec StkEl s -> m (Rec StkEl out)
InstrRunner m
runner Instr s out
bNil Rec StkEl s
Rec StkEl rs
r
runInstrImpl InstrRunner m
runner (IF_CONS Instr (a : 'TList a : s) out
bCons Instr s out
_) (StkEl (VList (Value' Instr t
lh : [Value' Instr t]
lr)) VarAnn
vn ntl :: Notes r
ntl@(NTList TypeAnn
_ Notes t
nhd) :& Rec StkEl rs
r) =
  Instr (a : 'TList a : s) out
-> Rec StkEl (a : 'TList a : s) -> m (Rec StkEl out)
InstrRunner m
runner Instr (a : 'TList a : s) out
bCons (Value' Instr t -> VarAnn -> Notes t -> StkEl t
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value' Instr t
lh VarAnn
vn Notes t
Notes t
nhd StkEl t
-> Rec StkEl ('TList t : rs) -> Rec StkEl (t : 'TList t : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Value ('TList t) -> VarAnn -> Notes ('TList t) -> StkEl ('TList t)
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl ([Value' Instr t] -> Value ('TList t)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
[Value' instr t] -> Value' instr ('TList t)
VList [Value' Instr t]
lr) VarAnn
vn Notes r
Notes ('TList t)
ntl StkEl ('TList t) -> Rec StkEl rs -> Rec StkEl ('TList t : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
runInstrImpl InstrRunner m
_ Instr inp out
SIZE (StkEl r
a :& Rec StkEl rs
r) = Rec StkEl ('TNat : rs) -> m (Rec StkEl ('TNat : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TNat : rs) -> m (Rec StkEl ('TNat : rs)))
-> Rec StkEl ('TNat : rs) -> m (Rec StkEl ('TNat : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TNat -> StkEl 'TNat
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Natural -> Value 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural -> Value 'TNat) -> Natural -> Value 'TNat
forall a b. (a -> b) -> a -> b
$ (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> (Int -> Integer) -> Int -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger) (Int -> Natural) -> Int -> Natural
forall a b. (a -> b) -> a -> b
$ Value' Instr r -> Int
forall (c :: T) (instr :: [T] -> [T] -> *).
SizeOp c =>
Value' instr c -> Int
evalSize (Value' Instr r -> Int) -> Value' Instr r -> Int
forall a b. (a -> b) -> a -> b
$ StkEl r -> Value' Instr r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a) StkEl 'TNat -> Rec StkEl rs -> Rec StkEl ('TNat : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
EMPTY_SET Rec StkEl inp
r = Rec StkEl ('TSet e : inp) -> m (Rec StkEl ('TSet e : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TSet e : inp) -> m (Rec StkEl ('TSet e : inp)))
-> Rec StkEl ('TSet e : inp) -> m (Rec StkEl ('TSet e : inp))
forall a b. (a -> b) -> a -> b
$ Value ('TSet e) -> StkEl ('TSet e)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Set (Value' Instr e) -> Value ('TSet e)
forall (t :: T) (instr :: [T] -> [T] -> *).
(SingI t, Comparable t) =>
Set (Value' instr t) -> Value' instr ('TSet t)
VSet Set (Value' Instr e)
forall a. Set a
Set.empty) StkEl ('TSet e) -> Rec StkEl inp -> Rec StkEl ('TSet e : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
EMPTY_MAP Rec StkEl inp
r = Rec StkEl ('TMap a b : inp) -> m (Rec StkEl ('TMap a b : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TMap a b : inp) -> m (Rec StkEl ('TMap a b : inp)))
-> Rec StkEl ('TMap a b : inp) -> m (Rec StkEl ('TMap a b : inp))
forall a b. (a -> b) -> a -> b
$ Value ('TMap a b) -> StkEl ('TMap a b)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Map (Value' Instr a) (Value' Instr b) -> Value ('TMap a b)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI k, SingI v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
VMap Map (Value' Instr a) (Value' Instr b)
forall k a. Map k a
Map.empty) StkEl ('TMap a b) -> Rec StkEl inp -> Rec StkEl ('TMap a b : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
EMPTY_BIG_MAP Rec StkEl inp
r = do
  Value ('TBigMap a b)
bigMap <- Value ('TBigMap a b) -> m (Value ('TBigMap a b))
forall (m :: * -> *) (t :: T). EvalM m => Value t -> m (Value t)
assignBigMapIds' (Value ('TBigMap a b) -> m (Value ('TBigMap a b)))
-> Value ('TBigMap a b) -> m (Value ('TBigMap a b))
forall a b. (a -> b) -> a -> b
$ Maybe Natural
-> Map (Value' Instr a) (Value' Instr b) -> Value ('TBigMap a b)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI k, SingI v, Comparable k, HasNoBigMap v) =>
Maybe Natural
-> Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VBigMap Maybe Natural
forall a. Maybe a
Nothing Map (Value' Instr a) (Value' Instr b)
forall k a. Map k a
Map.empty
  pure $ Value ('TBigMap a b) -> StkEl ('TBigMap a b)
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value ('TBigMap a b)
bigMap StkEl ('TBigMap a b)
-> Rec StkEl inp -> Rec StkEl ('TBigMap a b : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
runner (MAP (code :: Instr (MapOpInp c ': s) (b ': s))) (StkEl Value r
a VarAnn
vn Notes r
n :& Rec StkEl rs
r) = do
  -- Evaluation must preserve all stack modifications that @MAP@'s does.
  (Rec StkEl rs
newStack, [Value' Instr b]
newList) <- ((Rec StkEl rs, [Value' Instr b])
 -> StkEl (MapOpInp c) -> m (Rec StkEl rs, [Value' Instr b]))
-> (Rec StkEl rs, [Value' Instr b])
-> [StkEl (MapOpInp c)]
-> m (Rec StkEl rs, [Value' Instr b])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (\(Rec StkEl rs
curStack, [Value' Instr b]
curList) (val :: StkEl (MapOpInp c)) -> do
    Rec StkEl (b : s)
res <- Instr (MapOpInp c : rs) (b : s)
-> Rec StkEl (MapOpInp c : rs) -> m (Rec StkEl (b : s))
InstrRunner m
runner Instr (MapOpInp c : s) (b : s)
Instr (MapOpInp c : rs) (b : s)
code (StkEl (MapOpInp c)
val StkEl (MapOpInp c) -> Rec StkEl rs -> Rec StkEl (MapOpInp c : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
curStack)
    case Rec StkEl (b : s)
res of
      ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> nextVal :: T.Value b) :& Rec StkEl rs
nextStack) -> (Rec StkEl rs, [Value' Instr b])
-> m (Rec StkEl rs, [Value' Instr b])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl rs
nextStack, Value' Instr b
nextVal Value' Instr b -> [Value' Instr b] -> [Value' Instr b]
forall a. a -> [a] -> [a]
: [Value' Instr b]
curList))
    (Rec StkEl rs
r, []) ((\Value (MapOpInp c)
el -> Value (MapOpInp c)
-> VarAnn -> Notes (MapOpInp c) -> StkEl (MapOpInp c)
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value (MapOpInp c)
el VarAnn
vn (Notes r -> Notes (MapOpInp r)
forall (c :: T). MapOp c => Notes c -> Notes (MapOpInp c)
mapOpNotes Notes r
n)) (Value (MapOpInp c) -> StkEl (MapOpInp c))
-> [Value (MapOpInp c)] -> [StkEl (MapOpInp c)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value' Instr c -> [Value (MapOpInp c)]
forall (c :: T) (instr :: [T] -> [T] -> *).
MapOp c =>
Value' instr c -> [Value' instr (MapOpInp c)]
mapOpToList @c Value' Instr c
Value r
a)
  Rec StkEl (MapOpRes c b : rs) -> m (Rec StkEl (MapOpRes c b : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (MapOpRes c b : rs)
 -> m (Rec StkEl (MapOpRes c b : rs)))
-> Rec StkEl (MapOpRes c b : rs)
-> m (Rec StkEl (MapOpRes c b : rs))
forall a b. (a -> b) -> a -> b
$ Value (MapOpRes c b) -> StkEl (MapOpRes c b)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Value r -> [Value' Instr b] -> Value' Instr (MapOpRes r b)
forall (c :: T) (b :: T) (instr :: [T] -> [T] -> *).
(MapOp c, SingI b) =>
Value' instr c -> [Value' instr b] -> Value' instr (MapOpRes c b)
mapOpFromList Value r
a ([Value' Instr b] -> [Value' Instr b]
forall a. [a] -> [a]
reverse [Value' Instr b]
newList)) StkEl (MapOpRes c b)
-> Rec StkEl rs -> Rec StkEl (MapOpRes c b : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
newStack
runInstrImpl InstrRunner m
runner (ITER (code :: Instr (IterOpEl c ': s) s)) (StkEl Value r
a VarAnn
vn Notes r
n :& Rec StkEl rs
r) =
  case Value' Instr c
-> (Maybe (Value' Instr (IterOpEl c)), Value' Instr c)
forall (c :: T) (instr :: [T] -> [T] -> *).
IterOp c =>
Value' instr c
-> (Maybe (Value' instr (IterOpEl c)), Value' instr c)
iterOpDetachOne @c Value' Instr c
Value r
a of
    (Just Value' Instr (IterOpEl c)
x, Value' Instr c
xs) -> do
      Rec StkEl out
res <- Instr (IterOpEl c : rs) out
-> Rec StkEl (IterOpEl c : rs) -> m (Rec StkEl out)
InstrRunner m
runner Instr (IterOpEl c : out) out
Instr (IterOpEl c : rs) out
code (Value' Instr (IterOpEl c)
-> VarAnn -> Notes (IterOpEl c) -> StkEl (IterOpEl c)
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value' Instr (IterOpEl c)
x VarAnn
vn (Notes r -> Notes (IterOpEl r)
forall (c :: T). IterOp c => Notes c -> Notes (IterOpEl c)
iterOpNotes Notes r
n) StkEl (IterOpEl c) -> Rec StkEl rs -> Rec StkEl (IterOpEl c : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
      Instr (c : out) out -> Rec StkEl (c : out) -> m (Rec StkEl out)
InstrRunner m
runner (Instr (IterOpEl c : out) out -> Instr (c : out) out
forall (c :: T) (s :: [T]).
IterOp c =>
Instr (IterOpEl c : s) s -> Instr (c : s) s
ITER Instr (IterOpEl c : out) out
code) (Value' Instr c -> VarAnn -> Notes c -> StkEl c
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value' Instr c
xs VarAnn
vn Notes c
Notes r
n StkEl c -> Rec StkEl out -> Rec StkEl (c : out)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl out
res)
    (Maybe (Value' Instr (IterOpEl c))
Nothing, Value' Instr c
_) -> Rec StkEl rs -> m (Rec StkEl rs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
MEM (StkEl r
a :& StkEl r
b :& Rec StkEl rs
r) = Rec StkEl ('TBool : rs) -> m (Rec StkEl ('TBool : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBool : rs) -> m (Rec StkEl ('TBool : rs)))
-> Rec StkEl ('TBool : rs) -> m (Rec StkEl ('TBool : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TBool -> StkEl 'TBool
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Bool -> Value 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Value' Instr (MemOpKey r) -> Value' Instr r -> Bool
forall (c :: T) (instr :: [T] -> [T] -> *).
MemOp c =>
Value' instr (MemOpKey c) -> Value' instr c -> Bool
evalMem (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a) (StkEl r -> Value' Instr r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
b))) StkEl 'TBool -> Rec StkEl rs -> Rec StkEl ('TBool : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
GET (StkEl r
a :& StkEl r
b :& Rec StkEl rs
r) = Rec StkEl ('TOption (GetOpVal c) : rs)
-> m (Rec StkEl ('TOption (GetOpVal c) : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption (GetOpVal c) : rs)
 -> m (Rec StkEl ('TOption (GetOpVal c) : rs)))
-> Rec StkEl ('TOption (GetOpVal c) : rs)
-> m (Rec StkEl ('TOption (GetOpVal c) : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TOption (GetOpVal c)) -> StkEl ('TOption (GetOpVal c))
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value' Instr (GetOpVal c)) -> Value ('TOption (GetOpVal c))
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Value' Instr (GetOpKey r)
-> Value' Instr r -> Maybe (Value' Instr (GetOpVal r))
forall (c :: T) (instr :: [T] -> [T] -> *).
GetOp c =>
Value' instr (GetOpKey c)
-> Value' instr c -> Maybe (Value' instr (GetOpVal c))
evalGet (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a) (StkEl r -> Value' Instr r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
b))) StkEl ('TOption (GetOpVal c))
-> Rec StkEl rs -> Rec StkEl ('TOption (GetOpVal c) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ (GETN PeanoNatural ix
s) (StkEl Value r
pair VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = do
  Rec StkEl (GetN ix pair : rs) -> m (Rec StkEl (GetN ix pair : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (GetN ix pair : rs)
 -> m (Rec StkEl (GetN ix pair : rs)))
-> Rec StkEl (GetN ix pair : rs)
-> m (Rec StkEl (GetN ix pair : rs))
forall a b. (a -> b) -> a -> b
$ Value (GetN ix pair) -> StkEl (GetN ix pair)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (PeanoNatural ix -> Value r -> Value (GetN ix r)
forall (ix :: Peano) (a :: T).
ConstraintGetN ix a =>
PeanoNatural ix -> Value a -> Value (GetN ix a)
go PeanoNatural ix
s Value r
pair) StkEl (GetN ix pair)
-> Rec StkEl rs -> Rec StkEl (GetN ix pair : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
  where
    go
      :: forall ix a. ConstraintGetN ix a
      => PeanoNatural ix -> Value a
      -> Value (GetN ix a)
    go :: PeanoNatural ix -> Value a -> Value (GetN ix a)
go PeanoNatural ix
Zero            Value a
a                   = Value a
Value (GetN ix a)
a
    go (Succ PeanoNatural m
Zero)      (VPair (Value' Instr l
left, Value' Instr r
_))  = Value' Instr l
Value (GetN ix a)
left
    go (Succ (Succ PeanoNatural m
n')) (VPair (Value' Instr l
_, Value' Instr r
right)) = PeanoNatural m -> Value' Instr r -> Value (GetN m r)
forall (ix :: Peano) (a :: T).
ConstraintGetN ix a =>
PeanoNatural ix -> Value a -> Value (GetN ix a)
go PeanoNatural m
n' Value' Instr r
right
runInstrImpl InstrRunner m
_ Instr inp out
UPDATE (StkEl r
a :& StkEl r
b :& StkEl Value r
c VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl (r : rs) -> m (Rec StkEl (r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : rs) -> m (Rec StkEl (r : rs)))
-> Rec StkEl (r : rs) -> m (Rec StkEl (r : rs))
forall a b. (a -> b) -> a -> b
$ Value r -> StkEl r
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Value' Instr (UpdOpKey r)
-> Value' Instr (UpdOpParams r) -> Value r -> Value r
forall (c :: T) (instr :: [T] -> [T] -> *).
UpdOp c =>
Value' instr (UpdOpKey c)
-> Value' instr (UpdOpParams c) -> Value' instr c -> Value' instr c
evalUpd (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a) (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
b) Value r
c) StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ (UPDATEN PeanoNatural ix
s) (StkEl (Value r
val :: Value val) VarAnn
_ Notes r
_  :& StkEl Value r
pair VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = do
  Rec StkEl (UpdateN ix val pair : rs)
-> m (Rec StkEl (UpdateN ix val pair : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UpdateN ix val pair : rs)
 -> m (Rec StkEl (UpdateN ix val pair : rs)))
-> Rec StkEl (UpdateN ix val pair : rs)
-> m (Rec StkEl (UpdateN ix val pair : rs))
forall a b. (a -> b) -> a -> b
$ Value (UpdateN ix val pair) -> StkEl (UpdateN ix val pair)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (PeanoNatural ix -> Value r -> Value (UpdateN ix r r)
forall (ix :: Peano) (pair :: T).
ConstraintUpdateN ix pair =>
PeanoNatural ix -> Value pair -> Value (UpdateN ix r pair)
go PeanoNatural ix
s Value r
pair) StkEl (UpdateN ix val pair)
-> Rec StkEl rs -> Rec StkEl (UpdateN ix val pair : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
  where
    go
      :: forall ix pair. ConstraintUpdateN ix pair
      => PeanoNatural ix -> Value pair -> Value (UpdateN ix val pair)
    go :: PeanoNatural ix -> Value pair -> Value (UpdateN ix r pair)
go PeanoNatural ix
Zero             Value pair
_                      = Value r
Value (UpdateN ix r pair)
val
    go (Succ PeanoNatural m
Zero)      (VPair (Value' Instr l
_, Value' Instr r
right))     = (Value r, Value' Instr 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
val, Value' Instr r
right)
    go (Succ (Succ PeanoNatural m
n')) (VPair (Value' Instr l
left, Value' Instr r
right))  = (Value' Instr l, Value' Instr (UpdateN m val r))
-> Value' Instr ('TPair l (UpdateN m val r))
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value' Instr l
left, PeanoNatural m -> Value' Instr r -> Value (UpdateN m r r)
forall (ix :: Peano) (pair :: T).
ConstraintUpdateN ix pair =>
PeanoNatural ix -> Value pair -> Value (UpdateN ix r pair)
go PeanoNatural m
n' Value' Instr r
right)
runInstrImpl InstrRunner m
_ Instr inp out
GET_AND_UPDATE (StkEl Value r
key VarAnn
_ Notes r
_ :& StkEl Value r
valMb VarAnn
_ Notes r
_ :& StkEl Value r
collection VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl ('TOption (GetOpVal c) : r : rs)
-> m (Rec StkEl ('TOption (GetOpVal c) : r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption (GetOpVal c) : r : rs)
 -> m (Rec StkEl ('TOption (GetOpVal c) : r : rs)))
-> Rec StkEl ('TOption (GetOpVal c) : r : rs)
-> m (Rec StkEl ('TOption (GetOpVal c) : r : rs))
forall a b. (a -> b) -> a -> b
$
    Value ('TOption (GetOpVal c)) -> StkEl ('TOption (GetOpVal c))
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value' Instr (GetOpVal c)) -> Value ('TOption (GetOpVal c))
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI 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)
key Value r
collection))
    StkEl ('TOption (GetOpVal c))
-> Rec StkEl (r : rs) -> Rec StkEl ('TOption (GetOpVal c) : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Value r -> StkEl r
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Value' Instr (UpdOpKey r)
-> Value' Instr (UpdOpParams r) -> Value r -> Value r
forall (c :: T) (instr :: [T] -> [T] -> *).
UpdOp c =>
Value' instr (UpdOpKey c)
-> Value' instr (UpdOpParams c) -> Value' instr c -> Value' instr c
evalUpd Value r
Value' Instr (UpdOpKey r)
key Value r
Value' Instr (UpdOpParams r)
valMb Value r
collection)
    StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
runner (IF Instr s out
bTrue Instr s out
_) (StkEl (VBool Bool
True) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = Instr s out -> Rec StkEl s -> m (Rec StkEl out)
InstrRunner m
runner Instr s out
bTrue Rec StkEl s
Rec StkEl rs
r
runInstrImpl InstrRunner m
runner (IF Instr s out
_ Instr s out
bFalse) (StkEl (VBool Bool
False) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = Instr s out -> Rec StkEl s -> m (Rec StkEl out)
InstrRunner m
runner Instr s out
bFalse Rec StkEl s
Rec StkEl rs
r
runInstrImpl InstrRunner m
_ (LOOP Instr out ('TBool : out)
_) (StkEl (VBool Bool
False) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = Rec StkEl rs -> m (Rec StkEl rs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl rs -> m (Rec StkEl rs))
-> Rec StkEl rs -> m (Rec StkEl rs)
forall a b. (a -> b) -> a -> b
$ Rec StkEl rs
r
runInstrImpl InstrRunner m
runner (LOOP Instr out ('TBool : out)
ops) (StkEl (VBool Bool
True) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = do
  Rec StkEl ('TBool : out)
res <- Instr out ('TBool : out)
-> Rec StkEl out -> m (Rec StkEl ('TBool : out))
InstrRunner m
runner Instr out ('TBool : out)
ops Rec StkEl out
Rec StkEl rs
r
  Instr ('TBool : out) out
-> Rec StkEl ('TBool : out) -> m (Rec StkEl out)
InstrRunner m
runner (Instr out ('TBool : out) -> Instr ('TBool : out) out
forall (s :: [T]). Instr s ('TBool : s) -> Instr ('TBool : s) s
LOOP Instr out ('TBool : out)
ops) Rec StkEl ('TBool : out)
res
runInstrImpl InstrRunner m
_ (LOOP_LEFT Instr (a : s) ('TOr a b : s)
_) (StkEl (VOr (Right Value' Instr r
a)) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = Rec StkEl (r : rs) -> m (Rec StkEl (r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : rs) -> m (Rec StkEl (r : rs)))
-> Rec StkEl (r : rs) -> m (Rec StkEl (r : rs))
forall a b. (a -> b) -> a -> b
$ Value' Instr r -> StkEl r
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr r
a StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
runner (LOOP_LEFT Instr (a : s) ('TOr a b : s)
ops) (StkEl (VOr (Left Value' Instr l
a)) VarAnn
vn (NTOr TypeAnn
_ RootAnn
_ RootAnn
_ Notes p
nl Notes q
_) :& Rec StkEl rs
r) = do
  Rec StkEl ('TOr a b : s)
res <- Instr (a : s) ('TOr a b : s)
-> Rec StkEl (a : s) -> m (Rec StkEl ('TOr a b : s))
InstrRunner m
runner Instr (a : s) ('TOr a b : s)
ops (Value' Instr l -> VarAnn -> Notes l -> StkEl l
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value' Instr l
a VarAnn
vn Notes l
Notes p
nl StkEl l -> Rec StkEl rs -> Rec StkEl (l : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
  Instr ('TOr a b : s) (b : s)
-> Rec StkEl ('TOr a b : s) -> m (Rec StkEl (b : s))
InstrRunner m
runner (Instr (a : s) ('TOr a b : s) -> Instr ('TOr a b : s) (b : s)
forall (a :: T) (s :: [T]) (b :: T).
Instr (a : s) ('TOr a b : s) -> Instr ('TOr a b : s) (b : s)
LOOP_LEFT Instr (a : s) ('TOr a b : s)
ops) Rec StkEl ('TOr a b : s)
res
runInstrImpl InstrRunner m
_ (LAMBDA Value' Instr ('TLambda i o)
lam) Rec StkEl inp
r = Rec StkEl ('TLambda i o : inp)
-> m (Rec StkEl ('TLambda i o : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TLambda i o : inp)
 -> m (Rec StkEl ('TLambda i o : inp)))
-> Rec StkEl ('TLambda i o : inp)
-> m (Rec StkEl ('TLambda i o : inp))
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TLambda i o) -> StkEl ('TLambda i o)
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value' Instr ('TLambda i o)
lam StkEl ('TLambda i o)
-> Rec StkEl inp -> Rec StkEl ('TLambda i o : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
runner Instr inp out
EXEC (StkEl r
a :& StkEl (VLam (RemFail Instr '[inp] '[out] -> Instr '[inp] '[out]
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
T.rfAnyInstr -> Instr '[inp] '[out]
lBody)) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = do
  Rec StkEl '[out]
res <- Instr '[inp] '[out] -> Rec StkEl '[inp] -> m (Rec StkEl '[out])
InstrRunner m
runner Instr '[inp] '[out]
lBody (StkEl r
a StkEl r -> Rec StkEl '[] -> Rec StkEl '[r]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl '[]
forall u (a :: u -> *). Rec a '[]
RNil)
  pure $ Rec StkEl '[out]
res Rec StkEl '[out] -> Rec StkEl rs -> Rec StkEl ('[out] ++ rs)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
APPLY (StkEl (Value r
a :: T.Value a) VarAnn
_ Notes r
_ :& StkEl (VLam RemFail Instr '[inp] '[out]
lBody) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = do
  Rec StkEl ('TLambda b out : rs)
-> m (Rec StkEl ('TLambda b out : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TLambda b out : rs)
 -> m (Rec StkEl ('TLambda b out : rs)))
-> Rec StkEl ('TLambda b out : rs)
-> m (Rec StkEl ('TLambda b out : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TLambda b out) -> StkEl ('TLambda b out)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (RemFail Instr '[b] '[out] -> Value ('TLambda b out)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
RemFail instr '[inp] '[out] -> Value' instr ('TLambda inp out)
VLam ((forall (o' :: [T]). Instr '[inp] o' -> Instr '[b] o')
-> RemFail Instr '[inp] '[out] -> RemFail Instr '[b] '[out]
forall k (instr :: k -> k -> *) (i1 :: k) (i2 :: k) (o :: k).
(forall (o' :: k). instr i1 o' -> instr i2 o')
-> RemFail instr i1 o -> RemFail instr i2 o
T.rfMapAnyInstr forall (o' :: [T]). Instr '[inp] o' -> Instr '[b] o'
forall (i :: T) (s :: [T]) (o :: [T]).
Instr ('TPair r i : s) o -> Instr (i : s) o
doApply RemFail Instr '[inp] '[out]
lBody)) StkEl ('TLambda b out)
-> Rec StkEl rs -> Rec StkEl ('TLambda b out : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
  where
    doApply :: Instr ('TPair a i ': s) o -> Instr (i ': s) o
    doApply :: Instr ('TPair r i : s) o -> Instr (i : s) o
doApply 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 InstrRunner m
runner (DIP Instr a c
i) (StkEl r
a :& Rec StkEl rs
r) = do
  Rec StkEl c
res <- Instr a c -> Rec StkEl a -> m (Rec StkEl c)
InstrRunner m
runner Instr a c
i Rec StkEl a
Rec StkEl rs
r
  pure $ StkEl r
a StkEl r -> Rec StkEl c -> Rec StkEl (r : c)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl c
res
runInstrImpl InstrRunner m
runner (DIPN PeanoNatural n
s Instr s s'
i) Rec StkEl inp
stack =
  case PeanoNatural n
s of
    PeanoNatural n
Zero -> Instr s s' -> Rec StkEl s -> m (Rec StkEl s')
InstrRunner m
runner Instr s s'
i Rec StkEl inp
Rec StkEl s
stack
    Succ PeanoNatural m
s' -> case Rec StkEl inp
stack of
      (StkEl r
a :& Rec StkEl rs
r) -> (StkEl r
a StkEl r
-> Rec StkEl (Take m rs ++ s') -> Rec StkEl (r : (Take m rs ++ s'))
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) (Rec StkEl (Take m rs ++ s') -> Rec StkEl (r : (Take m rs ++ s')))
-> m (Rec StkEl (Take m rs ++ s'))
-> m (Rec StkEl (r : (Take m rs ++ s')))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InstrRunner m
-> Instr rs (Take m rs ++ s')
-> Rec StkEl rs
-> m (Rec StkEl (Take m rs ++ s'))
forall (m :: * -> *). EvalM m => InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner (PeanoNatural m -> Instr s s' -> Instr rs (Take m rs ++ s')
forall (n :: Peano) (inp :: [T]) (out :: [T]) (s :: [T])
       (s' :: [T]).
(ConstraintDIPN n inp out s s', NFData (Sing n)) =>
PeanoNatural n -> Instr s s' -> Instr inp out
DIPN PeanoNatural m
s' Instr s s'
i) Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
FAILWITH (StkEl r
a :& Rec StkEl rs
_) = MichelsonFailed -> m (Rec StkEl out)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (MichelsonFailed -> m (Rec StkEl out))
-> MichelsonFailed -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value r -> MichelsonFailed
forall (t :: T).
(SingI t, ConstantScope t) =>
Value t -> MichelsonFailed
MichelsonFailedWith (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a)
runInstrImpl InstrRunner m
_ Instr inp out
CAST (StkEl Value r
a VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = Rec StkEl (r : rs) -> m (Rec StkEl (r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : rs) -> m (Rec StkEl (r : rs)))
-> Rec StkEl (r : rs) -> m (Rec StkEl (r : rs))
forall a b. (a -> b) -> a -> b
$ Value r -> StkEl r
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value r
a StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
RENAME (StkEl Value r
a VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = Rec StkEl (r : rs) -> m (Rec StkEl (r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : rs) -> m (Rec StkEl (r : rs)))
-> Rec StkEl (r : rs) -> m (Rec StkEl (r : rs))
forall a b. (a -> b) -> a -> b
$ Value r -> StkEl r
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value r
a StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
PACK ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& Rec StkEl rs
r) = Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs)))
-> Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TBytes -> StkEl 'TBytes
forall (x :: T). Value x -> StkEl x
starNotesStkEl (ByteString -> Value 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value 'TBytes) -> ByteString -> Value 'TBytes
forall a b. (a -> b) -> a -> b
$ Value r -> ByteString
forall (t :: T). PackedValScope t => Value t -> ByteString
packValue' Value r
a) StkEl 'TBytes -> Rec StkEl rs -> Rec StkEl ('TBytes : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
UNPACK (StkEl (VBytes ByteString
a) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl ('TOption a : rs) -> m (Rec StkEl ('TOption a : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption a : rs) -> m (Rec StkEl ('TOption a : rs)))
-> Rec StkEl ('TOption a : rs) -> m (Rec StkEl ('TOption a : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TOption a) -> StkEl ('TOption a)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value' Instr a) -> Value ('TOption a)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' Instr a) -> Value ('TOption a))
-> (Either UnpackError (Value' Instr a) -> Maybe (Value' Instr a))
-> Either UnpackError (Value' Instr a)
-> Value ('TOption a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either UnpackError (Value' Instr a) -> Maybe (Value' Instr a)
forall l r. Either l r -> Maybe r
rightToMaybe (Either UnpackError (Value' Instr a) -> Value ('TOption a))
-> Either UnpackError (Value' Instr a) -> Value ('TOption a)
forall a b. (a -> b) -> a -> b
$ ByteString -> Either UnpackError (Value' Instr a)
forall (t :: T).
UnpackedValScope t =>
ByteString -> Either UnpackError (Value t)
runUnpack ByteString
a) StkEl ('TOption a) -> Rec StkEl rs -> Rec StkEl ('TOption a : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
CONCAT (StkEl r
a :& StkEl r
b :& Rec StkEl rs
r) = Rec StkEl (r : rs) -> m (Rec StkEl (r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (r : rs) -> m (Rec StkEl (r : rs)))
-> Rec StkEl (r : rs) -> m (Rec StkEl (r : rs))
forall a b. (a -> b) -> a -> b
$ Value r -> StkEl r
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Value r -> Value r -> Value r
forall (c :: T) (instr :: [T] -> [T] -> *).
ConcatOp c =>
Value' instr c -> Value' instr c -> Value' instr c
evalConcat (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
a) (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
b)) StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
CONCAT' (StkEl (VList [Value' Instr t]
a) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = Rec StkEl (t : rs) -> m (Rec StkEl (t : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (t : rs) -> m (Rec StkEl (t : rs)))
-> Rec StkEl (t : rs) -> m (Rec StkEl (t : rs))
forall a b. (a -> b) -> a -> b
$ Value' Instr t -> StkEl t
forall (x :: T). Value x -> StkEl x
starNotesStkEl ([Value' Instr t] -> Value' Instr t
forall (c :: T) (instr :: [T] -> [T] -> *).
ConcatOp c =>
[Value' instr c] -> Value' instr c
evalConcat' [Value' Instr t]
a) StkEl t -> Rec StkEl rs -> Rec StkEl (t : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
SLICE (StkEl (VNat Natural
o) VarAnn
_ Notes r
_ :& StkEl (VNat Natural
l) VarAnn
_ Notes r
_ :& StkEl Value r
s VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl ('TOption r : rs) -> m (Rec StkEl ('TOption r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption r : rs) -> m (Rec StkEl ('TOption r : rs)))
-> Rec StkEl ('TOption r : rs) -> m (Rec StkEl ('TOption r : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TOption r) -> StkEl ('TOption r)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value r) -> Value ('TOption r)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Natural -> Natural -> Value r -> Maybe (Value r)
forall (c :: T) (instr :: [T] -> [T] -> *).
SliceOp c =>
Natural -> Natural -> Value' instr c -> Maybe (Value' instr c)
evalSlice Natural
o Natural
l Value r
s)) StkEl ('TOption r) -> Rec StkEl rs -> Rec StkEl ('TOption r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
ISNAT (StkEl (VInt Integer
i) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
  then Rec StkEl ('TOption 'TNat : rs)
-> m (Rec StkEl ('TOption 'TNat : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption 'TNat : rs)
 -> m (Rec StkEl ('TOption 'TNat : rs)))
-> Rec StkEl ('TOption 'TNat : rs)
-> m (Rec StkEl ('TOption 'TNat : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TOption 'TNat) -> StkEl ('TOption 'TNat)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value 'TNat) -> Value ('TOption 'TNat)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption Maybe (Value 'TNat)
forall a. Maybe a
Nothing) StkEl ('TOption 'TNat)
-> Rec StkEl rs -> Rec StkEl ('TOption 'TNat : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
  else Rec StkEl ('TOption 'TNat : rs)
-> m (Rec StkEl ('TOption 'TNat : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption 'TNat : rs)
 -> m (Rec StkEl ('TOption 'TNat : rs)))
-> Rec StkEl ('TOption 'TNat : rs)
-> m (Rec StkEl ('TOption 'TNat : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TOption 'TNat) -> StkEl ('TOption 'TNat)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Maybe (Value 'TNat) -> Value ('TOption 'TNat)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Value 'TNat -> Maybe (Value 'TNat)
forall a. a -> Maybe a
Just (Natural -> Value 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural -> Value 'TNat) -> Natural -> Value 'TNat
forall a b. (a -> b) -> a -> b
$ Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i))) StkEl ('TOption 'TNat)
-> Rec StkEl rs -> Rec StkEl ('TOption 'TNat : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
ADD (StkEl r
l :& StkEl r
r :& Rec StkEl rs
rest) = (StkEl (ArithRes Add n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes Add n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes Add n m) -> Rec StkEl (ArithRes Add n m : rs))
-> m (StkEl (ArithRes Add n m))
-> m (Rec StkEl (ArithRes Add n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Add -> StkEl r -> StkEl r -> m (StkEl (ArithRes Add r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy Add
forall k (t :: k). Proxy t
Proxy @Add) StkEl r
l StkEl r
r
runInstrImpl InstrRunner m
_ Instr inp out
SUB (StkEl r
l :& StkEl r
r :& Rec StkEl rs
rest) = (StkEl (ArithRes Sub n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes Sub n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes Sub n m) -> Rec StkEl (ArithRes Sub n m : rs))
-> m (StkEl (ArithRes Sub n m))
-> m (Rec StkEl (ArithRes Sub n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Sub -> StkEl r -> StkEl r -> m (StkEl (ArithRes Sub r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy Sub
forall k (t :: k). Proxy t
Proxy @Sub) StkEl r
l StkEl r
r
runInstrImpl InstrRunner m
_ Instr inp out
MUL (StkEl r
l :& StkEl r
r :& Rec StkEl rs
rest) = (StkEl (ArithRes Mul n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes Mul n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes Mul n m) -> Rec StkEl (ArithRes Mul n m : rs))
-> m (StkEl (ArithRes Mul n m))
-> m (Rec StkEl (ArithRes Mul n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Mul -> StkEl r -> StkEl r -> m (StkEl (ArithRes Mul r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy Mul
forall k (t :: k). Proxy t
Proxy @Mul) StkEl r
l StkEl r
r
runInstrImpl InstrRunner m
_ Instr inp out
EDIV (StkEl r
l :& StkEl r
r :& Rec StkEl rs
rest) = Rec StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : rs)
-> m (Rec
        StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : rs)
 -> m (Rec
         StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : rs)))
-> Rec
     StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : rs)
-> m (Rec
        StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
-> StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Value' Instr r
-> Value' Instr r
-> Value' Instr ('TOption ('TPair (EDivOpRes r r) (EModOpRes r r)))
forall (n :: T) (m :: T) (instr :: [T] -> [T] -> *).
EDivOp n m =>
Value' instr n
-> Value' instr m
-> Value' instr ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
evalEDivOp (StkEl r -> Value' Instr r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
l) (StkEl r -> Value' Instr r
forall (x :: T). StkEl x -> Value x
seValue StkEl r
r)) StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)))
-> Rec StkEl rs
-> Rec
     StkEl ('TOption ('TPair (EDivOpRes n m) (EModOpRes n m)) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl InstrRunner m
_ Instr inp out
ABS ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Abs n : rs)
-> m (Rec StkEl (UnaryArithRes Abs n : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Abs n : rs)
 -> m (Rec StkEl (UnaryArithRes Abs n : rs)))
-> Rec StkEl (UnaryArithRes Abs n : rs)
-> m (Rec StkEl (UnaryArithRes Abs n : rs))
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Abs n) -> StkEl (UnaryArithRes Abs n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Abs -> Value r -> Value' Instr (UnaryArithRes Abs r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Abs
forall k (t :: k). Proxy t
Proxy @Abs) Value r
a) StkEl (UnaryArithRes Abs n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Abs n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl InstrRunner m
_ Instr inp out
NEG ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Neg n : rs)
-> m (Rec StkEl (UnaryArithRes Neg n : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Neg n : rs)
 -> m (Rec StkEl (UnaryArithRes Neg n : rs)))
-> Rec StkEl (UnaryArithRes Neg n : rs)
-> m (Rec StkEl (UnaryArithRes Neg n : rs))
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Neg n) -> StkEl (UnaryArithRes Neg n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Neg -> Value r -> Value' Instr (UnaryArithRes Neg r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Neg
forall k (t :: k). Proxy t
Proxy @Neg) Value r
a) StkEl (UnaryArithRes Neg n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Neg n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl InstrRunner m
_ Instr inp out
LSL (StkEl r
x :& StkEl r
s :& Rec StkEl rs
rest) = (StkEl (ArithRes Lsl n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes Lsl n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes Lsl n m) -> Rec StkEl (ArithRes Lsl n m : rs))
-> m (StkEl (ArithRes Lsl n m))
-> m (Rec StkEl (ArithRes Lsl n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Lsl -> StkEl r -> StkEl r -> m (StkEl (ArithRes Lsl r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy Lsl
forall k (t :: k). Proxy t
Proxy @Lsl) StkEl r
x StkEl r
s
runInstrImpl InstrRunner m
_ Instr inp out
LSR (StkEl r
x :& StkEl r
s :& Rec StkEl rs
rest) = (StkEl (ArithRes Lsr n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes Lsr n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes Lsr n m) -> Rec StkEl (ArithRes Lsr n m : rs))
-> m (StkEl (ArithRes Lsr n m))
-> m (Rec StkEl (ArithRes Lsr n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Lsr -> StkEl r -> StkEl r -> m (StkEl (ArithRes Lsr r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy Lsr
forall k (t :: k). Proxy t
Proxy @Lsr) StkEl r
x StkEl r
s
runInstrImpl InstrRunner m
_ Instr inp out
OR (StkEl r
l :& StkEl r
r :& Rec StkEl rs
rest) = (StkEl (ArithRes Or n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes Or n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes Or n m) -> Rec StkEl (ArithRes Or n m : rs))
-> m (StkEl (ArithRes Or n m))
-> m (Rec StkEl (ArithRes Or n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Or -> StkEl r -> StkEl r -> m (StkEl (ArithRes Or r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy Or
forall k (t :: k). Proxy t
Proxy @Or) StkEl r
l StkEl r
r
runInstrImpl InstrRunner m
_ Instr inp out
AND (StkEl r
l :& StkEl r
r :& Rec StkEl rs
rest) = (StkEl (ArithRes And n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes And n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes And n m) -> Rec StkEl (ArithRes And n m : rs))
-> m (StkEl (ArithRes And n m))
-> m (Rec StkEl (ArithRes And n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy And -> StkEl r -> StkEl r -> m (StkEl (ArithRes And r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy And
forall k (t :: k). Proxy t
Proxy @And) StkEl r
l StkEl r
r
runInstrImpl InstrRunner m
_ Instr inp out
XOR (StkEl r
l :& StkEl r
r :& Rec StkEl rs
rest) = (StkEl (ArithRes Xor n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes Xor n m : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl (ArithRes Xor n m) -> Rec StkEl (ArithRes Xor n m : rs))
-> m (StkEl (ArithRes Xor n m))
-> m (Rec StkEl (ArithRes Xor n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Xor -> StkEl r -> StkEl r -> m (StkEl (ArithRes Xor r r))
forall k (aop :: k) (n :: T) (m :: T) (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (Proxy Xor
forall k (t :: k). Proxy t
Proxy @Xor) StkEl r
l StkEl r
r
runInstrImpl InstrRunner m
_ Instr inp out
NOT ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Not n : rs)
-> m (Rec StkEl (UnaryArithRes Not n : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Not n : rs)
 -> m (Rec StkEl (UnaryArithRes Not n : rs)))
-> Rec StkEl (UnaryArithRes Not n : rs)
-> m (Rec StkEl (UnaryArithRes Not n : rs))
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Not n) -> StkEl (UnaryArithRes Not n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Not -> Value r -> Value' Instr (UnaryArithRes Not r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Not
forall k (t :: k). Proxy t
Proxy @Not) Value r
a) StkEl (UnaryArithRes Not n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Not n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl InstrRunner m
_ Instr inp out
COMPARE ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
l) :& (StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
r) :& Rec StkEl rs
rest) =
  Rec StkEl ('TInt : rs) -> m (Rec StkEl ('TInt : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TInt : rs) -> m (Rec StkEl ('TInt : rs)))
-> Rec StkEl ('TInt : rs) -> m (Rec StkEl ('TInt : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TInt -> StkEl 'TInt
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Integer -> Value 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
T.VInt (Value r -> Value r -> Integer
forall (t :: T) (i :: [T] -> [T] -> *).
Comparable t =>
Value' i t -> Value' i t -> Integer
compareOp Value r
l Value r
Value r
r)) StkEl 'TInt -> Rec StkEl rs -> Rec StkEl ('TInt : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl InstrRunner m
_ Instr inp out
EQ ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Eq' n : rs)
-> m (Rec StkEl (UnaryArithRes Eq' n : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Eq' n : rs)
 -> m (Rec StkEl (UnaryArithRes Eq' n : rs)))
-> Rec StkEl (UnaryArithRes Eq' n : rs)
-> m (Rec StkEl (UnaryArithRes Eq' n : rs))
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Eq' n) -> StkEl (UnaryArithRes Eq' n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Eq' -> Value r -> Value' Instr (UnaryArithRes Eq' r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Eq'
forall k (t :: k). Proxy t
Proxy @Eq') Value r
a) StkEl (UnaryArithRes Eq' n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Eq' n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl InstrRunner m
_ Instr inp out
NEQ ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Neq n : rs)
-> m (Rec StkEl (UnaryArithRes Neq n : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Neq n : rs)
 -> m (Rec StkEl (UnaryArithRes Neq n : rs)))
-> Rec StkEl (UnaryArithRes Neq n : rs)
-> m (Rec StkEl (UnaryArithRes Neq n : rs))
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Neq n) -> StkEl (UnaryArithRes Neq n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Neq -> Value r -> Value' Instr (UnaryArithRes Neq r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Neq
forall k (t :: k). Proxy t
Proxy @Neq) Value r
a) StkEl (UnaryArithRes Neq n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Neq n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl InstrRunner m
_ Instr inp out
LT ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Lt n : rs)
-> m (Rec StkEl (UnaryArithRes Lt n : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Lt n : rs)
 -> m (Rec StkEl (UnaryArithRes Lt n : rs)))
-> Rec StkEl (UnaryArithRes Lt n : rs)
-> m (Rec StkEl (UnaryArithRes Lt n : rs))
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Lt n) -> StkEl (UnaryArithRes Lt n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Lt -> Value r -> Value' Instr (UnaryArithRes Lt r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Lt
forall k (t :: k). Proxy t
Proxy @Lt) Value r
a) StkEl (UnaryArithRes Lt n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Lt n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl InstrRunner m
_ Instr inp out
GT ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Gt n : rs)
-> m (Rec StkEl (UnaryArithRes Gt n : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Gt n : rs)
 -> m (Rec StkEl (UnaryArithRes Gt n : rs)))
-> Rec StkEl (UnaryArithRes Gt n : rs)
-> m (Rec StkEl (UnaryArithRes Gt n : rs))
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Gt n) -> StkEl (UnaryArithRes Gt n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Gt -> Value r -> Value' Instr (UnaryArithRes Gt r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Gt
forall k (t :: k). Proxy t
Proxy @Gt) Value r
a) StkEl (UnaryArithRes Gt n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Gt n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl InstrRunner m
_ Instr inp out
LE ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Le n : rs)
-> m (Rec StkEl (UnaryArithRes Le n : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Le n : rs)
 -> m (Rec StkEl (UnaryArithRes Le n : rs)))
-> Rec StkEl (UnaryArithRes Le n : rs)
-> m (Rec StkEl (UnaryArithRes Le n : rs))
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Le n) -> StkEl (UnaryArithRes Le n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Le -> Value r -> Value' Instr (UnaryArithRes Le r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Le
forall k (t :: k). Proxy t
Proxy @Le) Value r
a) StkEl (UnaryArithRes Le n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Le n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl InstrRunner m
_ Instr inp out
GE ((StkEl r -> Value r
forall (x :: T). StkEl x -> Value x
seValue -> Value r
a) :& Rec StkEl rs
rest) =
  Rec StkEl (UnaryArithRes Ge n : rs)
-> m (Rec StkEl (UnaryArithRes Ge n : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (UnaryArithRes Ge n : rs)
 -> m (Rec StkEl (UnaryArithRes Ge n : rs)))
-> Rec StkEl (UnaryArithRes Ge n : rs)
-> m (Rec StkEl (UnaryArithRes Ge n : rs))
forall a b. (a -> b) -> a -> b
$ Value (UnaryArithRes Ge n) -> StkEl (UnaryArithRes Ge n)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Proxy Ge -> Value r -> Value' Instr (UnaryArithRes Ge r)
forall k (aop :: k) (n :: T) (proxy :: k -> *)
       (instr :: [T] -> [T] -> *).
UnaryArithOp aop n =>
proxy aop -> Value' instr n -> Value' instr (UnaryArithRes aop n)
evalUnaryArithOp (Proxy Ge
forall k (t :: k). Proxy t
Proxy @Ge) Value r
a) StkEl (UnaryArithRes Ge n)
-> Rec StkEl rs -> Rec StkEl (UnaryArithRes Ge n : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest
runInstrImpl InstrRunner m
_ Instr inp out
INT (StkEl Value r
a VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl ('TInt : rs) -> m (Rec StkEl ('TInt : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TInt : rs) -> m (Rec StkEl ('TInt : rs)))
-> Rec StkEl ('TInt : rs) -> m (Rec StkEl ('TInt : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TInt -> StkEl 'TInt
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Value r -> Value 'TInt
forall (n :: T) (instr :: [T] -> [T] -> *).
ToIntArithOp n =>
Value' instr n -> Value' instr 'TInt
evalToIntOp Value r
a) StkEl 'TInt -> Rec StkEl rs -> Rec StkEl ('TInt : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ (SELF SomeEntrypointCallT arg
sepc :: Instr inp out) Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
TcOriginatedContracts
ChainId
Timestamp
Mutez
GlobalCounter
Address
VotingPowers
RemainingSteps
ceLevel :: Natural
ceGlobalCounter :: GlobalCounter
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: Address
ceSource :: Address
ceSelf :: Address
ceContracts :: TcOriginatedContracts
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceLevel :: ContractEnv -> Natural
ceGlobalCounter :: ContractEnv -> GlobalCounter
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> Address
ceSource :: ContractEnv -> Address
ceSelf :: ContractEnv -> Address
ceContracts :: ContractEnv -> TcOriginatedContracts
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  case Proxy out
forall k (t :: k). Proxy t
Proxy @out of
    (_ :: Proxy ('TContract cp ': s)) -> do
      Rec StkEl ('TContract arg : inp)
-> m (Rec StkEl ('TContract arg : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TContract arg : inp)
 -> m (Rec StkEl ('TContract arg : inp)))
-> Rec StkEl ('TContract arg : inp)
-> m (Rec StkEl ('TContract arg : inp))
forall a b. (a -> b) -> a -> b
$ Value ('TContract arg) -> StkEl ('TContract arg)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Address -> SomeEntrypointCallT arg -> Value ('TContract arg)
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, HasNoOp arg) =>
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract Address
ceSelf SomeEntrypointCallT arg
sepc) StkEl ('TContract arg)
-> Rec StkEl inp -> Rec StkEl ('TContract arg : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ (CONTRACT (Notes p
nt :: T.Notes a) EpName
instrEpName) (StkEl (VAddress EpAddress
epAddr) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = do
  ContractEnv{Natural
Maybe OperationHash
TcOriginatedContracts
ChainId
Timestamp
Mutez
GlobalCounter
Address
VotingPowers
RemainingSteps
ceLevel :: Natural
ceGlobalCounter :: GlobalCounter
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: Address
ceSource :: Address
ceSelf :: Address
ceContracts :: TcOriginatedContracts
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceLevel :: ContractEnv -> Natural
ceGlobalCounter :: ContractEnv -> GlobalCounter
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> Address
ceSource :: ContractEnv -> Address
ceSelf :: ContractEnv -> Address
ceContracts :: ContractEnv -> TcOriginatedContracts
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  let T.EpAddress Address
addr EpName
addrEpName = EpAddress
epAddr
  let mepName :: Maybe EpName
mepName =
        case (EpName
instrEpName, EpName
addrEpName) of
          (EpName
DefEpName, EpName
DefEpName) -> EpName -> Maybe EpName
forall a. a -> Maybe a
Just EpName
DefEpName
          (EpName
DefEpName, EpName
en) -> EpName -> Maybe EpName
forall a. a -> Maybe a
Just EpName
en
          (EpName
en, EpName
DefEpName) -> EpName -> Maybe EpName
forall a. a -> Maybe a
Just EpName
en
          (EpName, EpName)
_ -> Maybe EpName
forall a. Maybe a
Nothing

  let withNotes :: Value ('TOption ('TContract p))
-> Rec StkEl ('TOption ('TContract p) : rs)
withNotes Value ('TOption ('TContract p))
v = Value ('TOption ('TContract p))
-> VarAnn
-> Notes ('TOption ('TContract p))
-> StkEl ('TOption ('TContract p))
forall (t :: T). Value t -> VarAnn -> Notes t -> StkEl t
StkEl Value ('TOption ('TContract p))
v VarAnn
forall k (a :: k). Annotation a
U.noAnn (TypeAnn -> Notes ('TContract p) -> Notes ('TOption ('TContract p))
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
forall k (a :: k). Annotation a
U.noAnn (Notes ('TContract p) -> Notes ('TOption ('TContract p)))
-> Notes ('TContract p) -> Notes ('TOption ('TContract p))
forall a b. (a -> b) -> a -> b
$ TypeAnn -> Notes p -> Notes ('TContract p)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TContract t)
NTContract TypeAnn
forall k (a :: k). Annotation a
U.noAnn Notes p
nt) StkEl ('TOption ('TContract p))
-> Rec StkEl rs -> Rec StkEl ('TOption ('TContract p) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
  Rec StkEl ('TOption ('TContract p) : rs)
-> m (Rec StkEl ('TOption ('TContract p) : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption ('TContract p) : rs)
 -> m (Rec StkEl ('TOption ('TContract p) : rs)))
-> Rec StkEl ('TOption ('TContract p) : rs)
-> m (Rec StkEl ('TOption ('TContract p) : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TOption ('TContract p))
-> Rec StkEl ('TOption ('TContract p) : rs)
withNotes (Value ('TOption ('TContract p))
 -> Rec StkEl ('TOption ('TContract p) : rs))
-> Value ('TOption ('TContract p))
-> Rec StkEl ('TOption ('TContract p) : rs)
forall a b. (a -> b) -> a -> b
$ case Maybe EpName
mepName of
    Maybe EpName
Nothing -> Maybe (Value' Instr ('TContract p))
-> Value ('TOption ('TContract p))
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption Maybe (Value' Instr ('TContract p))
forall a. Maybe a
Nothing
    Just EpName
epName ->
      case Address
addr of
        KeyAddress KeyHash
_ -> Address
-> EpName -> ParamNotes 'TUnit -> Value ('TOption ('TContract p))
forall (p :: T).
ParameterScope p =>
Address
-> EpName -> ParamNotes p -> Value ('TOption ('TContract p))
castContract Address
addr EpName
epName ParamNotes 'TUnit
T.tyImplicitAccountParam
        ContractAddress 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 Sing t
_ 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
            Maybe SomeParamType
Nothing -> Maybe (Value' Instr ('TContract p))
-> Value ('TOption ('TContract p))
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption Maybe (Value' Instr ('TContract p))
forall a. Maybe a
Nothing
  where
  castContract
    :: forall p. T.ParameterScope p
    => Address -> EpName -> T.ParamNotes p -> T.Value ('TOption ('TContract a))
  castContract :: Address
-> EpName -> ParamNotes p -> Value ('TOption ('TContract p))
castContract Address
addr EpName
epName ParamNotes p
param = Maybe (Value' Instr ('TContract p))
-> Value ('TOption ('TContract p))
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI 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 Notes arg
na 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 (p :~: arg
Refl, Notes p
_) <- 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 '[SingI] '[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 arg))
forall (m :: * -> *) a. Monad m => a -> m a
return (Value' Instr ('TContract arg)
 -> Maybe (Value' Instr ('TContract arg)))
-> Value' Instr ('TContract arg)
-> Maybe (Value' Instr ('TContract arg))
forall a b. (a -> b) -> a -> b
$ Address -> SomeEntrypointCallT arg -> Value' Instr ('TContract arg)
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, HasNoOp arg) =>
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 InstrRunner m
_ Instr inp out
TRANSFER_TOKENS
  (StkEl Value r
p VarAnn
_ Notes r
_ :& StkEl (VMutez Mutez
mutez) VarAnn
_ Notes r
_ :& StkEl Value r
contract VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl ('TOperation : rs) -> m (Rec StkEl ('TOperation : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOperation : rs) -> m (Rec StkEl ('TOperation : rs)))
-> Rec StkEl ('TOperation : rs) -> m (Rec StkEl ('TOperation : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TOperation -> StkEl 'TOperation
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Operation -> Value 'TOperation
forall (instr :: [T] -> [T] -> *).
Operation' instr -> Value' instr 'TOperation
VOp (TransferTokens Instr r -> Operation
forall (p :: T) (instr :: [T] -> [T] -> *).
ParameterScope p =>
TransferTokens instr p -> Operation' instr
OpTransferTokens (TransferTokens Instr r -> Operation)
-> TransferTokens Instr r -> Operation
forall a b. (a -> b) -> a -> b
$ Value r
-> Mutez -> Value' Instr ('TContract r) -> TransferTokens Instr r
forall (instr :: [T] -> [T] -> *) (p :: T).
Value' instr p
-> Mutez -> Value' instr ('TContract p) -> TransferTokens instr p
TransferTokens Value r
p Mutez
mutez Value r
Value' Instr ('TContract r)
contract)) StkEl 'TOperation -> Rec StkEl rs -> Rec StkEl ('TOperation : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
SET_DELEGATE (StkEl (VOption Maybe (Value' Instr t)
mbKeyHash) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  case Maybe (Value' Instr t)
mbKeyHash of
    Just (VKeyHash KeyHash
k) -> Rec StkEl ('TOperation : rs) -> m (Rec StkEl ('TOperation : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOperation : rs) -> m (Rec StkEl ('TOperation : rs)))
-> Rec StkEl ('TOperation : rs) -> m (Rec StkEl ('TOperation : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TOperation -> StkEl 'TOperation
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Operation -> Value 'TOperation
forall (instr :: [T] -> [T] -> *).
Operation' instr -> Value' instr 'TOperation
VOp (SetDelegate -> Operation
forall (instr :: [T] -> [T] -> *). SetDelegate -> Operation' instr
OpSetDelegate (SetDelegate -> Operation) -> SetDelegate -> Operation
forall a b. (a -> b) -> a -> b
$ Maybe KeyHash -> SetDelegate
SetDelegate (Maybe KeyHash -> SetDelegate) -> Maybe KeyHash -> SetDelegate
forall a b. (a -> b) -> a -> b
$ KeyHash -> Maybe KeyHash
forall a. a -> Maybe a
Just KeyHash
k)) StkEl 'TOperation -> Rec StkEl rs -> Rec StkEl ('TOperation : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
    Maybe (Value' Instr t)
Nothing -> Rec StkEl ('TOperation : rs) -> m (Rec StkEl ('TOperation : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOperation : rs) -> m (Rec StkEl ('TOperation : rs)))
-> Rec StkEl ('TOperation : rs) -> m (Rec StkEl ('TOperation : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TOperation -> StkEl 'TOperation
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Operation -> Value 'TOperation
forall (instr :: [T] -> [T] -> *).
Operation' instr -> Value' instr 'TOperation
VOp (SetDelegate -> Operation
forall (instr :: [T] -> [T] -> *). SetDelegate -> Operation' instr
OpSetDelegate (SetDelegate -> Operation) -> SetDelegate -> Operation
forall a b. (a -> b) -> a -> b
$ Maybe KeyHash -> SetDelegate
SetDelegate (Maybe KeyHash -> SetDelegate) -> Maybe KeyHash -> SetDelegate
forall a b. (a -> b) -> a -> b
$ Maybe KeyHash
forall a. Maybe a
Nothing)) StkEl 'TOperation -> Rec StkEl rs -> Rec StkEl ('TOperation : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ (CREATE_CONTRACT Contract p g
contract)
  (StkEl (VOption Maybe (Value' Instr t)
mbKeyHash) VarAnn
_ Notes r
_ :& StkEl (VMutez Mutez
m) VarAnn
_ Notes r
_ :& StkEl Value r
g VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = do
  Address
originator <- ContractEnv -> Address
ceSelf (ContractEnv -> Address) -> m ContractEnv -> m Address
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask

  OriginationIndex
originationNonce <- InterpreterState -> OriginationIndex
isOriginationNonce (InterpreterState -> OriginationIndex)
-> m InterpreterState -> m OriginationIndex
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m InterpreterState
forall (m :: * -> *). InterpreterStateMonad m => m InterpreterState
getInterpreterState
  GlobalCounter
globalCounter <- (ContractEnv -> GlobalCounter) -> m GlobalCounter
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ContractEnv -> GlobalCounter
ceGlobalCounter
  Maybe OperationHash
opHash <- ContractEnv -> Maybe OperationHash
ceOperationHash (ContractEnv -> Maybe OperationHash)
-> m ContractEnv -> m (Maybe OperationHash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  (InterpreterState -> InterpreterState) -> m ()
forall (m :: * -> *).
InterpreterStateMonad m =>
(InterpreterState -> InterpreterState) -> m ()
modifyInterpreterState ((InterpreterState -> InterpreterState) -> m ())
-> (InterpreterState -> InterpreterState) -> m ()
forall a b. (a -> b) -> a -> b
$ \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
+ Int32
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 OperationHash
hash -> OperationHash -> OriginationIndex -> GlobalCounter -> Address
mkContractAddress OperationHash
hash OriginationIndex
originationNonce GlobalCounter
globalCounter
          Maybe OperationHash
Nothing ->
            OperationHash -> OriginationIndex -> GlobalCounter -> Address
mkContractAddress
              (OriginationOperation -> OperationHash
mkOriginationOperationHash (Address
-> Maybe (Value 'TKeyHash)
-> Mutez
-> Contract p g
-> Value' Instr g
-> OriginationOperation
forall (param :: T) (store :: T).
(ParameterScope param, StorageScope store) =>
Address
-> Maybe (Value 'TKeyHash)
-> Mutez
-> Contract param store
-> Value' Instr store
-> OriginationOperation
createOrigOp Address
originator Maybe (Value' Instr t)
Maybe (Value 'TKeyHash)
mbKeyHash Mutez
m Contract p g
contract Value' Instr g
Value r
g))
              -- If opHash is Nothing it means that interpreter is running in some kind of test
              -- context, therefore we generate dummy contract address with its own origination
              -- operation.
              OriginationIndex
originationNonce
              GlobalCounter
globalCounter
  let resEpAddr :: EpAddress
resEpAddr = Address -> EpName -> EpAddress
EpAddress Address
resAddr EpName
DefEpName
  let resOp :: CreateContract Instr p r
resOp = Address
-> Maybe KeyHash
-> Mutez
-> Value r
-> Instr (ContractInp p r) (ContractOut r)
-> CreateContract Instr p r
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
(Show (instr (ContractInp cp st) (ContractOut st)),
 Eq (instr (ContractInp cp st) (ContractOut st))) =>
Address
-> Maybe KeyHash
-> Mutez
-> Value' instr st
-> instr (ContractInp cp st) (ContractOut st)
-> CreateContract instr cp st
CreateContract Address
originator (Maybe (Value 'TKeyHash) -> Maybe KeyHash
unwrapMbKeyHash Maybe (Value' Instr t)
Maybe (Value 'TKeyHash)
mbKeyHash) Mutez
m Value r
g ContractCode p g
Instr (ContractInp p r) (ContractOut r)
ops
  Rec StkEl ('TOperation : 'TAddress : rs)
-> m (Rec StkEl ('TOperation : 'TAddress : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOperation : 'TAddress : rs)
 -> m (Rec StkEl ('TOperation : 'TAddress : rs)))
-> Rec StkEl ('TOperation : 'TAddress : rs)
-> m (Rec StkEl ('TOperation : 'TAddress : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TOperation -> StkEl 'TOperation
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Operation -> Value 'TOperation
forall (instr :: [T] -> [T] -> *).
Operation' instr -> Value' instr 'TOperation
VOp (CreateContract Instr p r -> Operation
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
(Show (instr (ContractInp cp st) (ContractOut st)),
 NFData (instr (ContractInp cp st) (ContractOut st)),
 Typeable instr, ParameterScope cp, StorageScope st) =>
CreateContract instr cp st -> Operation' instr
OpCreateContract CreateContract Instr p r
resOp))
      StkEl 'TOperation
-> Rec StkEl ('TAddress : rs)
-> Rec StkEl ('TOperation : 'TAddress : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Value 'TAddress -> StkEl 'TAddress
forall (x :: T). Value x -> StkEl x
starNotesStkEl (EpAddress -> Value 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress EpAddress
resEpAddr)
      StkEl 'TAddress -> Rec StkEl rs -> Rec StkEl ('TAddress : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
IMPLICIT_ACCOUNT (StkEl (VKeyHash KeyHash
k) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl ('TContract 'TUnit : rs)
-> m (Rec StkEl ('TContract 'TUnit : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TContract 'TUnit : rs)
 -> m (Rec StkEl ('TContract 'TUnit : rs)))
-> Rec StkEl ('TContract 'TUnit : rs)
-> m (Rec StkEl ('TContract 'TUnit : rs))
forall a b. (a -> b) -> a -> b
$ (Value ('TContract 'TUnit) -> StkEl ('TContract 'TUnit)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Address -> SomeEntrypointCallT 'TUnit -> Value ('TContract 'TUnit)
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, HasNoOp arg) =>
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract (KeyHash -> Address
KeyAddress KeyHash
k) SomeEntrypointCallT 'TUnit
forall (t :: T).
(ParameterScope t, ForbidOr t) =>
SomeEntrypointCallT t
sepcPrimitive)) StkEl ('TContract 'TUnit)
-> Rec StkEl rs -> Rec StkEl ('TContract 'TUnit : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
NOW Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
TcOriginatedContracts
ChainId
Timestamp
Mutez
GlobalCounter
Address
VotingPowers
RemainingSteps
ceLevel :: Natural
ceGlobalCounter :: GlobalCounter
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: Address
ceSource :: Address
ceSelf :: Address
ceContracts :: TcOriginatedContracts
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceLevel :: ContractEnv -> Natural
ceGlobalCounter :: ContractEnv -> GlobalCounter
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> Address
ceSource :: ContractEnv -> Address
ceSelf :: ContractEnv -> Address
ceContracts :: ContractEnv -> TcOriginatedContracts
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TTimestamp : inp) -> m (Rec StkEl ('TTimestamp : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TTimestamp : inp)
 -> m (Rec StkEl ('TTimestamp : inp)))
-> Rec StkEl ('TTimestamp : inp)
-> m (Rec StkEl ('TTimestamp : inp))
forall a b. (a -> b) -> a -> b
$ Value 'TTimestamp -> StkEl 'TTimestamp
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Timestamp -> Value 'TTimestamp
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp Timestamp
ceNow) StkEl 'TTimestamp -> Rec StkEl inp -> Rec StkEl ('TTimestamp : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
AMOUNT Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
TcOriginatedContracts
ChainId
Timestamp
Mutez
GlobalCounter
Address
VotingPowers
RemainingSteps
ceLevel :: Natural
ceGlobalCounter :: GlobalCounter
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: Address
ceSource :: Address
ceSelf :: Address
ceContracts :: TcOriginatedContracts
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceLevel :: ContractEnv -> Natural
ceGlobalCounter :: ContractEnv -> GlobalCounter
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> Address
ceSource :: ContractEnv -> Address
ceSelf :: ContractEnv -> Address
ceContracts :: ContractEnv -> TcOriginatedContracts
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TMutez : inp) -> m (Rec StkEl ('TMutez : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TMutez : inp) -> m (Rec StkEl ('TMutez : inp)))
-> Rec StkEl ('TMutez : inp) -> m (Rec StkEl ('TMutez : inp))
forall a b. (a -> b) -> a -> b
$ Value 'TMutez -> StkEl 'TMutez
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Mutez -> Value 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez Mutez
ceAmount) StkEl 'TMutez -> Rec StkEl inp -> Rec StkEl ('TMutez : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
BALANCE Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
TcOriginatedContracts
ChainId
Timestamp
Mutez
GlobalCounter
Address
VotingPowers
RemainingSteps
ceLevel :: Natural
ceGlobalCounter :: GlobalCounter
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: Address
ceSource :: Address
ceSelf :: Address
ceContracts :: TcOriginatedContracts
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceLevel :: ContractEnv -> Natural
ceGlobalCounter :: ContractEnv -> GlobalCounter
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> Address
ceSource :: ContractEnv -> Address
ceSelf :: ContractEnv -> Address
ceContracts :: ContractEnv -> TcOriginatedContracts
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TMutez : inp) -> m (Rec StkEl ('TMutez : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TMutez : inp) -> m (Rec StkEl ('TMutez : inp)))
-> Rec StkEl ('TMutez : inp) -> m (Rec StkEl ('TMutez : inp))
forall a b. (a -> b) -> a -> b
$ Value 'TMutez -> StkEl 'TMutez
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Mutez -> Value 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez Mutez
ceBalance) StkEl 'TMutez -> Rec StkEl inp -> Rec StkEl ('TMutez : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
VOTING_POWER (StkEl (VKeyHash KeyHash
k) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = do
  ContractEnv{Natural
Maybe OperationHash
TcOriginatedContracts
ChainId
Timestamp
Mutez
GlobalCounter
Address
VotingPowers
RemainingSteps
ceLevel :: Natural
ceGlobalCounter :: GlobalCounter
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: Address
ceSource :: Address
ceSelf :: Address
ceContracts :: TcOriginatedContracts
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceLevel :: ContractEnv -> Natural
ceGlobalCounter :: ContractEnv -> GlobalCounter
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> Address
ceSource :: ContractEnv -> Address
ceSelf :: ContractEnv -> Address
ceContracts :: ContractEnv -> TcOriginatedContracts
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TNat : rs) -> m (Rec StkEl ('TNat : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TNat : rs) -> m (Rec StkEl ('TNat : rs)))
-> Rec StkEl ('TNat : rs) -> m (Rec StkEl ('TNat : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TNat -> StkEl 'TNat
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Natural -> Value 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural -> Value 'TNat) -> Natural -> Value 'TNat
forall a b. (a -> b) -> a -> b
$ KeyHash -> VotingPowers -> Natural
vpPick KeyHash
k VotingPowers
ceVotingPowers) StkEl 'TNat -> Rec StkEl rs -> Rec StkEl ('TNat : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
TOTAL_VOTING_POWER Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
TcOriginatedContracts
ChainId
Timestamp
Mutez
GlobalCounter
Address
VotingPowers
RemainingSteps
ceLevel :: Natural
ceGlobalCounter :: GlobalCounter
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: Address
ceSource :: Address
ceSelf :: Address
ceContracts :: TcOriginatedContracts
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceLevel :: ContractEnv -> Natural
ceGlobalCounter :: ContractEnv -> GlobalCounter
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> Address
ceSource :: ContractEnv -> Address
ceSelf :: ContractEnv -> Address
ceContracts :: ContractEnv -> TcOriginatedContracts
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TNat : inp) -> m (Rec StkEl ('TNat : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TNat : inp) -> m (Rec StkEl ('TNat : inp)))
-> Rec StkEl ('TNat : inp) -> m (Rec StkEl ('TNat : inp))
forall a b. (a -> b) -> a -> b
$ Value 'TNat -> StkEl 'TNat
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Natural -> Value 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural -> Value 'TNat) -> Natural -> Value 'TNat
forall a b. (a -> b) -> a -> b
$ VotingPowers -> Natural
vpTotal VotingPowers
ceVotingPowers) StkEl 'TNat -> Rec StkEl inp -> Rec StkEl ('TNat : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
CHECK_SIGNATURE
  (StkEl (VKey PublicKey
k) VarAnn
_ Notes r
_ :& StkEl (VSignature Signature
v) VarAnn
_ Notes r
_ :& StkEl (VBytes ByteString
b) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl ('TBool : rs) -> m (Rec StkEl ('TBool : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBool : rs) -> m (Rec StkEl ('TBool : rs)))
-> Rec StkEl ('TBool : rs) -> m (Rec StkEl ('TBool : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TBool -> StkEl 'TBool
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Bool -> Value 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Bool -> Value 'TBool) -> Bool -> Value 'TBool
forall a b. (a -> b) -> a -> b
$ PublicKey -> Signature -> ByteString -> Bool
checkSignature PublicKey
k Signature
v ByteString
b) StkEl 'TBool -> Rec StkEl rs -> Rec StkEl ('TBool : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
SHA256 (StkEl (VBytes ByteString
b) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs)))
-> Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TBytes -> StkEl 'TBytes
forall (x :: T). Value x -> StkEl x
starNotesStkEl (ByteString -> Value 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value 'TBytes) -> ByteString -> Value 'TBytes
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
sha256 ByteString
b) StkEl 'TBytes -> Rec StkEl rs -> Rec StkEl ('TBytes : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
SHA512 (StkEl (VBytes ByteString
b) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs)))
-> Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TBytes -> StkEl 'TBytes
forall (x :: T). Value x -> StkEl x
starNotesStkEl (ByteString -> Value 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value 'TBytes) -> ByteString -> Value 'TBytes
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
sha512 ByteString
b) StkEl 'TBytes -> Rec StkEl rs -> Rec StkEl ('TBytes : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
BLAKE2B (StkEl (VBytes ByteString
b) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs)))
-> Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TBytes -> StkEl 'TBytes
forall (x :: T). Value x -> StkEl x
starNotesStkEl (ByteString -> Value 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value 'TBytes) -> ByteString -> Value 'TBytes
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
blake2b ByteString
b) StkEl 'TBytes -> Rec StkEl rs -> Rec StkEl ('TBytes : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
SHA3 (StkEl (VBytes ByteString
b) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs)))
-> Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TBytes -> StkEl 'TBytes
forall (x :: T). Value x -> StkEl x
starNotesStkEl (ByteString -> Value 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value 'TBytes) -> ByteString -> Value 'TBytes
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
sha3 ByteString
b) StkEl 'TBytes -> Rec StkEl rs -> Rec StkEl ('TBytes : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
KECCAK (StkEl (VBytes ByteString
b) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs)))
-> Rec StkEl ('TBytes : rs) -> m (Rec StkEl ('TBytes : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TBytes -> StkEl 'TBytes
forall (x :: T). Value x -> StkEl x
starNotesStkEl (ByteString -> Value 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value 'TBytes) -> ByteString -> Value 'TBytes
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
keccak ByteString
b) StkEl 'TBytes -> Rec StkEl rs -> Rec StkEl ('TBytes : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
HASH_KEY (StkEl (VKey PublicKey
k) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl ('TKeyHash : rs) -> m (Rec StkEl ('TKeyHash : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TKeyHash : rs) -> m (Rec StkEl ('TKeyHash : rs)))
-> Rec StkEl ('TKeyHash : rs) -> m (Rec StkEl ('TKeyHash : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TKeyHash -> StkEl 'TKeyHash
forall (x :: T). Value x -> StkEl x
starNotesStkEl (KeyHash -> Value 'TKeyHash
forall (instr :: [T] -> [T] -> *).
KeyHash -> Value' instr 'TKeyHash
VKeyHash (KeyHash -> Value 'TKeyHash) -> KeyHash -> Value 'TKeyHash
forall a b. (a -> b) -> a -> b
$ PublicKey -> KeyHash
hashKey PublicKey
k) StkEl 'TKeyHash -> Rec StkEl rs -> Rec StkEl ('TKeyHash : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
PAIRING_CHECK (StkEl (VList [Value' Instr t]
pairs) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = do
  let pairs' :: [(Bls12381G1, Bls12381G2)]
pairs' = [ (Bls12381G1
g1, Bls12381G2
g2) | VPair (VBls12381G1 Bls12381G1
g1, VBls12381G2 Bls12381G2
g2) <- [Value' Instr t]
pairs ]
  Rec StkEl ('TBool : rs) -> m (Rec StkEl ('TBool : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TBool : rs) -> m (Rec StkEl ('TBool : rs)))
-> Rec StkEl ('TBool : rs) -> m (Rec StkEl ('TBool : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TBool -> StkEl 'TBool
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Bool -> Value 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool (Bool -> Value 'TBool) -> Bool -> Value 'TBool
forall a b. (a -> b) -> a -> b
$ [(Bls12381G1, Bls12381G2)] -> Bool
checkPairing [(Bls12381G1, Bls12381G2)]
pairs') StkEl 'TBool -> Rec StkEl rs -> Rec StkEl ('TBool : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
SOURCE Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
TcOriginatedContracts
ChainId
Timestamp
Mutez
GlobalCounter
Address
VotingPowers
RemainingSteps
ceLevel :: Natural
ceGlobalCounter :: GlobalCounter
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: Address
ceSource :: Address
ceSelf :: Address
ceContracts :: TcOriginatedContracts
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceLevel :: ContractEnv -> Natural
ceGlobalCounter :: ContractEnv -> GlobalCounter
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> Address
ceSource :: ContractEnv -> Address
ceSelf :: ContractEnv -> Address
ceContracts :: ContractEnv -> TcOriginatedContracts
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TAddress : inp) -> m (Rec StkEl ('TAddress : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TAddress : inp) -> m (Rec StkEl ('TAddress : inp)))
-> Rec StkEl ('TAddress : inp) -> m (Rec StkEl ('TAddress : inp))
forall a b. (a -> b) -> a -> b
$ Value 'TAddress -> StkEl 'TAddress
forall (x :: T). Value x -> StkEl x
starNotesStkEl (EpAddress -> Value 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (EpAddress -> Value 'TAddress) -> EpAddress -> Value 'TAddress
forall a b. (a -> b) -> a -> b
$ Address -> EpName -> EpAddress
EpAddress Address
ceSource EpName
DefEpName) StkEl 'TAddress -> Rec StkEl inp -> Rec StkEl ('TAddress : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
SENDER Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
TcOriginatedContracts
ChainId
Timestamp
Mutez
GlobalCounter
Address
VotingPowers
RemainingSteps
ceLevel :: Natural
ceGlobalCounter :: GlobalCounter
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: Address
ceSource :: Address
ceSelf :: Address
ceContracts :: TcOriginatedContracts
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceLevel :: ContractEnv -> Natural
ceGlobalCounter :: ContractEnv -> GlobalCounter
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> Address
ceSource :: ContractEnv -> Address
ceSelf :: ContractEnv -> Address
ceContracts :: ContractEnv -> TcOriginatedContracts
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TAddress : inp) -> m (Rec StkEl ('TAddress : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TAddress : inp) -> m (Rec StkEl ('TAddress : inp)))
-> Rec StkEl ('TAddress : inp) -> m (Rec StkEl ('TAddress : inp))
forall a b. (a -> b) -> a -> b
$ Value 'TAddress -> StkEl 'TAddress
forall (x :: T). Value x -> StkEl x
starNotesStkEl (EpAddress -> Value 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (EpAddress -> Value 'TAddress) -> EpAddress -> Value 'TAddress
forall a b. (a -> b) -> a -> b
$ Address -> EpName -> EpAddress
EpAddress Address
ceSender EpName
DefEpName) StkEl 'TAddress -> Rec StkEl inp -> Rec StkEl ('TAddress : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
ADDRESS (StkEl (VContract Address
a SomeEntrypointCallT arg
sepc) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) =
  Rec StkEl ('TAddress : rs) -> m (Rec StkEl ('TAddress : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TAddress : rs) -> m (Rec StkEl ('TAddress : rs)))
-> Rec StkEl ('TAddress : rs) -> m (Rec StkEl ('TAddress : rs))
forall a b. (a -> b) -> a -> b
$ Value 'TAddress -> StkEl 'TAddress
forall (x :: T). Value x -> StkEl x
starNotesStkEl (EpAddress -> Value 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (EpAddress -> Value 'TAddress) -> EpAddress -> Value 'TAddress
forall a b. (a -> b) -> a -> b
$ Address -> EpName -> EpAddress
EpAddress Address
a (SomeEntrypointCallT arg -> EpName
forall (arg :: T). SomeEntrypointCallT arg -> EpName
sepcName SomeEntrypointCallT arg
sepc)) StkEl 'TAddress -> Rec StkEl rs -> Rec StkEl ('TAddress : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
CHAIN_ID Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
TcOriginatedContracts
ChainId
Timestamp
Mutez
GlobalCounter
Address
VotingPowers
RemainingSteps
ceLevel :: Natural
ceGlobalCounter :: GlobalCounter
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: Address
ceSource :: Address
ceSelf :: Address
ceContracts :: TcOriginatedContracts
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceLevel :: ContractEnv -> Natural
ceGlobalCounter :: ContractEnv -> GlobalCounter
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> Address
ceSource :: ContractEnv -> Address
ceSelf :: ContractEnv -> Address
ceContracts :: ContractEnv -> TcOriginatedContracts
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TChainId : inp) -> m (Rec StkEl ('TChainId : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TChainId : inp) -> m (Rec StkEl ('TChainId : inp)))
-> Rec StkEl ('TChainId : inp) -> m (Rec StkEl ('TChainId : inp))
forall a b. (a -> b) -> a -> b
$ Value 'TChainId -> StkEl 'TChainId
forall (x :: T). Value x -> StkEl x
starNotesStkEl (ChainId -> Value 'TChainId
forall (instr :: [T] -> [T] -> *).
ChainId -> Value' instr 'TChainId
VChainId ChainId
ceChainId) StkEl 'TChainId -> Rec StkEl inp -> Rec StkEl ('TChainId : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
LEVEL Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
TcOriginatedContracts
ChainId
Timestamp
Mutez
GlobalCounter
Address
VotingPowers
RemainingSteps
ceLevel :: Natural
ceGlobalCounter :: GlobalCounter
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: Address
ceSource :: Address
ceSelf :: Address
ceContracts :: TcOriginatedContracts
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceLevel :: ContractEnv -> Natural
ceGlobalCounter :: ContractEnv -> GlobalCounter
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> Address
ceSource :: ContractEnv -> Address
ceSelf :: ContractEnv -> Address
ceContracts :: ContractEnv -> TcOriginatedContracts
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TNat : inp) -> m (Rec StkEl ('TNat : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TNat : inp) -> m (Rec StkEl ('TNat : inp)))
-> Rec StkEl ('TNat : inp) -> m (Rec StkEl ('TNat : inp))
forall a b. (a -> b) -> a -> b
$ Value 'TNat -> StkEl 'TNat
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Natural -> Value 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
ceLevel) StkEl 'TNat -> Rec StkEl inp -> Rec StkEl ('TNat : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
SELF_ADDRESS Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
TcOriginatedContracts
ChainId
Timestamp
Mutez
GlobalCounter
Address
VotingPowers
RemainingSteps
ceLevel :: Natural
ceGlobalCounter :: GlobalCounter
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: Address
ceSource :: Address
ceSelf :: Address
ceContracts :: TcOriginatedContracts
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceLevel :: ContractEnv -> Natural
ceGlobalCounter :: ContractEnv -> GlobalCounter
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> Address
ceSource :: ContractEnv -> Address
ceSelf :: ContractEnv -> Address
ceContracts :: ContractEnv -> TcOriginatedContracts
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TAddress : inp) -> m (Rec StkEl ('TAddress : inp))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TAddress : inp) -> m (Rec StkEl ('TAddress : inp)))
-> Rec StkEl ('TAddress : inp) -> m (Rec StkEl ('TAddress : inp))
forall a b. (a -> b) -> a -> b
$ Value 'TAddress -> StkEl 'TAddress
forall (x :: T). Value x -> StkEl x
starNotesStkEl (EpAddress -> Value 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (EpAddress -> Value 'TAddress) -> EpAddress -> Value 'TAddress
forall a b. (a -> b) -> a -> b
$ Address -> EpName -> EpAddress
EpAddress Address
ceSelf EpName
DefEpName) StkEl 'TAddress -> Rec StkEl inp -> Rec StkEl ('TAddress : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
r
runInstrImpl InstrRunner m
_ Instr inp out
TICKET (StkEl Value r
dat VarAnn
_ Notes r
_ :& StkEl (VNat Natural
am) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = do
  ContractEnv{Natural
Maybe OperationHash
TcOriginatedContracts
ChainId
Timestamp
Mutez
GlobalCounter
Address
VotingPowers
RemainingSteps
ceLevel :: Natural
ceGlobalCounter :: GlobalCounter
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: Address
ceSource :: Address
ceSelf :: Address
ceContracts :: TcOriginatedContracts
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceLevel :: ContractEnv -> Natural
ceGlobalCounter :: ContractEnv -> GlobalCounter
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> Address
ceSource :: ContractEnv -> Address
ceSelf :: ContractEnv -> Address
ceContracts :: ContractEnv -> TcOriginatedContracts
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Rec StkEl ('TTicket r : rs) -> m (Rec StkEl ('TTicket r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TTicket r : rs) -> m (Rec StkEl ('TTicket r : rs)))
-> Rec StkEl ('TTicket r : rs) -> m (Rec StkEl ('TTicket r : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TTicket r) -> StkEl ('TTicket r)
forall (x :: T). Value x -> StkEl x
starNotesStkEl (Address -> Value r -> Natural -> Value ('TTicket r)
forall (arg :: T) (instr :: [T] -> [T] -> *).
Comparable arg =>
Address
-> Value' instr arg -> Natural -> Value' instr ('TTicket arg)
VTicket Address
ceSelf Value r
dat Natural
am) StkEl ('TTicket r) -> Rec StkEl rs -> Rec StkEl ('TTicket r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
READ_TICKET (te :: StkEl r
te@(StkEl (VTicket Address
addr Value' Instr arg
dat Natural
am) VarAnn
_ Notes r
_) :& Rec StkEl rs
r) = do
  Rec StkEl ('TPair 'TAddress ('TPair arg 'TNat) : r : rs)
-> m (Rec StkEl ('TPair 'TAddress ('TPair arg 'TNat) : r : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TPair 'TAddress ('TPair arg 'TNat) : r : rs)
 -> m (Rec StkEl ('TPair 'TAddress ('TPair arg 'TNat) : r : rs)))
-> Rec StkEl ('TPair 'TAddress ('TPair arg 'TNat) : r : rs)
-> m (Rec StkEl ('TPair 'TAddress ('TPair arg 'TNat) : r : rs))
forall a b. (a -> b) -> a -> b
$
    Value ('TPair 'TAddress ('TPair arg 'TNat))
-> StkEl ('TPair 'TAddress ('TPair arg 'TNat))
forall (x :: T). Value x -> StkEl x
starNotesStkEl
      ((Value 'TAddress, Value' Instr ('TPair arg 'TNat))
-> Value ('TPair 'TAddress ('TPair arg 'TNat))
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (EpAddress -> Value 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (Address -> EpName -> EpAddress
EpAddress Address
addr EpName
DefEpName), ((Value' Instr arg, Value 'TNat) -> Value' Instr ('TPair arg 'TNat)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value' Instr arg
dat, Natural -> Value 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
am))))
    StkEl ('TPair 'TAddress ('TPair arg 'TNat))
-> Rec StkEl (r : rs)
-> Rec StkEl ('TPair 'TAddress ('TPair arg 'TNat) : r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StkEl r
te StkEl r -> Rec StkEl rs -> Rec StkEl (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
SPLIT_TICKET
    (StkEl tv :: Value r
tv@(VTicket Address
addr Value' Instr arg
dat Natural
am) VarAnn
_ Notes r
_ :&
     StkEl (VPair (VNat Natural
am1, VNat Natural
am2)) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = do
  let result :: Value ('TOption ('TPair ('TTicket a) ('TTicket a)))
result = Value r
-> (SingI r => Value ('TOption ('TPair ('TTicket a) ('TTicket a))))
-> Value ('TOption ('TPair ('TTicket a) ('TTicket a)))
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value r
tv ((SingI r => Value ('TOption ('TPair ('TTicket a) ('TTicket a))))
 -> Value ('TOption ('TPair ('TTicket a) ('TTicket a))))
-> (SingI r => Value ('TOption ('TPair ('TTicket a) ('TTicket a))))
-> Value ('TOption ('TPair ('TTicket a) ('TTicket a)))
forall a b. (a -> b) -> a -> b
$ Maybe (Value' Instr ('TPair ('TTicket arg) ('TTicket arg)))
-> Value' Instr ('TOption ('TPair ('TTicket arg) ('TTicket arg)))
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption do
        Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Natural
am1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
am2 Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
am)
        return $ (Value' Instr ('TTicket arg), Value' Instr ('TTicket arg))
-> Value' Instr ('TPair ('TTicket arg) ('TTicket arg))
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Address
-> Value' Instr arg -> Natural -> Value' Instr ('TTicket arg)
forall (arg :: T) (instr :: [T] -> [T] -> *).
Comparable arg =>
Address
-> Value' instr arg -> Natural -> Value' instr ('TTicket arg)
VTicket Address
addr Value' Instr arg
dat Natural
am1, Address
-> Value' Instr arg -> Natural -> Value' Instr ('TTicket arg)
forall (arg :: T) (instr :: [T] -> [T] -> *).
Comparable arg =>
Address
-> Value' instr arg -> Natural -> Value' instr ('TTicket arg)
VTicket Address
addr Value' Instr arg
dat Natural
am2)
  Rec StkEl ('TOption ('TPair ('TTicket a) ('TTicket a)) : rs)
-> m (Rec StkEl ('TOption ('TPair ('TTicket a) ('TTicket a)) : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption ('TPair ('TTicket a) ('TTicket a)) : rs)
 -> m (Rec
         StkEl ('TOption ('TPair ('TTicket a) ('TTicket a)) : rs)))
-> Rec StkEl ('TOption ('TPair ('TTicket a) ('TTicket a)) : rs)
-> m (Rec StkEl ('TOption ('TPair ('TTicket a) ('TTicket a)) : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TOption ('TPair ('TTicket a) ('TTicket a)))
-> StkEl ('TOption ('TPair ('TTicket a) ('TTicket a)))
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value ('TOption ('TPair ('TTicket a) ('TTicket a)))
result StkEl ('TOption ('TPair ('TTicket a) ('TTicket a)))
-> Rec StkEl rs
-> Rec StkEl ('TOption ('TPair ('TTicket a) ('TTicket a)) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r
runInstrImpl InstrRunner m
_ Instr inp out
JOIN_TICKETS
  (StkEl (VPair (tv1 :: Value' Instr l
tv1@(VTicket Address
addr1 Value' Instr arg
dat1 Natural
am1), VTicket Address
addr2 Value' Instr arg
dat2 Natural
am2)) VarAnn
_ Notes r
_ :& Rec StkEl rs
r) = do
  let result :: Value ('TOption ('TTicket a))
result = Value' Instr l
-> (SingI l => Value ('TOption ('TTicket a)))
-> Value ('TOption ('TTicket a))
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value' Instr l
tv1 ((SingI l => Value ('TOption ('TTicket a)))
 -> Value ('TOption ('TTicket a)))
-> (SingI l => Value ('TOption ('TTicket a)))
-> Value ('TOption ('TTicket a))
forall a b. (a -> b) -> a -> b
$ Maybe (Value' Instr ('TTicket arg))
-> Value' Instr ('TOption ('TTicket arg))
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption do
        Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Address
addr1 Address -> Address -> Bool
forall a. Eq a => a -> a -> Bool
== Address
addr2)
        Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Value' Instr arg
dat1 Value' Instr arg -> Value' Instr arg -> Bool
forall a. Eq a => a -> a -> Bool
== Value' Instr arg
Value' Instr arg
dat2)
        return $ Address
-> Value' Instr arg -> Natural -> Value' Instr ('TTicket arg)
forall (arg :: T) (instr :: [T] -> [T] -> *).
Comparable arg =>
Address
-> Value' instr arg -> Natural -> Value' instr ('TTicket arg)
VTicket Address
addr1 Value' Instr arg
dat1 (Natural
am1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
am2)
  Rec StkEl ('TOption ('TTicket a) : rs)
-> m (Rec StkEl ('TOption ('TTicket a) : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption ('TTicket a) : rs)
 -> m (Rec StkEl ('TOption ('TTicket a) : rs)))
-> Rec StkEl ('TOption ('TTicket a) : rs)
-> m (Rec StkEl ('TOption ('TTicket a) : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TOption ('TTicket a)) -> StkEl ('TOption ('TTicket a))
forall (x :: T). Value x -> StkEl x
starNotesStkEl Value ('TOption ('TTicket a))
result StkEl ('TOption ('TTicket a))
-> Rec StkEl rs -> Rec StkEl ('TOption ('TTicket a) : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r

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

-- | Unpacks given raw data into a typed value.
runUnpack
  :: forall t. (UnpackedValScope t)
  => ByteString
  -> Either UnpackError (T.Value t)
runUnpack :: ByteString -> Either UnpackError (Value t)
runUnpack 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).
  -- Fortunately, 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 Address
originator Maybe (Value 'TKeyHash)
mbDelegate Mutez
bal Contract param store
contract Value' Instr store
storage =
  OriginationOperation :: 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 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

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

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

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

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

assignBigMapIds' :: EvalM m => Value t -> m (Value t)
assignBigMapIds' :: Value t -> m (Value t)
assignBigMapIds' Value t
val = do
  BigMapCounter
bigMapCounter0 <- Getting BigMapCounter InterpreterState BigMapCounter
-> InterpreterState -> BigMapCounter
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting BigMapCounter InterpreterState BigMapCounter
Lens' InterpreterState BigMapCounter
isBigMapCounterL (InterpreterState -> BigMapCounter)
-> m InterpreterState -> m BigMapCounter
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m InterpreterState
forall (m :: * -> *). InterpreterStateMonad m => m InterpreterState
getInterpreterState
  let (Value t
storageWithIds, BigMapCounter
bigMapCounter1) = State BigMapCounter (Value t)
-> BigMapCounter -> (Value t, BigMapCounter)
forall s a. State s a -> s -> (a, s)
runState (Value t -> State BigMapCounter (Value t)
forall (m :: * -> *) (t :: T).
MonadState BigMapCounter m =>
Value t -> m (Value t)
assignBigMapIds Value t
val) BigMapCounter
bigMapCounter0
  (InterpreterState -> InterpreterState) -> m ()
forall (m :: * -> *).
InterpreterStateMonad m =>
(InterpreterState -> InterpreterState) -> m ()
modifyInterpreterState (ASetter
  InterpreterState InterpreterState BigMapCounter BigMapCounter
-> BigMapCounter -> InterpreterState -> InterpreterState
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter
  InterpreterState InterpreterState BigMapCounter BigMapCounter
Lens' InterpreterState BigMapCounter
isBigMapCounterL BigMapCounter
bigMapCounter1)
  pure Value t
storageWithIds

-- | All big_maps stored in a chain have a globally unique ID.
--
-- We use this function to assign a new ID whenever a big_map is created.
assignBigMapIds :: MonadState BigMapCounter m => Value t -> m (Value t)
assignBigMapIds :: Value t -> m (Value t)
assignBigMapIds =
  (forall (t' :: T). Value t' -> m (Value t'))
-> Value t -> m (Value t)
forall (t :: T) (m :: * -> *).
Monad m =>
(forall (t' :: T). Value t' -> m (Value t'))
-> Value t -> m (Value t)
dfsTraverseValue \case
    VBigMap Maybe Natural
_ Map (Value' Instr k) (Value' Instr v)
vBigMap -> do
      Natural
bigMapId <- (Natural -> (Natural, Natural))
-> BigMapCounter -> (Natural, BigMapCounter)
Iso' BigMapCounter Natural
bigMapCounter ((Natural -> (Natural, Natural))
 -> BigMapCounter -> (Natural, BigMapCounter))
-> Natural -> m Natural
forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
LensLike' ((,) a) s a -> a -> m a
<<+= Natural
1
      pure $ Maybe Natural
-> Map (Value' Instr k) (Value' Instr v)
-> Value' Instr ('TBigMap k v)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI k, SingI v, Comparable k, HasNoBigMap v) =>
Maybe Natural
-> Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VBigMap (Natural -> Maybe Natural
forall a. a -> Maybe a
Just Natural
bigMapId) Map (Value' Instr k) (Value' Instr v)
vBigMap
    Value t'
v -> Value t' -> m (Value t')
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t'
v

(deriveGADTNFData ''MichelsonFailed)