-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

-- | Module, containing function to interpret Michelson
-- instructions against given context and input stack.
module Morley.Michelson.Interpret
  ( ContractEnv (..)
  , InterpreterState (..)
  , MichelsonFailed (..)
  , MichelsonFailureWithStack(..)
  , RemainingSteps (..)
  , SomeItStack (..)
  , MorleyLogs (..)
  , buildMorleyLogs
  , MorleyLogsBuilder (..)

  , interpret
  , interpretInstr
  , interpretInstrAnnotated
  , ContractReturn

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

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

    -- * Prisms
  , _MorleyLogs
  ) where

import Prelude hiding (EQ, GT, LT)

import Control.Lens (makeLensesFor, makePrisms, traverseOf, (<<+=))
import Control.Monad.Except (MonadError, throwError)
import Control.Monad.RWS.Strict (RWS, RWST, runRWS)
import Control.Monad.Writer (MonadWriter, WriterT, tell)
import Data.Default (Default(..))
import Data.Map qualified as Map
import Data.Set qualified as Set
import Data.Singletons.Decide (decideEquality)
import Data.Vinyl (Rec(..), (<+>))
import Data.Vinyl.Recursive (rmap)
import Fmt (Buildable(build), blockListF, pretty, prettyLn, (+|), (|+))
import Unsafe qualified (fromIntegral)

import Morley.Michelson.ErrorPos (ErrorSrcPos(..))
import Morley.Michelson.Interpret.Pack (packValue')
import Morley.Michelson.Interpret.Unpack (UnpackError, unpackValue')
import Morley.Michelson.Runtime.GState
import Morley.Michelson.TypeCheck (eqType)
import Morley.Michelson.Typed hiding (Branch(..))
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Typed.Operation
  (OperationHash(..), OriginationOperation(..), mkContractAddress, mkOriginationOperationHash)
import Morley.Michelson.Untyped (unAnnotation)
import Morley.Tezos.Address
import Morley.Tezos.Address.Alias
import Morley.Tezos.Core (ChainId, Mutez, Timestamp, zeroMutez)
import Morley.Tezos.Crypto
  (KeyHash, OpeningResult(..), blake2b, checkSignature, hashKey, keccak, mkTLTime, openChest,
  sha256, sha3, sha512)
import Morley.Tezos.Crypto.BLS12381 (checkPairing)
import Morley.Util.Peano (LongerThan, Peano)
import Morley.Util.PeanoNatural (PeanoNatural(..))
import Morley.Util.Sing (eqParamSing)
import Morley.Util.Type
import Morley.Util.Typeable

-- | Morley logs appearing as interpreter result.
newtype MorleyLogs = MorleyLogs { MorleyLogs -> [Text]
unMorleyLogs :: [Text] }
  deriving stock (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, 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, (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 (NonEmpty MorleyLogs -> MorleyLogs
MorleyLogs -> MorleyLogs -> MorleyLogs
(MorleyLogs -> MorleyLogs -> MorleyLogs)
-> (NonEmpty MorleyLogs -> MorleyLogs)
-> (forall b. Integral b => b -> MorleyLogs -> MorleyLogs)
-> Semigroup MorleyLogs
forall b. Integral b => b -> MorleyLogs -> MorleyLogs
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: forall b. Integral b => b -> MorleyLogs -> MorleyLogs
$cstimes :: forall b. Integral b => b -> MorleyLogs -> MorleyLogs
sconcat :: NonEmpty MorleyLogs -> MorleyLogs
$csconcat :: NonEmpty MorleyLogs -> MorleyLogs
<> :: MorleyLogs -> MorleyLogs -> MorleyLogs
$c<> :: MorleyLogs -> MorleyLogs -> MorleyLogs
Semigroup, Semigroup MorleyLogs
MorleyLogs
Semigroup MorleyLogs
-> MorleyLogs
-> (MorleyLogs -> MorleyLogs -> MorleyLogs)
-> ([MorleyLogs] -> MorleyLogs)
-> Monoid MorleyLogs
[MorleyLogs] -> MorleyLogs
MorleyLogs -> MorleyLogs -> MorleyLogs
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [MorleyLogs] -> MorleyLogs
$cmconcat :: [MorleyLogs] -> MorleyLogs
mappend :: MorleyLogs -> MorleyLogs -> MorleyLogs
$cmappend :: MorleyLogs -> MorleyLogs -> MorleyLogs
mempty :: MorleyLogs
$cmempty :: MorleyLogs
Monoid)
  deriving anyclass (MorleyLogs -> ()
(MorleyLogs -> ()) -> NFData MorleyLogs
forall a. (a -> ()) -> NFData a
rnf :: MorleyLogs -> ()
$crnf :: MorleyLogs -> ()
NFData)

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]
unMorleyLogs

-- | Morley logs accumulator, for incremental building.
newtype MorleyLogsBuilder = MorleyLogsBuilder (Endo [Text])
  deriving stock ((forall x. MorleyLogsBuilder -> Rep MorleyLogsBuilder x)
-> (forall x. Rep MorleyLogsBuilder x -> MorleyLogsBuilder)
-> Generic MorleyLogsBuilder
forall x. Rep MorleyLogsBuilder x -> MorleyLogsBuilder
forall x. MorleyLogsBuilder -> Rep MorleyLogsBuilder x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MorleyLogsBuilder x -> MorleyLogsBuilder
$cfrom :: forall x. MorleyLogsBuilder -> Rep MorleyLogsBuilder x
Generic)
  deriving newtype (MorleyLogsBuilder
MorleyLogsBuilder -> Default MorleyLogsBuilder
forall a. a -> Default a
def :: MorleyLogsBuilder
$cdef :: MorleyLogsBuilder
Default, NonEmpty MorleyLogsBuilder -> MorleyLogsBuilder
MorleyLogsBuilder -> MorleyLogsBuilder -> MorleyLogsBuilder
(MorleyLogsBuilder -> MorleyLogsBuilder -> MorleyLogsBuilder)
-> (NonEmpty MorleyLogsBuilder -> MorleyLogsBuilder)
-> (forall b.
    Integral b =>
    b -> MorleyLogsBuilder -> MorleyLogsBuilder)
-> Semigroup MorleyLogsBuilder
forall b. Integral b => b -> MorleyLogsBuilder -> MorleyLogsBuilder
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: forall b. Integral b => b -> MorleyLogsBuilder -> MorleyLogsBuilder
$cstimes :: forall b. Integral b => b -> MorleyLogsBuilder -> MorleyLogsBuilder
sconcat :: NonEmpty MorleyLogsBuilder -> MorleyLogsBuilder
$csconcat :: NonEmpty MorleyLogsBuilder -> MorleyLogsBuilder
<> :: MorleyLogsBuilder -> MorleyLogsBuilder -> MorleyLogsBuilder
$c<> :: MorleyLogsBuilder -> MorleyLogsBuilder -> MorleyLogsBuilder
Semigroup, Semigroup MorleyLogsBuilder
MorleyLogsBuilder
Semigroup MorleyLogsBuilder
-> MorleyLogsBuilder
-> (MorleyLogsBuilder -> MorleyLogsBuilder -> MorleyLogsBuilder)
-> ([MorleyLogsBuilder] -> MorleyLogsBuilder)
-> Monoid MorleyLogsBuilder
[MorleyLogsBuilder] -> MorleyLogsBuilder
MorleyLogsBuilder -> MorleyLogsBuilder -> MorleyLogsBuilder
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [MorleyLogsBuilder] -> MorleyLogsBuilder
$cmconcat :: [MorleyLogsBuilder] -> MorleyLogsBuilder
mappend :: MorleyLogsBuilder -> MorleyLogsBuilder -> MorleyLogsBuilder
$cmappend :: MorleyLogsBuilder -> MorleyLogsBuilder -> MorleyLogsBuilder
mempty :: MorleyLogsBuilder
$cmempty :: MorleyLogsBuilder
Monoid)

buildMorleyLogs :: MorleyLogsBuilder -> MorleyLogs
buildMorleyLogs :: MorleyLogsBuilder -> MorleyLogs
buildMorleyLogs (MorleyLogsBuilder Endo [Text]
builder) =
  [Text] -> MorleyLogs
MorleyLogs ([Text] -> MorleyLogs) -> [Text] -> MorleyLogs
forall a b. (a -> b) -> a -> b
$ Endo [Text] -> [Text] -> [Text]
forall a. Endo a -> a -> a
appEndo Endo [Text]
builder []

instance One MorleyLogsBuilder where
  type OneItem MorleyLogsBuilder = Text
  one :: OneItem MorleyLogsBuilder -> MorleyLogsBuilder
one OneItem MorleyLogsBuilder
log = Endo [Text] -> MorleyLogsBuilder
MorleyLogsBuilder (Endo [Text] -> MorleyLogsBuilder)
-> Endo [Text] -> MorleyLogsBuilder
forall a b. (a -> b) -> a -> b
$ ([Text] -> [Text]) -> Endo [Text]
forall a. (a -> a) -> Endo a
Endo (Text
OneItem MorleyLogsBuilder
log Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:)

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
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 -> RemainingSteps
isRemainingSteps :: RemainingSteps
  , InterpreterState -> GlobalCounter
isGlobalCounter :: GlobalCounter
  , 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
  [ ("isBigMapCounter", "isBigMapCounterL")
  ]
  ''InterpreterState

makePrisms ''MorleyLogs

newtype StkEl t = StkEl
  { forall (t :: T). StkEl t -> Value t
seValue :: Value 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")
  ]
  ''StkEl

-- | 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 -> Map ContractAddress ContractState
ceContracts :: Map ContractAddress ContractState
  -- ^ Information stored about the existing contracts.
  , ContractEnv -> ContractAddress
ceSelf :: ContractAddress
  -- ^ Address of the interpreted contract.
  , ContractEnv -> L1Address
ceSource :: L1Address
  -- ^ The contract that initiated the current transaction. Note that this
  -- contract should in normal operation be an implicit account.
  , ContractEnv -> L1Address
ceSender :: L1Address
  -- ^ The contract that initiated the current internal transaction. This may
  -- either be an implicit account or a smart contract.
  , 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 -> Natural
ceLevel :: Natural
  -- ^ Number of blocks before the given one in the chain
  , ContractEnv -> ErrorSrcPos
ceErrorSrcPos :: ErrorSrcPos
  -- ^ Current source position information
  , ContractEnv -> Natural
ceMinBlockTime :: Natural
  -- ^ Minimum time between blocks
  }

-- | Errors that can be thrown by the interpreter. The @ext@ type variable
-- allow the downstreams consumer to add additional exceptions.
data MichelsonFailed ext where
  MichelsonFailedWith :: (SingI t, ConstantScope t) => T.Value t -> MichelsonFailed ext
    -- ^ Represents @[FAILED]@ state of a Michelson program. Contains
    -- value that was on top of the stack when @FAILWITH@ was called.
  MichelsonArithError
    :: (Typeable n, Typeable m)
    => ArithError (Value n) (Value m) -> MichelsonFailed ext
  MichelsonGasExhaustion :: MichelsonFailed ext
  MichelsonFailedTestAssert :: Text -> MichelsonFailed ext
  MichelsonUnsupported :: Text -> MichelsonFailed ext
  MichelsonExt :: ext -> MichelsonFailed ext

deriving stock instance Show ext => Show (MichelsonFailed ext)

instance Eq ext => Eq (MichelsonFailed ext) where
  MichelsonFailedWith Value t
v1 == :: MichelsonFailed ext -> MichelsonFailed ext -> 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 ext
_ = Bool
False
  MichelsonArithError ArithError (Value n) (Value m)
ae1 == MichelsonArithError ArithError (Value n) (Value m)
ae2 = ArithError (Value n) (Value m)
ae1 ArithError (Value n) (Value m)
-> ArithError (Value n) (Value 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 n) (Value m)
ae2
  MichelsonArithError ArithError (Value n) (Value m)
_ == MichelsonFailed ext
_ = Bool
False
  MichelsonFailed ext
MichelsonGasExhaustion == MichelsonFailed ext
MichelsonGasExhaustion = Bool
True
  MichelsonFailed ext
MichelsonGasExhaustion == MichelsonFailed ext
_ = 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 ext
_ = Bool
False
  MichelsonUnsupported Text
i1 == MichelsonUnsupported Text
i2 = Text
i1 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
i2
  MichelsonUnsupported Text
_ == MichelsonFailed ext
_ = Bool
False
  MichelsonExt ext
i1 == MichelsonExt ext
i2 = ext
i1 ext -> ext -> Bool
forall a. Eq a => a -> a -> Bool
== ext
i2
  MichelsonExt ext
_ == MichelsonFailed ext
_ = Bool
False

instance Buildable ext => Buildable (MichelsonFailed ext) where
  build :: MichelsonFailed ext -> Builder
build =
    \case
      MichelsonFailedWith Value t
v ->
        Builder
"Reached FAILWITH instruction with " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Value t
v Value t -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""
      MichelsonArithError ArithError (Value n) (Value m)
v -> ArithError (Value n) (Value m) -> Builder
forall p. Buildable p => p -> Builder
build ArithError (Value n) (Value m)
v
      MichelsonFailed ext
MichelsonGasExhaustion ->
        Builder
"Gas limit exceeded on contract execution"
      MichelsonFailedTestAssert Text
t -> Text -> Builder
forall p. Buildable p => p -> Builder
build Text
t
      MichelsonUnsupported Text
instr ->
        Text -> Builder
forall p. Buildable p => p -> Builder
build Text
instr Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" instruction is not supported."
      MichelsonExt ext
x -> ext -> Builder
forall p. Buildable p => p -> Builder
build ext
x

-- | Carries a 'MichelsonFailed' @ext@ error and the 'ErrorSrcPos' at which it was raised
data MichelsonFailureWithStack ext = MichelsonFailureWithStack
  { forall ext. MichelsonFailureWithStack ext -> MichelsonFailed ext
mfwsFailed :: MichelsonFailed ext
  , forall ext. MichelsonFailureWithStack ext -> ErrorSrcPos
mfwsErrorSrcPos :: ErrorSrcPos
  } deriving stock (Int -> MichelsonFailureWithStack ext -> ShowS
[MichelsonFailureWithStack ext] -> ShowS
MichelsonFailureWithStack ext -> String
(Int -> MichelsonFailureWithStack ext -> ShowS)
-> (MichelsonFailureWithStack ext -> String)
-> ([MichelsonFailureWithStack ext] -> ShowS)
-> Show (MichelsonFailureWithStack ext)
forall ext.
Show ext =>
Int -> MichelsonFailureWithStack ext -> ShowS
forall ext. Show ext => [MichelsonFailureWithStack ext] -> ShowS
forall ext. Show ext => MichelsonFailureWithStack ext -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MichelsonFailureWithStack ext] -> ShowS
$cshowList :: forall ext. Show ext => [MichelsonFailureWithStack ext] -> ShowS
show :: MichelsonFailureWithStack ext -> String
$cshow :: forall ext. Show ext => MichelsonFailureWithStack ext -> String
showsPrec :: Int -> MichelsonFailureWithStack ext -> ShowS
$cshowsPrec :: forall ext.
Show ext =>
Int -> MichelsonFailureWithStack ext -> ShowS
Show, (forall x.
 MichelsonFailureWithStack ext
 -> Rep (MichelsonFailureWithStack ext) x)
-> (forall x.
    Rep (MichelsonFailureWithStack ext) x
    -> MichelsonFailureWithStack ext)
-> Generic (MichelsonFailureWithStack ext)
forall x.
Rep (MichelsonFailureWithStack ext) x
-> MichelsonFailureWithStack ext
forall x.
MichelsonFailureWithStack ext
-> Rep (MichelsonFailureWithStack ext) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall ext x.
Rep (MichelsonFailureWithStack ext) x
-> MichelsonFailureWithStack ext
forall ext x.
MichelsonFailureWithStack ext
-> Rep (MichelsonFailureWithStack ext) x
$cto :: forall ext x.
Rep (MichelsonFailureWithStack ext) x
-> MichelsonFailureWithStack ext
$cfrom :: forall ext x.
MichelsonFailureWithStack ext
-> Rep (MichelsonFailureWithStack ext) x
Generic, MichelsonFailureWithStack ext
-> MichelsonFailureWithStack ext -> Bool
(MichelsonFailureWithStack ext
 -> MichelsonFailureWithStack ext -> Bool)
-> (MichelsonFailureWithStack ext
    -> MichelsonFailureWithStack ext -> Bool)
-> Eq (MichelsonFailureWithStack ext)
forall ext.
Eq ext =>
MichelsonFailureWithStack ext
-> MichelsonFailureWithStack ext -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MichelsonFailureWithStack ext
-> MichelsonFailureWithStack ext -> Bool
$c/= :: forall ext.
Eq ext =>
MichelsonFailureWithStack ext
-> MichelsonFailureWithStack ext -> Bool
== :: MichelsonFailureWithStack ext
-> MichelsonFailureWithStack ext -> Bool
$c== :: forall ext.
Eq ext =>
MichelsonFailureWithStack ext
-> MichelsonFailureWithStack ext -> Bool
Eq)

instance Buildable ext => Buildable (MichelsonFailureWithStack ext) where
  build :: MichelsonFailureWithStack ext -> Builder
build (MichelsonFailureWithStack MichelsonFailed ext
err ErrorSrcPos
loc) = MichelsonFailed ext -> Builder
forall p. Buildable p => p -> Builder
build MichelsonFailed ext
err Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" at " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> ErrorSrcPos -> Builder
forall p. Buildable p => p -> Builder
build ErrorSrcPos
loc

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

deriving stock instance Show ext => Show (InterpretError ext)

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

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

deriving stock instance Show InterpretResult

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

type ContractReturn st =
  (Either (MichelsonFailureWithStack Void) ([Operation], T.Value st), (InterpreterState, MorleyLogs))

handleContractReturn
  :: (StorageScope st)
  => ContractReturn st -> Either (InterpretError Void) InterpretResult
handleContractReturn :: forall (st :: T).
StorageScope st =>
ContractReturn st -> Either (InterpretError Void) InterpretResult
handleContractReturn (Either (MichelsonFailureWithStack Void) ([Operation], Value st)
ei, (InterpreterState
s, MorleyLogs
l)) =
  (MichelsonFailureWithStack Void -> InterpretError Void)
-> (([Operation], Value st) -> InterpretResult)
-> Either (MichelsonFailureWithStack Void) ([Operation], Value st)
-> Either (InterpretError Void) InterpretResult
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((MichelsonFailureWithStack Void, MorleyLogs) -> InterpretError Void
forall ext.
(MichelsonFailureWithStack ext, MorleyLogs) -> InterpretError ext
InterpretError ((MichelsonFailureWithStack Void, MorleyLogs)
 -> InterpretError Void)
-> (MichelsonFailureWithStack Void
    -> (MichelsonFailureWithStack Void, MorleyLogs))
-> MichelsonFailureWithStack Void
-> InterpretError Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, MorleyLogs
l)) ((([Operation], Value st), InterpreterState, MorleyLogs)
-> InterpretResult
forall (st :: T).
StorageScope st =>
(([Operation], Value' Instr st), InterpreterState, MorleyLogs)
-> InterpretResult
constructIR ((([Operation], Value st), InterpreterState, MorleyLogs)
 -> InterpretResult)
-> (([Operation], Value st)
    -> (([Operation], Value st), InterpreterState, MorleyLogs))
-> ([Operation], Value st)
-> InterpretResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, InterpreterState
s, MorleyLogs
l)) Either (MichelsonFailureWithStack Void) ([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 :: forall (inp :: [T]). Rec (Value' Instr) inp -> Rec StkEl inp
mapToStkEl = (forall (t :: T). Value t -> StkEl t)
-> Rec (Value' Instr) 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 (t :: T). Value t -> StkEl t
StkEl

-- | 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 :: forall (inp :: [T]). Rec StkEl inp -> Rec (Value' Instr) inp
mapToValue = (forall (t :: T). StkEl t -> Value t)
-> Rec StkEl inp -> Rec (Value' Instr) inp
forall {u} (f :: u -> *) (g :: u -> *) (rs :: [u]).
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap forall (t :: T). StkEl t -> Value t
seValue

interpret'
  :: forall cp st arg.
     Contract cp st
  -> EntrypointCallT cp arg
  -> T.Value arg
  -> T.Value st
  -> ContractEnv
  -> InterpreterState
  -> ContractReturn st
interpret' :: forall (cp :: T) (st :: T) (arg :: T).
Contract cp st
-> EntrypointCallT cp arg
-> Value arg
-> Value st
-> ContractEnv
-> InterpreterState
-> ContractReturn st
interpret' Contract{EntriesOrder
Notes st
ViewsSet' Instr st
ParamNotes cp
ContractCode' Instr cp st
cEntriesOrder :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> EntriesOrder
cViews :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> ViewsSet' instr st
cStoreNotes :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> Notes st
cParamNotes :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> ParamNotes cp
cCode :: forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> ContractCode' instr cp st
cEntriesOrder :: EntriesOrder
cViews :: ViewsSet' Instr st
cStoreNotes :: Notes st
cParamNotes :: ParamNotes cp
cCode :: ContractCode' Instr cp st
..} EntrypointCallT cp arg
epc Value arg
param Value st
initSt ContractEnv
env InterpreterState
ist = (Either
   (MichelsonFailureWithStack Void) (Rec StkEl (ContractOut st))
 -> Either (MichelsonFailureWithStack Void) ([Operation], Value st))
-> (Either
      (MichelsonFailureWithStack Void) (Rec StkEl (ContractOut st)),
    (InterpreterState, MorleyLogs))
-> (Either
      (MichelsonFailureWithStack Void) ([Operation], Value st),
    (InterpreterState, MorleyLogs))
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Rec StkEl (ContractOut st) -> ([Operation], Value st))
-> Either
     (MichelsonFailureWithStack Void) (Rec StkEl (ContractOut st))
-> Either (MichelsonFailureWithStack Void) ([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
    (MichelsonFailureWithStack Void) (Rec StkEl (ContractOut st)),
  (InterpreterState, MorleyLogs))
 -> (Either
       (MichelsonFailureWithStack Void) ([Operation], Value st),
     (InterpreterState, MorleyLogs)))
-> (Either
      (MichelsonFailureWithStack Void) (Rec StkEl (ContractOut st)),
    (InterpreterState, MorleyLogs))
-> (Either
      (MichelsonFailureWithStack Void) ([Operation], Value st),
    (InterpreterState, MorleyLogs))
forall a b. (a -> b) -> a -> b
$
  EvalOp (Rec StkEl (ContractOut st))
-> ContractEnv
-> InterpreterState
-> (Either
      (MichelsonFailureWithStack Void) (Rec StkEl (ContractOut st)),
    (InterpreterState, MorleyLogs))
forall a.
EvalOp a
-> ContractEnv
-> InterpreterState
-> (Either (MichelsonFailureWithStack Void) a,
    (InterpreterState, MorleyLogs))
runEvalOp
    (Instr (ContractInp cp st) (ContractOut st)
-> Rec StkEl (ContractInp cp st)
-> EvalOp (Rec StkEl (ContractOut st))
forall (m :: * -> *). EvalM m => InstrRunner m
runInstr (ContractCode' Instr cp st
-> Instr (ContractInp cp st) (ContractOut st)
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
ContractCode' instr cp st
-> instr (ContractInp cp st) (ContractOut st)
unContractCode ContractCode' Instr 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 -> Value st -> Rec StkEl (ContractInp cp st)
forall (param :: T) (st :: T).
Value param -> Value 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) Value st
initSt)
    ContractEnv
env
    InterpreterState
ist

mkInitStack
  :: T.Value param
  -> T.Value st
  -> Rec StkEl (ContractInp param st)
mkInitStack :: forall (param :: T) (st :: T).
Value param -> Value st -> Rec StkEl (ContractInp param st)
mkInitStack Value param
param Value st
st = Value ('TPair param st) -> StkEl ('TPair param st)
forall (t :: T). Value 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))
    StkEl ('TPair param st)
-> Rec StkEl '[] -> Rec StkEl '[ 'TPair 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 :: forall (st :: T).
Rec StkEl (ContractOut st) -> ([Operation], Value st)
fromFinalStack (StkEl (T.VPair (T.VList [Value' Instr t1]
ops, Value' Instr r
st)) :& Rec StkEl rs
RNil) =
  ((Value' Instr t1 -> Operation) -> [Value' Instr t1] -> [Operation]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (\(T.VOp Operation
op) -> Operation
op) [Value' Instr t1]
ops, Value' Instr st
Value' Instr r
st)

interpret
  :: Contract cp st
  -> EntrypointCallT cp arg
  -> T.Value arg
  -> T.Value st
  -> GlobalCounter
  -> BigMapCounter
  -> ContractEnv
  -> ContractReturn st
interpret :: forall (cp :: T) (st :: T) (arg :: T).
Contract cp st
-> EntrypointCallT cp arg
-> Value arg
-> Value st
-> GlobalCounter
-> BigMapCounter
-> ContractEnv
-> ContractReturn st
interpret Contract cp st
contract EntrypointCallT cp arg
epc Value arg
param Value st
initSt GlobalCounter
globalCounter 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 (GlobalCounter -> BigMapCounter -> ContractEnv -> InterpreterState
initInterpreterState GlobalCounter
globalCounter BigMapCounter
bmCounter ContractEnv
env)

initInterpreterState :: GlobalCounter -> BigMapCounter -> ContractEnv -> InterpreterState
initInterpreterState :: GlobalCounter -> BigMapCounter -> ContractEnv -> InterpreterState
initInterpreterState GlobalCounter
globalCounter BigMapCounter
bmCounter ContractEnv
env =
  RemainingSteps
-> GlobalCounter -> BigMapCounter -> InterpreterState
InterpreterState (ContractEnv -> RemainingSteps
ceMaxSteps ContractEnv
env) GlobalCounter
globalCounter BigMapCounter
bmCounter

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

-- | Interpret an instruction in vacuum, putting no extra constraints on
-- its execution while preserving its annotations.
--
-- Mostly for testing purposes.
interpretInstrAnnotated
  :: ContractEnv
  -> Instr inp out
  -> Rec T.Value inp
  -> Either (MichelsonFailureWithStack Void) (Rec StkEl out)
interpretInstrAnnotated :: forall (inp :: [T]) (out :: [T]).
ContractEnv
-> Instr inp out
-> Rec (Value' Instr) inp
-> Either (MichelsonFailureWithStack Void) (Rec StkEl out)
interpretInstrAnnotated ContractEnv
env Instr inp out
instr Rec (Value' Instr) inp
inpSt =
  (Either (MichelsonFailureWithStack Void) (Rec StkEl out),
 (InterpreterState, MorleyLogs))
-> Either (MichelsonFailureWithStack Void) (Rec StkEl out)
forall a b. (a, b) -> a
fst ((Either (MichelsonFailureWithStack Void) (Rec StkEl out),
  (InterpreterState, MorleyLogs))
 -> Either (MichelsonFailureWithStack Void) (Rec StkEl out))
-> (Either (MichelsonFailureWithStack Void) (Rec StkEl out),
    (InterpreterState, MorleyLogs))
-> Either (MichelsonFailureWithStack Void) (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$
  EvalOp (Rec StkEl out)
-> ContractEnv
-> InterpreterState
-> (Either (MichelsonFailureWithStack Void) (Rec StkEl out),
    (InterpreterState, MorleyLogs))
forall a.
EvalOp a
-> ContractEnv
-> InterpreterState
-> (Either (MichelsonFailureWithStack Void) a,
    (InterpreterState, MorleyLogs))
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' Instr) inp -> Rec StkEl inp
forall (inp :: [T]). Rec (Value' Instr) inp -> Rec StkEl inp
mapToStkEl Rec (Value' Instr) inp
inpSt)
    ContractEnv
env
    InterpreterState :: RemainingSteps
-> GlobalCounter -> BigMapCounter -> InterpreterState
InterpreterState
      { isRemainingSteps :: RemainingSteps
isRemainingSteps = RemainingSteps
9999999999
      , isBigMapCounter :: BigMapCounter
isBigMapCounter = BigMapCounter
0
      , isGlobalCounter :: GlobalCounter
isGlobalCounter = GlobalCounter
0
      }

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

type EvalOp =
  ExceptT (MichelsonFailureWithStack Void) $
  RWS ContractEnv MorleyLogsBuilder InterpreterState

runEvalOp
  :: EvalOp a
  -> ContractEnv
  -> InterpreterState
  -> (Either (MichelsonFailureWithStack Void) a, (InterpreterState, MorleyLogs))
runEvalOp :: forall a.
EvalOp a
-> ContractEnv
-> InterpreterState
-> (Either (MichelsonFailureWithStack Void) a,
    (InterpreterState, MorleyLogs))
runEvalOp EvalOp a
act ContractEnv
env InterpreterState
initSt =
  let (Either (MichelsonFailureWithStack Void) a
res, InterpreterState
is, MorleyLogsBuilder
logs) = RWS
  ContractEnv
  MorleyLogsBuilder
  InterpreterState
  (Either (MichelsonFailureWithStack Void) a)
-> ContractEnv
-> InterpreterState
-> (Either (MichelsonFailureWithStack Void) a, InterpreterState,
    MorleyLogsBuilder)
forall r w s a. RWS r w s a -> r -> s -> (a, s, w)
runRWS (EvalOp a
-> RWS
     ContractEnv
     MorleyLogsBuilder
     InterpreterState
     (Either (MichelsonFailureWithStack Void) a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT EvalOp a
act) ContractEnv
env InterpreterState
initSt
  in (Either (MichelsonFailureWithStack Void) a
res, (InterpreterState
is, MorleyLogsBuilder -> MorleyLogs
buildMorleyLogs MorleyLogsBuilder
logs))

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 Monad m => InterpreterStateMonad (StateT InterpreterState m) where
  stateInterpreterState :: forall a.
(InterpreterState -> (a, InterpreterState))
-> StateT InterpreterState m a
stateInterpreterState = (InterpreterState -> (a, InterpreterState))
-> StateT InterpreterState m a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state
instance (Monad m, Monoid w) => InterpreterStateMonad (RWST r w InterpreterState m) where
  stateInterpreterState :: forall a.
(InterpreterState -> (a, InterpreterState))
-> RWST r w InterpreterState m a
stateInterpreterState = (InterpreterState -> (a, InterpreterState))
-> RWST r w InterpreterState m a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state

instance InterpreterStateMonad m => InterpreterStateMonad (ReaderT r m) where
  stateInterpreterState :: forall a.
(InterpreterState -> (a, InterpreterState)) -> ReaderT r m a
stateInterpreterState = m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> ReaderT r m a)
-> ((InterpreterState -> (a, InterpreterState)) -> m a)
-> (InterpreterState -> (a, InterpreterState))
-> ReaderT r m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InterpreterState -> (a, InterpreterState)) -> m a
forall (m :: * -> *) a.
InterpreterStateMonad m =>
(InterpreterState -> (a, InterpreterState)) -> m a
stateInterpreterState
instance (InterpreterStateMonad m, Monoid w) => InterpreterStateMonad (WriterT w m) where
  stateInterpreterState :: forall a.
(InterpreterState -> (a, InterpreterState)) -> WriterT w m a
stateInterpreterState = m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> WriterT w m a)
-> ((InterpreterState -> (a, InterpreterState)) -> m a)
-> (InterpreterState -> (a, InterpreterState))
-> WriterT w m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InterpreterState -> (a, InterpreterState)) -> m a
forall (m :: * -> *) a.
InterpreterStateMonad m =>
(InterpreterState -> (a, InterpreterState)) -> m a
stateInterpreterState
instance {-# OVERLAPPABLE #-} InterpreterStateMonad m => InterpreterStateMonad (StateT w m) where
  stateInterpreterState :: forall a.
(InterpreterState -> (a, InterpreterState)) -> StateT w m a
stateInterpreterState = m a -> StateT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> StateT w m a)
-> ((InterpreterState -> (a, InterpreterState)) -> m a)
-> (InterpreterState -> (a, InterpreterState))
-> StateT w m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InterpreterState -> (a, InterpreterState)) -> m a
forall (m :: * -> *) a.
InterpreterStateMonad m =>
(InterpreterState -> (a, InterpreterState)) -> m a
stateInterpreterState
instance {-# OVERLAPPABLE #-}
         (InterpreterStateMonad m, Monoid w) => InterpreterStateMonad (RWST r w s m) where
  stateInterpreterState :: forall a.
(InterpreterState -> (a, InterpreterState)) -> RWST r w s m a
stateInterpreterState = m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> RWST r w s m a)
-> ((InterpreterState -> (a, InterpreterState)) -> m a)
-> (InterpreterState -> (a, InterpreterState))
-> RWST r w s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InterpreterState -> (a, InterpreterState)) -> m a
forall (m :: * -> *) a.
InterpreterStateMonad m =>
(InterpreterState -> (a, InterpreterState)) -> m a
stateInterpreterState
instance InterpreterStateMonad m => InterpreterStateMonad (ExceptT e m) where
  stateInterpreterState :: forall a.
(InterpreterState -> (a, InterpreterState)) -> ExceptT e m a
stateInterpreterState = m a -> ExceptT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> ExceptT e m a)
-> ((InterpreterState -> (a, InterpreterState)) -> m a)
-> (InterpreterState -> (a, InterpreterState))
-> ExceptT e m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InterpreterState -> (a, InterpreterState)) -> m a
forall (m :: * -> *) a.
InterpreterStateMonad m =>
(InterpreterState -> (a, InterpreterState)) -> m a
stateInterpreterState

type EvalM' ext m =
  ( MonadReader ContractEnv m
  , InterpreterStateMonad m
  , MonadWriter MorleyLogsBuilder m
  , MonadError (MichelsonFailureWithStack ext) m
  )

type EvalM m = EvalM' Void m

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

throwMichelson :: EvalM' ext m => MichelsonFailed ext -> m a
throwMichelson :: forall ext (m :: * -> *) a.
EvalM' ext m =>
MichelsonFailed ext -> m a
throwMichelson MichelsonFailed ext
mf = (ContractEnv -> ErrorSrcPos) -> m ErrorSrcPos
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ContractEnv -> ErrorSrcPos
ceErrorSrcPos m ErrorSrcPos -> (ErrorSrcPos -> m a) -> m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= MichelsonFailureWithStack ext -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (MichelsonFailureWithStack ext -> m a)
-> (ErrorSrcPos -> MichelsonFailureWithStack ext)
-> ErrorSrcPos
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MichelsonFailed ext -> ErrorSrcPos -> MichelsonFailureWithStack ext
forall ext.
MichelsonFailed ext -> ErrorSrcPos -> MichelsonFailureWithStack ext
MichelsonFailureWithStack MichelsonFailed ext
mf

-- | Function to change amount of remaining steps stored in State monad.
runInstr :: EvalM m => InstrRunner m
runInstr :: forall (m :: * -> *). EvalM m => InstrRunner m
runInstr i :: Instr inp out
i@(Seq Instr inp b
_i1 Instr b out
_i2) Rec StkEl inp
r = InstrRunner m -> InstrRunner m
forall ext (m :: * -> *).
EvalM' ext 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 ErrorSrcPos
_ Instr inp out
_) Rec StkEl inp
r = InstrRunner m -> InstrRunner m
forall ext (m :: * -> *).
EvalM' ext 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@(Meta SomeMeta
_ Instr inp out
_i1) Rec StkEl inp
r = InstrRunner m -> InstrRunner m
forall ext (m :: * -> *).
EvalM' ext 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 -> InstrRunner m
forall ext (m :: * -> *).
EvalM' ext 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 -> InstrRunner m
forall ext (m :: * -> *).
EvalM' ext 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 -> InstrRunner m
forall ext (m :: * -> *).
EvalM' ext 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 Void -> m (Rec StkEl out)
forall ext (m :: * -> *) a.
EvalM' ext m =>
MichelsonFailed ext -> m a
throwMichelson MichelsonFailed Void
forall ext. MichelsonFailed ext
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 -> InstrRunner m
forall ext (m :: * -> *).
EvalM' ext 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 :: forall (m :: * -> *). EvalM m => InstrRunner m
runInstrNoGas = InstrRunner m -> InstrRunner m
forall ext (m :: * -> *).
EvalM' ext m =>
InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
forall (m :: * -> *). EvalM m => InstrRunner m
runInstrNoGas

-- | Function to interpret Michelson instruction(s) against given stack.
-- The @ext@ type variable specifies additional exceptions that can be thrown from the inner
-- runner function (via 'MichelsonExt'). In Morley, it's set to 'Void', but downstream consumers
-- may use other type here.
runInstrImpl :: forall ext m. EvalM' ext m => InstrRunner m -> InstrRunner m
runInstrImpl :: forall ext (m :: * -> *).
EvalM' ext m =>
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 ErrorSrcPos
ics Instr inp out
i) Rec StkEl inp
r = (ContractEnv -> ContractEnv)
-> m (Rec StkEl out) -> m (Rec StkEl out)
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ContractEnv
env -> ContractEnv
env{ceErrorSrcPos :: ErrorSrcPos
ceErrorSrcPos = ErrorSrcPos
ics}) (m (Rec StkEl out) -> m (Rec StkEl out))
-> m (Rec StkEl out) -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ 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 (Meta SomeMeta
_ 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 (FrameInstr (Proxy s
_ :: Proxy s) Instr a b
i) Rec StkEl inp
r = do
  let (Rec StkEl a
inp, Rec StkEl s
end) = 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 -> InstrRunner m
forall ext (m :: * -> *).
EvalM' ext 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 ext (m :: * -> *).
EvalM' ext m =>
InstrRunner m -> SomeItStack -> m ()
interpretExt InstrRunner m
runner (ExtInstr inp -> Rec StkEl inp -> SomeItStack
forall (n :: [T]). ExtInstr n -> Rec StkEl n -> 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 -> InstrRunner m
forall ext (m :: * -> *).
EvalM' ext m =>
InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner Instr inp out
sq 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 -> InstrRunner m
forall ext (m :: * -> *).
EvalM' ext m =>
InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner (PeanoNatural m -> Instr rs (Drop m rs)
forall (n :: Peano) (inp :: [T]).
RequireLongerOrSameLength inp n =>
PeanoNatural n -> Instr inp (Drop n inp)
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
_ AnnDUP{} (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 a
duplicateStkEl <- LensLike m (StkEl r) (StkEl a) (Value a) (Value a)
-> LensLike m (StkEl r) (StkEl a) (Value a) (Value a)
forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf LensLike m (StkEl r) (StkEl a) (Value a) (Value a)
forall (t :: T) (t :: T).
Iso (StkEl t) (StkEl t) (Value t) (Value t)
seValueL Value a -> m (Value a)
forall ext (m :: * -> *) (t :: T).
EvalM' ext m =>
Value t -> m (Value t)
assignBigMapIds' StkEl r
stkEl
  pure $ StkEl a
duplicateStkEl StkEl a -> Rec StkEl (r : rs) -> Rec StkEl (a : 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
_ (AnnDUPN AnnVar
_ 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 :: forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDUPN n inp out a =>
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 a
duplicateStkEl <- LensLike m (StkEl r) (StkEl a) (Value a) (Value a)
-> LensLike m (StkEl r) (StkEl a) (Value a) (Value a)
forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf LensLike m (StkEl r) (StkEl a) (Value a) (Value a)
forall (t :: T) (t :: T).
Iso (StkEl t) (StkEl t) (Value t) (Value t)
seValueL Value a -> m (Value a)
forall ext (m :: * -> *) (t :: T).
EvalM' ext m =>
Value t -> m (Value t)
assignBigMapIds' StkEl r
stkEl
        pure $ StkEl a
duplicateStkEl StkEl a -> Rec StkEl inp -> Rec StkEl (a : 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 : (LazyTake m (Tail inp) ++ (a : Drop n inp))))
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 : (LazyTake m (Tail inp) ++ (a : Drop n inp))))
-> (Rec StkEl (a : (LazyTake m (Tail inp) ++ (a : Drop n inp)))
    -> 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 :: 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
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 : (LazyTake
             m
             (LazyTake m (Tail (LazyTake n inp ++ Drop ('S n) inp))
              ++ (a : Drop n (LazyTake n inp ++ Drop ('S n) inp)))
           ++ 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 :: 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
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
     (LazyTake m (Tail (LazyTake n out ++ Drop ('S n) out))
      ++ (a : Drop n (LazyTake n out ++ Drop ('S n) out)))
-> Rec
     StkEl
     (r : (LazyTake m (Tail (LazyTake n out ++ Drop ('S n) out))
           ++ (a : Drop n (LazyTake n out ++ Drop ('S n) out))))
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
     (LazyTake m (Tail (LazyTake n out ++ Drop ('S n) out))
      ++ (a : Drop n (LazyTake n out ++ Drop ('S n) 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 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
_ AnnSOME{} ((StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
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 (t :: T). Value t -> StkEl t
StkEl (Maybe (Value r) -> Value ('TOption r)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
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
_ (AnnPUSH Anns '[VarAnn, Notes t]
_ 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 (t :: T). Value t -> StkEl t
StkEl 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
_ AnnNONE{} 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 (t :: T). Value t -> StkEl t
StkEl (Maybe (Value' Instr a) -> Value ('TOption a)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
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
_ AnnUNIT{} 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 (t :: T). Value t -> StkEl t
StkEl 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 t1
a)) :& 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 t1 -> StkEl t1
forall (t :: T). Value t -> StkEl t
StkEl Value' Instr t1
a StkEl t1 -> Rec StkEl rs -> Rec StkEl (t1 : 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 t1)
Nothing) :& 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) :& (StkEl Value r
b) :& 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 (t :: T). Value t -> StkEl t
StkEl ((Value r, Value r) -> Value ('TPair r r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value r
a, Value r
b)) 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))) :& 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 (t :: T). Value t -> StkEl t
StkEl 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 (t :: T). Value t -> StkEl t
StkEl 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
_ (AnnPAIRN AnnVar
_ 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 (RightComb (LazyTake n inp) : Drop 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 :: forall (n :: Peano) (inp :: [T]).
ConstraintPairN n inp =>
PeanoNatural n -> Rec StkEl inp -> Rec StkEl (PairN n inp)
go (Succ (Succ PeanoNatural m
Zero)) (StkEl Value r
a :& StkEl Value r
b :& Rec StkEl rs
r) =
      -- if n=2
      Value ('TPair r r) -> StkEl ('TPair r r)
forall (t :: T). Value t -> StkEl t
StkEl ((Value r, Value r) -> Value ('TPair r r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value r
a, Value r
b)) 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 :& 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 :& Rec StkEl rs
r' ->
            Value ('TPair r r) -> StkEl ('TPair r r)
forall (t :: T). Value t -> StkEl t
StkEl ((Value r, Value r) -> Value ('TPair r r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value r
a, Value r
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 :& 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 -> Rec StkEl (UnpairN n r)
forall (n :: Peano) (pair :: T).
ConstraintUnpairN n pair =>
PeanoNatural n -> Value pair -> Rec StkEl (UnpairN n pair)
go PeanoNatural n
s Value r
pair0 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
      -> Rec StkEl (UnpairN n pair)
    go :: forall (n :: Peano) (pair :: T).
ConstraintUnpairN n pair =>
PeanoNatural n -> Value pair -> Rec StkEl (UnpairN n pair)
go PeanoNatural n
n Value pair
pair =
      case (PeanoNatural n
n, Value pair
pair) of
        -- if n=2
        (Succ (Succ PeanoNatural m
Zero), VPair (Value' Instr l
a, Value' Instr r
b)) ->
          Value' Instr l -> StkEl l
forall (t :: T). Value t -> StkEl t
StkEl Value' Instr l
a
            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 -> StkEl r
forall (t :: T). Value t -> StkEl t
StkEl Value' Instr r
b
            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)
_))) ->
          Value' Instr l -> StkEl l
forall (t :: T). Value t -> StkEl t
StkEl Value' Instr l
a
            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 -> Rec StkEl (UnpairN m r)
forall (n :: Peano) (pair :: T).
ConstraintUnpairN n pair =>
PeanoNatural n -> Value pair -> Rec StkEl (UnpairN n pair)
go PeanoNatural m
n' Value' Instr r
b
runInstrImpl InstrRunner m
_ AnnCAR{} (StkEl (VPair (Value' Instr l
a, Value' Instr r
_b)) :& 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 (t :: T). Value t -> StkEl t
StkEl 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{} (StkEl (VPair (Value' Instr l
_a, Value' Instr 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' Instr r -> StkEl r
forall (t :: T). Value t -> StkEl t
StkEl 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{} ((StkEl 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 ('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) -> StkEl ('TOr r b)
forall (t :: T). Value 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) 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{} ((StkEl Value r
b) :& 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) -> StkEl ('TOr a r)
forall (t :: T). Value 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) 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)) :& Rec StkEl rs
r) =
  Instr (a : s) out -> Rec StkEl (a : s) -> m (Rec StkEl out)
InstrRunner m
runner Instr (a : s) out
bLeft (Value' Instr l -> StkEl l
forall (t :: T). Value t -> StkEl t
StkEl 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
runner (IF_LEFT Instr (a : s) out
_ Instr (b : s) out
bRight) (StkEl (VOr (Right Value' Instr r
a)) :& Rec StkEl rs
r) =
  Instr (b : s) out -> Rec StkEl (b : s) -> m (Rec StkEl out)
InstrRunner m
runner Instr (b : s) out
bRight (Value' Instr r -> StkEl r
forall (t :: T). Value t -> StkEl t
StkEl 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
_ AnnNIL{} 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 (t :: T). Value t -> StkEl t
StkEl ([Value' Instr p] -> Value ('TList p)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
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
_ AnnCONS{} (StkEl r
a :& StkEl (VList [Value' Instr t1]
l) :& 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 (t :: T). Value t -> StkEl t
StkEl ([Value' Instr r] -> Value ('TList r)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList (StkEl r -> Value' Instr r
forall (t :: T). StkEl t -> Value t
seValue StkEl r
a Value' Instr r -> [Value' Instr r] -> [Value' Instr r]
forall a. a -> [a] -> [a]
: [Value' Instr r]
[Value' Instr t1]
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 []) :& 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 t1
lh : [Value' Instr t1]
lr)) :& 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 t1 -> StkEl t1
forall (t :: T). Value t -> StkEl t
StkEl Value' Instr t1
lh StkEl t1
-> Rec StkEl ('TList t1 : rs) -> Rec StkEl (t1 : 'TList t1 : rs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Value ('TList t1) -> StkEl ('TList t1)
forall (t :: T). Value t -> StkEl t
StkEl ([Value' Instr t1] -> Value ('TList t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList [Value' Instr t1]
lr) StkEl ('TList t1) -> Rec StkEl rs -> Rec StkEl ('TList t1 : 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
_ AnnSIZE{} (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 (t :: T). Value t -> StkEl t
StkEl (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
$ forall a b. (HasCallStack, Integral a, Integral b) => a -> b
Unsafe.fromIntegral @Int @Natural (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 (t :: T). StkEl t -> Value t
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
_ AnnEMPTY_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 (t :: T). Value t -> StkEl t
StkEl (Set (Value' Instr e) -> Value ('TSet e)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
(SingI t1, Comparable t1) =>
Set (Value' instr t1) -> Value' instr ('TSet t1)
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
_ AnnEMPTY_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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnEMPTY_BIG_MAP{} Rec StkEl inp
r = do
  Value ('TBigMap a b)
bigMap <- Value ('TBigMap a b) -> m (Value ('TBigMap a b))
forall ext (m :: * -> *) (t :: T).
EvalM' ext 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 (t :: T). Value t -> StkEl t
StkEl 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 (AnnMAP AnnVar
_ (Instr (MapOpInp c : s) (b : s)
code :: Instr (MapOpInp c ': s) (b ': s))) (StkEl Value r
a :& 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) (StkEl (MapOpInp c)
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 (t :: T). StkEl t -> Value t
seValue -> Value' Instr b
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) -> StkEl (MapOpInp c)
forall (t :: T). Value t -> StkEl t
StkEl Value (MapOpInp c)
el) (Value (MapOpInp c) -> StkEl (MapOpInp c))
-> [Value (MapOpInp c)] -> [StkEl (MapOpInp c)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (t :: T). Value t -> StkEl t
StkEl (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 (Instr (IterOpEl c : out) out
code :: Instr (IterOpEl c ': s) s)) (StkEl Value r
a :& Rec StkEl rs
r) =
  case 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) -> StkEl (IterOpEl c)
forall (t :: T). Value t -> StkEl t
StkEl Value' Instr (IterOpEl c)
x StkEl (IterOpEl c) -> Rec StkEl rs -> Rec StkEl (IterOpEl c : rs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
      Instr (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) (out :: [T]).
IterOp c =>
Instr (IterOpEl c : out) out -> Instr (c : out) out
ITER Instr (IterOpEl c : out) out
code) (Value' Instr c -> StkEl c
forall (t :: T). Value t -> StkEl t
StkEl Value' Instr c
xs 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
_ AnnMEM{} (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 (t :: T). Value t -> StkEl t
StkEl (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 (t :: T). StkEl t -> Value t
seValue StkEl r
a) (StkEl r -> Value' Instr r
forall (t :: T). StkEl t -> Value t
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
_ AnnGET{} (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 (t :: T). Value t -> StkEl t
StkEl (Maybe (Value' Instr (GetOpVal c)) -> Value ('TOption (GetOpVal c))
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
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 (t :: T). StkEl t -> Value t
seValue StkEl r
a) (StkEl r -> Value' Instr r
forall (t :: T). StkEl t -> Value t
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
_ (AnnGETN AnnVar
_ PeanoNatural ix
s) (StkEl Value r
pair :& 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 (t :: T). Value t -> StkEl t
StkEl (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 :: forall (ix :: Peano) (a :: T).
ConstraintGetN ix a =>
PeanoNatural ix -> Value a -> Value (GetN ix a)
go PeanoNatural ix
Zero            Value a
a                   = Value a
Value' Instr (GetN ix a)
a
    go (Succ PeanoNatural m
Zero)      (VPair (Value' Instr l
left, Value' Instr r
_))  = Value' Instr l
Value' Instr (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
_ AnnUPDATE{} (StkEl r
a :& StkEl r
b :& StkEl Value r
c :& 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 (t :: T). Value t -> StkEl t
StkEl (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 (t :: T). StkEl t -> Value t
seValue StkEl r
a) (StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
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
_ (AnnUPDATEN AnnVar
_ PeanoNatural ix
s) (StkEl (Value r
val :: Value val) :& StkEl Value r
pair :& 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 (t :: T). Value t -> StkEl t
StkEl (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 :: forall (ix :: Peano) (pair :: T).
ConstraintUpdateN ix pair =>
PeanoNatural ix -> Value pair -> Value (UpdateN ix r pair)
go PeanoNatural ix
Zero             Value pair
_                      = Value r
Value' Instr (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
_ AnnGET_AND_UPDATE{} (StkEl Value r
key :& StkEl Value r
valMb :& StkEl Value r
collection :& 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 (t :: T). Value t -> StkEl t
StkEl (Maybe (Value' Instr (GetOpVal c)) -> Value ('TOption (GetOpVal c))
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
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 (t :: T). Value t -> StkEl t
StkEl (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) :& 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) :& 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) :& 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) :& 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 (out :: [T]).
Instr out ('TBool : out) -> Instr ('TBool : out) out
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)) :& 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 (t :: T). Value t -> StkEl t
StkEl 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)) :& Rec StkEl rs
r) = do
  Rec StkEl ('TOr a b : s)
res <- Instr (a : s) ('TOr a b : s)
-> Rec StkEl (a : s) -> m (Rec StkEl ('TOr a b : s))
InstrRunner m
runner Instr (a : s) ('TOr a b : s)
ops (Value' Instr l -> StkEl l
forall (t :: T). Value t -> StkEl t
StkEl Value' Instr l
a StkEl l -> Rec StkEl rs -> Rec StkEl (l : rs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
  Instr ('TOr a b : s) (b : s)
-> Rec StkEl ('TOr a b : s) -> m (Rec StkEl (b : s))
InstrRunner m
runner (Instr (a : s) ('TOr a b : s) -> Instr ('TOr a b : s) (b : s)
forall (a :: T) (s :: [T]) (b :: T).
Instr (a : s) ('TOr a b : s) -> Instr ('TOr a b : s) (b : s)
LOOP_LEFT Instr (a : s) ('TOr a b : s)
ops) Rec StkEl ('TOr a b : s)
res
runInstrImpl InstrRunner m
_ (AnnLAMBDA Anns '[VarAnn, Notes i, Notes o]
_ RemFail Instr '[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 ('TLambda i o) -> StkEl ('TLambda i o)
forall (t :: T). Value t -> StkEl t
StkEl ((IsNotInView => RemFail Instr '[i] '[o]) -> Value ('TLambda i o)
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)) =>
(IsNotInView => RemFail instr '[inp] '[out])
-> Value' instr ('TLambda inp out)
mkVLam RemFail Instr '[i] '[o]
IsNotInView => RemFail Instr '[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
_ (AnnLAMBDA_REC Anns '[VarAnn, Notes i, Notes o]
_ RemFail Instr '[i, 'TLambda i o] '[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 ('TLambda i o) -> StkEl ('TLambda i o)
forall (t :: T). Value t -> StkEl t
StkEl ((IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o])
-> Value ('TLambda i o)
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)) =>
(IsNotInView => RemFail instr '[inp, 'TLambda inp out] '[out])
-> Value' instr ('TLambda inp out)
mkVLamRec RemFail Instr '[i, 'TLambda i o] '[o]
IsNotInView => RemFail Instr '[i, 'TLambda i o] '[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 AnnEXEC{} (StkEl r
a :& self :: StkEl r
self@(StkEl (VLam LambdaCode' Instr inp out
code)) :& Rec StkEl rs
r) =
  case LambdaCode' Instr inp out
code of
    LambdaCode (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) -> 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
    LambdaCodeRec (RemFail Instr '[inp, 'TLambda inp out] '[out]
-> Instr '[inp, 'TLambda inp out] '[out]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
RemFail instr i o -> instr i o
T.rfAnyInstr -> Instr '[inp, 'TLambda inp out] '[out]
lBody) -> do
      Rec StkEl '[out]
res <- Instr '[inp, 'TLambda inp out] '[out]
-> Rec StkEl '[inp, 'TLambda inp out] -> m (Rec StkEl '[out])
InstrRunner m
runner Instr '[inp, 'TLambda inp out] '[out]
lBody (StkEl r
a StkEl r -> Rec StkEl '[r] -> Rec StkEl '[r, r]
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StkEl r
self 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
_ i :: Instr inp out
i@AnnAPPLY{} (StkEl (Value r
a :: T.Value a) :& StkEl (VLam LambdaCode' Instr inp out
code) :& Rec StkEl rs
r)
  | Instr (r : 'TLambda ('TPair r b) out : s) ('TLambda b out : s)
_ :: Instr (a : 'TLambda ('TPair a b) c : s) ('TLambda b c : s) <- Instr inp out
i
  , LambdaCode' Instr ('TPair r b) out
_ :: LambdaCode' Instr ('TPair a b) c <- LambdaCode' Instr inp out
code
  = case LambdaCode' Instr inp out
code of
      LambdaCode RemFail Instr '[inp] '[out]
lBody -> 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 (t :: T). Value t -> StkEl t
StkEl (LambdaCode' 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)) =>
LambdaCode' instr inp out -> Value' instr ('TLambda inp out)
VLam (LambdaCode' Instr b out -> Value ('TLambda b out))
-> LambdaCode' Instr b out -> Value ('TLambda b out)
forall a b. (a -> b) -> a -> b
$ RemFail Instr '[b] '[out] -> LambdaCode' Instr b out
forall (instr :: [T] -> [T] -> *) (inp :: T) (out :: T).
(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] -> LambdaCode' instr inp out
LambdaCode ((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
      LambdaCodeRec RemFail Instr '[inp, 'TLambda inp out] '[out]
lBody ->
        let res :: RemFail Instr '[b] '[c]
res = Instr '[b] '[c] -> RemFail Instr '[b] '[c]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
RfNormal (Instr '[b] '[c] -> RemFail Instr '[b] '[c])
-> Instr '[b] '[c] -> RemFail Instr '[b] '[c]
forall a b. (a -> b) -> a -> b
$ Value r -> Instr '[b] '[a, b]
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value r
a Instr '[b] '[a, b]
-> Instr '[a, b] '[ 'TPair a b] -> Instr '[b] '[ 'TPair a b]
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr '[a, b] '[ 'TPair a b]
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR Instr '[b] '[ 'TPair a b]
-> Instr '[ 'TPair a b] '[ 'TLambda ('TPair a b) c, 'TPair a b]
-> Instr '[b] '[ 'TLambda ('TPair a b) c, 'TPair a b]
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` (IsNotInView =>
 RemFail Instr '[ 'TPair a b, 'TLambda ('TPair a b) c] '[c])
-> Instr '[ 'TPair a b] '[ 'TLambda ('TPair a b) c, 'TPair a b]
forall (s :: [T]) (r :: [T]) (i :: T) (o :: T).
(SingI i, SingI o, r ~ ('TLambda i o : s)) =>
(IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o]) -> Instr s r
LAMBDA_REC RemFail Instr '[inp, 'TLambda inp out] '[out]
IsNotInView =>
RemFail Instr '[ 'TPair a b, 'TLambda ('TPair a b) c] '[c]
lBody Instr '[b] '[ 'TLambda ('TPair a b) c, 'TPair a b]
-> Instr
     '[ 'TLambda ('TPair a b) c, 'TPair a b]
     '[ 'TPair a b, 'TLambda ('TPair a b) c]
-> Instr '[b] '[ 'TPair a b, 'TLambda ('TPair a b) c]
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr
  '[ 'TLambda ('TPair a b) c, 'TPair a b]
  '[ 'TPair a b, 'TLambda ('TPair a b) c]
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP Instr '[b] '[ 'TPair a b, 'TLambda ('TPair a b) c]
-> Instr '[ 'TPair a b, 'TLambda ('TPair a b) c] '[c]
-> Instr '[b] '[c]
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr '[ 'TPair a b, 'TLambda ('TPair a b) c] '[c]
forall {inp :: [T]} {out :: [T]} (t1 :: T) (t2 :: T) (s :: [T]).
(inp ~ (t1 : 'TLambda t1 t2 : s), out ~ (t2 : s)) =>
Instr inp out
EXEC
        in Rec StkEl ('TLambda b c : rs) -> m (Rec StkEl ('TLambda b c : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TLambda b c : rs)
 -> m (Rec StkEl ('TLambda b c : rs)))
-> Rec StkEl ('TLambda b c : rs)
-> m (Rec StkEl ('TLambda b c : rs))
forall a b. (a -> b) -> a -> b
$ Value ('TLambda b c) -> StkEl ('TLambda b c)
forall (t :: T). Value t -> StkEl t
StkEl (LambdaCode' Instr b c -> Value ('TLambda b c)
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)) =>
LambdaCode' instr inp out -> Value' instr ('TLambda inp out)
VLam (LambdaCode' Instr b c -> Value ('TLambda b c))
-> LambdaCode' Instr b c -> Value ('TLambda b c)
forall a b. (a -> b) -> a -> b
$ RemFail Instr '[b] '[c] -> LambdaCode' Instr b c
forall (instr :: [T] -> [T] -> *) (inp :: T) (out :: T).
(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] -> LambdaCode' instr inp out
LambdaCode RemFail Instr '[b] '[c]
res) StkEl ('TLambda b c)
-> Rec StkEl rs -> Rec StkEl ('TLambda b c : 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 :: forall (i :: T) (s :: [T]) (o :: [T]).
Instr ('TPair r i : s) o -> Instr (i : s) o
doApply Instr ('TPair r i : s) o
b = Value r -> Instr (i : s) (a : i : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value r
a Instr (i : s) (a : i : s)
-> Instr (a : i : s) ('TPair r i : s)
-> Instr (i : s) ('TPair r i : s)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr (a : i : s) ('TPair r i : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR Instr (i : s) ('TPair r i : s)
-> Instr ('TPair r i : s) o -> Instr (i : s) o
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`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 (LazyTake m (Tail inp) ++ s')
-> Rec StkEl (r : (LazyTake m (Tail inp) ++ s'))
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) (Rec StkEl (LazyTake m (Tail inp) ++ s')
 -> Rec StkEl (r : (LazyTake m (Tail inp) ++ s')))
-> m (Rec StkEl (LazyTake m (Tail inp) ++ s'))
-> m (Rec StkEl (r : (LazyTake m (Tail inp) ++ s')))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InstrRunner m -> InstrRunner m
forall ext (m :: * -> *).
EvalM' ext m =>
InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner (PeanoNatural m
-> Instr s s' -> Instr rs (LazyTake m (Tail inp) ++ s')
forall (n :: Peano) (inp :: [T]) (out :: [T]) (s :: [T])
       (s' :: [T]).
ConstraintDIPN n inp out s s' =>
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 ext -> m (Rec StkEl out)
forall ext (m :: * -> *) a.
EvalM' ext m =>
MichelsonFailed ext -> m a
throwMichelson (MichelsonFailed ext -> m (Rec StkEl out))
-> MichelsonFailed ext -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Value r -> MichelsonFailed ext
forall (n :: T) ext.
(SingI n, ConstantScope n) =>
Value n -> MichelsonFailed ext
MichelsonFailedWith (StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
seValue StkEl r
a)
runInstrImpl InstrRunner m
_ AnnCAST{} Rec StkEl inp
s = Rec StkEl inp -> m (Rec StkEl inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec StkEl inp
s
runInstrImpl InstrRunner m
_ AnnRENAME{} Rec StkEl inp
s = Rec StkEl inp -> m (Rec StkEl inp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec StkEl inp
s
runInstrImpl InstrRunner m
_ AnnPACK{} ((StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnUNPACK{} (StkEl (VBytes ByteString
a) :& 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 (t :: T). Value t -> StkEl t
StkEl (Maybe (Value' Instr a) -> Value ('TOption a)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
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
_ AnnCONCAT{} (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 (t :: T). Value t -> StkEl t
StkEl (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 (t :: T). StkEl t -> Value t
seValue StkEl r
a) (StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
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
_ AnnCONCAT'{} (StkEl (VList [Value' Instr t1]
a) :& Rec StkEl rs
r) = Rec StkEl (t1 : rs) -> m (Rec StkEl (t1 : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl (t1 : rs) -> m (Rec StkEl (t1 : rs)))
-> Rec StkEl (t1 : rs) -> m (Rec StkEl (t1 : rs))
forall a b. (a -> b) -> a -> b
$ Value' Instr t1 -> StkEl t1
forall (t :: T). Value t -> StkEl t
StkEl ([Value' Instr t1] -> Value' Instr t1
forall (c :: T) (instr :: [T] -> [T] -> *).
ConcatOp c =>
[Value' instr c] -> Value' instr c
evalConcat' [Value' Instr t1]
a) StkEl t1 -> Rec StkEl rs -> Rec StkEl (t1 : 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
_ AnnSLICE{} (StkEl (VNat Natural
o) :& StkEl (VNat Natural
l) :& StkEl Value r
s :& 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 (t :: T). Value t -> StkEl t
StkEl (Maybe (Value r) -> Value ('TOption r)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
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
_ AnnISNAT{} (StkEl (VInt Integer
i) :& 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 (t :: T). Value t -> StkEl t
StkEl (Maybe (Value 'TNat) -> Value ('TOption 'TNat)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
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 (t :: T). Value t -> StkEl t
StkEl (Maybe (Value 'TNat) -> Value ('TOption 'TNat)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
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. (HasCallStack, Integral 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
_ AnnADD{} (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) ext (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM' ext monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Add) StkEl r
l StkEl r
r
runInstrImpl InstrRunner m
_ AnnSUB{} (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) ext (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM' ext monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Sub) StkEl r
l StkEl r
r
runInstrImpl InstrRunner m
_ AnnSUB_MUTEZ{} (StkEl r
l :& StkEl r
r :& Rec StkEl rs
rest) = (StkEl ('TOption 'TMutez)
-> Rec StkEl rs -> Rec StkEl ('TOption 'TMutez : rs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
rest) (StkEl ('TOption 'TMutez) -> Rec StkEl ('TOption 'TMutez : rs))
-> m (StkEl ('TOption 'TMutez))
-> m (Rec StkEl ('TOption 'TMutez : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy SubMutez
-> StkEl r -> StkEl r -> m (StkEl (ArithRes SubMutez r r))
forall {k} (aop :: k) (n :: T) (m :: T) ext (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM' ext monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @SubMutez) StkEl r
l StkEl r
r
runInstrImpl InstrRunner m
_ AnnMUL{} (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) ext (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM' ext monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Mul) StkEl r
l StkEl r
r
runInstrImpl InstrRunner m
_ AnnEDIV{} (StkEl r
l :& StkEl r
r :& Rec StkEl rs
rest) = (StkEl (ArithRes EDiv n m)
-> Rec StkEl rs -> Rec StkEl (ArithRes EDiv 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 EDiv n m) -> Rec StkEl (ArithRes EDiv n m : rs))
-> m (StkEl (ArithRes EDiv n m))
-> m (Rec StkEl (ArithRes EDiv n m : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy EDiv -> StkEl r -> StkEl r -> m (StkEl (ArithRes EDiv r r))
forall {k} (aop :: k) (n :: T) (m :: T) ext (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM' ext monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @EDiv) StkEl r
l StkEl r
r
runInstrImpl InstrRunner m
_ AnnABS{} ((StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
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 (t :: T). Value t -> StkEl t
StkEl (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 (forall {t}. Proxy t
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
_ AnnNEG{} ((StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
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 (t :: T). Value t -> StkEl t
StkEl (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 (forall {t}. Proxy t
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
_ AnnLSL{} (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) ext (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM' ext monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Lsl) StkEl r
x StkEl r
s
runInstrImpl InstrRunner m
_ AnnLSR{} (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) ext (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM' ext monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Lsr) StkEl r
x StkEl r
s
runInstrImpl InstrRunner m
_ AnnOR{} (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) ext (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM' ext monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Or) StkEl r
l StkEl r
r
runInstrImpl InstrRunner m
_ AnnAND{} (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) ext (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM' ext monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @And) StkEl r
l StkEl r
r
runInstrImpl InstrRunner m
_ AnnXOR{} (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) ext (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM' ext monad) =>
proxy aop -> StkEl n -> StkEl m -> monad (StkEl (ArithRes aop n m))
runArithOp (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Xor) StkEl r
l StkEl r
r
runInstrImpl InstrRunner m
_ AnnNOT{} ((StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
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 (t :: T). Value t -> StkEl t
StkEl (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 (forall {t}. Proxy t
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
_ AnnCOMPARE{} ((StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
seValue -> Value r
l) :& (StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnEQ{} ((StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
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 (t :: T). Value t -> StkEl t
StkEl (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 (forall {t}. Proxy t
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
_ AnnNEQ{} ((StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
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 (t :: T). Value t -> StkEl t
StkEl (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 (forall {t}. Proxy t
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
_ AnnLT{} ((StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
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 (t :: T). Value t -> StkEl t
StkEl (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 (forall {t}. Proxy t
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
_ AnnGT{} ((StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
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 (t :: T). Value t -> StkEl t
StkEl (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 (forall {t}. Proxy t
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
_ AnnLE{} ((StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
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 (t :: T). Value t -> StkEl t
StkEl (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 (forall {t}. Proxy t
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
_ AnnGE{} ((StkEl r -> Value r
forall (t :: T). StkEl t -> Value t
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 (t :: T). Value t -> StkEl t
StkEl (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 (forall {t}. Proxy t
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
_ AnnINT{} (StkEl Value r
a :& 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 (t :: T). Value t -> StkEl t
StkEl (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
runner (AnnVIEW (Anns2' VarAnn
_ (Notes ret
_ :: Notes ret)) ViewName
name)
                    (StkEl (Value r
arg :: Value arg) :& StkEl (VAddress EpAddress
epAddr) :& Rec StkEl rs
r) = do
  ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  Value ('TOption ret)
res :: Value ('TOption ret) <- Maybe (Value' Instr ret) -> Value ('TOption ret)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption (Maybe (Value' Instr ret) -> Value ('TOption ret))
-> m (Maybe (Value' Instr ret)) -> m (Value ('TOption ret))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeT m (Value' Instr ret) -> m (Maybe (Value' Instr ret))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT do
    EpAddress addr :: KindedAddress kind
addr@ContractAddress{} EpName
_ <- EpAddress -> MaybeT m EpAddress
forall (f :: * -> *) a. Applicative f => a -> f a
pure EpAddress
epAddr
    Just ContractState
viewedContractState <- Maybe ContractState -> MaybeT m (Maybe ContractState)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe ContractState -> MaybeT m (Maybe ContractState))
-> Maybe ContractState -> MaybeT m (Maybe ContractState)
forall a b. (a -> b) -> a -> b
$ KindedAddress kind
-> Map (KindedAddress kind) ContractState -> Maybe ContractState
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KindedAddress kind
addr Map (KindedAddress kind) ContractState
Map ContractAddress ContractState
ceContracts
    ContractState
      { csContract :: ()
csContract = Contract cp st
viewedContract
      , csStorage :: ()
csStorage = Value st
viewedContractStorage
      } <- ContractState -> MaybeT m ContractState
forall (f :: * -> *) a. Applicative f => a -> f a
pure ContractState
viewedContractState
    Just SomeView' Instr st
view_ <- Maybe (SomeView' Instr st) -> MaybeT m (Maybe (SomeView' Instr st))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (SomeView' Instr st)
 -> MaybeT m (Maybe (SomeView' Instr st)))
-> Maybe (SomeView' Instr st)
-> MaybeT m (Maybe (SomeView' Instr st))
forall a b. (a -> b) -> a -> b
$ ViewName -> ViewsSet' Instr st -> Maybe (SomeView' Instr st)
forall (instr :: [T] -> [T] -> *) (st :: T).
ViewName -> ViewsSet' instr st -> Maybe (SomeView' instr st)
lookupView ViewName
name (Contract cp st -> ViewsSet' Instr st
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> ViewsSet' instr st
cViews Contract cp st
viewedContract)
    SomeView (View{ ViewCode' Instr arg st ret
vCode :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewCode' instr arg st ret
vCode :: ViewCode' Instr arg st ret
vCode } :: View arg' st ret') <- SomeView' Instr st -> MaybeT m (SomeView' Instr st)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeView' Instr st
view_
    Just arg :~: arg
Refl <- Maybe (arg :~: arg) -> MaybeT m (Maybe (arg :~: arg))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (arg :~: arg) -> MaybeT m (Maybe (arg :~: arg)))
-> Maybe (arg :~: arg) -> MaybeT m (Maybe (arg :~: arg))
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @arg Sing arg -> Sing arg -> Maybe (arg :~: arg)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
`decideEquality` forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @arg'
    Just ret :~: ret
Refl <- Maybe (ret :~: ret) -> MaybeT m (Maybe (ret :~: ret))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (ret :~: ret) -> MaybeT m (Maybe (ret :~: ret)))
-> Maybe (ret :~: ret) -> MaybeT m (Maybe (ret :~: ret))
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @ret Sing ret -> Sing ret -> Maybe (ret :~: ret)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
`decideEquality` forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @ret'
    Rec StkEl '[ret]
resSt <- m (Rec StkEl '[ret]) -> MaybeT m (Rec StkEl '[ret])
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Rec StkEl '[ret]) -> MaybeT m (Rec StkEl '[ret]))
-> m (Rec StkEl '[ret]) -> MaybeT m (Rec StkEl '[ret])
forall a b. (a -> b) -> a -> b
$
      (ContractEnv -> ContractEnv)
-> m (Rec StkEl '[ret]) -> m (Rec StkEl '[ret])
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (ContractAddress -> ContractState -> ContractEnv -> ContractEnv
mkViewEnv KindedAddress kind
ContractAddress
addr ContractState
viewedContractState) (m (Rec StkEl '[ret]) -> m (Rec StkEl '[ret]))
-> m (Rec StkEl '[ret]) -> m (Rec StkEl '[ret])
forall a b. (a -> b) -> a -> b
$
        InstrRunner m -> InstrRunner m
forall ext (m :: * -> *).
EvalM' ext m =>
InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner ViewCode' Instr arg st ret
vCode (Rec StkEl '[ 'TPair arg st] -> m (Rec StkEl '[ret]))
-> Rec StkEl '[ 'TPair arg st] -> m (Rec StkEl '[ret])
forall a b. (a -> b) -> a -> b
$
          Value ('TPair r st) -> StkEl ('TPair r st)
forall (t :: T). Value t -> StkEl t
StkEl ((Value r, Value st) -> Value ('TPair r st)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value r
arg, Value st
viewedContractStorage)) StkEl ('TPair r st) -> Rec StkEl '[] -> Rec StkEl '[ 'TPair r 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
    let StkEl Value' Instr ret
res :& Rec StkEl rs
RNil = Rec StkEl '[ret]
resSt
    Value' Instr ret -> MaybeT m (Value' Instr ret)
forall (m :: * -> *) a. Monad m => a -> m a
return Value' Instr ret
res
  pure (Value ('TOption ret) -> StkEl ('TOption ret)
forall (t :: T). Value t -> StkEl t
StkEl Value ('TOption ret)
res StkEl ('TOption ret)
-> Rec StkEl rs -> Rec StkEl ('TOption ret : rs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
r)
  where
    mkViewEnv :: ContractAddress -> ContractState -> ContractEnv -> ContractEnv
    mkViewEnv :: ContractAddress -> ContractState -> ContractEnv -> ContractEnv
mkViewEnv ContractAddress
calledAddr ContractState
viewedContractState ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} = ContractEnv :: Timestamp
-> RemainingSteps
-> Mutez
-> Map ContractAddress ContractState
-> ContractAddress
-> L1Address
-> L1Address
-> Mutez
-> VotingPowers
-> ChainId
-> Maybe OperationHash
-> Natural
-> ErrorSrcPos
-> Natural
-> ContractEnv
ContractEnv
      { ceBalance :: Mutez
ceBalance = ContractState -> Mutez
csBalance ContractState
viewedContractState
      , ceSender :: L1Address
ceSender = ContractAddress -> L1Address
forall {k} (c :: k -> Constraint) (f :: k -> *) (a :: k).
c a =>
f a -> Constrained c f
Constrained ContractAddress
ceSelf
      , ceSelf :: ContractAddress
ceSelf = ContractAddress
calledAddr
      , L1Address
ceSource :: L1Address
ceSource :: L1Address
ceSource
      , ceAmount :: Mutez
ceAmount = Mutez
zeroMutez
      , Map ContractAddress ContractState
ceContracts :: Map ContractAddress ContractState
ceContracts :: Map ContractAddress ContractState
ceContracts
      , Timestamp
ceNow :: Timestamp
ceNow :: Timestamp
ceNow, RemainingSteps
ceMaxSteps :: RemainingSteps
ceMaxSteps :: RemainingSteps
ceMaxSteps, VotingPowers
ceVotingPowers :: VotingPowers
ceVotingPowers :: VotingPowers
ceVotingPowers, ChainId
ceChainId :: ChainId
ceChainId :: ChainId
ceChainId, Maybe OperationHash
ceOperationHash :: Maybe OperationHash
ceOperationHash :: Maybe OperationHash
ceOperationHash, Natural
ceLevel :: Natural
ceLevel :: Natural
ceLevel
      , ErrorSrcPos
ceErrorSrcPos :: ErrorSrcPos
ceErrorSrcPos :: ErrorSrcPos
ceErrorSrcPos, Natural
ceMinBlockTime :: Natural
ceMinBlockTime :: Natural
ceMinBlockTime
      }

runInstrImpl InstrRunner m
_ (AnnSELF AnnVar
_ SomeEntrypointCallT arg
sepc :: Instr inp out) Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  case forall {t :: [T]}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @out of
    (Proxy ('TContract arg : inp)
_ :: 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 (t :: T). Value t -> StkEl t
StkEl (Address -> SomeEntrypointCallT arg -> Value ('TContract arg)
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, HasNoOp arg) =>
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract (ContractAddress -> Address
forall (kind :: AddressKind). KindedAddress kind -> Address
MkAddress ContractAddress
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
_ (AnnCONTRACT (Anns2' VarAnn
_ (Notes p
_ :: T.Notes a)) EpName
instrEpName) (StkEl (VAddress EpAddress
epAddr) :& Rec StkEl rs
r) = do
  ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  T.EpAddress' (Constrained KindedAddress a
addr) EpName
addrEpName <- EpAddress -> m EpAddress
forall (f :: * -> *) a. Applicative f => a -> f a
pure 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)) -> StkEl ('TOption ('TContract p))
forall (t :: T). Value t -> StkEl t
StkEl Value ('TOption ('TContract p))
v 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
  Value ('TOption ('TContract p))
-> Rec StkEl ('TOption ('TContract p) : rs)
withNotes (Value ('TOption ('TContract p))
 -> Rec StkEl ('TOption ('TContract p) : rs))
-> m (Value ('TOption ('TContract p)))
-> m (Rec StkEl ('TOption ('TContract p) : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case Maybe EpName
mepName of
    Maybe EpName
Nothing -> Value ('TOption ('TContract p))
-> m (Value ('TOption ('TContract p)))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TOption ('TContract p))
 -> m (Value ('TOption ('TContract p))))
-> Value ('TOption ('TContract p))
-> m (Value ('TOption ('TContract p)))
forall a b. (a -> b) -> a -> b
$ Maybe (Value' Instr ('TContract p))
-> Value ('TOption ('TContract p))
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption Maybe (Value' Instr ('TContract p))
forall a. Maybe a
Nothing
    Just EpName
epName -> case KindedAddress a
addr of
      ImplicitAddress{} -> Value ('TOption ('TContract p))
-> m (Value ('TOption ('TContract p)))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TOption ('TContract p))
 -> m (Value ('TOption ('TContract p))))
-> Value ('TOption ('TContract p))
-> m (Value ('TOption ('TContract p)))
forall a b. (a -> b) -> a -> b
$ KindedAddress a
-> EpName -> ParamNotes 'TUnit -> Value ('TOption ('TContract p))
forall (p :: T) (kind :: AddressKind).
ParameterScope p =>
KindedAddress kind
-> EpName -> ParamNotes p -> Value ('TOption ('TContract p))
castContract KindedAddress a
addr EpName
epName ParamNotes 'TUnit
T.tyImplicitAccountParam
      ContractAddress{} -> Value ('TOption ('TContract p))
-> m (Value ('TOption ('TContract p)))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TOption ('TContract p))
 -> m (Value ('TOption ('TContract p))))
-> Value ('TOption ('TContract p))
-> m (Value ('TOption ('TContract p)))
forall a b. (a -> b) -> a -> b
$
        case KindedAddress a
-> Map (KindedAddress a) ContractState -> Maybe ContractState
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KindedAddress a
addr Map (KindedAddress a) ContractState
Map ContractAddress ContractState
ceContracts of
          Just ContractState{Maybe KeyHash
Mutez
Contract cp st
Value st
csDelegate :: ContractState -> Maybe KeyHash
csDelegate :: Maybe KeyHash
csStorage :: Value st
csContract :: Contract cp st
csBalance :: Mutez
csBalance :: ContractState -> Mutez
csStorage :: ()
csContract :: ()
..} ->
            KindedAddress a
-> EpName -> ParamNotes cp -> Value ('TOption ('TContract p))
forall (p :: T) (kind :: AddressKind).
ParameterScope p =>
KindedAddress kind
-> EpName -> ParamNotes p -> Value ('TOption ('TContract p))
castContract KindedAddress a
addr EpName
epName (Contract cp st -> ParamNotes cp
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
Contract' instr cp st -> ParamNotes cp
cParamNotes Contract cp st
csContract)
          Maybe ContractState
Nothing -> Maybe (Value' Instr ('TContract p))
-> Value ('TOption ('TContract p))
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption Maybe (Value' Instr ('TContract p))
forall a. Maybe a
Nothing
      TxRollupAddress{} ->
        -- TODO [#838]: support transaction rollups on the emulator
        MichelsonFailed ext -> m (Value ('TOption ('TContract p)))
forall ext (m :: * -> *) a.
EvalM' ext m =>
MichelsonFailed ext -> m a
throwMichelson (MichelsonFailed ext -> m (Value ('TOption ('TContract p))))
-> MichelsonFailed ext -> m (Value ('TOption ('TContract p)))
forall a b. (a -> b) -> a -> b
$ Text -> MichelsonFailed ext
forall ext. Text -> MichelsonFailed ext
MichelsonUnsupported Text
"txr1 addresses with CONTRACT"
  where
  castContract
    :: forall p kind. (T.ParameterScope p)
    => KindedAddress kind -> EpName -> T.ParamNotes p -> T.Value ('TOption ('TContract a))
  castContract :: forall (p :: T) (kind :: AddressKind).
ParameterScope p =>
KindedAddress kind
-> EpName -> ParamNotes p -> Value ('TOption ('TContract p))
castContract KindedAddress kind
addr EpName
epName ParamNotes p
param = Maybe (Value' Instr ('TContract p))
-> Value ('TOption ('TContract p))
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
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
_ :: Notes a') 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 <- Either TcTypeError (p :~: arg)
-> Maybe (Either TcTypeError (p :~: arg))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either TcTypeError (p :~: arg)
 -> Maybe (Either TcTypeError (p :~: arg)))
-> Either TcTypeError (p :~: arg)
-> Maybe (Either TcTypeError (p :~: arg))
forall a b. (a -> b) -> a -> b
$ forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TcTypeError (a :~: b)
eqType @a @a'
    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 (KindedAddress kind -> Address
forall (kind :: AddressKind). KindedAddress kind -> Address
MkAddress KindedAddress kind
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
_ AnnTRANSFER_TOKENS{}
  (StkEl Value r
p :& StkEl (VMutez Mutez
mutez) :& StkEl Value r
contract :& Rec StkEl rs
r) = do
    m ()
forall (m :: * -> *). InterpreterStateMonad m => m ()
incrementCounter
    GlobalCounter
globalCounter <- InterpreterState -> GlobalCounter
isGlobalCounter (InterpreterState -> GlobalCounter)
-> m InterpreterState -> m GlobalCounter
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m InterpreterState
forall (m :: * -> *). InterpreterStateMonad m => m InterpreterState
getInterpreterState
    pure $ Value 'TOperation -> StkEl 'TOperation
forall (t :: T). Value t -> StkEl t
StkEl (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)
-> GlobalCounter
-> TransferTokens Instr r
forall (instr :: [T] -> [T] -> *) (p :: T).
Value' instr p
-> Mutez
-> Value' instr ('TContract p)
-> GlobalCounter
-> TransferTokens instr p
TransferTokens Value r
p Mutez
mutez Value r
Value' Instr ('TContract r)
contract GlobalCounter
globalCounter)) 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
_ AnnSET_DELEGATE{} (StkEl (VOption Maybe (Value' Instr t1)
mbKeyHash) :& Rec StkEl rs
r) = do
  m ()
forall (m :: * -> *). InterpreterStateMonad m => m ()
incrementCounter
  GlobalCounter
globalCounter <- InterpreterState -> GlobalCounter
isGlobalCounter (InterpreterState -> GlobalCounter)
-> m InterpreterState -> m GlobalCounter
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m InterpreterState
forall (m :: * -> *). InterpreterStateMonad m => m InterpreterState
getInterpreterState
  case Maybe (Value' Instr t1)
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 (t :: T). Value t -> StkEl t
StkEl (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 -> GlobalCounter -> SetDelegate
SetDelegate (KeyHash -> Maybe KeyHash
forall a. a -> Maybe a
Just KeyHash
k) GlobalCounter
globalCounter)) 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 t1)
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 (t :: T). Value t -> StkEl t
StkEl (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 -> GlobalCounter -> SetDelegate
SetDelegate Maybe KeyHash
forall a. Maybe a
Nothing GlobalCounter
globalCounter)) 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
_ (AnnCREATE_CONTRACT Anns '[VarAnn, VarAnn]
_ Contract' Instr p g
contract)
  (StkEl (VOption Maybe (Value' Instr t1)
mbKeyHash) :& StkEl (VMutez Mutez
m) :& StkEl Value r
g :& Rec StkEl rs
r) = do
  ContractAddress
originator <- ContractEnv -> ContractAddress
ceSelf (ContractEnv -> ContractAddress)
-> m ContractEnv -> m ContractAddress
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  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
  m ()
forall (m :: * -> *). InterpreterStateMonad m => m ()
incrementCounter
  GlobalCounter
globalCounter <- InterpreterState -> GlobalCounter
isGlobalCounter (InterpreterState -> GlobalCounter)
-> m InterpreterState -> m GlobalCounter
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m InterpreterState
forall (m :: * -> *). InterpreterStateMonad m => m InterpreterState
getInterpreterState
  let resAddr :: ContractAddress
resAddr =
        case Maybe OperationHash
opHash of
          Just OperationHash
hash -> OperationHash -> GlobalCounter -> ContractAddress
mkContractAddress OperationHash
hash GlobalCounter
globalCounter
          Maybe OperationHash
Nothing ->
            OperationHash -> GlobalCounter -> ContractAddress
mkContractAddress
              (OriginationOperation -> OperationHash
mkOriginationOperationHash (OriginationOperation -> OperationHash)
-> OriginationOperation -> OperationHash
forall a b. (a -> b) -> a -> b
$
                  ContractAddress
-> Maybe ContractAlias
-> Maybe (Value 'TKeyHash)
-> Mutez
-> Contract' Instr p g
-> Value' Instr g
-> GlobalCounter
-> OriginationOperation
forall (param :: T) (store :: T) (kind :: AddressKind).
(ParameterScope param, StorageScope store, L1AddressKind kind) =>
KindedAddress kind
-> Maybe ContractAlias
-> Maybe (Value 'TKeyHash)
-> Mutez
-> Contract param store
-> Value' Instr store
-> GlobalCounter
-> OriginationOperation
createOrigOp ContractAddress
originator Maybe ContractAlias
forall a. Maybe a
Nothing Maybe (Value' Instr t1)
Maybe (Value 'TKeyHash)
mbKeyHash Mutez
m Contract' Instr p g
contract Value' Instr g
Value r
g GlobalCounter
globalCounter
              )
              -- 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.
              GlobalCounter
globalCounter
  let resEpAddr :: EpAddress
resEpAddr = ContractAddress -> EpName -> EpAddress
forall (kind :: AddressKind).
KindedAddress kind -> EpName -> EpAddress
EpAddress ContractAddress
resAddr EpName
DefEpName
  let resOp :: CreateContract Instr p r
resOp = L1Address
-> Maybe KeyHash
-> Mutez
-> Value r
-> Contract' Instr p r
-> GlobalCounter
-> CreateContract Instr p r
forall (instr :: [T] -> [T] -> *) (cp :: T) (st :: T).
(forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o)) =>
L1Address
-> Maybe KeyHash
-> Mutez
-> Value' instr st
-> Contract' instr cp st
-> GlobalCounter
-> CreateContract instr cp st
CreateContract
        (ContractAddress -> L1Address
forall {k} (c :: k -> Constraint) (f :: k -> *) (a :: k).
c a =>
f a -> Constrained c f
Constrained ContractAddress
originator) (Maybe (Value 'TKeyHash) -> Maybe KeyHash
unwrapMbKeyHash Maybe (Value' Instr t1)
Maybe (Value 'TKeyHash)
mbKeyHash) Mutez
m Value r
g Contract' Instr p g
Contract' Instr p r
contract GlobalCounter
globalCounter
  pure $ Value 'TOperation -> StkEl 'TOperation
forall (t :: T). Value t -> StkEl t
StkEl (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).
(forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o), 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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnIMPLICIT_ACCOUNT{} (StkEl (VKeyHash KeyHash
k) :& 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 (t :: T). Value t -> StkEl t
StkEl (Address -> SomeEntrypointCallT 'TUnit -> Value ('TContract 'TUnit)
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, HasNoOp arg) =>
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract (KindedAddress 'AddressKindImplicit -> Address
forall (kind :: AddressKind). KindedAddress kind -> Address
MkAddress (KindedAddress 'AddressKindImplicit -> Address)
-> KindedAddress 'AddressKindImplicit -> Address
forall a b. (a -> b) -> a -> b
$ KeyHash -> KindedAddress 'AddressKindImplicit
ImplicitAddress 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
_ AnnNOW{} Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnAMOUNT{} Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnBALANCE{} Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnVOTING_POWER{} (StkEl (VKeyHash KeyHash
k) :& Rec StkEl rs
r) = do
  ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnTOTAL_VOTING_POWER{} Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnCHECK_SIGNATURE{}
  (StkEl (VKey PublicKey
k) :& StkEl (VSignature Signature
v) :& StkEl (VBytes ByteString
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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnSHA256{} (StkEl (VBytes ByteString
b) :& 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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnSHA512{} (StkEl (VBytes ByteString
b) :& 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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnBLAKE2B{} (StkEl (VBytes ByteString
b) :& 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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnSHA3{} (StkEl (VBytes ByteString
b) :& 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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnKECCAK{} (StkEl (VBytes ByteString
b) :& 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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnHASH_KEY{} (StkEl (VKey PublicKey
k) :& 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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnPAIRING_CHECK{} (StkEl (VList [Value' Instr t1]
pairs) :& Rec StkEl rs
r) = do
  let pairs' :: [(Bls12381G1, Bls12381G2)]
pairs' = [ (Bls12381G1
g1, Bls12381G2
g2) | VPair (VBls12381G1 Bls12381G1
g1, VBls12381G2 Bls12381G2
g2) <- [Value' Instr t1]
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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnSOURCE{} Rec StkEl inp
r = do
  ContractEnv{ceSource :: ContractEnv -> L1Address
ceSource=Constrained KindedAddress a
ceSource} <- 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 (t :: T). Value t -> StkEl t
StkEl (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
$ KindedAddress a -> EpName -> EpAddress
forall (kind :: AddressKind).
KindedAddress kind -> EpName -> EpAddress
EpAddress KindedAddress a
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
_ AnnSENDER{} Rec StkEl inp
r = do
  ContractEnv{ceSender :: ContractEnv -> L1Address
ceSender=Constrained KindedAddress a
ceSender} <- 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 (t :: T). Value t -> StkEl t
StkEl (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
$ KindedAddress a -> EpName -> EpAddress
forall (kind :: AddressKind).
KindedAddress kind -> EpName -> EpAddress
EpAddress KindedAddress a
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
_ AnnADDRESS{} (StkEl (VContract Address
a SomeEntrypointCallT arg
sepc) :& 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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnCHAIN_ID{} Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnLEVEL{} Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
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 (t :: T). Value t -> StkEl t
StkEl (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
_ AnnSELF_ADDRESS{} Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
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 (t :: T). Value t -> StkEl t
StkEl (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
$ ContractAddress -> EpName -> EpAddress
forall (kind :: AddressKind).
KindedAddress kind -> EpName -> EpAddress
EpAddress ContractAddress
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
_ AnnTICKET{} (StkEl Value r
dat :& StkEl (VNat Natural
am) :& Rec StkEl rs
r) = do
  ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
ceBalance :: ContractEnv -> Mutez
ceMaxSteps :: ContractEnv -> RemainingSteps
ceNow :: ContractEnv -> Timestamp
..} <- m ContractEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  let result :: Value' Instr ('TOption ('TTicket r))
result = Maybe (Value' Instr ('TTicket r))
-> Value' Instr ('TOption ('TTicket r))
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption do
        Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Natural
am Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
/= Natural
0)
        pure $ Address -> Value r -> Natural -> Value' Instr ('TTicket r)
forall (arg :: T) (instr :: [T] -> [T] -> *).
Comparable arg =>
Address
-> Value' instr arg -> Natural -> Value' instr ('TTicket arg)
VTicket (ContractAddress -> Address
forall (kind :: AddressKind). KindedAddress kind -> Address
MkAddress ContractAddress
ceSelf) Value r
dat Natural
am
  Rec StkEl ('TOption ('TTicket r) : rs)
-> m (Rec StkEl ('TOption ('TTicket r) : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOption ('TTicket r) : rs)
 -> m (Rec StkEl ('TOption ('TTicket r) : rs)))
-> Rec StkEl ('TOption ('TTicket r) : rs)
-> m (Rec StkEl ('TOption ('TTicket r) : rs))
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TOption ('TTicket r))
-> StkEl ('TOption ('TTicket r))
forall (t :: T). Value t -> StkEl t
StkEl (Value' Instr ('TOption ('TTicket r))
result) StkEl ('TOption ('TTicket r))
-> Rec StkEl rs -> Rec StkEl ('TOption ('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
_ AnnTICKET_DEPRECATED{} (StkEl Value r
dat :& StkEl (VNat Natural
am) :& Rec StkEl rs
r) = do
  ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
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 (t :: T). Value t -> StkEl t
StkEl (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 (ContractAddress -> Address
forall (kind :: AddressKind). KindedAddress kind -> Address
MkAddress ContractAddress
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
_ AnnREAD_TICKET{} (te :: StkEl r
te@(StkEl (VTicket Address
addr Value' Instr arg
dat Natural
am)) :& 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 (t :: T). Value t -> StkEl t
StkEl
      ((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
_ AnnSPLIT_TICKET{}
    (StkEl tv :: Value r
tv@(VTicket Address
addr Value' Instr arg
dat Natural
am) :&
     StkEl (VPair (VNat Natural
am1, VNat Natural
am2)) :& 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 (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
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 (t :: T). Value t -> StkEl t
StkEl 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
_ AnnJOIN_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)) :& 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 (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
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 (t :: T). Value t -> StkEl t
StkEl 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
runInstrImpl InstrRunner m
_ AnnOPEN_CHEST{}
  (StkEl (VChestKey ChestKey
ck) :& StkEl (VChest Chest
c) :& StkEl (VNat Natural
nat) :& Rec StkEl rs
r) = do
  let result :: Value' Instr ('TOr 'TBytes 'TBool)
result = case Natural -> Either Text TLTime
forall i. Integral i => i -> Either Text TLTime
mkTLTime Natural
nat of
        Right TLTime
time -> case Chest -> ChestKey -> TLTime -> OpeningResult
openChest Chest
c ChestKey
ck TLTime
time of
          Correct ByteString
bytes -> Either (Value 'TBytes) (Value 'TBool)
-> Value' Instr ('TOr 'TBytes 'TBool)
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 (Value 'TBytes -> Either (Value 'TBytes) (Value 'TBool)
forall a b. a -> Either a b
Left (ByteString -> Value 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes ByteString
bytes))
          OpeningResult
BogusOpening  -> Either (Value 'TBytes) (Value 'TBool)
-> Value' Instr ('TOr 'TBytes 'TBool)
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 (Value 'TBool -> Either (Value 'TBytes) (Value 'TBool)
forall a b. b -> Either a b
Right (Bool -> Value 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool Bool
True))
          OpeningResult
BogusCipher   -> Either (Value 'TBytes) (Value 'TBool)
-> Value' Instr ('TOr 'TBytes 'TBool)
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 (Value 'TBool -> Either (Value 'TBytes) (Value 'TBool)
forall a b. b -> Either a b
Right (Bool -> Value 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool Bool
False))
        Left Text
_ -> Either (Value 'TBytes) (Value 'TBool)
-> Value' Instr ('TOr 'TBytes 'TBool)
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 (Value 'TBool -> Either (Value 'TBytes) (Value 'TBool)
forall a b. b -> Either a b
Right (Bool -> Value 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool Bool
True))
  Rec StkEl ('TOr 'TBytes 'TBool : rs)
-> m (Rec StkEl ('TOr 'TBytes 'TBool : rs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rec StkEl ('TOr 'TBytes 'TBool : rs)
 -> m (Rec StkEl ('TOr 'TBytes 'TBool : rs)))
-> Rec StkEl ('TOr 'TBytes 'TBool : rs)
-> m (Rec StkEl ('TOr 'TBytes 'TBool : rs))
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TOr 'TBytes 'TBool) -> StkEl ('TOr 'TBytes 'TBool)
forall (t :: T). Value t -> StkEl t
StkEl Value' Instr ('TOr 'TBytes 'TBool)
result StkEl ('TOr 'TBytes 'TBool)
-> Rec StkEl rs -> Rec StkEl ('TOr 'TBytes '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
_ AnnSAPLING_EMPTY_STATE{} Rec StkEl inp
_ = MichelsonFailed ext -> m (Rec StkEl out)
forall ext (m :: * -> *) a.
EvalM' ext m =>
MichelsonFailed ext -> m a
throwMichelson (MichelsonFailed ext -> m (Rec StkEl out))
-> MichelsonFailed ext -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Text -> MichelsonFailed ext
forall ext. Text -> MichelsonFailed ext
MichelsonUnsupported Text
"SAPLING_EMPTY_STATE"
runInstrImpl InstrRunner m
_ AnnSAPLING_VERIFY_UPDATE{} Rec StkEl inp
_ = MichelsonFailed ext -> m (Rec StkEl out)
forall ext (m :: * -> *) a.
EvalM' ext m =>
MichelsonFailed ext -> m a
throwMichelson (MichelsonFailed ext -> m (Rec StkEl out))
-> MichelsonFailed ext -> m (Rec StkEl out)
forall a b. (a -> b) -> a -> b
$ Text -> MichelsonFailed ext
forall ext. Text -> MichelsonFailed ext
MichelsonUnsupported Text
"SAPLING_VERIFY_UPDATE"
runInstrImpl InstrRunner m
_ AnnMIN_BLOCK_TIME{} Rec StkEl inp
r = do
  ContractEnv{Natural
Maybe OperationHash
Map ContractAddress ContractState
ErrorSrcPos
L1Address
ChainId
Timestamp
Mutez
ContractAddress
VotingPowers
RemainingSteps
ceMinBlockTime :: Natural
ceErrorSrcPos :: ErrorSrcPos
ceLevel :: Natural
ceOperationHash :: Maybe OperationHash
ceChainId :: ChainId
ceVotingPowers :: VotingPowers
ceAmount :: Mutez
ceSender :: L1Address
ceSource :: L1Address
ceSelf :: ContractAddress
ceContracts :: Map ContractAddress ContractState
ceBalance :: Mutez
ceMaxSteps :: RemainingSteps
ceNow :: Timestamp
ceMinBlockTime :: ContractEnv -> Natural
ceErrorSrcPos :: ContractEnv -> ErrorSrcPos
ceLevel :: ContractEnv -> Natural
ceOperationHash :: ContractEnv -> Maybe OperationHash
ceChainId :: ContractEnv -> ChainId
ceVotingPowers :: ContractEnv -> VotingPowers
ceAmount :: ContractEnv -> Mutez
ceSender :: ContractEnv -> L1Address
ceSource :: ContractEnv -> L1Address
ceSelf :: ContractEnv -> ContractAddress
ceContracts :: ContractEnv -> Map ContractAddress ContractState
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 (t :: T). Value t -> StkEl t
StkEl (Natural -> Value 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
ceMinBlockTime) 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
_ (AnnEMIT AnnVar
_ (FieldAnn -> Text
forall {k} (tag :: k). Annotation tag -> Text
unAnnotation -> Text
emTag) Maybe (Notes t)
mNotes) ((StkEl Value r
emValue) :& Rec StkEl rs
r) = do
  m ()
forall (m :: * -> *). InterpreterStateMonad m => m ()
incrementCounter
  GlobalCounter
emCounter <- InterpreterState -> GlobalCounter
isGlobalCounter (InterpreterState -> GlobalCounter)
-> m InterpreterState -> m GlobalCounter
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m InterpreterState
forall (m :: * -> *). InterpreterStateMonad m => m InterpreterState
getInterpreterState
  let emNotes :: Notes t
emNotes = Notes t -> Maybe (Notes t) -> Notes t
forall a. a -> Maybe a -> a
fromMaybe Notes t
forall (t :: T). SingI t => Notes t
starNotes Maybe (Notes t)
mNotes
  pure $ Value 'TOperation -> StkEl 'TOperation
forall (t :: T). Value t -> StkEl t
StkEl (Operation -> Value 'TOperation
forall (instr :: [T] -> [T] -> *).
Operation' instr -> Value' instr 'TOperation
VOp (Emit Instr t -> Operation
forall (t :: T) (instr :: [T] -> [T] -> *).
PackedValScope t =>
Emit instr t -> Operation' instr
OpEmit Emit :: forall (instr :: [T] -> [T] -> *) (t :: T).
PackedValScope t =>
Text -> Notes t -> Value' instr t -> GlobalCounter -> Emit instr t
Emit{Text
GlobalCounter
Notes t
Value' Instr t
Value r
emCounter :: GlobalCounter
emValue :: Value' Instr t
emNotes :: Notes t
emTag :: Text
emNotes :: Notes t
emCounter :: GlobalCounter
emValue :: Value r
emTag :: Text
..})) 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

-- | Evaluates an arithmetic operation and either fails or proceeds.
runArithOp
  :: (ArithOp aop n m, EvalM' ext monad)
  => proxy aop
  -> StkEl n
  -> StkEl m
  -> monad (StkEl (ArithRes aop n m))
runArithOp :: forall {k} (aop :: k) (n :: T) (m :: T) ext (monad :: * -> *)
       (proxy :: k -> *).
(ArithOp aop n m, EvalM' ext monad) =>
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 (t :: T). StkEl t -> Value t
seValue StkEl n
l) (StkEl m -> Value' Instr m
forall (t :: T). StkEl t -> Value t
seValue StkEl m
r) of
  Left  ArithError (Value' Instr n) (Value' Instr m)
err -> MichelsonFailed ext -> monad (StkEl (ArithRes aop n m))
forall ext (m :: * -> *) a.
EvalM' ext m =>
MichelsonFailed ext -> m a
throwMichelson (MichelsonFailed ext -> monad (StkEl (ArithRes aop n m)))
-> MichelsonFailed ext -> monad (StkEl (ArithRes aop n m))
forall a b. (a -> b) -> a -> b
$ ArithError (Value' Instr n) (Value' Instr m) -> MichelsonFailed ext
forall (n :: T) (m :: T) ext.
(Typeable n, Typeable m) =>
ArithError (Value n) (Value m) -> MichelsonFailed ext
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 (t :: T). Value t -> StkEl t
StkEl 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 :: forall (t :: T).
UnpackedValScope t =>
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, L1AddressKind kind)
  => KindedAddress kind
  -> Maybe ContractAlias
  -> Maybe (T.Value 'T.TKeyHash)
  -> Mutez
  -> Contract param store
  -> Value' Instr store
  -> GlobalCounter
  -> OriginationOperation
createOrigOp :: forall (param :: T) (store :: T) (kind :: AddressKind).
(ParameterScope param, StorageScope store, L1AddressKind kind) =>
KindedAddress kind
-> Maybe ContractAlias
-> Maybe (Value 'TKeyHash)
-> Mutez
-> Contract param store
-> Value' Instr store
-> GlobalCounter
-> OriginationOperation
createOrigOp KindedAddress kind
originator Maybe ContractAlias
mbAlias Maybe (Value 'TKeyHash)
mbDelegate Mutez
bal Contract param store
contract Value' Instr store
storage GlobalCounter
counter =
  OriginationOperation :: forall (cp :: T) (st :: T) (kind :: AddressKind).
(StorageScope st, ParameterScope cp, L1AddressKind kind) =>
KindedAddress kind
-> Maybe KeyHash
-> Mutez
-> Value st
-> Contract cp st
-> GlobalCounter
-> Maybe ContractAlias
-> OriginationOperation
OriginationOperation
    { ooOriginator :: KindedAddress kind
ooOriginator = KindedAddress kind
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
    , ooCounter :: GlobalCounter
ooCounter = GlobalCounter
counter
    , ooAlias :: Maybe ContractAlias
ooAlias = Maybe ContractAlias
mbAlias
    }

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' ext m => InstrRunner m -> SomeItStack -> m ()
interpretExt :: forall ext (m :: * -> *).
EvalM' ext m =>
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 a b. (Buildable a, FromBuilder b) => a -> b
pretty (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 (t :: T). StkEl t -> Value t
seValue)
  MorleyLogsBuilder -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (MorleyLogsBuilder -> m ())
-> (Text -> MorleyLogsBuilder) -> Text -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> MorleyLogsBuilder
forall x. One x => OneItem x -> x
one (Text -> m ()) -> Text -> m ()
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)

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 -> InstrRunner m
forall ext (m :: * -> *).
EvalM' ext m =>
InstrRunner m -> InstrRunner m
runInstrImpl InstrRunner m
runner Instr inp ('TBool : out)
instr Rec StkEl inp
st
  let ((StkEl r -> Value 'TBool
forall (t :: T). StkEl t -> Value t
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 ext (m :: * -> *).
EvalM' ext m =>
InstrRunner m -> SomeItStack -> m ()
interpretExt InstrRunner m
runner (ExtInstr inp -> Rec StkEl inp -> SomeItStack
forall (n :: [T]). ExtInstr n -> Rec StkEl n -> SomeItStack
SomeItStack (PrintComment inp -> ExtInstr inp
forall (s :: [T]). PrintComment s -> ExtInstr s
T.PRINT PrintComment inp
pc) Rec StkEl inp
st)
    MichelsonFailed ext -> m ()
forall ext (m :: * -> *) a.
EvalM' ext m =>
MichelsonFailed ext -> m a
throwMichelson (MichelsonFailed ext -> m ()) -> MichelsonFailed ext -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> MichelsonFailed ext
forall ext. Text -> MichelsonFailed ext
MichelsonFailedTestAssert (Text -> MichelsonFailed ext) -> Text -> MichelsonFailed ext
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 :: forall (st :: [T]) a.
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 :: forall (s :: [T]) (n :: Peano).
LongerThan s n =>
(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' ext m => Value t -> m (Value t)
assignBigMapIds' :: forall ext (m :: * -> *) (t :: T).
EvalM' ext m =>
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 (Bool -> Value t -> State BigMapCounter (Value t)
forall (m :: * -> *) (t :: T).
MonadState BigMapCounter m =>
Bool -> Value t -> m (Value t)
assignBigMapIds Bool
True 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)
  => Bool
  -- ^ If true, assign a new ID even if the bigmap already has one.
  -- Otherwise, assign IDs only to bigmaps that don't have one yet.
  -> Value t -> m (Value t)
assignBigMapIds :: forall (m :: * -> *) (t :: T).
MonadState BigMapCounter m =>
Bool -> Value t -> m (Value t)
assignBigMapIds Bool
overwriteExistingId =
  DfsSettings m -> Value t -> m (Value t)
forall (t :: T) (m :: * -> *).
Monad m =>
DfsSettings m -> Value t -> m (Value t)
dfsTraverseValue DfsSettings m
forall a. Default a => a
def{ dsValueStep :: forall (t' :: T). Value t' -> m (Value t')
dsValueStep = \case
      VBigMap Maybe Natural
existingId Map (Value' Instr k) (Value' Instr v)
vBigMap | Bool
overwriteExistingId Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
|| Maybe Natural -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Natural
existingId -> 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
    }

incrementCounter :: (InterpreterStateMonad m) => m ()
incrementCounter :: forall (m :: * -> *). InterpreterStateMonad m => m ()
incrementCounter = (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 { isGlobalCounter :: GlobalCounter
isGlobalCounter = InterpreterState -> GlobalCounter
isGlobalCounter InterpreterState
iState GlobalCounter -> GlobalCounter -> GlobalCounter
forall a. Num a => a -> a -> a
+ GlobalCounter
1 }

instance NFData ext => NFData (MichelsonFailed ext) where
  rnf :: MichelsonFailed ext -> ()
rnf = \case
    MichelsonFailedWith Value t
x -> Value t -> ()
forall a. NFData a => a -> ()
rnf Value t
x
    MichelsonArithError ArithError (Value n) (Value m)
x -> ArithError (Value n) (Value m) -> ()
forall a. NFData a => a -> ()
rnf ArithError (Value n) (Value m)
x
    MichelsonFailed ext
MichelsonGasExhaustion -> ()
    MichelsonFailedTestAssert Text
x -> Text -> ()
forall a. NFData a => a -> ()
rnf Text
x
    MichelsonUnsupported Text
x -> Text -> ()
forall a. NFData a => a -> ()
rnf Text
x
    MichelsonExt ext
x -> ext -> ()
forall a. NFData a => a -> ()
rnf ext
x

instance NFData ext => NFData (MichelsonFailureWithStack ext)