{-# LANGUAGE DerivingStrategies #-}
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
data Instr (inp :: [T]) (out :: [T]) where
Seq :: Instr a b -> Instr b c -> Instr a c
Nop :: Instr s s
Ext :: ExtInstr s -> Instr s s
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)
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)
data StackRef (st :: [T]) where
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 ||+ "}"
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)
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)