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

{-# OPTIONS_GHC -Wno-orphans #-}

-- | Module, containing data types for Michelson value.
module Morley.Michelson.Typed.Instr
  ( Instr (..)
  , castInstr
  , pattern (:#)
  , ExtInstr (..)
  , CommentType (..)
  , StackRef (..)
  , mkStackRef
  , PrintComment (..)
  , TestAssert (..)
  , SomeMeta (..)
  , pattern CAR
  , pattern CDR
  , pattern LEFT
  , pattern PAIR
  , pattern RIGHT
  , pattern UNPAIR
  , ConstraintDUPN
  , ConstraintDUPN'
  , ConstraintDIPN
  , ConstraintDIPN'
  , ConstraintDIG
  , ConstraintDIG'
  , ConstraintDUG
  , ConstraintDUG'
  , ConstraintPairN
  , PairN
  , RightComb
  , ConstraintUnpairN
  , UnpairN
  , ConstraintGetN
  , GetN
  , ConstraintUpdateN
  , UpdateN
  ) where

import Data.Type.Equality ((:~:)(..))
import Data.Vinyl (RMap, Rec(..), RecordToList, ReifyConstraint(..))
import Fmt ((+||), (||+))
import GHC.TypeNats (type (+))
import qualified GHC.TypeNats as GHC (Nat)
import qualified Text.Show

import Morley.Michelson.Doc
import Morley.Michelson.ErrorPos
import Morley.Michelson.Typed.Annotation (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 (Comparable, Value'(..))
import Morley.Michelson.Typed.View
import Morley.Michelson.Untyped
  (Annotation(..), FieldAnn, StackFn, StackTypePattern, TypeAnn, VarAnn, VarAnns)
import Morley.Util.Peano
import Morley.Util.PeanoNatural
import Morley.Util.Sing (eqI)
import Morley.Util.TH
import Morley.Util.Type (If, KnownList, type (++))
import Morley.Util.TypeLits (ErrorMessage(ShowType, Text, (:$$:), (:<>:)), TypeErrorUnless)

{-
Note [Annotations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

When typechecking a sequence of instructions:

1. We'll typecheck an "untyped instruction" like `EMPTY_SET :ta @va unit`, producing:
    * a "typed instruction" `EMPTY_SET :: Instr s (TSet TUnit : s)`, and
    * an output stack with a `@va set :ta int` at the top.
2. In `Morley.Michelson.TypeCheck.Helpers.wrapWithNotes`:
    * if the original instruction had a var annotation (e.g. `SOME_INSTR @some_ann`),
      then we wrap the "typed instruction" in `InstrWithVarNotes`.
    * if the element at the top of the output stack has a var annotation,
      we wrap it in `InstrWithVarAnns`.
    * if the element at the top of the output stack has field/type anns,
      we wrap it in `InstrWithNotes`
        ```
        InstrWithNotes Proxy (NTSet "ta" (NTUnit "")) $
          InstrWithVarNotes (one "va") $
            InstrWithVarAnns (OneVarAnn "va") $
              EMPTY_SET
        ```

These "meta-instruction" wrappers are later used in the interpreter/serializer.

The interpreter ('Morley.Michelson.Interpret'):
  * Looks at the typed instruction (e.g. `EMPTY_SET`), and simply adds/removes/moves elements
    in the stack, without caring about annotations.
  * Looks at the `InstrWithNotes` and `InstrWithVarAnns` meta-instructions, and blindly
    applies a series of annotations to the output stack, without caring about the underlying
    instruction.

The serializer ('Morley.Michelson.Interpret.Pack'):
  * Looks at the `InstrWithNotes` and `InstrWithVarNotes` meta-instructions, and infers
    that the original `EMPTY_SET` instruction must have had two explicit `:ta` and `@va` annotations.

Notice that the interpreter does not care about the `InstrWithVarNotes` meta-instruction, and
the serializer does not care about the `InstrWithVarAnns` meta-instruction.



Note [Annotations - Exceptional scenarios]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

For the most part, this works without a hitch.
However, `wrapWithNotes` makes the assumption that we can infer an instruction's
original annotations by simply looking at the output stack, e.g.:

> If after running an `EMPTY_SET` instruction we end up with a `@va set :ta int`
> at the top of output stack, then we can infer that the `EMPTY_SET` instruction
> had two `@va` and `:ta` annotations.

Unfortunately, that assumption doesn't always hold.
Here are some counter examples:

* Special annotations.
    These 3 `CAR` instructions will all put a `@p.a nat` at the top of the stack:

    > PUSH @p (pair (nat %a) nat) (Pair 1 2);
    > CAR @%%;

    > PUSH (pair (nat %p.a) nat) (Pair 1 2);
    > CAR @%;

    > PUSH (pair (nat %p.a) nat) (Pair 1 2);
    > CAR @p.a;

    Therefore, it's impossible for `wrapWithNotes` to figure out what
    CAR's original var annotation was.

    This scenario affects all instructions that can take special annotations:
    - PAIR, LEFT, RIGHT: accept special field anns
    - UNPAIR, CAR, CDR: accept special var anns

* Annotations that do not affect the output stack whatsoever.
    For example, CAR may take a field annotation, but it's only used by the typechecker
    to verify that the pair in the input stack has a matching field ann.

    The following instructions will generate the exact same output stack,
    with an un-annotated `nat` at the top.

    > PUSH (pair (nat %a) nat) (Pair 1 2);
    > CAR %a;

    > PUSH (pair (nat %a) nat) (Pair 1 2);
    > CAR;

    Therefore, it's impossible for `wrapWithNotes` to figure out whether
    CAR had a field annotation.

    This scenario affects: UNPAIR, CAR, CDR.


In situations like the above, where the instruction's annotations cannot be inferred from
looking at the output stack, we have to save and store the instruction's annotations inside
the typed instruction's constructor, instead of using meta-instructions.
E.g.:

> AnnCAR :: VarAnn -> FieldAnn -> Instr ('TPair a b ': s) (a ': s)

TODO [#580]: address the assumptions mentioned above.

-}

-- 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
-- >>> :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 ~ (Take (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
  , ((Take n inp) ++ s) ~ inp
  , ((Take n inp) ++ s') ~ 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
  , inp ~ (Take n inp ++ (a ': Drop ('S n) inp))
  , out ~ (a ': Take n inp ++ Drop ('S n) inp)
  )

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) =
  ( RequireLongerThan out n
  , inp ~ (a ': Drop ('S 'Z) inp)
  , out ~ (Take n (Drop ('S 'Z) inp) ++ (a ': Drop ('S n) inp))
  )

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

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

type PairN (n :: Peano) (s :: [T]) = (RightComb (Take 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) =
  ( TypeErrorUnless (n >= ToPeano 2)
      ('Text "'UNPAIR n' expects n ≥ 2")

  , TypeErrorUnless (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) =
  ( TypeErrorUnless (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) =
  ( TypeErrorUnless (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.
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 :: InstrCallStack -> 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

  -- | A wrapper for instructions that, when interpreted, will
  -- place field/type annotations on one or more of the elements at
  -- the top of the stack.
  --
  -- This can wrap only instructions with at least one non-failing execution
  -- branch.
  --
  -- See: Note [Annotations]
  InstrWithNotes
    :: forall a (topElems :: [T]) (s :: [T]).
      ( RMap topElems
      , RecordToList topElems
      , ReifyConstraint Show Notes topElems
      , ReifyConstraint NFData Notes topElems
      , Each '[ SingI ] topElems
      )
    => Proxy s -> Rec Notes topElems
    -> Instr a (topElems ++ s) -> Instr a (topElems ++ s)

  -- | A wrapper for instructions that have var annotations, e.g. `SOME_INSTR @ann1`.
  --
  -- This information is necessary for serializing the instruction back to json/binary.
  --
  -- See: Note [Annotations]
  InstrWithVarNotes :: NonEmpty VarAnn -> Instr a b -> Instr a b

  -- | A wrapper for instructions that, when interpreted, will
  -- place var annotations on one or more of the elements at
  -- the top of the stack.
  --
  -- See: Note [Annotations]
  InstrWithVarAnns :: VarAnns -> 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, KnownList b)
    => 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
  -- | Represents a typed stack function.
  -- This is not part of 'ExtInstr' because it does not behave like 'Nop';
  -- instead, it inherits the behaviour of the instruction put within it.
  Fn :: Text -> StackFn -> Instr inp out -> Instr inp out

  -- | CAR and CDR's original annotations must be retained inside
  -- the instruction's constructor.
  -- See: Note [Annotations - Exceptional scenarios].
  AnnCAR :: VarAnn -> FieldAnn -> Instr ('TPair a b ': s) (a ': s)
  AnnCDR :: 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)
  DUP :: DupableScope a => Instr (a ': s) (a ': a ': s)
  DUPN
    :: forall (n :: Peano) inp out a. (ConstraintDUPN n inp out a, DupableScope a)
    => 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
  PUSH
    :: forall t s . ConstantScope t
    => Value' Instr t -> Instr s (t ': s)
  SOME :: Instr (a ': s) ('TOption a ': s)
  NONE :: forall a s . SingI a => Instr s ('TOption a ': s)
  UNIT :: Instr s ('TUnit ': s)
  IF_NONE
    :: Instr s s'
    -> Instr (a ': s) s'
    -> Instr ('TOption a ': s) s'
  -- | PAIR's original annotations must be retained inside
  -- the instruction's constructor.
  -- See: Note [Annotations - Exceptional scenarios].
  AnnPAIR :: TypeAnn -> FieldAnn -> FieldAnn -> Instr (a ': b ': s) ('TPair a b ': s)
  -- | UNPAIR's original annotations must be retained inside
  -- the instruction's constructor.
  -- See: Note [Annotations - Exceptional scenarios].
  AnnUNPAIR :: 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:
  -- ...
  PAIRN
    :: forall n inp. ConstraintPairN n inp
    => 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)

  -- | LEFT and RIGHT's original annotations must be retained inside
  -- the instruction's constructor.
  -- See: Note [Annotations - Exceptional scenarios].
  AnnLEFT :: SingI b => TypeAnn -> FieldAnn -> FieldAnn -> Instr (a ': s) ('TOr a b ': s)
  AnnRIGHT :: SingI a => TypeAnn -> FieldAnn -> FieldAnn -> Instr (b ': s) ('TOr a b ': s)
  IF_LEFT
    :: Instr (a ': s) s'
    -> Instr (b ': s) s'
    -> Instr ('TOr a b ': s) s'
  NIL :: SingI p => Instr s ('TList p ': s)
  CONS :: Instr (a ': 'TList a ': s) ('TList a ': s)
  IF_CONS
    :: Instr (a ': 'TList a ': s) s'
    -> Instr s s'
    -> Instr ('TList a ': s) s'
  SIZE :: SizeOp c => Instr (c ': s) ('TNat ': s)
  EMPTY_SET :: (SingI e, Comparable e) => Instr s ('TSet e ': s)
  EMPTY_MAP :: (SingI a, SingI b, Comparable a) => Instr s ('TMap a b ': s)
  EMPTY_BIG_MAP :: (SingI a, SingI b, Comparable a, HasNoBigMap b) => Instr s ('TBigMap a b ': s)
  MAP :: (MapOp c, SingI b)
      => 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
  MEM :: MemOp c => Instr (MemOpKey c ': c ': s) ('TBool ': s)
  GET
    :: (GetOp c, SingI (GetOpVal c))
    => 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]
  GETN
    :: forall (ix :: Peano) (pair :: T) (s :: [T]).
       ConstraintGetN ix pair
    => PeanoNatural ix
    -> Instr (pair : s) (GetN ix pair ': s)
  UPDATE
    :: UpdOp c
    => 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]
  UPDATEN
    :: forall (ix :: Peano) (val :: T) (pair :: T) (s :: [T]).
       ConstraintUpdateN ix pair
    => PeanoNatural ix
    -> Instr (val : pair : s) (UpdateN ix val pair ': s)
  GET_AND_UPDATE
    :: ( GetOp c, UpdOp c, SingI (GetOpVal c)
       , UpdOpKey c ~ GetOpKey c
       )
    => 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)
  LAMBDA :: forall i o s . (SingI i, SingI o)
         => Value' Instr ('TLambda i o) -> Instr s ('TLambda i o ': s)
  EXEC :: Instr (t1 ': 'TLambda t1 t2 ': s) (t2 ': s)
  APPLY
    :: forall a b c s . (ConstantScope a, SingI b)
    => 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
  CAST :: forall a s . SingI a => Instr (a ': s) (a ': s)
  RENAME :: Instr (a ': s) (a ': s)
  PACK :: PackedValScope a => Instr (a ': s) ('TBytes ': s)
  UNPACK :: (UnpackedValScope a, SingI a) => Instr ('TBytes ': s) ('TOption a ': s)
  CONCAT :: ConcatOp c => Instr (c ': c ': s) (c ': s)
  CONCAT' :: ConcatOp c => Instr ('TList c ': s) (c ': s)
  SLICE
    :: (SliceOp c, SingI c)
    => Instr ('TNat ': 'TNat ': c ': s) ('TOption c ': s)
  ISNAT :: Instr ('TInt ': s) ('TOption ('TNat) ': s)
  ADD
    :: ArithOp Add n m
    => Instr (n ': m ': s) (ArithRes Add n m ': s)
  SUB
    :: ArithOp Sub n m
    => Instr (n ': m ': s) (ArithRes Sub n m ': s)
  MUL
    :: ArithOp Mul n m
    => Instr (n ':  m ': s) (ArithRes Mul n m ': s)
  EDIV
    :: ArithOp EDiv n m
    => Instr (n ':  m ': s) (ArithRes EDiv n m ': s)
  ABS
    :: UnaryArithOp Abs n
    => Instr (n ': s) (UnaryArithRes Abs n ': s)
  NEG
    :: UnaryArithOp Neg n
    => Instr (n ': s) (UnaryArithRes Neg n ': s)
  LSL
    :: ArithOp Lsl n m
    => Instr (n ': m ': s) (ArithRes Lsl n m ': s)
  LSR
    :: ArithOp Lsr n m
    => Instr (n ':  m ': s) (ArithRes Lsr n m ': s)
  OR
    :: ArithOp Or n m
    => Instr (n ': m ': s) (ArithRes Or n m ': s)
  AND
    :: ArithOp And n m
    => Instr (n ': m ': s) (ArithRes And n m ': s)
  XOR
    :: ArithOp Xor n m
    => Instr (n ': m ': s) (ArithRes Xor n m ': s)
  NOT
    :: UnaryArithOp Not n
    => Instr (n ': s) (UnaryArithRes Not n ': s)
  COMPARE
    :: (Comparable n, SingI n)
    => Instr (n ': n ': s) ('TInt ': s)
  EQ
    :: UnaryArithOp Eq' n
    => Instr (n ': s) (UnaryArithRes Eq' n ': s)
  NEQ
    :: UnaryArithOp Neq n
    => Instr (n ': s) (UnaryArithRes Neq n ': s)
  LT
    :: UnaryArithOp Lt n
    => Instr (n ': s) (UnaryArithRes Lt n ': s)
  GT
    :: UnaryArithOp Gt n
    => Instr (n ': s) (UnaryArithRes Gt n ': s)
  LE
    :: UnaryArithOp Le n
    => Instr (n ': s) (UnaryArithRes Le n ': s)
  GE
    :: UnaryArithOp Ge n
    => Instr (n ': s) (UnaryArithRes Ge n ': s)
  INT
    :: ToIntArithOp n
    => Instr (n ': s) ('TInt ': s)
  VIEW
       -- Here really only the return type is constrainted
       -- because it is given explicitly
    :: (SingI arg, ViewableScope ret)
    => ViewName
    -> Notes ret
    -> Instr (arg ': 'TAddress ': s) ('TOption ret ': s)
  SELF
    :: forall (arg :: T) s .
       (ParameterScope arg)
    => SomeEntrypointCallT arg
    -> Instr s ('TContract arg ': s)
  CONTRACT
    :: (ParameterScope p)
    => Notes p   -- Store Notes to be able to verify CONTRACT in typechecker
    -> EpName
    -> Instr ('TAddress ': s) ('TOption ('TContract p) ': s)
  TRANSFER_TOKENS
    :: (ParameterScope p) =>
       Instr (p ': 'TMutez ': 'TContract p ': s)
                   ('TOperation ': s)
  SET_DELEGATE
    :: Instr ('TOption 'TKeyHash ': s) ('TOperation ': s)

  CREATE_CONTRACT
    :: (ParameterScope p, StorageScope g)
    => Contract' Instr p g
    -> Instr ('TOption 'TKeyHash ':
              'TMutez ':
               g ': s)
             ('TOperation ': 'TAddress ': s)
  IMPLICIT_ACCOUNT
    :: Instr ('TKeyHash ': s) ('TContract 'TUnit ': s)
  NOW :: Instr s ('TTimestamp ': s)
  AMOUNT :: Instr s ('TMutez ': s)
  BALANCE :: Instr s ('TMutez ': s)
  VOTING_POWER :: Instr ('TKeyHash ': s) ('TNat ': s)
  TOTAL_VOTING_POWER :: Instr s ('TNat ': s)
  CHECK_SIGNATURE
    :: Instr ('TKey ': 'TSignature ': 'TBytes ': s)
                   ('TBool ': s)
  SHA256 :: Instr ('TBytes ': s) ('TBytes ': s)
  SHA512 :: Instr ('TBytes ': s) ('TBytes ': s)
  BLAKE2B :: Instr ('TBytes ': s) ('TBytes ': s)
  SHA3 :: Instr ('TBytes ': s) ('TBytes ': s)
  KECCAK :: Instr ('TBytes ': s) ('TBytes ': s)
  HASH_KEY :: Instr ('TKey ': s) ('TKeyHash ': s)
  PAIRING_CHECK
    :: Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) ': s) ('TBool ': s)
  SOURCE :: Instr s ('TAddress ': s)
  SENDER :: Instr s ('TAddress ': s)
  ADDRESS :: Instr ('TContract a ': s) ('TAddress ': s)
  CHAIN_ID :: Instr s ('TChainId ': s)
  LEVEL :: Instr s ('TNat ': s)
  SELF_ADDRESS :: Instr s ('TAddress ': s)
  NEVER :: Instr ('TNever ': s) t
  TICKET
    :: (Comparable a)
    => Instr (a ': 'TNat ': s) ('TTicket a ': s)
  READ_TICKET
    :: Instr ('TTicket a ': s)
             (RightComb ['TAddress, a, 'TNat] ': 'TTicket a ': s)
  SPLIT_TICKET
    :: Instr ('TTicket a ': 'TPair 'TNat 'TNat ': s)
             ('TOption ('TPair ('TTicket a) ('TTicket a)) ': s)
  JOIN_TICKETS
    :: Instr ('TPair ('TTicket a) ('TTicket a) ': s)
             ('TOption ('TTicket a) ': s)
  OPEN_CHEST
    :: Instr ('TChestKey ': 'TChest ': 'TNat ': s)
             ('TOr 'TBytes 'TBool ': s)

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'.
--
-- >>> show (DROP :# UNIT :# Nop) == 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

-- We have to write down pattern like this because simple
-- @Instr (TPair a b : s) (a : s)@ signature would assume that we /expect/
-- the input stack to have pair on top, but we want to /provide/ this info
-- in scope of a pattern-match.
-- In pattern declaration we have to write down the two mentioned constraints
-- explicitly.
--
-- Note that internally GADT constructors are rewritten in the very same way.
pattern CAR :: () => (i ~ ('TPair a b : s), o ~ (a : s)) => Instr i o
pattern CAR = AnnCAR (UnsafeAnnotation "") (UnsafeAnnotation "")

pattern CDR :: () => (i ~ ('TPair a b : s), o ~ (b : s)) => Instr i o
pattern CDR = AnnCDR (UnsafeAnnotation "") (UnsafeAnnotation "")

pattern UNPAIR :: () => (i ~ ('TPair a b : s), o ~ (a : b : s)) => Instr i o
pattern UNPAIR = AnnUNPAIR (UnsafeAnnotation "") (UnsafeAnnotation "") (UnsafeAnnotation "") (UnsafeAnnotation "")

pattern PAIR :: () => (i ~ (a ': b ': s), o ~ ('TPair a b ': s)) => Instr i o
pattern PAIR = AnnPAIR (UnsafeAnnotation "") (UnsafeAnnotation "") (UnsafeAnnotation "")

pattern LEFT :: () => (SingI b, i ~ (a ': s), o ~ ('TOr a b ': s)) => Instr i o
pattern LEFT = AnnLEFT (UnsafeAnnotation "") (UnsafeAnnotation "") (UnsafeAnnotation "")

pattern RIGHT :: () => (SingI a, i ~ (b ': s), o ~ ('TOr a b ': s)) => Instr i o
pattern RIGHT = AnnRIGHT (UnsafeAnnotation "") (UnsafeAnnotation "") (UnsafeAnnotation "")

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

deriving stock instance Show (TestAssert s)
instance NFData (TestAssert s) where
  rnf (TestAssert a b c) = rnf (a, b, c)

-- | 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
  show (StackRef snat) = "StackRef {" +|| fromPeanoNatural snat ||+ "}"

-- | Create a stack reference, performing checks at compile time.
mkStackRef
  :: forall (gn :: GHC.Nat) st n.
      (n ~ ToPeano gn, SingI (ToPeano 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)

instance NFData (ExtInstr s)

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

$(deriveGADTNFData ''Instr)