-- 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 instr =
  case (eqI @inp1 @inp2, eqI @out1 @out2) of
    (Just Refl, Just Refl) -> Just instr
    (_,_) -> 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 :# b = Seq a b
infixr 8 :#

deriving stock instance Show (Instr inp out)

instance Semigroup (Instr s s) where
  (<>) = Seq
instance Monoid (Instr s s) where
  mempty = 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 s) = rnf s

instance Eq (StackRef st) where
  StackRef snat1 == StackRef snat2 = fromPeanoNatural snat1 == fromPeanoNatural snat2

instance Show (StackRef st) where
  showsPrec d (StackRef snat) = T.showParen (d > app_prec) $
    T.showString "StackRef " .
    T.showParen True (T.showString "toPeanoNatural' @" . T.shows (fromPeanoNatural snat))
    where
      app_prec = 10

instance Buildable (StackRef st) where
  build (StackRef snat) = "StackRef {" +| fromPeanoNatural snat |+ "}"

-- | 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 = StackRef $ toPeanoNatural' @gn

-- | A print format with references into the stack
newtype PrintComment (st :: [T]) = PrintComment
  { unPrintComment :: [Either Text (StackRef st)]
  } deriving stock (Eq, Show, Generic)
    deriving newtype (Semigroup, Monoid)

instance NFData (PrintComment st)

instance IsString (PrintComment st) where
  fromString = PrintComment . one . Left . fromString

data CommentType
 = FunctionStarts Text
 | FunctionEnds Text
 | StatementStarts Text
 | StatementEnds Text
 | JustComment Text
 | StackTypeComment (Maybe [T]) -- ^ 'Nothing' for any stack type
 deriving stock (Show, Generic)

instance NFData CommentType

instance IsString CommentType where
  fromString = JustComment . 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 (Show, Generic)

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

instance NFData SomeMeta where
  rnf (SomeMeta meta) = rnf 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 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 LAMBDA code <- AnnLAMBDA _ code
  where LAMBDA code = AnnLAMBDA def $ giveNotInView 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 LAMBDA_REC code <- AnnLAMBDA_REC _ code
  where LAMBDA_REC code = AnnLAMBDA_REC def $ giveNotInView 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 = \case
  Seq i1 i2 -> Seq (go i1) (go i2)
  WithLoc loc instr -> WithLoc loc $ go instr
  Meta m instr -> Meta m $ go instr
  Nested i1 -> Nested $ go i1
  DocGroup dg i1 -> DocGroup dg $ go i1
  IF_NONE i1 i2 -> IF_NONE (go i1) (go i2)
  IF_LEFT i1 i2 -> IF_LEFT (go i1) (go i2)
  IF_CONS i1 i2 -> IF_CONS (go i1) (go i2)
  IF i1 i2 -> IF (go i1) (go i2)
  AnnMAP ann i1 -> AnnMAP ann $ go i1
  ITER i1 -> ITER $ go i1
  LOOP i1 -> LOOP $ go i1
  LOOP_LEFT i1 -> LOOP_LEFT $ go i1
  DIP i1 -> DIP $ go i1
  DIPN n (i1 :: Instr s1 s1') -> DIPN n (go i1) \\ dipNExtensionThm @s @a @b @s1 @s1' n
  AnnPUSH ann v -> AnnPUSH ann v
  AnnLAMBDA ann lam -> AnnLAMBDA ann lam
  AnnLAMBDA_REC ann lam -> AnnLAMBDA_REC ann lam
  AnnCREATE_CONTRACT ann contract -> AnnCREATE_CONTRACT ann contract
  Nop -> Nop
  Ext (TEST_ASSERT (TestAssert t c i)) -> Ext $ TEST_ASSERT $ TestAssert t (comment c) (go i)
  Ext (PRINT x) -> Ext $ PRINT $ comment x
  Ext (DOC_ITEM x) -> Ext (DOC_ITEM x)
  Ext (COMMENT_ITEM x) -> Ext (COMMENT_ITEM x)
  Ext (STACKTYPE x) -> Ext (STACKTYPE x)
  AnnCAR anns                   -> AnnCAR anns
  AnnCDR anns                   -> AnnCDR anns
  DROP                          -> DROP
  DROPN n                       -> DROPN n \\ dropNExtensionThm @s @a n
  AnnDUP anns                   -> AnnDUP anns
  AnnDUPN anns n                -> AnnDUPN anns n \\ dupNExtensionThm @s @a @b n
  SWAP                          -> SWAP
  DIG n                         -> DIG n \\ digNExtensionThm @s @a @b n
  DUG n                         -> DUG n \\ dugNExtensionThm @s @a @b n
  AnnSOME anns                  -> AnnSOME anns
  AnnNONE anns                  -> AnnNONE anns
  AnnUNIT anns                  -> AnnUNIT anns
  AnnPAIR anns                  -> AnnPAIR anns
  AnnUNPAIR anns                -> AnnUNPAIR anns
  AnnPAIRN anns n               -> AnnPAIRN anns n \\ pairNExtensionThm @s @a n
  UNPAIRN n                     -> UNPAIRN n \\ unpairNExtensionThm @s @a n
  AnnLEFT anns                  -> AnnLEFT anns
  AnnRIGHT anns                 -> AnnRIGHT anns
  AnnNIL anns                   -> AnnNIL anns
  AnnCONS anns                  -> AnnCONS anns
  AnnSIZE anns                  -> AnnSIZE anns
  AnnEMPTY_SET anns             -> AnnEMPTY_SET anns
  AnnEMPTY_MAP anns             -> AnnEMPTY_MAP anns
  AnnEMPTY_BIG_MAP anns         -> AnnEMPTY_BIG_MAP anns
  AnnMEM anns                   -> AnnMEM anns
  AnnGET anns                   -> AnnGET anns
  AnnGETN anns n                -> AnnGETN anns n
  AnnUPDATE anns                -> AnnUPDATE anns
  AnnUPDATEN anns n             -> AnnUPDATEN anns n
  AnnGET_AND_UPDATE anns        -> AnnGET_AND_UPDATE anns
  AnnEXEC anns                  -> AnnEXEC anns
  AnnAPPLY anns                 -> AnnAPPLY anns
  FAILWITH                      -> FAILWITH
  AnnCAST anns                  -> AnnCAST anns
  AnnRENAME anns                -> AnnRENAME anns
  AnnPACK anns                  -> AnnPACK anns
  AnnUNPACK anns                -> AnnUNPACK anns
  AnnCONCAT anns                -> AnnCONCAT anns
  AnnCONCAT' anns               -> AnnCONCAT' anns
  AnnSLICE anns                 -> AnnSLICE anns
  AnnISNAT anns                 -> AnnISNAT anns
  AnnADD anns                   -> AnnADD anns
  AnnSUB anns                   -> AnnSUB anns
  AnnSUB_MUTEZ anns             -> AnnSUB_MUTEZ anns
  AnnMUL anns                   -> AnnMUL anns
  AnnEDIV anns                  -> AnnEDIV anns
  AnnABS anns                   -> AnnABS anns
  AnnNEG anns                   -> AnnNEG anns
  AnnLSL anns                   -> AnnLSL anns
  AnnLSR anns                   -> AnnLSR anns
  AnnOR anns                    -> AnnOR anns
  AnnAND anns                   -> AnnAND anns
  AnnXOR anns                   -> AnnXOR anns
  AnnNOT anns                   -> AnnNOT anns
  AnnCOMPARE anns               -> AnnCOMPARE anns
  AnnEQ anns                    -> AnnEQ anns
  AnnNEQ anns                   -> AnnNEQ anns
  AnnLT anns                    -> AnnLT anns
  AnnGT anns                    -> AnnGT anns
  AnnLE anns                    -> AnnLE anns
  AnnGE anns                    -> AnnGE anns
  AnnINT anns                   -> AnnINT anns
  AnnVIEW anns n                -> AnnVIEW anns n
  AnnSELF anns ep               -> AnnSELF anns ep
  AnnCONTRACT anns c            -> AnnCONTRACT anns c
  AnnTRANSFER_TOKENS anns       -> AnnTRANSFER_TOKENS anns
  AnnSET_DELEGATE anns          -> AnnSET_DELEGATE anns
  AnnIMPLICIT_ACCOUNT anns      -> AnnIMPLICIT_ACCOUNT anns
  AnnNOW anns                   -> AnnNOW anns
  AnnAMOUNT anns                -> AnnAMOUNT anns
  AnnBALANCE anns               -> AnnBALANCE anns
  AnnVOTING_POWER anns          -> AnnVOTING_POWER anns
  AnnTOTAL_VOTING_POWER anns    -> AnnTOTAL_VOTING_POWER anns
  AnnCHECK_SIGNATURE anns       -> AnnCHECK_SIGNATURE anns
  AnnSHA256 anns                -> AnnSHA256 anns
  AnnSHA512 anns                -> AnnSHA512 anns
  AnnBLAKE2B anns               -> AnnBLAKE2B anns
  AnnSHA3 anns                  -> AnnSHA3 anns
  AnnKECCAK anns                -> AnnKECCAK anns
  AnnHASH_KEY anns              -> AnnHASH_KEY anns
  AnnPAIRING_CHECK anns         -> AnnPAIRING_CHECK anns
  AnnSOURCE anns                -> AnnSOURCE anns
  AnnSENDER anns                -> AnnSENDER anns
  AnnADDRESS anns               -> AnnADDRESS anns
  AnnCHAIN_ID anns              -> AnnCHAIN_ID anns
  AnnLEVEL anns                 -> AnnLEVEL anns
  AnnSELF_ADDRESS anns          -> AnnSELF_ADDRESS anns
  NEVER                         -> NEVER
  AnnTICKET anns                -> AnnTICKET anns
  AnnTICKET_DEPRECATED anns     -> AnnTICKET_DEPRECATED anns
  AnnREAD_TICKET anns           -> AnnREAD_TICKET anns
  AnnSPLIT_TICKET anns          -> AnnSPLIT_TICKET anns
  AnnJOIN_TICKETS anns          -> AnnJOIN_TICKETS anns
  AnnOPEN_CHEST anns            -> AnnOPEN_CHEST anns
  AnnSAPLING_EMPTY_STATE anns n -> AnnSAPLING_EMPTY_STATE anns n
  AnnSAPLING_VERIFY_UPDATE anns -> AnnSAPLING_VERIFY_UPDATE anns
  AnnMIN_BLOCK_TIME anns        -> AnnMIN_BLOCK_TIME anns
  AnnEMIT anns tag ty           -> AnnEMIT anns tag ty
  AnnBYTES anns                 -> AnnBYTES anns
  AnnNAT anns                   -> AnnNAT anns
  where
    go :: forall a' b'. Instr a' b' -> Instr (a' ++ s) (b' ++ s)
    go = frameInstr @s

    comment :: PrintComment a -> PrintComment (a ++ s)
    comment (PrintComment c) = PrintComment $ c <&> \case
      Left t -> Left t
      Right (StackRef n) -> Right $ StackRef @(a ++ s) n
        \\ isLongerThanExtThm @a @s n

deriveGADTNFData ''Instr

instance NFData (ExtInstr s)

instance NFData (TestAssert s) where
  rnf (TestAssert a b c) = rnf (a, b, 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" #-}