{-# LANGUAGE DerivingStrategies #-}

-- | Module, containing data types for Michelson value.

module Michelson.Typed.Instr
  ( Instr (..)
  , ExtInstr (..)
  , StackRef (..)
  , mkStackRef
  , PrintComment (..)
  , TestAssert (..)
  , Contract
  ) where

import Data.Singletons (SingI(..))
import Fmt ((+||), (||+))
import qualified Text.Show

import Michelson.Typed.Annotation (Notes)
import Michelson.Typed.Arith
import Michelson.Typed.Polymorphic
import Michelson.Typed.Scope
import Michelson.Typed.T (CT(..), T(..))
import Michelson.Typed.Value (ContractInp, ContractOut, Value'(..))
import Util.Peano

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

  DROP :: Instr (a ': s) s
  DUP  :: Instr (a ': s) (a ': a ': s)
  SWAP :: Instr (a ': b ': s) (b ': a ': s)
  PUSH
    :: forall t s . (SingI t, HasNoOp t, HasNoBigMap 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 :: Instr (a ': b ': s) ('TPair a b ': s)
  CAR :: Instr ('TPair a b ': s) (a ': s)
  CDR :: Instr ('TPair a b ': s) (b ': s)
  LEFT :: forall b a s . SingI b => Instr (a ': s) ('TOr a b ': s)
  RIGHT :: forall a b s . SingI a => 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) ('Tc 'CNat ': s)
  EMPTY_SET :: (Typeable e, SingI e) => Instr s ('TSet e ': s)
  EMPTY_MAP :: (Typeable a, Typeable b, SingI a, SingI b) => Instr s ('TMap a b ': s)
  MAP :: MapOp c
      => 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 ('Tc (MemOpKey c) ': c ': s) ('Tc 'CBool ': s)
  GET
    :: GetOp c
    => Instr ('Tc (GetOpKey c) ': c ': s) ('TOption (GetOpVal c) ': s)
  UPDATE
    :: UpdOp c
    => Instr ('Tc (UpdOpKey c) ': UpdOpParams c ': c ': s) (c ': s)
  IF :: Instr s s'
     -> Instr s s'
     -> Instr ('Tc 'CBool ': s) s'
  LOOP :: Instr s ('Tc 'CBool ': s)
       -> Instr ('Tc 'CBool ': s) s
  LOOP_LEFT
    :: Instr (a ': s) ('TOr a b ': s)
    -> Instr ('TOr a b ': s) (b ': s)
  LAMBDA :: forall i o s . (Each [Typeable, SingI] [i, o])
         => Value' Instr ('TLambda i o) -> Instr s ('TLambda i o ': s)
  EXEC :: Instr (t1 ': 'TLambda t1 t2 ': s) (t2 ': s)
  DIP :: Instr a c -> Instr (b ': a) (b ': c)
  FAILWITH :: (Typeable a, SingI a) => Instr (a ': s) t
  CAST :: forall a s . SingI a => Instr (a ': s) (a ': s)
  RENAME :: Instr (a ': s) (a ': s)
  PACK :: (SingI a, HasNoOp a, HasNoBigMap a) => Instr (a ': s) ('Tc 'CBytes ': s)
  UNPACK :: (SingI a, HasNoOp a, HasNoBigMap a) => Instr ('Tc 'CBytes ': 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
    => Instr ('Tc 'CNat ': 'Tc 'CNat ': c ': s) ('TOption c ': s)
  ISNAT :: Instr ('Tc 'CInt ': s) ('TOption ('Tc 'CNat) ': s)
  ADD
    :: (ArithOp Add n m, Typeable n, Typeable m)
    => Instr ('Tc n ': 'Tc m ': s) ('Tc (ArithRes Add n m) ': s)
  SUB
    :: (ArithOp Sub n m, Typeable n, Typeable m)
    => Instr ('Tc n ': 'Tc m ': s) ('Tc (ArithRes Sub n m) ': s)
  MUL
    :: (ArithOp Mul n m, Typeable n, Typeable m)
    => Instr ('Tc n ': 'Tc m ': s) ('Tc (ArithRes Mul n m) ': s)
  EDIV
    :: EDivOp n m
    => Instr ('Tc n ': 'Tc m ': s)
                 (('TOption ('TPair ('Tc (EDivOpRes n m))
                                      ('Tc (EModOpRes n m)))) ': s)
  ABS
    :: UnaryArithOp Abs n
    => Instr ('Tc n ': s) ('Tc (UnaryArithRes Abs n) ': s)
  NEG
    :: UnaryArithOp Neg n
    => Instr ('Tc n ': s) ('Tc (UnaryArithRes Neg n) ': s)
  LSL
    :: (ArithOp Lsl n m, Typeable n, Typeable m)
    => Instr ('Tc n ': 'Tc m ': s) ('Tc (ArithRes Lsl n m) ': s)
  LSR
    :: (ArithOp Lsr n m, Typeable n, Typeable m)
    => Instr ('Tc n ': 'Tc m ': s) ('Tc (ArithRes Lsr n m) ': s)
  OR
    :: (ArithOp Or n m, Typeable n, Typeable m)
    => Instr ('Tc n ': 'Tc m ': s) ('Tc (ArithRes Or n m) ': s)
  AND
    :: (ArithOp And n m, Typeable n, Typeable m)
    => Instr ('Tc n ': 'Tc m ': s) ('Tc (ArithRes And n m) ': s)
  XOR
    :: (ArithOp Xor n m, Typeable n, Typeable m)
    => Instr ('Tc n ': 'Tc m ': s) ('Tc (ArithRes Xor n m) ': s)
  NOT
    :: UnaryArithOp Not n
    => Instr ('Tc n ': s) ('Tc (UnaryArithRes Not n) ': s)
  COMPARE
    :: (ArithOp Compare n m, Typeable n, Typeable m)
    => Instr ('Tc n ': 'Tc m ': s) ('Tc (ArithRes Compare n m) ': s)
  EQ
    :: UnaryArithOp Eq' n
    => Instr ('Tc n ': s) ('Tc (UnaryArithRes Eq' n) ': s)
  NEQ
    :: UnaryArithOp Neq n
    => Instr ('Tc n ': s) ('Tc (UnaryArithRes Neq n) ': s)
  LT
    :: UnaryArithOp Lt n
    => Instr ('Tc n ': s) ('Tc (UnaryArithRes Lt n) ': s)
  GT
    :: UnaryArithOp Gt n
    => Instr ('Tc n ': s) ('Tc (UnaryArithRes Gt n) ': s)
  LE
    :: UnaryArithOp Le n
    => Instr ('Tc n ': s) ('Tc (UnaryArithRes Le n) ': s)
  GE
    :: UnaryArithOp Ge n
    => Instr ('Tc n ': s) ('Tc (UnaryArithRes Ge n) ': s)
  INT :: Instr ('Tc 'CNat ': s) ('Tc 'CInt ': s)
  SELF :: forall (cp :: T) s . Instr s ('TContract cp ': s)
  CONTRACT
    :: (SingI p, Typeable p) => Notes p -> Instr ('Tc 'CAddress ': s) ('TOption ('TContract p) ': s)
  -- Store Notes to be able to verify CONTRACT in typechecker
  TRANSFER_TOKENS
    :: (Typeable p, SingI p, HasNoOp p, HasNoBigMap p) =>
       Instr (p ': 'Tc 'CMutez ': 'TContract p ': s)
                   ('TOperation ': s)
  SET_DELEGATE
    :: Instr ('TOption ('Tc 'CKeyHash) ': s) ('TOperation ': s)

  CREATE_ACCOUNT
    :: Instr
        ('Tc 'CKeyHash ': 'TOption ('Tc 'CKeyHash) ': 'Tc 'CBool
         ': 'Tc 'CMutez ': s) ('TOperation ': 'Tc 'CAddress ': s)

  CREATE_CONTRACT
    :: (Each [Typeable, SingI, HasNoOp] [p, g], HasNoBigMap p, BigMapConstraint g)
    => Instr '[ 'TPair p g ] '[ 'TPair ('TList 'TOperation) g ]
    -> Instr ('Tc 'CKeyHash ':
              'TOption ('Tc 'CKeyHash) ':
              'Tc 'CBool ':
              'Tc 'CBool ':
              'Tc 'CMutez ':
               g ': s)
             ('TOperation ': 'Tc 'CAddress ': s)

  IMPLICIT_ACCOUNT
    :: Instr ('Tc 'CKeyHash ': s) ('TContract 'TUnit ': s)
  NOW :: Instr s ('Tc 'CTimestamp ': s)
  AMOUNT :: Instr s ('Tc 'CMutez ': s)
  BALANCE :: Instr s ('Tc 'CMutez ': s)
  CHECK_SIGNATURE
    :: Instr ('TKey ': 'TSignature ': 'Tc 'CBytes ': s)
                   ('Tc 'CBool ': s)
  SHA256 :: Instr ('Tc 'CBytes ': s) ('Tc 'CBytes ': s)
  SHA512 :: Instr ('Tc 'CBytes ': s) ('Tc 'CBytes ': s)
  BLAKE2B :: Instr ('Tc 'CBytes ': s) ('Tc 'CBytes ': s)
  HASH_KEY :: Instr ('TKey ': s) ('Tc 'CKeyHash ': s)
  STEPS_TO_QUOTA :: Instr s ('Tc 'CNat ': s)
  SOURCE :: Instr s ('Tc 'CAddress ': s)
  SENDER :: Instr s ('Tc 'CAddress ': s)
  ADDRESS :: Instr ('TContract a ': s) ('Tc 'CAddress ': s)

deriving instance Show (Instr inp out)

---------------------------------------------------

data TestAssert (s :: [T]) where
  TestAssert
    :: (Typeable out)
    => Text
    -> PrintComment inp
    -> Instr inp ('Tc 'CBool ': out)
    -> TestAssert inp

deriving 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
    :: (KnownPeano idx, LongerThan st idx)
    => Sing (idx :: Peano) -> StackRef st

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

instance Show (StackRef st) where
  show (StackRef snat) = "StackRef {" +|| peanoVal snat ||+ "}"

-- | Create a stack reference, performing checks at compile time.
mkStackRef
  :: forall (gn :: Nat) st n.
      (n ~ ToPeano gn, SingI n, KnownPeano n, RequireLongerThan st n)
  => StackRef st
mkStackRef = requiredLongerThan @st @n $ StackRef $ sing @(ToPeano 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 IsString (PrintComment st) where
  fromString = PrintComment . one . Left . fromString

data ExtInstr s
  = TEST_ASSERT (TestAssert s)
  | PRINT (PrintComment s)
  deriving (Show)

---------------------------------------------------

type Contract cp st = Instr (ContractInp cp st) (ContractOut st)