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

-- | Module, containing data types for Michelson value.
module Morley.Michelson.Typed.Instr
  ( Instr (..
          , CAR
          , CDR
          , DUP
          , DUPN
          , PUSH
          , SOME
          , NONE
          , UNIT
          , PAIR
          , UNPAIR
          , PAIRN
          , LEFT
          , RIGHT
          , NIL
          , CONS
          , SIZE
          , EMPTY_SET
          , EMPTY_MAP
          , EMPTY_BIG_MAP
          , MAP
          , MEM
          , GET
          , GETN
          , UPDATE
          , UPDATEN
          , GET_AND_UPDATE
          , LAMBDA
          , LAMBDA_REC
          , EXEC
          , APPLY
          , CAST
          , RENAME
          , PACK
          , UNPACK
          , CONCAT
          , CONCAT'
          , SLICE
          , ISNAT
          , ADD
          , SUB
          , SUB_MUTEZ
          , MUL
          , EDIV
          , ABS
          , NEG
          , LSL
          , LSR
          , OR
          , AND
          , XOR
          , NOT
          , COMPARE
          , EQ
          , NEQ
          , LT
          , GT
          , LE
          , GE
          , INT
          , VIEW
          , SELF
          , CONTRACT
          , TRANSFER_TOKENS
          , SET_DELEGATE
          , CREATE_CONTRACT
          , IMPLICIT_ACCOUNT
          , NOW
          , AMOUNT
          , BALANCE
          , VOTING_POWER
          , TOTAL_VOTING_POWER
          , CHECK_SIGNATURE
          , SHA256
          , SHA512
          , BLAKE2B
          , SHA3
          , KECCAK
          , HASH_KEY
          , PAIRING_CHECK
          , SOURCE
          , SENDER
          , ADDRESS
          , CHAIN_ID
          , LEVEL
          , SELF_ADDRESS
          , TICKET
          , TICKET_DEPRECATED
          , READ_TICKET
          , SPLIT_TICKET
          , JOIN_TICKETS
          , OPEN_CHEST
          , SAPLING_EMPTY_STATE
          , SAPLING_VERIFY_UPDATE
          , MIN_BLOCK_TIME
          , EMIT
          , BYTES
          , NAT
          )
  , castInstr
  , pattern (:#)
  , ExtInstr (..)
  , CommentType (..)
  , StackRef (..)
  , mkStackRef
  , PrintComment (..)
  , TestAssert (..)
  , SomeMeta (..)
  , pattern ConcreteMeta
  , frameInstr
  ) where

import Prelude hiding (EQ, GT, LT)

import Data.Constraint ((\\))
import Data.Default (def)
import Data.List (stripPrefix)
import Data.Singletons (Sing)
import Data.Type.Equality ((:~:)(..))
import Data.Typeable (cast)
import Fmt (Buildable(..), (+|), (|+))
import GHC.TypeNats (Nat)
import Language.Haskell.TH
import Text.Show qualified as T

import Morley.Michelson.Doc
import Morley.Michelson.ErrorPos
import Morley.Michelson.Typed.Annotation (AnnVar, Anns, Notes(..))
import Morley.Michelson.Typed.Arith
import Morley.Michelson.Typed.Contract
import Morley.Michelson.Typed.Entrypoints
import Morley.Michelson.Typed.Instr.Constraints
import Morley.Michelson.Typed.Instr.Internal.Proofs
import Morley.Michelson.Typed.Polymorphic
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.T (T(..))
import Morley.Michelson.Typed.Value (RemFail(..), Value'(..))
import Morley.Michelson.Typed.View
import Morley.Michelson.Untyped (AnyAnn, FieldAnn, StackTypePattern, TypeAnn, VarAnn)
import Morley.Util.Peano
import Morley.Util.PeanoNatural
import Morley.Util.Sing (eqI)
import Morley.Util.TH
import Morley.Util.Type (type (++))

{-# ANN module ("HLint: ignore Language.Haskell.TH should be imported post-qualified or with an explicit import list" :: Text) #-}

-- This next comment is needed to run the doctest examples throughout this module.

-- $setup
-- >>> :m +Morley.Michelson.Typed.T Morley.Util.Peano Morley.Util.PeanoNatural
-- >>> import qualified Debug (show)
-- >>> :set -XPartialTypeSignatures

infixr 8 `Seq`

-- | Representation of Michelson instruction or sequence
-- of instructions.
--
-- Each Michelson instruction is represented by exactly one
-- constructor of this data type. Sequence of instructions
-- is represented with use of @Seq@ constructor in following
-- way: @SWAP; DROP ; DUP;@ -> @SWAP \`Seq\` DROP \`Seq\` DUP@.
-- Special case where there are no instructions is represented
-- by constructor @Nop@, e.g. @IF_NONE {} { SWAP; DROP; }@ ->
-- @IF_NONE Nop (SWAP \`Seq\` DROP)@.
--
-- Type parameter @inp@ states for input stack type. That is,
-- type of the stack that is required for operation to execute.
--
-- Type parameter @out@ states for output stack type or type
-- of stack that will be left after instruction's execution.
--
-- Each constructor here corresponding to an instruction that can have
-- annotations is represented as @AnnX@, where @X@ is the name of
-- the instruction. These constructors accept a typed heterogenous list of
-- annotations as the first argument. Pattern synonyms without the @Ann@
-- prefix are provided, those ignore annotations entirely.
--
-- We need this @AnnX@ constructors to carry annotations for @PACK@.
--
-- When typechecking a sequence of instructions, we'll attach annotations from the
-- "untyped" instruction to the typed one. Note that if an instruction has a type argument,
-- e.g. `PUSH (int :t) 2` we'll attach typed 'Notes' for this type instead; other
-- annotations are used as-is.
--
-- The interpreter mostly ignores annotations, with the exception of those used for
-- entrypoint resolution.
--
-- The serializer ("Morley.Michelson.Interpret.Pack") can restore the original "untyped"
-- instruction from annotations on the "typed" one.
--
-- 'AnnSELF' and 'AnnCONTRACT' are a special case: field annotations on these
-- instructions carry semantic meaning (specify the entrypoint), hence those
-- are stored separately from other annotations, to simplify checking for
-- invariants in "typed" contracts.
data Instr (inp :: [T]) (out :: [T]) where
  -- | A wrapper carrying original source location of the instruction.
  --
  -- TODO [#283]: replace this wrapper with something more clever and abstract.
  WithLoc :: ErrorSrcPos -> Instr a b -> Instr a b

  -- | A wrapper allowing arbitrary user metadata to be stored by some instruction.
  -- TODO [#689]: Use this instead of `DOC_ITEM`.
  Meta :: SomeMeta -> Instr a b -> Instr a b
  Seq :: Instr a b -> Instr b c -> Instr a c
  -- | Nop operation. Missing in Michelson spec, added to parse construction
  -- like  `IF {} { SWAP; DROP; }`.
  Nop :: Instr s s
  Ext :: ExtInstr s -> Instr s s
  -- | Nested wrapper is going to wrap a sequence of instructions with { }.
  -- It is crucial because serialisation of a contract
  -- depends on precise structure of its code.
  Nested :: Instr inp out -> Instr inp out
  -- | Places documentation generated for given instruction under some group.
  -- This is not part of 'ExtInstr' because it does not behave like 'Nop';
  -- instead, it inherits the behaviour of the instruction put within it.
  DocGroup :: DocGrouping -> Instr inp out -> Instr inp out

  AnnCAR :: Anns '[VarAnn, FieldAnn] -> Instr ('TPair a b ': s) (a ': s)
  AnnCDR :: Anns '[VarAnn, FieldAnn] -> Instr ('TPair a b ': s) (b ': s)

  -- Note that we can not merge DROP and DROPN into one instruction
  -- because they are packed differently.
  DROP :: Instr (a ': s) s
  DROPN
    :: forall (n :: Peano) s.
    (RequireLongerOrSameLength s n)
    => PeanoNatural n -> Instr s (Drop n s)
  AnnDUP :: DupableScope a => AnnVar -> Instr (a ': s) (a ': a ': s)
  AnnDUPN
    :: forall (n :: Peano) inp out a. (ConstraintDUPN n inp out a, DupableScope a)
    => AnnVar -> PeanoNatural n -> Instr inp out
  SWAP :: Instr (a ': b ': s) (b ': a ': s)
  DIG
    :: forall (n :: Peano) inp out a. (ConstraintDIG n inp out a)
    => PeanoNatural n -> Instr inp out
  DUG
    :: forall (n :: Peano) inp out a. (ConstraintDUG n inp out a)
    => PeanoNatural n -> Instr inp out
  AnnPUSH
    :: forall t s . ConstantScope t
    => Anns '[VarAnn, Notes t] -> Value' Instr t -> Instr s (t ': s)
  AnnSOME :: Anns '[TypeAnn, VarAnn] -> Instr (a ': s) ('TOption a ': s)
  AnnNONE :: forall a s . SingI a => Anns '[TypeAnn, VarAnn, Notes a] -> Instr s ('TOption a ': s)
  AnnUNIT :: Anns '[TypeAnn, VarAnn] -> Instr s ('TUnit ': s)
  IF_NONE
    :: Instr s s'
    -> Instr (a ': s) s'
    -> Instr ('TOption a ': s) s'
  AnnPAIR :: Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn] -> Instr (a ': b ': s) ('TPair a b ': s)
  AnnUNPAIR :: Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn] -> Instr ('TPair a b ': s) (a ': b ': s)
  -- |
  -- >>> :t PAIRN (toPeanoNatural' @3) :: Instr '[ 'TInt, 'TUnit, 'TString ] _
  -- ...
  -- ...:: Instr
  -- ...    '[ 'TInt, 'TUnit, 'TString]
  -- ...    '[ 'TPair 'TInt ('TPair 'TUnit 'TString)]
  --
  --
  -- >>> PAIRN (toPeanoNatural' @1) :: Instr '[ 'TInt, 'TInt ] _
  -- ...
  -- ... 'PAIR n' expects n ≥ 2
  -- ...
  --
  -- >>> PAIRN (toPeanoNatural' @3) :: Instr '[ 'TInt, 'TInt ] _
  -- ...
  -- ... Expected stack with length >= 3
  -- ... Current stack has size of only 2:
  -- ...
  AnnPAIRN
    :: forall n inp. ConstraintPairN n inp
    => AnnVar -> PeanoNatural n -> Instr inp (PairN n inp)
  -- |
  -- >>> :t UNPAIRN (toPeanoNatural' @3) :: Instr '[ 'TPair 'TInt ('TPair 'TUnit 'TString) ] _
  -- ...
  -- ...:: Instr
  -- ...   '[ 'TPair 'TInt ('TPair 'TUnit 'TString)]
  -- ...   '[ 'TInt, 'TUnit, 'TString]
  --
  -- >>> :t UNPAIRN (toPeanoNatural' @3) :: Instr '[ 'TPair 'TInt ('TPair 'TUnit ('TPair 'TString 'TNat)) ] _
  -- ...
  -- ...:: Instr
  -- ...   '[ 'TPair 'TInt ('TPair 'TUnit ('TPair 'TString 'TNat))]
  -- ...   '[ 'TInt, 'TUnit, 'TPair 'TString 'TNat]
  --
  -- >>> UNPAIRN (toPeanoNatural' @1) :: Instr '[ 'TPair 'TInt 'TUnit ] _
  -- ...
  -- ...'UNPAIR n' expects n ≥ 2
  -- ...
  --
  -- >>> UNPAIRN (toPeanoNatural' @2) :: Instr '[ 'TInt, 'TUnit, 'TString ] _
  -- ...
  -- ...Expected a pair at the top of the stack, but found: 'TInt
  -- ...
  --
  -- >>> UNPAIRN (toPeanoNatural' @3) :: Instr '[ 'TPair 'TInt 'TUnit ] _
  -- ...
  -- ...'UNPAIR 3' expects a right-combed pair with at least 3 elements at the top of the stack,
  -- ...but the pair only contains 2 elements.
  -- ...
  UNPAIRN
    :: forall (n :: Peano) (pair :: T) (s :: [T]).
       ConstraintUnpairN n pair
    => PeanoNatural n
    -> Instr (pair : s) (UnpairN n pair ++ s)

  AnnLEFT :: SingI b => Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes b] -> Instr (a ': s) ('TOr a b ': s)
  AnnRIGHT :: SingI a => Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a] -> Instr (b ': s) ('TOr a b ': s)
  IF_LEFT
    :: Instr (a ': s) s'
    -> Instr (b ': s) s'
    -> Instr ('TOr a b ': s) s'
  AnnNIL :: SingI p => Anns '[TypeAnn, VarAnn, Notes p] -> Instr s ('TList p ': s)
  AnnCONS :: AnnVar -> Instr (a ': 'TList a ': s) ('TList a ': s)
  IF_CONS
    :: Instr (a ': 'TList a ': s) s'
    -> Instr s s'
    -> Instr ('TList a ': s) s'
  AnnSIZE :: SizeOp c => AnnVar -> Instr (c ': s) ('TNat ': s)
  AnnEMPTY_SET
    :: Comparable e
    => Anns '[TypeAnn, VarAnn, Notes e] -> Instr s ('TSet e ': s)
  AnnEMPTY_MAP
    :: (SingI b, Comparable a)
    => Anns '[TypeAnn, VarAnn, Notes a, Notes b] -> Instr s ('TMap a b ': s)
  AnnEMPTY_BIG_MAP
    :: (SingI b, Comparable a, ForbidBigMap b)
    => Anns '[TypeAnn, VarAnn, Notes a, Notes b] -> Instr s ('TBigMap a b ': s)
  AnnMAP :: (MapOp c, SingI b)
      => AnnVar
      -> Instr (MapOpInp c ': s) (b ': s)
      -> Instr (c ': s) (MapOpRes c b ': s)
  ITER :: IterOp c => Instr (IterOpEl c ': s) s -> Instr (c ': s) s
  AnnMEM :: MemOp c => AnnVar -> Instr (MemOpKey c ': c ': s) ('TBool ': s)
  AnnGET
    :: (GetOp c, SingI (GetOpVal c))
    => AnnVar -> Instr (GetOpKey c ': c ': s) ('TOption (GetOpVal c) ': s)
  -- | Get the node at index @ix@ of a right-combed pair.
  -- Nodes are 0-indexed, and are numbered in a breadth-first,
  -- left-to-right fashion.
  --
  -- For example, a pair with 3 elements @pair a b c@ will be
  -- represented as a tree with 5 nodes:
  --
  -- >    pair
  -- >    /   \
  -- >  a     pair
  -- >        /   \
  -- >      b       c
  --
  -- Where the nodes are numbered as follows:
  --
  -- >      0
  -- >    /   \
  -- >  1       2
  -- >        /   \
  -- >      3       4
  --
  -- >>> :t GETN (toPeanoNatural' @1) :: Instr '[ 'TPair 'TInt 'TUnit] _
  -- ...
  -- ...:: Instr '[ 'TPair 'TInt 'TUnit] '[ 'TInt]
  --
  -- >>> GETN (toPeanoNatural' @1) :: Instr '[ 'TUnit ] _
  -- ...
  -- ...Expected a pair at the top of the stack, but found: 'TUnit
  -- ...
  --
  -- >>> GETN (toPeanoNatural' @3) :: Instr '[ 'TPair 'TInt 'TUnit ] _
  -- ...
  -- ...'GET 3' expects a right-combed pair with at least 4 nodes at the top of the stack,
  -- ...but the pair only contains 3 nodes.
  -- ...
  --
  -- Note that @GET 0@ is just the identity function and works for all types (not just pairs).
  --
  -- >>> :t GETN (toPeanoNatural' @0) :: Instr '[ 'TInt ] _
  -- ...
  -- ...:: Instr '[ 'TInt] '[ 'TInt]
  AnnGETN
    :: forall (ix :: Peano) (pair :: T) (s :: [T]).
       ConstraintGetN ix pair
    => AnnVar
    -> PeanoNatural ix
    -> Instr (pair : s) (GetN ix pair ': s)
  AnnUPDATE
    :: UpdOp c
    => AnnVar
    -> Instr (UpdOpKey c ': UpdOpParams c ': c ': s) (c ': s)
  -- | Update the node at index @ix@ of a right-combed pair.
  --
  -- >>> :t UPDATEN (toPeanoNatural' @1) :: Instr '[ 'TString, 'TPair 'TInt 'TUnit] _
  -- ...
  -- ...:: Instr
  -- ...     '[ 'TString, 'TPair 'TInt 'TUnit] '[ 'TPair 'TString 'TUnit]
  --
  -- >>> UPDATEN (toPeanoNatural' @1) :: Instr '[ 'TUnit, 'TInt ] _
  -- ...
  -- ...Expected the 2nd element of the stack to be a pair, but found: 'TInt
  -- ...
  --
  -- >>> UPDATEN (toPeanoNatural' @3) :: Instr '[ 'TString, 'TPair 'TInt 'TUnit ] _
  -- ...
  -- ...'UPDATE 3' expects the 2nd element of the stack to be a right-combed pair with at least 4 nodes,
  -- ...but the pair only contains 3 nodes.
  -- ...
  --
  -- Note that @UPDATE 0@ is equivalent to @DIP { DROP }@.
  --
  -- >>> :t UPDATEN (toPeanoNatural' @0) :: Instr '[ 'TInt, 'TString ] _
  -- ...
  -- ...:: Instr '[ 'TInt, 'TString] '[ 'TInt]
  AnnUPDATEN
    :: forall (ix :: Peano) (val :: T) (pair :: T) (s :: [T]).
       ConstraintUpdateN ix pair
    => AnnVar
    -> PeanoNatural ix
    -> Instr (val : pair : s) (UpdateN ix val pair ': s)
  AnnGET_AND_UPDATE
    :: ( GetOp c, UpdOp c, SingI (GetOpVal c)
       , UpdOpKey c ~ GetOpKey c
       )
    => AnnVar
    -> Instr (UpdOpKey c ': UpdOpParams c ': c ': s) ('TOption (GetOpVal c) : c ': s)
  IF :: Instr s s'
     -> Instr s s'
     -> Instr ('TBool ': s) s'
  LOOP :: Instr s ('TBool ': s)
       -> Instr ('TBool ': s) s
  LOOP_LEFT
    :: Instr (a ': s) ('TOr a b ': s)
    -> Instr ('TOr a b ': s) (b ': s)
  AnnLAMBDA
    :: forall i o s . (SingI i, SingI o)
    => Anns '[VarAnn, Notes i, Notes o]
    -> RemFail Instr '[i] '[o]
    -> Instr s ('TLambda i o ': s)
  AnnLAMBDA_REC
    :: forall i o s . (SingI i, SingI o)
    => Anns '[VarAnn, Notes i, Notes o]
    -> RemFail Instr '[i, 'TLambda i o] '[o]
    -> Instr s ('TLambda i o ': s)
  AnnEXEC :: AnnVar -> Instr (t1 ': 'TLambda t1 t2 ': s) (t2 ': s)
  AnnAPPLY
    :: forall a b c s . (ConstantScope a, SingI b)
    => AnnVar -> Instr (a ': 'TLambda ('TPair a b) c ': s) ('TLambda b c ': s)
  DIP :: Instr a c -> Instr (b ': a) (b ': c)
  DIPN
    :: forall (n :: Peano) inp out s s'. (ConstraintDIPN n inp out s s')
    => PeanoNatural n -> Instr s s' -> Instr inp out
  -- Since 008 it's prohibited to fail with non-packable values and with the
  -- 'Contract t' type values, which is equivalent to our @ConstantScope@ constraint.
  -- See https://gitlab.com/tezos/tezos/-/issues/1093#note_496066354 for more information.
  FAILWITH :: (SingI a, ConstantScope a) => Instr (a ': s) t
  AnnCAST :: forall a s . SingI a => Anns '[VarAnn, Notes a] -> Instr (a ': s) (a ': s)
  AnnRENAME :: AnnVar -> Instr (a ': s) (a ': s)
  AnnPACK :: PackedValScope a => AnnVar -> Instr (a ': s) ('TBytes ': s)
  AnnUNPACK
    :: (UnpackedValScope a, SingI a)
    => Anns '[TypeAnn, VarAnn, Notes a]
    -> Instr ('TBytes ': s) ('TOption a ': s)
  AnnCONCAT :: ConcatOp c => AnnVar -> Instr (c ': c ': s) (c ': s)
  AnnCONCAT' :: ConcatOp c => AnnVar -> Instr ('TList c ': s) (c ': s)
  AnnSLICE
    :: (SliceOp c, SingI c)
    => AnnVar
    -> Instr ('TNat ': 'TNat ': c ': s) ('TOption c ': s)
  AnnISNAT :: AnnVar -> Instr ('TInt ': s) ('TOption ('TNat) ': s)
  AnnADD
    :: ArithOp Add n m
    => AnnVar
    -> Instr (n ': m ': s) (ArithRes Add n m ': s)
  AnnSUB
    :: ArithOp Sub n m
    => AnnVar
    -> Instr (n ': m ': s) (ArithRes Sub n m ': s)
  AnnSUB_MUTEZ :: AnnVar -> Instr ('TMutez ': 'TMutez ': s) ('TOption 'TMutez ': s)
  AnnMUL
    :: ArithOp Mul n m
    => AnnVar
    -> Instr (n ':  m ': s) (ArithRes Mul n m ': s)
  AnnEDIV
    :: ArithOp EDiv n m
    => AnnVar
    -> Instr (n ':  m ': s) (ArithRes EDiv n m ': s)
  AnnABS
    :: UnaryArithOp Abs n
    => AnnVar
    -> Instr (n ': s) (UnaryArithRes Abs n ': s)
  AnnNEG
    :: UnaryArithOp Neg n
    => AnnVar
    -> Instr (n ': s) (UnaryArithRes Neg n ': s)
  AnnLSL
    :: ArithOp Lsl n m
    => AnnVar
    -> Instr (n ': m ': s) (ArithRes Lsl n m ': s)
  AnnLSR
    :: ArithOp Lsr n m
    => AnnVar
    -> Instr (n ':  m ': s) (ArithRes Lsr n m ': s)
  AnnOR
    :: ArithOp Or n m
    => AnnVar
    -> Instr (n ': m ': s) (ArithRes Or n m ': s)
  AnnAND
    :: ArithOp And n m
    => AnnVar
    -> Instr (n ': m ': s) (ArithRes And n m ': s)
  AnnXOR
    :: ArithOp Xor n m
    => AnnVar
    -> Instr (n ': m ': s) (ArithRes Xor n m ': s)
  AnnNOT
    :: (SingI n, UnaryArithOp Not n)
    => AnnVar
    -> Instr (n ': s) (UnaryArithRes Not n ': s)
  AnnCOMPARE
    :: Comparable n
    => AnnVar
    -> Instr (n ': n ': s) ('TInt ': s)
  AnnEQ
    :: UnaryArithOp Eq' n
    => AnnVar
    -> Instr (n ': s) (UnaryArithRes Eq' n ': s)
  AnnNEQ
    :: UnaryArithOp Neq n
    => AnnVar
    -> Instr (n ': s) (UnaryArithRes Neq n ': s)
  AnnLT
    :: UnaryArithOp Lt n
    => AnnVar
    -> Instr (n ': s) (UnaryArithRes Lt n ': s)
  AnnGT
    :: UnaryArithOp Gt n
    => AnnVar
    -> Instr (n ': s) (UnaryArithRes Gt n ': s)
  AnnLE
    :: UnaryArithOp Le n
    => AnnVar
    -> Instr (n ': s) (UnaryArithRes Le n ': s)
  AnnGE
    :: UnaryArithOp Ge n
    => AnnVar
    -> Instr (n ': s) (UnaryArithRes Ge n ': s)
  AnnINT
    :: ToIntArithOp n
    => AnnVar
    -> Instr (n ': s) ('TInt ': s)
  AnnBYTES
    :: ToBytesArithOp n
    => AnnVar
    -> Instr (n ': s) ('TBytes ': s)
  AnnNAT
    :: AnnVar
    -> Instr ('TBytes ': s) ('TNat ': s)
  AnnVIEW
       -- Here really only the return type is constrained
       -- because it is given explicitly
    :: (SingI arg, ViewableScope ret)
    => Anns '[VarAnn, Notes ret]
    -> ViewName
    -> Instr (arg ': 'TAddress ': s) ('TOption ret ': s)
  -- | Note that the field annotation on @SELF@ is stored as the second
  -- parameter to 'AnnSELF', because it's not as much an annotation
  -- as an entrypoint specification.
  AnnSELF
    :: forall (arg :: T) s .
       (ParameterScope arg, IsNotInView)
    => AnnVar
    -> SomeEntrypointCallT arg
    -> Instr s ('TContract arg ': s)
  -- | Note that the field annotation on @CONTRACT@ is stored as the second
  -- parameter to 'AnnCONTRACT', because it's not as much an annotation
  -- as an entrypoint specification.
  AnnCONTRACT
    :: (ParameterScope p)
    => Anns '[VarAnn, Notes p]
    -> EpName
    -> Instr ('TAddress ': s) ('TOption ('TContract p) ': s)
  AnnTRANSFER_TOKENS
    :: (ParameterScope p, IsNotInView)
    => AnnVar
    -> Instr (p ': 'TMutez ': 'TContract p ': s) ('TOperation ': s)
  AnnSET_DELEGATE
    :: IsNotInView
    => AnnVar
    -> Instr ('TOption 'TKeyHash ': s) ('TOperation ': s)

  AnnCREATE_CONTRACT
    :: (ParameterScope p, StorageScope g, IsNotInView)
    => Anns '[VarAnn, VarAnn]
    -> Contract' Instr p g
    -> Instr ('TOption 'TKeyHash ':
              'TMutez ':
               g ': s)
             ('TOperation ': 'TAddress ': s)
  AnnIMPLICIT_ACCOUNT
    :: AnnVar
    -> Instr ('TKeyHash ': s) ('TContract 'TUnit ': s)
  AnnNOW :: AnnVar -> Instr s ('TTimestamp ': s)
  AnnAMOUNT :: AnnVar -> Instr s ('TMutez ': s)
  AnnBALANCE :: AnnVar -> Instr s ('TMutez ': s)
  AnnVOTING_POWER :: AnnVar -> Instr ('TKeyHash ': s) ('TNat ': s)
  AnnTOTAL_VOTING_POWER :: AnnVar -> Instr s ('TNat ': s)
  AnnCHECK_SIGNATURE
    :: AnnVar
    -> Instr ('TKey ': 'TSignature ': 'TBytes ': s) ('TBool ': s)
  AnnSHA256 :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
  AnnSHA512 :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
  AnnBLAKE2B :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
  AnnSHA3 :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
  AnnKECCAK :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
  AnnHASH_KEY :: AnnVar -> Instr ('TKey ': s) ('TKeyHash ': s)
  AnnPAIRING_CHECK
    :: AnnVar
    -> Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) ': s) ('TBool ': s)
  AnnSOURCE :: AnnVar -> Instr s ('TAddress ': s)
  AnnSENDER :: AnnVar -> Instr s ('TAddress ': s)
  AnnADDRESS :: AnnVar -> Instr ('TContract a ': s) ('TAddress ': s)
  AnnCHAIN_ID :: AnnVar -> Instr s ('TChainId ': s)
  AnnLEVEL :: AnnVar -> Instr s ('TNat ': s)
  AnnSELF_ADDRESS :: AnnVar -> Instr s ('TAddress ': s)
  NEVER :: Instr ('TNever ': s) t
  AnnTICKET_DEPRECATED
    :: Comparable a
    => AnnVar
    -> Instr (a ': 'TNat ': s) ('TTicket a ': s)
  AnnTICKET
    :: Comparable a
    => AnnVar
    -> Instr (a ': 'TNat ': s) ('TOption ('TTicket a) ': s)
  AnnREAD_TICKET
    :: AnnVar
    -> Instr ('TTicket a ': s) (RightComb ['TAddress, a, 'TNat] ': 'TTicket a ': s)
  AnnSPLIT_TICKET
    :: AnnVar
    -> Instr ('TTicket a ': 'TPair 'TNat 'TNat ': s)
             ('TOption ('TPair ('TTicket a) ('TTicket a)) ': s)
  AnnJOIN_TICKETS
    :: AnnVar
    -> Instr ('TPair ('TTicket a) ('TTicket a) ': s)
             ('TOption ('TTicket a) ': s)
  AnnOPEN_CHEST
    :: AnnVar
    -> Instr ('TChestKey ': 'TChest ': 'TNat ': s)
             ('TOr 'TBytes 'TBool ': s)
  AnnSAPLING_EMPTY_STATE
    :: AnnVar
    -> Sing n
    -> Instr s
             ('TSaplingState n ': s)
  AnnSAPLING_VERIFY_UPDATE
    :: AnnVar
    -> Instr ('TSaplingTransaction n : 'TSaplingState n ': s)
             ('TOption ('TPair 'TBytes ('TPair 'TInt ('TSaplingState n))) ': s)
  AnnMIN_BLOCK_TIME :: [AnyAnn] -> Instr s ('TNat ': s)
  AnnEMIT
    :: PackedValScope t
    => AnnVar
    -> FieldAnn
    -> Maybe (Notes t)
    -> Instr (t ': s) ('TOperation : s)
  -- NB: In EMIT we need to differentiate between "has no type annotation" and
  -- "has type annotation, but it doesn't have any additional annotations on
  -- it", because these cases are represented and interpreted differently. We
  -- also don't want FieldAnn to be hidden, as it has semantic meaning.

castInstr
  :: forall inp1 out1 inp2 out2.
  ( SingI inp1
  , SingI out1
  , SingI inp2
  , SingI out2
  )
  => Instr inp1 out1 -> Maybe (Instr inp2 out2)
castInstr :: forall (inp1 :: [T]) (out1 :: [T]) (inp2 :: [T]) (out2 :: [T]).
(SingI inp1, SingI out1, SingI inp2, SingI out2) =>
Instr inp1 out1 -> Maybe (Instr inp2 out2)
castInstr Instr inp1 out1
instr =
  case (forall (a :: [T]) (b :: [T]).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @inp1 @inp2, forall (a :: [T]) (b :: [T]).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @out1 @out2) of
    (Just inp1 :~: inp2
Refl, Just out1 :~: out2
Refl) -> Instr inp2 out2 -> Maybe (Instr inp2 out2)
forall a. a -> Maybe a
Just Instr inp1 out1
Instr inp2 out2
instr
    (Maybe (inp1 :~: inp2)
_,Maybe (out1 :~: out2)
_) -> Maybe (Instr inp2 out2)
forall a. Maybe a
Nothing

-- | Right-associative operator for v'Seq'.
--
-- >>> Debug.show (DROP :# UNIT :# Nop) == Debug.show (DROP :# (UNIT :# Nop))
-- True
pattern (:#) :: Instr a b -> Instr b c -> Instr a c
pattern a $m:# :: forall {r} {a :: [T]} {c :: [T]}.
Instr a c
-> (forall {b :: [T]}. Instr a b -> Instr b c -> r)
-> ((# #) -> r)
-> r
$b:# :: forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# b = Seq a b
infixr 8 :#

deriving stock instance Show (Instr inp out)

instance Semigroup (Instr s s) where
  <> :: Instr s s -> Instr s s -> Instr s s
(<>) = Instr s s -> Instr s s -> Instr s s
forall (a :: [T]) (a :: [T]) (c :: [T]).
Instr a a -> Instr a c -> Instr a c
Seq
instance Monoid (Instr s s) where
  mempty :: Instr s s
mempty = Instr s s
forall (s :: [T]). Instr s s
Nop

data TestAssert (s :: [T]) where
  TestAssert
    :: Text
    -> PrintComment inp
    -> Instr inp ('TBool ': out)
    -> TestAssert inp

deriving stock instance Show (TestAssert s)

-- | A reference into the stack of a given type.
data StackRef (st :: [T]) where
  -- | Keeps 0-based index to a stack element counting from the top.
  StackRef
    :: RequireLongerThan st idx
    => PeanoNatural idx -> StackRef st

instance NFData (StackRef st) where
  rnf :: StackRef st -> ()
rnf (StackRef PeanoNatural idx
s) = PeanoNatural idx -> ()
forall a. NFData a => a -> ()
rnf PeanoNatural idx
s

instance Eq (StackRef st) where
  StackRef PeanoNatural idx
snat1 == :: StackRef st -> StackRef st -> Bool
== StackRef PeanoNatural idx
snat2 = PeanoNatural idx -> Nat
forall (n :: Peano). PeanoNatural n -> Nat
fromPeanoNatural PeanoNatural idx
snat1 Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== PeanoNatural idx -> Nat
forall (n :: Peano). PeanoNatural n -> Nat
fromPeanoNatural PeanoNatural idx
snat2

instance Show (StackRef st) where
  showsPrec :: Int -> StackRef st -> ShowS
showsPrec Int
d (StackRef PeanoNatural idx
snat) = Bool -> ShowS -> ShowS
T.showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
app_prec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
T.showString String
"StackRef " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Bool -> ShowS -> ShowS
T.showParen Bool
True (String -> ShowS
T.showString String
"toPeanoNatural' @" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> ShowS
forall a. Show a => a -> ShowS
T.shows (PeanoNatural idx -> Nat
forall (n :: Peano). PeanoNatural n -> Nat
fromPeanoNatural PeanoNatural idx
snat))
    where
      app_prec :: Int
app_prec = Int
10

instance Buildable (StackRef st) where
  build :: StackRef st -> Doc
build (StackRef PeanoNatural idx
snat) = Doc
"StackRef {" Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| PeanoNatural idx -> Nat
forall (n :: Peano). PeanoNatural n -> Nat
fromPeanoNatural PeanoNatural idx
snat Nat -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
"}"

-- | Create a stack reference, performing checks at compile time.
mkStackRef
  :: forall (gn :: Nat) st n.
      (n ~ ToPeano gn, SingIPeano gn, RequireLongerThan st n)
  => StackRef st
mkStackRef :: forall (gn :: Nat) (st :: [T]) (n :: Peano).
(n ~ ToPeano gn, SingIPeano gn, RequireLongerThan st n) =>
StackRef st
mkStackRef = PeanoNatural (ToPeano gn) -> StackRef st
forall (st :: [T]) (a :: Peano).
RequireLongerThan st a =>
PeanoNatural a -> StackRef st
StackRef (PeanoNatural (ToPeano gn) -> StackRef st)
-> PeanoNatural (ToPeano gn) -> StackRef st
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SingIPeano n => PeanoNatural (ToPeano n)
toPeanoNatural' @gn

-- | A print format with references into the stack
newtype PrintComment (st :: [T]) = PrintComment
  { forall (st :: [T]). PrintComment st -> [Either Text (StackRef st)]
unPrintComment :: [Either Text (StackRef st)]
  } deriving stock (PrintComment st -> PrintComment st -> Bool
(PrintComment st -> PrintComment st -> Bool)
-> (PrintComment st -> PrintComment st -> Bool)
-> Eq (PrintComment st)
forall (st :: [T]). PrintComment st -> PrintComment st -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (st :: [T]). PrintComment st -> PrintComment st -> Bool
== :: PrintComment st -> PrintComment st -> Bool
$c/= :: forall (st :: [T]). PrintComment st -> PrintComment st -> Bool
/= :: PrintComment st -> PrintComment st -> Bool
Eq, Int -> PrintComment st -> ShowS
[PrintComment st] -> ShowS
PrintComment st -> String
(Int -> PrintComment st -> ShowS)
-> (PrintComment st -> String)
-> ([PrintComment st] -> ShowS)
-> Show (PrintComment st)
forall (st :: [T]). Int -> PrintComment st -> ShowS
forall (st :: [T]). [PrintComment st] -> ShowS
forall (st :: [T]). PrintComment st -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (st :: [T]). Int -> PrintComment st -> ShowS
showsPrec :: Int -> PrintComment st -> ShowS
$cshow :: forall (st :: [T]). PrintComment st -> String
show :: PrintComment st -> String
$cshowList :: forall (st :: [T]). [PrintComment st] -> ShowS
showList :: [PrintComment st] -> ShowS
Show, (forall x. PrintComment st -> Rep (PrintComment st) x)
-> (forall x. Rep (PrintComment st) x -> PrintComment st)
-> Generic (PrintComment st)
forall (st :: [T]) x. Rep (PrintComment st) x -> PrintComment st
forall (st :: [T]) x. PrintComment st -> Rep (PrintComment st) x
forall x. Rep (PrintComment st) x -> PrintComment st
forall x. PrintComment st -> Rep (PrintComment st) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (st :: [T]) x. PrintComment st -> Rep (PrintComment st) x
from :: forall x. PrintComment st -> Rep (PrintComment st) x
$cto :: forall (st :: [T]) x. Rep (PrintComment st) x -> PrintComment st
to :: forall x. Rep (PrintComment st) x -> PrintComment st
Generic)
    deriving newtype (NonEmpty (PrintComment st) -> PrintComment st
PrintComment st -> PrintComment st -> PrintComment st
(PrintComment st -> PrintComment st -> PrintComment st)
-> (NonEmpty (PrintComment st) -> PrintComment st)
-> (forall b.
    Integral b =>
    b -> PrintComment st -> PrintComment st)
-> Semigroup (PrintComment st)
forall (st :: [T]). NonEmpty (PrintComment st) -> PrintComment st
forall (st :: [T]).
PrintComment st -> PrintComment st -> PrintComment st
forall (st :: [T]) b.
Integral b =>
b -> PrintComment st -> PrintComment st
forall b. Integral b => b -> PrintComment st -> PrintComment st
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: forall (st :: [T]).
PrintComment st -> PrintComment st -> PrintComment st
<> :: PrintComment st -> PrintComment st -> PrintComment st
$csconcat :: forall (st :: [T]). NonEmpty (PrintComment st) -> PrintComment st
sconcat :: NonEmpty (PrintComment st) -> PrintComment st
$cstimes :: forall (st :: [T]) b.
Integral b =>
b -> PrintComment st -> PrintComment st
stimes :: forall b. Integral b => b -> PrintComment st -> PrintComment st
Semigroup, Semigroup (PrintComment st)
PrintComment st
Semigroup (PrintComment st)
-> PrintComment st
-> (PrintComment st -> PrintComment st -> PrintComment st)
-> ([PrintComment st] -> PrintComment st)
-> Monoid (PrintComment st)
[PrintComment st] -> PrintComment st
PrintComment st -> PrintComment st -> PrintComment st
forall (st :: [T]). Semigroup (PrintComment st)
forall (st :: [T]). PrintComment st
forall (st :: [T]). [PrintComment st] -> PrintComment st
forall (st :: [T]).
PrintComment st -> PrintComment st -> PrintComment st
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: forall (st :: [T]). PrintComment st
mempty :: PrintComment st
$cmappend :: forall (st :: [T]).
PrintComment st -> PrintComment st -> PrintComment st
mappend :: PrintComment st -> PrintComment st -> PrintComment st
$cmconcat :: forall (st :: [T]). [PrintComment st] -> PrintComment st
mconcat :: [PrintComment st] -> PrintComment st
Monoid)

instance NFData (PrintComment st)

instance IsString (PrintComment st) where
  fromString :: String -> PrintComment st
fromString = [Either Text (StackRef st)] -> PrintComment st
forall (st :: [T]). [Either Text (StackRef st)] -> PrintComment st
PrintComment ([Either Text (StackRef st)] -> PrintComment st)
-> (String -> [Either Text (StackRef st)])
-> String
-> PrintComment st
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Text (StackRef st) -> [Either Text (StackRef st)]
OneItem [Either Text (StackRef st)] -> [Either Text (StackRef st)]
forall x. One x => OneItem x -> x
one (Either Text (StackRef st) -> [Either Text (StackRef st)])
-> (String -> Either Text (StackRef st))
-> String
-> [Either Text (StackRef st)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either Text (StackRef st)
forall a b. a -> Either a b
Left (Text -> Either Text (StackRef st))
-> (String -> Text) -> String -> Either Text (StackRef st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
forall a. IsString a => String -> a
fromString

data CommentType
 = FunctionStarts Text
 | FunctionEnds Text
 | StatementStarts Text
 | StatementEnds Text
 | JustComment Text
 | StackTypeComment (Maybe [T]) -- ^ 'Nothing' for any stack type
 deriving stock (Int -> CommentType -> ShowS
[CommentType] -> ShowS
CommentType -> String
(Int -> CommentType -> ShowS)
-> (CommentType -> String)
-> ([CommentType] -> ShowS)
-> Show CommentType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CommentType -> ShowS
showsPrec :: Int -> CommentType -> ShowS
$cshow :: CommentType -> String
show :: CommentType -> String
$cshowList :: [CommentType] -> ShowS
showList :: [CommentType] -> ShowS
Show, (forall x. CommentType -> Rep CommentType x)
-> (forall x. Rep CommentType x -> CommentType)
-> Generic CommentType
forall x. Rep CommentType x -> CommentType
forall x. CommentType -> Rep CommentType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CommentType -> Rep CommentType x
from :: forall x. CommentType -> Rep CommentType x
$cto :: forall x. Rep CommentType x -> CommentType
to :: forall x. Rep CommentType x -> CommentType
Generic)

instance NFData CommentType

instance IsString CommentType where
  fromString :: String -> CommentType
fromString = Text -> CommentType
JustComment (Text -> CommentType) -> (String -> Text) -> String -> CommentType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
forall a. IsString a => String -> a
fromString

data ExtInstr s
  = TEST_ASSERT (TestAssert s)
  | PRINT (PrintComment s)
  -- TODO [#689]: Use `Meta` instead of `DOC_ITEM`.
  | DOC_ITEM SomeDocItem
  | COMMENT_ITEM CommentType
  | STACKTYPE StackTypePattern
  deriving stock (Int -> ExtInstr s -> ShowS
[ExtInstr s] -> ShowS
ExtInstr s -> String
(Int -> ExtInstr s -> ShowS)
-> (ExtInstr s -> String)
-> ([ExtInstr s] -> ShowS)
-> Show (ExtInstr s)
forall (s :: [T]). Int -> ExtInstr s -> ShowS
forall (s :: [T]). [ExtInstr s] -> ShowS
forall (s :: [T]). ExtInstr s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (s :: [T]). Int -> ExtInstr s -> ShowS
showsPrec :: Int -> ExtInstr s -> ShowS
$cshow :: forall (s :: [T]). ExtInstr s -> String
show :: ExtInstr s -> String
$cshowList :: forall (s :: [T]). [ExtInstr s] -> ShowS
showList :: [ExtInstr s] -> ShowS
Show, (forall x. ExtInstr s -> Rep (ExtInstr s) x)
-> (forall x. Rep (ExtInstr s) x -> ExtInstr s)
-> Generic (ExtInstr s)
forall (s :: [T]) x. Rep (ExtInstr s) x -> ExtInstr s
forall (s :: [T]) x. ExtInstr s -> Rep (ExtInstr s) x
forall x. Rep (ExtInstr s) x -> ExtInstr s
forall x. ExtInstr s -> Rep (ExtInstr s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (s :: [T]) x. ExtInstr s -> Rep (ExtInstr s) x
from :: forall x. ExtInstr s -> Rep (ExtInstr s) x
$cto :: forall (s :: [T]) x. Rep (ExtInstr s) x -> ExtInstr s
to :: forall x. Rep (ExtInstr s) x -> ExtInstr s
Generic)

data SomeMeta where
  SomeMeta
    :: forall meta
     . With [NFData, Show, Typeable] meta
    => meta
    -> SomeMeta

instance NFData SomeMeta where
  rnf :: SomeMeta -> ()
rnf (SomeMeta meta
meta) = meta -> ()
forall a. NFData a => a -> ()
rnf meta
meta

deriving stock instance Show SomeMeta

-- | A convenience pattern synonym for v'Meta',
-- matching on a concrete given type wrapped by @SomeMeta@, e.g.
--
-- > \case { ContreteMeta (x :: Word) -> ... }
pattern ConcreteMeta :: Typeable meta => meta -> Instr i o -> Instr i o
pattern $mConcreteMeta :: forall {r} {meta} {i :: [T]} {o :: [T]}.
Typeable meta =>
Instr i o -> (meta -> Instr i o -> r) -> ((# #) -> r) -> r
ConcreteMeta meta instr <- Meta (SomeMeta (cast -> Just meta)) instr

pattern LAMBDA
  :: forall s r . ()
  => forall i o. (SingI i, SingI o, r ~ ('TLambda i o ': s))
  => (IsNotInView => RemFail Instr '[i] '[o])
  -> Instr s r
pattern $mLAMBDA :: forall {r} {s :: [T]} {r :: [T]}.
Instr s r
-> (forall {i :: T} {o :: T}.
    (SingI i, SingI o, r ~ ('TLambda i o : s)) =>
    (IsNotInView => RemFail Instr '[i] '[o]) -> r)
-> ((# #) -> r)
-> r
$bLAMBDA :: forall (s :: [T]) (r :: [T]) (i :: T) (o :: T).
(SingI i, SingI o, r ~ ('TLambda i o : s)) =>
(IsNotInView => RemFail Instr '[i] '[o]) -> Instr s r
LAMBDA code <- AnnLAMBDA _ code
  where LAMBDA IsNotInView => RemFail Instr '[i] '[o]
code = Anns '[VarAnn, Notes i, Notes o]
-> RemFail Instr '[i] '[o] -> Instr s ('TLambda i o : s)
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b) =>
Anns '[VarAnn, Notes a, Notes b]
-> RemFail Instr '[a] '[b] -> Instr s ('TLambda a b : s)
AnnLAMBDA Anns '[VarAnn, Notes i, Notes o]
forall a. Default a => a
def (RemFail Instr '[i] '[o] -> Instr s ('TLambda i o : s))
-> RemFail Instr '[i] '[o] -> Instr s ('TLambda i o : s)
forall a b. (a -> b) -> a -> b
$ (IsNotInView => RemFail Instr '[i] '[o]) -> RemFail Instr '[i] '[o]
forall r. (IsNotInView => r) -> r
giveNotInView RemFail Instr '[i] '[o]
IsNotInView => RemFail Instr '[i] '[o]
code

pattern LAMBDA_REC
  :: forall s r . ()
  => forall i o. (SingI i, SingI o, r ~ ('TLambda i o ': s))
  => (IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o])
  -> Instr s r
pattern $mLAMBDA_REC :: forall {r} {s :: [T]} {r :: [T]}.
Instr s r
-> (forall {i :: T} {o :: T}.
    (SingI i, SingI o, r ~ ('TLambda i o : s)) =>
    (IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o]) -> r)
-> ((# #) -> r)
-> r
$bLAMBDA_REC :: 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 code <- AnnLAMBDA_REC _ code
  where LAMBDA_REC IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o]
code = Anns '[VarAnn, Notes i, Notes o]
-> RemFail Instr '[i, 'TLambda i o] '[o]
-> Instr s ('TLambda i o : s)
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b) =>
Anns '[VarAnn, Notes a, Notes b]
-> RemFail Instr '[a, 'TLambda a b] '[b]
-> Instr s ('TLambda a b : s)
AnnLAMBDA_REC Anns '[VarAnn, Notes i, Notes o]
forall a. Default a => a
def (RemFail Instr '[i, 'TLambda i o] '[o]
 -> Instr s ('TLambda i o : s))
-> RemFail Instr '[i, 'TLambda i o] '[o]
-> Instr s ('TLambda i o : s)
forall a b. (a -> b) -> a -> b
$ (IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o])
-> RemFail Instr '[i, 'TLambda i o] '[o]
forall r. (IsNotInView => r) -> r
giveNotInView RemFail Instr '[i, 'TLambda i o] '[o]
IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o]
code

-- | Execute given instruction on truncated stack.
--
-- This is sound because for all Michelson instructions the following property
-- holds: if some code accepts stack @i@ and produces stack @o@, when it can
-- also be run on stack @i + s@ producing stack @o + s@; and also because
-- Michelson never makes implicit assumptions on types, rather you have to
-- express all "yet ambiguous" type information in code.
--
-- The complexity of this operation is linear in the number of instructions. If
-- possible, avoid nested uses as that would imply multiple traversals. Worst
-- case, complexity can become quadratic.
frameInstr :: forall s a b. Instr a b -> Instr (a ++ s) (b ++ s)
frameInstr :: forall (s :: [T]) (a :: [T]) (b :: [T]).
Instr a b -> Instr (a ++ s) (b ++ s)
frameInstr = \case
  Seq Instr a b
i1 Instr b b
i2 -> Instr (a ++ s) (b ++ s)
-> Instr (b ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall (a :: [T]) (a :: [T]) (c :: [T]).
Instr a a -> Instr a c -> Instr a c
Seq (Instr a b -> Instr (a ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr a b
i1) (Instr b b -> Instr (b ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr b b
i2)
  WithLoc ErrorSrcPos
loc Instr a b
instr -> ErrorSrcPos -> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall (a :: [T]) (b :: [T]). ErrorSrcPos -> Instr a b -> Instr a b
WithLoc ErrorSrcPos
loc (Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s))
-> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall a b. (a -> b) -> a -> b
$ Instr a b -> Instr (a ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr a b
instr
  Meta SomeMeta
m Instr a b
instr -> SomeMeta -> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall (a :: [T]) (b :: [T]). SomeMeta -> Instr a b -> Instr a b
Meta SomeMeta
m (Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s))
-> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall a b. (a -> b) -> a -> b
$ Instr a b -> Instr (a ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr a b
instr
  Nested Instr a b
i1 -> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
Nested (Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s))
-> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall a b. (a -> b) -> a -> b
$ Instr a b -> Instr (a ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr a b
i1
  DocGroup DocGrouping
dg Instr a b
i1 -> DocGrouping -> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall (inp :: [T]) (out :: [T]).
DocGrouping -> Instr inp out -> Instr inp out
DocGroup DocGrouping
dg (Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s))
-> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall a b. (a -> b) -> a -> b
$ Instr a b -> Instr (a ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr a b
i1
  IF_NONE Instr s b
i1 Instr (a : s) b
i2 -> Instr (s ++ s) (b ++ s)
-> Instr (a : (s ++ s)) (b ++ s)
-> Instr ('TOption a : (s ++ s)) (b ++ s)
forall (a :: [T]) (s' :: [T]) (b :: T).
Instr a s' -> Instr (b : a) s' -> Instr ('TOption b : a) s'
IF_NONE (Instr s b -> Instr (s ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr s b
i1) (Instr (a : s) b -> Instr ((a : s) ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr (a : s) b
i2)
  IF_LEFT Instr (a : s) b
i1 Instr (b : s) b
i2 -> Instr (a : (s ++ s)) (b ++ s)
-> Instr (b : (s ++ s)) (b ++ s)
-> Instr ('TOr a b : (s ++ s)) (b ++ s)
forall (a :: T) (b :: [T]) (s' :: [T]) (s :: T).
Instr (a : b) s' -> Instr (s : b) s' -> Instr ('TOr a s : b) s'
IF_LEFT (Instr (a : s) b -> Instr ((a : s) ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr (a : s) b
i1) (Instr (b : s) b -> Instr ((b : s) ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr (b : s) b
i2)
  IF_CONS Instr (a : 'TList a : s) b
i1 Instr s b
i2 -> Instr (a : 'TList a : (s ++ s)) (b ++ s)
-> Instr (s ++ s) (b ++ s) -> Instr ('TList a : (s ++ s)) (b ++ s)
forall (a :: T) (b :: [T]) (s' :: [T]).
Instr (a : 'TList a : b) s'
-> Instr b s' -> Instr ('TList a : b) s'
IF_CONS (Instr (a : 'TList a : s) b
-> Instr ((a : 'TList a : s) ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr (a : 'TList a : s) b
i1) (Instr s b -> Instr (s ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr s b
i2)
  IF Instr s b
i1 Instr s b
i2 -> Instr (s ++ s) (b ++ s)
-> Instr (s ++ s) (b ++ s) -> Instr ('TBool : (s ++ s)) (b ++ s)
forall (a :: [T]) (s' :: [T]).
Instr a s' -> Instr a s' -> Instr ('TBool : a) s'
IF (Instr s b -> Instr (s ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr s b
i1) (Instr s b -> Instr (s ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr s b
i2)
  AnnMAP AnnVar
ann Instr (MapOpInp c : s) (b : s)
i1 -> AnnVar
-> Instr (MapOpInp c : (s ++ s)) (b : (s ++ s))
-> Instr (c : (s ++ s)) (MapOpRes c b : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
(MapOp a, SingI b) =>
AnnVar
-> Instr (MapOpInp a : s) (b : s)
-> Instr (a : s) (MapOpRes a b : s)
AnnMAP AnnVar
ann (Instr (MapOpInp c : (s ++ s)) (b : (s ++ s))
 -> Instr (c : (s ++ s)) (MapOpRes c b : (s ++ s)))
-> Instr (MapOpInp c : (s ++ s)) (b : (s ++ s))
-> Instr (c : (s ++ s)) (MapOpRes c b : (s ++ s))
forall a b. (a -> b) -> a -> b
$ Instr (MapOpInp c : s) (b : s)
-> Instr ((MapOpInp c : s) ++ s) ((b : s) ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr (MapOpInp c : s) (b : s)
i1
  ITER Instr (IterOpEl c : b) b
i1 -> Instr (IterOpEl c : (b ++ s)) (b ++ s)
-> Instr (c : (b ++ s)) (b ++ s)
forall (a :: T) (s :: [T]).
IterOp a =>
Instr (IterOpEl a : s) s -> Instr (a : s) s
ITER (Instr (IterOpEl c : (b ++ s)) (b ++ s)
 -> Instr (c : (b ++ s)) (b ++ s))
-> Instr (IterOpEl c : (b ++ s)) (b ++ s)
-> Instr (c : (b ++ s)) (b ++ s)
forall a b. (a -> b) -> a -> b
$ Instr (IterOpEl c : b) b -> Instr ((IterOpEl c : b) ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr (IterOpEl c : b) b
i1
  LOOP Instr b ('TBool : b)
i1 -> Instr (b ++ s) ('TBool : (b ++ s))
-> Instr ('TBool : (b ++ s)) (b ++ s)
forall (s :: [T]). Instr s ('TBool : s) -> Instr ('TBool : s) s
LOOP (Instr (b ++ s) ('TBool : (b ++ s))
 -> Instr ('TBool : (b ++ s)) (b ++ s))
-> Instr (b ++ s) ('TBool : (b ++ s))
-> Instr ('TBool : (b ++ s)) (b ++ s)
forall a b. (a -> b) -> a -> b
$ Instr b ('TBool : b) -> Instr (b ++ s) (('TBool : b) ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr b ('TBool : b)
i1
  LOOP_LEFT Instr (a : s) ('TOr a b : s)
i1 -> Instr (a : (s ++ s)) ('TOr a b : (s ++ s))
-> Instr ('TOr a b : (s ++ s)) (b : (s ++ s))
forall (a :: T) (b :: [T]) (s :: T).
Instr (a : b) ('TOr a s : b) -> Instr ('TOr a s : b) (s : b)
LOOP_LEFT (Instr (a : (s ++ s)) ('TOr a b : (s ++ s))
 -> Instr ('TOr a b : (s ++ s)) (b : (s ++ s)))
-> Instr (a : (s ++ s)) ('TOr a b : (s ++ s))
-> Instr ('TOr a b : (s ++ s)) (b : (s ++ s))
forall a b. (a -> b) -> a -> b
$ Instr (a : s) ('TOr a b : s)
-> Instr ((a : s) ++ s) (('TOr a b : s) ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr (a : s) ('TOr a b : s)
i1
  DIP Instr a c
i1 -> Instr (a ++ s) (c ++ s) -> Instr (b : (a ++ s)) (b : (c ++ s))
forall (a :: [T]) (b :: [T]) (s :: T).
Instr a b -> Instr (s : a) (s : b)
DIP (Instr (a ++ s) (c ++ s) -> Instr (b : (a ++ s)) (b : (c ++ s)))
-> Instr (a ++ s) (c ++ s) -> Instr (b : (a ++ s)) (b : (c ++ s))
forall a b. (a -> b) -> a -> b
$ Instr a c -> Instr (a ++ s) (c ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr a c
i1
  DIPN PeanoNatural n
n (Instr s s'
i1 :: Instr s1 s1') -> PeanoNatural n
-> Instr (Drop n (a ++ s)) (Drop n (b ++ s))
-> Instr (a ++ s) (b ++ s)
forall (a :: Peano) (inp :: [T]) (out :: [T]) (b :: [T])
       (s :: [T]).
ConstraintDIPN a inp out b s =>
PeanoNatural a -> Instr b s -> Instr inp out
DIPN PeanoNatural n
n (Instr s s' -> Instr (s ++ s) (s' ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr s s'
i1) ((RequireLongerOrSameLength (a ++ s) n,
  (LazyTake n (a ++ s) ++ (s ++ s)) ~ (a ++ s),
  (LazyTake n (a ++ s) ++ (s' ++ s)) ~ (b ++ s),
  (s ++ s) ~ Drop n (a ++ s), (s' ++ s) ~ Drop n (b ++ s)) =>
 Instr (a ++ s) (b ++ s))
-> Dict
     (RequireLongerOrSameLength (a ++ s) n,
      (LazyTake n (a ++ s) ++ (s ++ s)) ~ (a ++ s),
      (LazyTake n (a ++ s) ++ (s' ++ s)) ~ (b ++ s),
      (s ++ s) ~ Drop n (a ++ s), (s' ++ s) ~ Drop n (b ++ s))
-> Instr (a ++ s) (b ++ s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [T]) (a :: [T]) (b :: [T]) (s1 :: [T]) (s1' :: [T])
       (n :: Peano).
ConstraintDIPN n a b s1 s1' =>
PeanoNatural n
-> Dict (ConstraintDIPN n (a ++ s) (b ++ s) (s1 ++ s) (s1' ++ s))
dipNExtensionThm @s @a @b @s1 @s1' PeanoNatural n
n
  AnnPUSH Anns '[VarAnn, Notes t]
ann Value' Instr t
v -> Anns '[VarAnn, Notes t]
-> Value' Instr t -> Instr (a ++ s) (t : (a ++ s))
forall (a :: T) (s :: [T]).
ConstantScope a =>
Anns '[VarAnn, Notes a] -> Value' Instr a -> Instr s (a : s)
AnnPUSH Anns '[VarAnn, Notes t]
ann Value' Instr t
v
  AnnLAMBDA Anns '[VarAnn, Notes i, Notes o]
ann RemFail Instr '[i] '[o]
lam -> Anns '[VarAnn, Notes i, Notes o]
-> RemFail Instr '[i] '[o]
-> Instr (a ++ s) ('TLambda i o : (a ++ s))
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b) =>
Anns '[VarAnn, Notes a, Notes b]
-> RemFail Instr '[a] '[b] -> Instr s ('TLambda a b : s)
AnnLAMBDA Anns '[VarAnn, Notes i, Notes o]
ann RemFail Instr '[i] '[o]
lam
  AnnLAMBDA_REC Anns '[VarAnn, Notes i, Notes o]
ann RemFail Instr '[i, 'TLambda i o] '[o]
lam -> Anns '[VarAnn, Notes i, Notes o]
-> RemFail Instr '[i, 'TLambda i o] '[o]
-> Instr (a ++ s) ('TLambda i o : (a ++ s))
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b) =>
Anns '[VarAnn, Notes a, Notes b]
-> RemFail Instr '[a, 'TLambda a b] '[b]
-> Instr s ('TLambda a b : s)
AnnLAMBDA_REC Anns '[VarAnn, Notes i, Notes o]
ann RemFail Instr '[i, 'TLambda i o] '[o]
lam
  AnnCREATE_CONTRACT Anns '[VarAnn, VarAnn]
ann Contract' Instr p g
contract -> Anns '[VarAnn, VarAnn]
-> Contract' Instr p g
-> Instr
     ('TOption 'TKeyHash : 'TMutez : g : (s ++ s))
     ('TOperation : 'TAddress : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
(ParameterScope a, StorageScope b, IsNotInView) =>
Anns '[VarAnn, VarAnn]
-> Contract' Instr a b
-> Instr
     ('TOption 'TKeyHash : 'TMutez : b : s)
     ('TOperation : 'TAddress : s)
AnnCREATE_CONTRACT Anns '[VarAnn, VarAnn]
ann Contract' Instr p g
contract
  Instr a b
Nop -> Instr (a ++ s) (a ++ s)
Instr (a ++ s) (b ++ s)
forall (s :: [T]). Instr s s
Nop
  Ext (TEST_ASSERT (TestAssert Text
t PrintComment a
c Instr a ('TBool : out)
i)) -> ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s)
forall (s :: [T]). ExtInstr s -> Instr s s
Ext (ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s))
-> ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s)
forall a b. (a -> b) -> a -> b
$ TestAssert (a ++ s) -> ExtInstr (a ++ s)
forall (s :: [T]). TestAssert s -> ExtInstr s
TEST_ASSERT (TestAssert (a ++ s) -> ExtInstr (a ++ s))
-> TestAssert (a ++ s) -> ExtInstr (a ++ s)
forall a b. (a -> b) -> a -> b
$ Text
-> PrintComment (a ++ s)
-> Instr (a ++ s) ('TBool : (out ++ s))
-> TestAssert (a ++ s)
forall (inp :: [T]) (a :: [T]).
Text
-> PrintComment inp -> Instr inp ('TBool : a) -> TestAssert inp
TestAssert Text
t (PrintComment a -> PrintComment (a ++ s)
comment PrintComment a
c) (Instr a ('TBool : out) -> Instr (a ++ s) (('TBool : out) ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr a ('TBool : out)
i)
  Ext (PRINT PrintComment a
x) -> ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s)
forall (s :: [T]). ExtInstr s -> Instr s s
Ext (ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s))
-> ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s)
forall a b. (a -> b) -> a -> b
$ PrintComment (a ++ s) -> ExtInstr (a ++ s)
forall (s :: [T]). PrintComment s -> ExtInstr s
PRINT (PrintComment (a ++ s) -> ExtInstr (a ++ s))
-> PrintComment (a ++ s) -> ExtInstr (a ++ s)
forall a b. (a -> b) -> a -> b
$ PrintComment a -> PrintComment (a ++ s)
comment PrintComment a
x
  Ext (DOC_ITEM SomeDocItem
x) -> ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s)
forall (s :: [T]). ExtInstr s -> Instr s s
Ext (SomeDocItem -> ExtInstr (a ++ s)
forall (s :: [T]). SomeDocItem -> ExtInstr s
DOC_ITEM SomeDocItem
x)
  Ext (COMMENT_ITEM CommentType
x) -> ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s)
forall (s :: [T]). ExtInstr s -> Instr s s
Ext (CommentType -> ExtInstr (a ++ s)
forall (s :: [T]). CommentType -> ExtInstr s
COMMENT_ITEM CommentType
x)
  Ext (STACKTYPE StackTypePattern
x) -> ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s)
forall (s :: [T]). ExtInstr s -> Instr s s
Ext (StackTypePattern -> ExtInstr (a ++ s)
forall (s :: [T]). StackTypePattern -> ExtInstr s
STACKTYPE StackTypePattern
x)
  AnnCAR Anns '[VarAnn, FieldAnn]
anns                   -> Anns '[VarAnn, FieldAnn]
-> Instr ('TPair a b : (s ++ s)) (a : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
Anns '[VarAnn, FieldAnn] -> Instr ('TPair a b : s) (a : s)
AnnCAR Anns '[VarAnn, FieldAnn]
anns
  AnnCDR Anns '[VarAnn, FieldAnn]
anns                   -> Anns '[VarAnn, FieldAnn]
-> Instr ('TPair a b : (s ++ s)) (b : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
Anns '[VarAnn, FieldAnn] -> Instr ('TPair a b : s) (b : s)
AnnCDR Anns '[VarAnn, FieldAnn]
anns
  Instr a b
DROP                          -> Instr (a : (b ++ s)) (b ++ s)
Instr (a ++ s) (b ++ s)
forall (a :: T) (s :: [T]). Instr (a : s) s
DROP
  DROPN PeanoNatural n
n                       -> PeanoNatural n -> Instr (a ++ s) (Drop n (a ++ s))
forall (a :: Peano) (s :: [T]).
RequireLongerOrSameLength s a =>
PeanoNatural a -> Instr s (Drop a s)
DROPN PeanoNatural n
n ((Drop n (a ++ s) ~ (b ++ s),
  IsLongerOrSameLength (a ++ s) n ~ 'True) =>
 Instr (a ++ s) (b ++ s))
-> Dict
     (Drop n (a ++ s) ~ (b ++ s),
      IsLongerOrSameLength (a ++ s) n ~ 'True)
-> Instr (a ++ s) (b ++ s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [T]) (a :: [T]) (b :: [T]) (n :: Peano).
(Drop n a ~ b, IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n
-> Dict
     (Drop n (a ++ s) ~ (b ++ s),
      IsLongerOrSameLength (a ++ s) n ~ 'True)
forall {k} (s :: [k]) (a :: [k]) (b :: [k]) (n :: Peano).
(Drop n a ~ b, IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n
-> Dict
     (Drop n (a ++ s) ~ (b ++ s),
      IsLongerOrSameLength (a ++ s) n ~ 'True)
dropNExtensionThm @s @a PeanoNatural n
n
  AnnDUP AnnVar
anns                   -> AnnVar -> Instr (a : (s ++ s)) (a : a : (s ++ s))
forall (a :: T) (b :: [T]).
DupableScope a =>
AnnVar -> Instr (a : b) (a : a : b)
AnnDUP AnnVar
anns
  AnnDUPN AnnVar
anns PeanoNatural n
n                -> AnnVar -> PeanoNatural n -> Instr (a ++ s) (a : (a ++ s))
forall (a :: Peano) (inp :: [T]) (out :: [T]) (b :: T).
(ConstraintDUPN a inp out b, DupableScope b) =>
AnnVar -> PeanoNatural a -> Instr inp out
AnnDUPN AnnVar
anns PeanoNatural n
n ((RequireLongerOrSameLength (a ++ s) n, 'True ~ 'True,
  (a ++ s)
  ~ (LazyTake (Decrement n) (a ++ s) ++ (a : Drop n (a ++ s))),
  (a : (a ++ s)) ~ (a : (a ++ s))) =>
 Instr (a ++ s) (a : (a ++ s)))
-> Dict
     (RequireLongerOrSameLength (a ++ s) n, 'True ~ 'True,
      (a ++ s)
      ~ (LazyTake (Decrement n) (a ++ s) ++ (a : Drop n (a ++ s))),
      (a : (a ++ s)) ~ (a : (a ++ s)))
-> Instr (a ++ s) (a : (a ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [T]) (a :: [T]) (b :: [T]) (n :: Peano) (x :: T).
ConstraintDUPN n a b x =>
PeanoNatural n -> Dict (ConstraintDUPN n (a ++ s) (b ++ s) x)
dupNExtensionThm @s @a @b PeanoNatural n
n
  Instr a b
SWAP                          -> Instr (a : b : (s ++ s)) (b : a : (s ++ s))
Instr (a ++ s) (b ++ s)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP
  DIG PeanoNatural n
n                         -> PeanoNatural n
-> Instr
     (a ++ s) (a : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s)))
forall (a :: Peano) (inp :: [T]) (out :: [T]) (b :: T).
ConstraintDIG a inp out b =>
PeanoNatural a -> Instr inp out
DIG PeanoNatural n
n ((RequireLongerThan (a ++ s) n,
  (a : ((LazyTake n a ++ Drop ('S n) a) ++ s))
  ~ (a : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
  (a ++ s)
  ~ (LazyTake n ((LazyTake n a ++ Drop ('S n) a) ++ s)
     ++ (a : Drop n ((LazyTake n a ++ Drop ('S n) a) ++ s)))) =>
 Instr (a ++ s) (a : ((LazyTake n a ++ Drop ('S n) a) ++ s)))
-> Dict
     (RequireLongerThan (a ++ s) n,
      (a : ((LazyTake n a ++ Drop ('S n) a) ++ s))
      ~ (a : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
      (a ++ s)
      ~ (LazyTake n ((LazyTake n a ++ Drop ('S n) a) ++ s)
         ++ (a : Drop n ((LazyTake n a ++ Drop ('S n) a) ++ s))))
-> Instr (a ++ s) (a : ((LazyTake n a ++ Drop ('S n) a) ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [T]) (a :: [T]) (b :: [T]) (x :: T) (r :: [T])
       (n :: Peano).
(b ~ (x : r), ConstraintDIG n a b x) =>
PeanoNatural n -> Dict (ConstraintDIG n (a ++ s) (b ++ s) x)
digNExtensionThm @s @a @b PeanoNatural n
n
  DUG PeanoNatural n
n                         -> PeanoNatural n
-> Instr
     (a : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))) (b ++ s)
forall (a :: Peano) (inp :: [T]) (out :: [T]) (b :: T).
ConstraintDUG a inp out b =>
PeanoNatural a -> Instr inp out
DUG PeanoNatural n
n ((RequireLongerThan (b ++ s) n,
  (a : ((LazyTake n b ++ Drop ('S n) b) ++ s))
  ~ (a : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
  (b ++ s)
  ~ (LazyTake n ((LazyTake n b ++ Drop ('S n) b) ++ s)
     ++ (a : Drop n ((LazyTake n b ++ Drop ('S n) b) ++ s)))) =>
 Instr (a : ((LazyTake n b ++ Drop ('S n) b) ++ s)) (b ++ s))
-> Dict
     (RequireLongerThan (b ++ s) n,
      (a : ((LazyTake n b ++ Drop ('S n) b) ++ s))
      ~ (a : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
      (b ++ s)
      ~ (LazyTake n ((LazyTake n b ++ Drop ('S n) b) ++ s)
         ++ (a : Drop n ((LazyTake n b ++ Drop ('S n) b) ++ s))))
-> Instr (a : ((LazyTake n b ++ Drop ('S n) b) ++ s)) (b ++ s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [T]) (a :: [T]) (b :: [T]) (x :: T) (r :: [T])
       (n :: Peano).
(a ~ (x : r), ConstraintDUG n a b x) =>
PeanoNatural n -> Dict (ConstraintDUG n (a ++ s) (b ++ s) x)
dugNExtensionThm @s @a @b PeanoNatural n
n
  AnnSOME Anns '[TypeAnn, VarAnn]
anns                  -> Anns '[TypeAnn, VarAnn]
-> Instr (a : (s ++ s)) ('TOption a : (s ++ s))
forall (a :: T) (b :: [T]).
Anns '[TypeAnn, VarAnn] -> Instr (a : b) ('TOption a : b)
AnnSOME Anns '[TypeAnn, VarAnn]
anns
  AnnNONE Anns '[TypeAnn, VarAnn, Notes a]
anns                  -> Anns '[TypeAnn, VarAnn, Notes a]
-> Instr (a ++ s) ('TOption a : (a ++ s))
forall (a :: T) (s :: [T]).
SingI a =>
Anns '[TypeAnn, VarAnn, Notes a] -> Instr s ('TOption a : s)
AnnNONE Anns '[TypeAnn, VarAnn, Notes a]
anns
  AnnUNIT Anns '[TypeAnn, VarAnn]
anns                  -> Anns '[TypeAnn, VarAnn] -> Instr (a ++ s) ('TUnit : (a ++ s))
forall (s :: [T]). Anns '[TypeAnn, VarAnn] -> Instr s ('TUnit : s)
AnnUNIT Anns '[TypeAnn, VarAnn]
anns
  AnnPAIR Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
anns                  -> Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr (a : b : (s ++ s)) ('TPair a b : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr (a : b : s) ('TPair a b : s)
AnnPAIR Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
anns
  AnnUNPAIR Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn]
anns                -> Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr ('TPair a b : (s ++ s)) (a : b : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr ('TPair a b : s) (a : b : s)
AnnUNPAIR Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn]
anns
  AnnPAIRN AnnVar
anns PeanoNatural n
n               -> AnnVar -> PeanoNatural n -> Instr (a ++ s) (PairN n (a ++ s))
forall (a :: Peano) (inp :: [T]).
ConstraintPairN a inp =>
AnnVar -> PeanoNatural a -> Instr inp (PairN a inp)
AnnPAIRN AnnVar
anns PeanoNatural n
n (((RequireLongerOrSameLength (a ++ s) n,
   (() :: Constraint, 'True ~ 'True)),
  RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
  Drop n (a ++ s) ~ (Drop n a ++ s)) =>
 Instr (a ++ s) (RightComb (LazyTake n a) : (Drop n a ++ s)))
-> Dict
     ((RequireLongerOrSameLength (a ++ s) n,
       (() :: Constraint, 'True ~ 'True)),
      RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
      Drop n (a ++ s) ~ (Drop n a ++ s))
-> Instr (a ++ s) (RightComb (LazyTake n a) : (Drop n a ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [T]) (a :: [T]) (n :: Peano).
((n >= ToPeano 2) ~ 'True, IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n
-> Dict
     (ConstraintPairN n (a ++ s),
      RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
      Drop n (a ++ s) ~ (Drop n a ++ s))
pairNExtensionThm @s @a PeanoNatural n
n
  UNPAIRN PeanoNatural n
n                     -> PeanoNatural n
-> Instr (pair : (s ++ s)) (UnpairN n pair ++ (s ++ s))
forall (a :: Peano) (b :: T) (s :: [T]).
ConstraintUnpairN a b =>
PeanoNatural a -> Instr (b : s) (UnpairN a b ++ s)
UNPAIRN PeanoNatural n
n ((((() :: Constraint, 'True ~ 'True),
   (() :: Constraint, 'True ~ 'True)),
  (UnpairN n pair ++ (s ++ s)) ~ (b ++ s)) =>
 Instr (pair : (s ++ s)) (b ++ s))
-> Dict
     (((() :: Constraint, 'True ~ 'True),
       (() :: Constraint, 'True ~ 'True)),
      (UnpairN n pair ++ (s ++ s)) ~ (b ++ s))
-> Instr (pair : (s ++ s)) (b ++ s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [T]) (a :: [T]) (b :: [T]) (n :: Peano) (x :: T)
       (r :: [T]).
(a ~ (x : r), CombedPairLeafCountIsAtLeast n x ~ 'True,
 (n >= ToPeano 2) ~ 'True, (UnpairN n x ++ r) ~ b) =>
PeanoNatural n
-> Dict
     (ConstraintUnpairN n x, (UnpairN n x ++ (r ++ s)) ~ (b ++ s))
unpairNExtensionThm @s @a PeanoNatural n
n
  AnnLEFT Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes b]
anns                  -> Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes b]
-> Instr (a : (s ++ s)) ('TOr a b : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
SingI a =>
Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a]
-> Instr (b : s) ('TOr b a : s)
AnnLEFT Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes b]
anns
  AnnRIGHT Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a]
anns                 -> Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a]
-> Instr (b : (s ++ s)) ('TOr a b : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
SingI a =>
Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a]
-> Instr (b : s) ('TOr a b : s)
AnnRIGHT Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a]
anns
  AnnNIL Anns '[TypeAnn, VarAnn, Notes p]
anns                   -> Anns '[TypeAnn, VarAnn, Notes p]
-> Instr (a ++ s) ('TList p : (a ++ s))
forall (a :: T) (s :: [T]).
SingI a =>
Anns '[TypeAnn, VarAnn, Notes a] -> Instr s ('TList a : s)
AnnNIL Anns '[TypeAnn, VarAnn, Notes p]
anns
  AnnCONS AnnVar
anns                  -> AnnVar -> Instr (a : 'TList a : (s ++ s)) ('TList a : (s ++ s))
forall (a :: T) (b :: [T]).
AnnVar -> Instr (a : 'TList a : b) ('TList a : b)
AnnCONS AnnVar
anns
  AnnSIZE AnnVar
anns                  -> AnnVar -> Instr (c : (s ++ s)) ('TNat : (s ++ s))
forall (a :: T) (b :: [T]).
SizeOp a =>
AnnVar -> Instr (a : b) ('TNat : b)
AnnSIZE AnnVar
anns
  AnnEMPTY_SET Anns '[TypeAnn, VarAnn, Notes e]
anns             -> Anns '[TypeAnn, VarAnn, Notes e]
-> Instr (a ++ s) ('TSet e : (a ++ s))
forall (a :: T) (s :: [T]).
Comparable a =>
Anns '[TypeAnn, VarAnn, Notes a] -> Instr s ('TSet a : s)
AnnEMPTY_SET Anns '[TypeAnn, VarAnn, Notes e]
anns
  AnnEMPTY_MAP Anns '[TypeAnn, VarAnn, Notes a, Notes b]
anns             -> Anns '[TypeAnn, VarAnn, Notes a, Notes b]
-> Instr (a ++ s) ('TMap a b : (a ++ s))
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, Comparable b) =>
Anns '[TypeAnn, VarAnn, Notes b, Notes a]
-> Instr s ('TMap b a : s)
AnnEMPTY_MAP Anns '[TypeAnn, VarAnn, Notes a, Notes b]
anns
  AnnEMPTY_BIG_MAP Anns '[TypeAnn, VarAnn, Notes a, Notes b]
anns         -> Anns '[TypeAnn, VarAnn, Notes a, Notes b]
-> Instr (a ++ s) ('TBigMap a b : (a ++ s))
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, Comparable b, ForbidBigMap a) =>
Anns '[TypeAnn, VarAnn, Notes b, Notes a]
-> Instr s ('TBigMap b a : s)
AnnEMPTY_BIG_MAP Anns '[TypeAnn, VarAnn, Notes a, Notes b]
anns
  AnnMEM AnnVar
anns                   -> AnnVar -> Instr (MemOpKey c : c : (s ++ s)) ('TBool : (s ++ s))
forall (a :: T) (b :: [T]).
MemOp a =>
AnnVar -> Instr (MemOpKey a : a : b) ('TBool : b)
AnnMEM AnnVar
anns
  AnnGET AnnVar
anns                   -> AnnVar
-> Instr
     (GetOpKey c : c : (s ++ s)) ('TOption (GetOpVal c) : (s ++ s))
forall (a :: T) (b :: [T]).
(GetOp a, SingI (GetOpVal a)) =>
AnnVar -> Instr (GetOpKey a : a : b) ('TOption (GetOpVal a) : b)
AnnGET AnnVar
anns
  AnnGETN AnnVar
anns PeanoNatural ix
n                -> AnnVar
-> PeanoNatural ix
-> Instr (pair : (s ++ s)) (GetN ix pair : (s ++ s))
forall (a :: Peano) (b :: T) (s :: [T]).
ConstraintGetN a b =>
AnnVar -> PeanoNatural a -> Instr (b : s) (GetN a b : s)
AnnGETN AnnVar
anns PeanoNatural ix
n
  AnnUPDATE AnnVar
anns                -> AnnVar
-> Instr (UpdOpKey c : UpdOpParams c : c : (s ++ s)) (c : (s ++ s))
forall (a :: T) (b :: [T]).
UpdOp a =>
AnnVar -> Instr (UpdOpKey a : UpdOpParams a : a : b) (a : b)
AnnUPDATE AnnVar
anns
  AnnUPDATEN AnnVar
anns PeanoNatural ix
n             -> AnnVar
-> PeanoNatural ix
-> Instr (val : pair : (s ++ s)) (UpdateN ix val pair : (s ++ s))
forall (a :: Peano) (b :: T) (s :: T) (s :: [T]).
ConstraintUpdateN a s =>
AnnVar -> PeanoNatural a -> Instr (b : s : s) (UpdateN a b s : s)
AnnUPDATEN AnnVar
anns PeanoNatural ix
n
  AnnGET_AND_UPDATE AnnVar
anns        -> AnnVar
-> Instr
     (UpdOpKey c : UpdOpParams c : c : (s ++ s))
     ('TOption (GetOpVal c) : c : (s ++ s))
forall (a :: T) (b :: [T]).
(GetOp a, UpdOp a, SingI (GetOpVal a), UpdOpKey a ~ GetOpKey a) =>
AnnVar
-> Instr
     (UpdOpKey a : UpdOpParams a : a : b)
     ('TOption (GetOpVal a) : a : b)
AnnGET_AND_UPDATE AnnVar
anns
  AnnEXEC AnnVar
anns                  -> AnnVar -> Instr (t1 : 'TLambda t1 t2 : (s ++ s)) (t2 : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
AnnVar -> Instr (a : 'TLambda a b : s) (b : s)
AnnEXEC AnnVar
anns
  AnnAPPLY AnnVar
anns                 -> AnnVar
-> Instr
     (a : 'TLambda ('TPair a b) c : (s ++ s)) ('TLambda b c : (s ++ s))
forall (a :: T) (b :: T) (s :: T) (s :: [T]).
(ConstantScope a, SingI b) =>
AnnVar
-> Instr (a : 'TLambda ('TPair a b) s : s) ('TLambda b s : s)
AnnAPPLY AnnVar
anns
  Instr a b
FAILWITH                      -> Instr (a : (s ++ s)) (b ++ s)
Instr (a ++ s) (b ++ s)
forall (a :: T) (b :: [T]) (t :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : b) t
FAILWITH
  AnnCAST Anns '[VarAnn, Notes a]
anns                  -> Anns '[VarAnn, Notes a] -> Instr (a : (s ++ s)) (a : (s ++ s))
forall (a :: T) (b :: [T]).
SingI a =>
Anns '[VarAnn, Notes a] -> Instr (a : b) (a : b)
AnnCAST Anns '[VarAnn, Notes a]
anns
  AnnRENAME AnnVar
anns                -> AnnVar -> Instr (a : (s ++ s)) (a : (s ++ s))
forall (a :: T) (b :: [T]). AnnVar -> Instr (a : b) (a : b)
AnnRENAME AnnVar
anns
  AnnPACK AnnVar
anns                  -> AnnVar -> Instr (a : (s ++ s)) ('TBytes : (s ++ s))
forall (a :: T) (b :: [T]).
PackedValScope a =>
AnnVar -> Instr (a : b) ('TBytes : b)
AnnPACK AnnVar
anns
  AnnUNPACK Anns '[TypeAnn, VarAnn, Notes a]
anns                -> Anns '[TypeAnn, VarAnn, Notes a]
-> Instr ('TBytes : (s ++ s)) ('TOption a : (s ++ s))
forall (a :: T) (b :: [T]).
(UnpackedValScope a, SingI a) =>
Anns '[TypeAnn, VarAnn, Notes a]
-> Instr ('TBytes : b) ('TOption a : b)
AnnUNPACK Anns '[TypeAnn, VarAnn, Notes a]
anns
  AnnCONCAT AnnVar
anns                -> AnnVar -> Instr (c : c : (s ++ s)) (c : (s ++ s))
forall (a :: T) (b :: [T]).
ConcatOp a =>
AnnVar -> Instr (a : a : b) (a : b)
AnnCONCAT AnnVar
anns
  AnnCONCAT' AnnVar
anns               -> AnnVar -> Instr ('TList c : (s ++ s)) (c : (s ++ s))
forall (a :: T) (b :: [T]).
ConcatOp a =>
AnnVar -> Instr ('TList a : b) (a : b)
AnnCONCAT' AnnVar
anns
  AnnSLICE AnnVar
anns                 -> AnnVar
-> Instr ('TNat : 'TNat : c : (s ++ s)) ('TOption c : (s ++ s))
forall (a :: T) (b :: [T]).
(SliceOp a, SingI a) =>
AnnVar -> Instr ('TNat : 'TNat : a : b) ('TOption a : b)
AnnSLICE AnnVar
anns
  AnnISNAT AnnVar
anns                 -> AnnVar -> Instr ('TInt : (s ++ s)) ('TOption 'TNat : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TInt : a) ('TOption 'TNat : a)
AnnISNAT AnnVar
anns
  AnnADD AnnVar
anns                   -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes Add n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp Add a b =>
AnnVar -> Instr (a : b : s) (ArithRes Add a b : s)
AnnADD AnnVar
anns
  AnnSUB AnnVar
anns                   -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes Sub n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp Sub a b =>
AnnVar -> Instr (a : b : s) (ArithRes Sub a b : s)
AnnSUB AnnVar
anns
  AnnSUB_MUTEZ AnnVar
anns             -> AnnVar
-> Instr
     ('TMutez : 'TMutez : (s ++ s)) ('TOption 'TMutez : (s ++ s))
forall (a :: [T]).
AnnVar -> Instr ('TMutez : 'TMutez : a) ('TOption 'TMutez : a)
AnnSUB_MUTEZ AnnVar
anns
  AnnMUL AnnVar
anns                   -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes Mul n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp Mul a b =>
AnnVar -> Instr (a : b : s) (ArithRes Mul a b : s)
AnnMUL AnnVar
anns
  AnnEDIV AnnVar
anns                  -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes EDiv n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp EDiv a b =>
AnnVar -> Instr (a : b : s) (ArithRes EDiv a b : s)
AnnEDIV AnnVar
anns
  AnnABS AnnVar
anns                   -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Abs n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Abs a =>
AnnVar -> Instr (a : b) (UnaryArithRes Abs a : b)
AnnABS AnnVar
anns
  AnnNEG AnnVar
anns                   -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Neg n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Neg a =>
AnnVar -> Instr (a : b) (UnaryArithRes Neg a : b)
AnnNEG AnnVar
anns
  AnnLSL AnnVar
anns                   -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes Lsl n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp Lsl a b =>
AnnVar -> Instr (a : b : s) (ArithRes Lsl a b : s)
AnnLSL AnnVar
anns
  AnnLSR AnnVar
anns                   -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes Lsr n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp Lsr a b =>
AnnVar -> Instr (a : b : s) (ArithRes Lsr a b : s)
AnnLSR AnnVar
anns
  AnnOR AnnVar
anns                    -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes Or n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp Or a b =>
AnnVar -> Instr (a : b : s) (ArithRes Or a b : s)
AnnOR AnnVar
anns
  AnnAND AnnVar
anns                   -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes And n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp And a b =>
AnnVar -> Instr (a : b : s) (ArithRes And a b : s)
AnnAND AnnVar
anns
  AnnXOR AnnVar
anns                   -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes Xor n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp Xor a b =>
AnnVar -> Instr (a : b : s) (ArithRes Xor a b : s)
AnnXOR AnnVar
anns
  AnnNOT AnnVar
anns                   -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Not n : (s ++ s))
forall (a :: T) (b :: [T]).
(SingI a, UnaryArithOp Not a) =>
AnnVar -> Instr (a : b) (UnaryArithRes Not a : b)
AnnNOT AnnVar
anns
  AnnCOMPARE AnnVar
anns               -> AnnVar -> Instr (n : n : (s ++ s)) ('TInt : (s ++ s))
forall (a :: T) (b :: [T]).
Comparable a =>
AnnVar -> Instr (a : a : b) ('TInt : b)
AnnCOMPARE AnnVar
anns
  AnnEQ AnnVar
anns                    -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Eq' n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Eq' a =>
AnnVar -> Instr (a : b) (UnaryArithRes Eq' a : b)
AnnEQ AnnVar
anns
  AnnNEQ AnnVar
anns                   -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Neq n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Neq a =>
AnnVar -> Instr (a : b) (UnaryArithRes Neq a : b)
AnnNEQ AnnVar
anns
  AnnLT AnnVar
anns                    -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Lt n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Lt a =>
AnnVar -> Instr (a : b) (UnaryArithRes Lt a : b)
AnnLT AnnVar
anns
  AnnGT AnnVar
anns                    -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Gt n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Gt a =>
AnnVar -> Instr (a : b) (UnaryArithRes Gt a : b)
AnnGT AnnVar
anns
  AnnLE AnnVar
anns                    -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Le n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Le a =>
AnnVar -> Instr (a : b) (UnaryArithRes Le a : b)
AnnLE AnnVar
anns
  AnnGE AnnVar
anns                    -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Ge n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Ge a =>
AnnVar -> Instr (a : b) (UnaryArithRes Ge a : b)
AnnGE AnnVar
anns
  AnnINT AnnVar
anns                   -> AnnVar -> Instr (n : (s ++ s)) ('TInt : (s ++ s))
forall (a :: T) (b :: [T]).
ToIntArithOp a =>
AnnVar -> Instr (a : b) ('TInt : b)
AnnINT AnnVar
anns
  AnnVIEW Anns '[VarAnn, Notes ret]
anns ViewName
n                -> Anns '[VarAnn, Notes ret]
-> ViewName
-> Instr (arg : 'TAddress : (s ++ s)) ('TOption ret : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, ViewableScope b) =>
Anns '[VarAnn, Notes b]
-> ViewName -> Instr (a : 'TAddress : s) ('TOption b : s)
AnnVIEW Anns '[VarAnn, Notes ret]
anns ViewName
n
  AnnSELF AnnVar
anns SomeEntrypointCallT arg
ep               -> AnnVar
-> SomeEntrypointCallT arg
-> Instr (a ++ s) ('TContract arg : (a ++ s))
forall (a :: T) (s :: [T]).
(ParameterScope a, IsNotInView) =>
AnnVar -> SomeEntrypointCallT a -> Instr s ('TContract a : s)
AnnSELF AnnVar
anns SomeEntrypointCallT arg
ep
  AnnCONTRACT Anns '[VarAnn, Notes p]
anns EpName
c            -> Anns '[VarAnn, Notes p]
-> EpName
-> Instr
     ('TAddress : (s ++ s)) ('TOption ('TContract p) : (s ++ s))
forall (a :: T) (b :: [T]).
ParameterScope a =>
Anns '[VarAnn, Notes a]
-> EpName -> Instr ('TAddress : b) ('TOption ('TContract a) : b)
AnnCONTRACT Anns '[VarAnn, Notes p]
anns EpName
c
  AnnTRANSFER_TOKENS AnnVar
anns       -> AnnVar
-> Instr
     (p : 'TMutez : 'TContract p : (s ++ s)) ('TOperation : (s ++ s))
forall (a :: T) (b :: [T]).
(ParameterScope a, IsNotInView) =>
AnnVar -> Instr (a : 'TMutez : 'TContract a : b) ('TOperation : b)
AnnTRANSFER_TOKENS AnnVar
anns
  AnnSET_DELEGATE AnnVar
anns          -> AnnVar
-> Instr ('TOption 'TKeyHash : (s ++ s)) ('TOperation : (s ++ s))
forall (a :: [T]).
IsNotInView =>
AnnVar -> Instr ('TOption 'TKeyHash : a) ('TOperation : a)
AnnSET_DELEGATE AnnVar
anns
  AnnIMPLICIT_ACCOUNT AnnVar
anns      -> AnnVar
-> Instr ('TKeyHash : (s ++ s)) ('TContract 'TUnit : (s ++ s))
forall (a :: [T]).
AnnVar -> Instr ('TKeyHash : a) ('TContract 'TUnit : a)
AnnIMPLICIT_ACCOUNT AnnVar
anns
  AnnNOW AnnVar
anns                   -> AnnVar -> Instr (a ++ s) ('TTimestamp : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TTimestamp : s)
AnnNOW AnnVar
anns
  AnnAMOUNT AnnVar
anns                -> AnnVar -> Instr (a ++ s) ('TMutez : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TMutez : s)
AnnAMOUNT AnnVar
anns
  AnnBALANCE AnnVar
anns               -> AnnVar -> Instr (a ++ s) ('TMutez : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TMutez : s)
AnnBALANCE AnnVar
anns
  AnnVOTING_POWER AnnVar
anns          -> AnnVar -> Instr ('TKeyHash : (s ++ s)) ('TNat : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TKeyHash : a) ('TNat : a)
AnnVOTING_POWER AnnVar
anns
  AnnTOTAL_VOTING_POWER AnnVar
anns    -> AnnVar -> Instr (a ++ s) ('TNat : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TNat : s)
AnnTOTAL_VOTING_POWER AnnVar
anns
  AnnCHECK_SIGNATURE AnnVar
anns       -> AnnVar
-> Instr
     ('TKey : 'TSignature : 'TBytes : (s ++ s)) ('TBool : (s ++ s))
forall (a :: [T]).
AnnVar -> Instr ('TKey : 'TSignature : 'TBytes : a) ('TBool : a)
AnnCHECK_SIGNATURE AnnVar
anns
  AnnSHA256 AnnVar
anns                -> AnnVar -> Instr ('TBytes : (s ++ s)) ('TBytes : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TBytes : a) ('TBytes : a)
AnnSHA256 AnnVar
anns
  AnnSHA512 AnnVar
anns                -> AnnVar -> Instr ('TBytes : (s ++ s)) ('TBytes : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TBytes : a) ('TBytes : a)
AnnSHA512 AnnVar
anns
  AnnBLAKE2B AnnVar
anns               -> AnnVar -> Instr ('TBytes : (s ++ s)) ('TBytes : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TBytes : a) ('TBytes : a)
AnnBLAKE2B AnnVar
anns
  AnnSHA3 AnnVar
anns                  -> AnnVar -> Instr ('TBytes : (s ++ s)) ('TBytes : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TBytes : a) ('TBytes : a)
AnnSHA3 AnnVar
anns
  AnnKECCAK AnnVar
anns                -> AnnVar -> Instr ('TBytes : (s ++ s)) ('TBytes : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TBytes : a) ('TBytes : a)
AnnKECCAK AnnVar
anns
  AnnHASH_KEY AnnVar
anns              -> AnnVar -> Instr ('TKey : (s ++ s)) ('TKeyHash : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TKey : a) ('TKeyHash : a)
AnnHASH_KEY AnnVar
anns
  AnnPAIRING_CHECK AnnVar
anns         -> AnnVar
-> Instr
     ('TList ('TPair 'TBls12381G1 'TBls12381G2) : (s ++ s))
     ('TBool : (s ++ s))
forall (a :: [T]).
AnnVar
-> Instr
     ('TList ('TPair 'TBls12381G1 'TBls12381G2) : a) ('TBool : a)
AnnPAIRING_CHECK AnnVar
anns
  AnnSOURCE AnnVar
anns                -> AnnVar -> Instr (a ++ s) ('TAddress : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TAddress : s)
AnnSOURCE AnnVar
anns
  AnnSENDER AnnVar
anns                -> AnnVar -> Instr (a ++ s) ('TAddress : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TAddress : s)
AnnSENDER AnnVar
anns
  AnnADDRESS AnnVar
anns               -> AnnVar -> Instr ('TContract a : (s ++ s)) ('TAddress : (s ++ s))
forall (a :: T) (b :: [T]).
AnnVar -> Instr ('TContract a : b) ('TAddress : b)
AnnADDRESS AnnVar
anns
  AnnCHAIN_ID AnnVar
anns              -> AnnVar -> Instr (a ++ s) ('TChainId : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TChainId : s)
AnnCHAIN_ID AnnVar
anns
  AnnLEVEL AnnVar
anns                 -> AnnVar -> Instr (a ++ s) ('TNat : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TNat : s)
AnnLEVEL AnnVar
anns
  AnnSELF_ADDRESS AnnVar
anns          -> AnnVar -> Instr (a ++ s) ('TAddress : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TAddress : s)
AnnSELF_ADDRESS AnnVar
anns
  Instr a b
NEVER                         -> Instr ('TNever : (s ++ s)) (b ++ s)
Instr (a ++ s) (b ++ s)
forall (a :: [T]) (t :: [T]). Instr ('TNever : a) t
NEVER
  AnnTICKET AnnVar
anns                -> AnnVar
-> Instr (a : 'TNat : (s ++ s)) ('TOption ('TTicket a) : (s ++ s))
forall (a :: T) (b :: [T]).
Comparable a =>
AnnVar -> Instr (a : 'TNat : b) ('TOption ('TTicket a) : b)
AnnTICKET AnnVar
anns
  AnnTICKET_DEPRECATED AnnVar
anns     -> AnnVar -> Instr (a : 'TNat : (s ++ s)) ('TTicket a : (s ++ s))
forall (a :: T) (b :: [T]).
Comparable a =>
AnnVar -> Instr (a : 'TNat : b) ('TTicket a : b)
AnnTICKET_DEPRECATED AnnVar
anns
  AnnREAD_TICKET AnnVar
anns           -> AnnVar
-> Instr
     ('TTicket a : (s ++ s))
     (RightComb '[ 'TAddress, a, 'TNat] : 'TTicket a : (s ++ s))
forall (a :: T) (b :: [T]).
AnnVar
-> Instr
     ('TTicket a : b)
     (RightComb '[ 'TAddress, a, 'TNat] : 'TTicket a : b)
AnnREAD_TICKET AnnVar
anns
  AnnSPLIT_TICKET AnnVar
anns          -> AnnVar
-> Instr
     ('TTicket a : 'TPair 'TNat 'TNat : (s ++ s))
     ('TOption ('TPair ('TTicket a) ('TTicket a)) : (s ++ s))
forall (a :: T) (b :: [T]).
AnnVar
-> Instr
     ('TTicket a : 'TPair 'TNat 'TNat : b)
     ('TOption ('TPair ('TTicket a) ('TTicket a)) : b)
AnnSPLIT_TICKET AnnVar
anns
  AnnJOIN_TICKETS AnnVar
anns          -> AnnVar
-> Instr
     ('TPair ('TTicket a) ('TTicket a) : (s ++ s))
     ('TOption ('TTicket a) : (s ++ s))
forall (a :: T) (b :: [T]).
AnnVar
-> Instr
     ('TPair ('TTicket a) ('TTicket a) : b) ('TOption ('TTicket a) : b)
AnnJOIN_TICKETS AnnVar
anns
  AnnOPEN_CHEST AnnVar
anns            -> AnnVar
-> Instr
     ('TChestKey : 'TChest : 'TNat : (s ++ s))
     ('TOr 'TBytes 'TBool : (s ++ s))
forall (a :: [T]).
AnnVar
-> Instr
     ('TChestKey : 'TChest : 'TNat : a) ('TOr 'TBytes 'TBool : a)
AnnOPEN_CHEST AnnVar
anns
  AnnSAPLING_EMPTY_STATE AnnVar
anns Sing n
n -> AnnVar -> Sing n -> Instr (a ++ s) ('TSaplingState n : (a ++ s))
forall (a :: Peano) (s :: [T]).
AnnVar -> Sing a -> Instr s ('TSaplingState a : s)
AnnSAPLING_EMPTY_STATE AnnVar
anns Sing n
n
  AnnSAPLING_VERIFY_UPDATE AnnVar
anns -> AnnVar
-> Instr
     ('TSaplingTransaction n : 'TSaplingState n : (s ++ s))
     ('TOption ('TPair 'TBytes ('TPair 'TInt ('TSaplingState n)))
        : (s ++ s))
forall (a :: Peano) (b :: [T]).
AnnVar
-> Instr
     ('TSaplingTransaction a : 'TSaplingState a : b)
     ('TOption ('TPair 'TBytes ('TPair 'TInt ('TSaplingState a))) : b)
AnnSAPLING_VERIFY_UPDATE AnnVar
anns
  AnnMIN_BLOCK_TIME [AnyAnn]
anns        -> [AnyAnn] -> Instr (a ++ s) ('TNat : (a ++ s))
forall (s :: [T]). [AnyAnn] -> Instr s ('TNat : s)
AnnMIN_BLOCK_TIME [AnyAnn]
anns
  AnnEMIT AnnVar
anns FieldAnn
tag Maybe (Notes t)
ty           -> AnnVar
-> FieldAnn
-> Maybe (Notes t)
-> Instr (t : (s ++ s)) ('TOperation : (s ++ s))
forall (a :: T) (b :: [T]).
PackedValScope a =>
AnnVar
-> FieldAnn -> Maybe (Notes a) -> Instr (a : b) ('TOperation : b)
AnnEMIT AnnVar
anns FieldAnn
tag Maybe (Notes t)
ty
  AnnBYTES AnnVar
anns                 -> AnnVar -> Instr (n : (s ++ s)) ('TBytes : (s ++ s))
forall (a :: T) (b :: [T]).
ToBytesArithOp a =>
AnnVar -> Instr (a : b) ('TBytes : b)
AnnBYTES AnnVar
anns
  AnnNAT AnnVar
anns                   -> AnnVar -> Instr ('TBytes : (s ++ s)) ('TNat : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TBytes : a) ('TNat : a)
AnnNAT AnnVar
anns
  where
    go :: forall a' b'. Instr a' b' -> Instr (a' ++ s) (b' ++ s)
    go :: forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go = forall (s :: [T]) (a :: [T]) (b :: [T]).
Instr a b -> Instr (a ++ s) (b ++ s)
frameInstr @s

    comment :: PrintComment a -> PrintComment (a ++ s)
    comment :: PrintComment a -> PrintComment (a ++ s)
comment (PrintComment [Either Text (StackRef a)]
c) = [Either Text (StackRef (a ++ s))] -> PrintComment (a ++ s)
forall (st :: [T]). [Either Text (StackRef st)] -> PrintComment st
PrintComment ([Either Text (StackRef (a ++ s))] -> PrintComment (a ++ s))
-> [Either Text (StackRef (a ++ s))] -> PrintComment (a ++ s)
forall a b. (a -> b) -> a -> b
$ [Either Text (StackRef a)]
c [Either Text (StackRef a)]
-> (Either Text (StackRef a) -> Either Text (StackRef (a ++ s)))
-> [Either Text (StackRef (a ++ s))]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
      Left Text
t -> Text -> Either Text (StackRef (a ++ s))
forall a b. a -> Either a b
Left Text
t
      Right (StackRef PeanoNatural idx
n) -> StackRef (a ++ s) -> Either Text (StackRef (a ++ s))
forall a b. b -> Either a b
Right (StackRef (a ++ s) -> Either Text (StackRef (a ++ s)))
-> StackRef (a ++ s) -> Either Text (StackRef (a ++ s))
forall a b. (a -> b) -> a -> b
$ forall (st :: [T]) (a :: Peano).
RequireLongerThan st a =>
PeanoNatural a -> StackRef st
StackRef @(a ++ s) PeanoNatural idx
n
        ((IsLongerThan (a ++ s) idx ~ 'True) => StackRef (a ++ s))
-> (IsLongerThan (a ++ s) idx :~: 'True) -> StackRef (a ++ s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
isLongerThanExtThm @a @s PeanoNatural idx
n

deriveGADTNFData ''Instr

instance NFData (ExtInstr s)

instance NFData (TestAssert s) where
  rnf :: TestAssert s -> ()
rnf (TestAssert Text
a PrintComment s
b Instr s ('TBool : out)
c) = (Text, PrintComment s, Instr s ('TBool : out)) -> ()
forall a. NFData a => a -> ()
rnf (Text
a, PrintComment s
b, Instr s ('TBool : out)
c)

-- This TH splice generates pattern synonyms for @AnnX@ data constructors
-- without the @Ann@ prefix, ignoring annotations. Matching simply ignores
-- the first argument (containing the list of annotations), and construction
-- uses @def@.
do
  TyConI (DataD _ _ _ _ cons _) <- reify ''Instr
  let go forallSig = \case
        ForallC varbndrs cxt'' con -> go (Just (varbndrs, cxt'')) con
        GadtC nms btys (AppT (AppT _ inpT) outT) -> concatForM nms \nm -> do
          case "Ann" `stripPrefix` nameBase nm of
            Just base -> lookupValueName base >>= \case
              Just{} -> pure [] -- skip if already defined
              Nothing -> do
                let btys' = drop 1 btys
                args <- forM btys' \_ -> newName "arg"
                inpV <- newName "inp"
                outV <- newName "out"
                let pat = PatSynD baseName (PrefixPatSyn args) (ExplBidir [cl])
                      (ConP nm [] $ WildP : (VarP <$> args))
                    baseName = mkName base
                    cl = Clause (VarP <$> args) (NormalB body) []
                    body = foldl' AppE (ConE nm) $ (VarE $ 'def):(VarE <$> args)
                    inpout = [PlainTV inpV InferredSpec, PlainTV outV InferredSpec]
                    eqT x y = AppT (AppT EqualityT x) y
                    forallc
                      | Just (vars, cxt') <- forallSig
                      = ForallT inpout [] . ForallT vars (eqT (VarT inpV) inpT : eqT (VarT outV) outT : cxt')
                      | otherwise = id
                    patsig = forallc $
                      foldr (AppT . AppT ArrowT . snd) (AppT (AppT (ConT ''Instr) (VarT inpV)) (VarT outV)) btys'
                pure [PatSynSigD baseName patsig, pat]
            Nothing -> pure []
        _ -> pure []
      conName = \case
        ForallC _ _ con -> conName con
        GadtC nms _ _ -> nameBase <$> nms
        NormalC nm _ -> [nameBase nm]
        RecC nm _ -> [nameBase nm]
        InfixC _ nm _ -> [nameBase nm]
        RecGadtC nms _ _ -> nameBase <$> nms
      stripAnn x = fromMaybe x $ "Ann" `stripPrefix` x

  pats <- concat <$> traverse (go Nothing) cons
  pure $ (PragmaD $ CompleteP (mkName . stripAnn <$> concatMap conName cons) Nothing) : pats

{-# DEPRECATED OPEN_CHEST
  "Due to a vulnerability discovered in time-lock protocol, \
  \OPEN_CHEST is temporarily deprecated since Lima" #-}