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

{-# OPTIONS_GHC -Wno-orphans #-}

-- | 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
          )
  , castInstr
  , pattern (:#)
  , ExtInstr (..)
  , CommentType (..)
  , StackRef (..)
  , mkStackRef
  , PrintComment (..)
  , TestAssert (..)
  , SomeMeta (..)
  , pattern ConcreteMeta
  , ConstraintDUPN
  , ConstraintDUPN'
  , ConstraintDIPN
  , ConstraintDIPN'
  , ConstraintDIG
  , ConstraintDIG'
  , ConstraintDUG
  , ConstraintDUG'
  , ConstraintPairN
  , PairN
  , RightComb
  , ConstraintUnpairN
  , UnpairN
  , ConstraintGetN
  , GetN
  , ConstraintUpdateN
  , UpdateN
  ) where

import Prelude hiding (EQ, GT, LT)

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, type (+))
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.Polymorphic
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.T (T(..))
import Morley.Michelson.Typed.TypeLevel
  (CombedPairLeafCount, CombedPairLeafCountIsAtLeast, CombedPairNodeCount,
  CombedPairNodeIndexIsValid, IsPair)
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 (FailUnless, If, KnownList, type (++))
import Morley.Util.TypeLits (ErrorMessage(ShowType, Text, (:$$:), (:<>:)))

{-# 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

-- | Constraint that is used in DUPN, we want to share it with
-- typechecking code and eDSL code.
type ConstraintDUPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) =
  ( RequireLongerOrSameLength inp n, n > 'Z ~ 'True
  , inp ~ (LazyTake (Decrement n) inp ++ (a ': Drop n inp))
  , out ~ (a ': inp)
  )

type ConstraintDUPN n inp out a = ConstraintDUPN' T n inp out a

-- | Constraint that is used in DIPN, we want to share it with
-- typechecking code and eDSL code.
type ConstraintDIPN' kind (n :: Peano) (inp :: [kind])
  (out :: [kind]) (s :: [kind]) (s' :: [kind]) =
  ( RequireLongerOrSameLength inp n
  , LazyTake n inp ++ s ~ inp
  , LazyTake n inp ++ s' ~ out
  , s ~ Drop n inp
  , s' ~ Drop n out
  )

type ConstraintDIPN n inp out s s' = ConstraintDIPN' T n inp out s s'

-- | Constraint that is used in DIG, we want to share it with
-- typechecking code and eDSL code.
type ConstraintDIG' kind (n :: Peano) (inp :: [kind])
  (out :: [kind]) (a :: kind) =
  ( RequireLongerThan inp n
  , out ~ a ': LazyTake n inp ++ Drop ('S n) inp
  , inp ~ LazyTake n (Drop ('S 'Z) out) ++ (a ': Drop ('S n) out)
  )

type ConstraintDIG n inp out a = ConstraintDIG' T n inp out a

-- | Constraint that is used in DUG, we want to share it with
-- typechecking code and eDSL code.
type ConstraintDUG' kind (n :: Peano) (inp :: [kind])
  (out :: [kind]) (a :: kind) =
  ConstraintDIG' kind n out inp a

type ConstraintDUG n inp out a = ConstraintDUG' T n inp out a

type ConstraintPairN (n :: Peano) (inp :: [T]) =
  ( RequireLongerOrSameLength inp n
  , FailUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n ≥ 2")
  )

type PairN (n :: Peano) (s :: [T]) = RightComb (LazyTake n s) ': Drop n s

-- | Folds a stack into a right-combed pair.
--
-- > RightComb '[ 'TInt,  'TString, 'TUnit ]
-- > ~
-- > 'TPair 'TInt ('TPair 'TString 'TUnit)
type family RightComb (s :: [T]) :: T where
  RightComb '[ x, y ] = 'TPair x y
  RightComb (x ': xs) = 'TPair x (RightComb xs)

type ConstraintUnpairN (n :: Peano) (pair :: T) =
  ( FailUnless (n >= ToPeano 2)
      ('Text "'UNPAIR n' expects n ≥ 2")

  , FailUnless (CombedPairLeafCountIsAtLeast n pair)
      (If (IsPair pair)
        ('Text "'UNPAIR "
          ':<>: 'ShowType (FromPeano n)
          ':<>: 'Text "' expects a right-combed pair with at least "
          ':<>: 'ShowType (FromPeano n)
          ':<>: 'Text " elements at the top of the stack,"
          ':$$: 'Text "but the pair only contains "
          ':<>: 'ShowType (FromPeano (CombedPairLeafCount pair))
          ':<>: 'Text " elements.")
        ('Text "Expected a pair at the top of the stack, but found: "
          ':<>: 'ShowType pair
        )
      )
  )

-- | Splits a right-combed pair into @n@ elements.
--
-- > UnpairN (ToPeano 3) ('TPair 'TInt ('TPair 'TString 'TUnit))
-- > ~
-- > '[ 'TInt, 'TString, 'TUnit]
--
-- > UnpairN (ToPeano 3) ('TPair 'TInt ('TPair 'TString ('TPair 'TUnit 'TInt)))
-- > ~
-- > '[ 'TInt, 'TString, 'TPair 'TUnit 'TInt]
type family UnpairN (n :: Peano) (s :: T) :: [T] where
  UnpairN ('S ('S 'Z)) ('TPair x y) = [x, y]
  UnpairN ('S n)       ('TPair x y) = x : UnpairN n y

type ConstraintGetN (ix :: Peano) (pair :: T) =
  ( FailUnless (CombedPairNodeIndexIsValid ix pair)
      (If (IsPair pair)
        ('Text "'GET "
          ':<>: 'ShowType (FromPeano ix)
          ':<>: 'Text "' expects a right-combed pair with at least "
          ':<>: 'ShowType (FromPeano ix + 1)
          ':<>: 'Text " nodes at the top of the stack,"
          ':$$: 'Text "but the pair only contains "
          ':<>: 'ShowType (FromPeano (CombedPairNodeCount pair))
          ':<>: 'Text " nodes.")
        ('Text "Expected a pair at the top of the stack, but found: "
          ':<>: 'ShowType pair
        )
      )
  )

-- | Get the node at index @ix@ of a right-combed pair.
type family GetN (ix :: Peano) (pair :: T) :: T where
  GetN 'Z val                       = val
  GetN ('S 'Z) ('TPair left _)      = left
  GetN ('S ('S n)) ('TPair _ right) = GetN n right

type ConstraintUpdateN (ix :: Peano) (pair :: T) =
  ( FailUnless (CombedPairNodeIndexIsValid ix pair)
      (If (IsPair pair)
        ('Text "'UPDATE "
          ':<>: 'ShowType (FromPeano ix)
          ':<>: 'Text "' expects the 2nd element of the stack to be a right-combed pair with at least "
          ':<>: 'ShowType (FromPeano ix + 1)
          ':<>: 'Text " nodes,"
          ':$$: 'Text "but the pair only contains "
          ':<>: 'ShowType (FromPeano (CombedPairNodeCount pair))
          ':<>: 'Text " nodes.")
        ('Text "Expected the 2nd element of the stack to be a pair, but found: "
          ':<>: 'ShowType pair
        )
      )
  )

-- | Update the node at index @ix@ of a right-combed pair.
type family UpdateN (ix :: Peano) (val :: T) (pair :: T) :: T where
  UpdateN 'Z          val _                   = val
  UpdateN ('S 'Z)     val ('TPair _  right)   = 'TPair val right
  UpdateN ('S ('S n)) val ('TPair left right) = 'TPair left (UpdateN n val right)

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

  -- | Execute given instruction on truncated stack.
  --
  -- This can wrap only instructions with at least one non-failing execution
  -- branch.
  --
  -- Morley has no such instruction, it is used solely in eDSLs.
  -- This instruction 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.
  -- We could make this not an instruction but rather a function
  -- which modifies an instruction (this would also automatically prove
  -- soundness of used transformation), but it occurred to be tricky
  -- (in particular for TestAssert and DipN and family), so let's leave
  -- this for future work.
  FrameInstr
    :: forall a b s.
       KnownList a
    => Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)

  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 :: (SingI e, Comparable e) => Anns '[TypeAnn, VarAnn, Notes e] -> Instr s ('TSet e ': s)
  AnnEMPTY_MAP :: (SingI a, SingI b, Comparable a) => Anns '[TypeAnn, VarAnn, Notes a, Notes b] -> Instr s ('TMap a b ': s)
  AnnEMPTY_BIG_MAP :: (SingI a, SingI b, Comparable a, HasNoBigMap 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
    :: UnaryArithOp Not n
    => AnnVar
    -> Instr (n ': s) (UnaryArithRes Not n ': s)
  AnnCOMPARE
    :: (Comparable n, SingI 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)
  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

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" #-}