Safe Haskell | None |
---|---|
Language | Haskell2010 |
Module, containing data types for Michelson value.
Synopsis
- data Instr (inp :: [T]) (out :: [T]) where
- WithLoc :: InstrCallStack -> Instr a b -> Instr a b
- Meta :: SomeMeta -> Instr a b -> Instr a b
- 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)
- InstrWithVarNotes :: NonEmpty VarAnn -> Instr a b -> Instr a b
- InstrWithVarAnns :: VarAnns -> Instr a b -> Instr a b
- 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 :: Instr s s
- Ext :: ExtInstr s -> Instr s s
- Nested :: Instr inp out -> Instr inp out
- DocGroup :: DocGrouping -> Instr inp out -> Instr inp out
- Fn :: Text -> StackFn -> Instr inp out -> Instr inp out
- AnnCAR :: VarAnn -> FieldAnn -> Instr ('TPair a b ': s) (a ': s)
- AnnCDR :: VarAnn -> FieldAnn -> Instr ('TPair a b ': s) (b ': s)
- 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'
- AnnPAIR :: TypeAnn -> FieldAnn -> FieldAnn -> Instr (a ': (b ': s)) ('TPair a b ': s)
- AnnUNPAIR :: VarAnn -> VarAnn -> FieldAnn -> FieldAnn -> Instr ('TPair a b ': s) (a ': (b ': s))
- PAIRN :: forall n inp. ConstraintPairN n inp => PeanoNatural n -> Instr inp (PairN n inp)
- UNPAIRN :: forall (n :: Peano) (pair :: T) (s :: [T]). ConstraintUnpairN n pair => PeanoNatural n -> Instr (pair ': s) (UnpairN n pair ++ s)
- 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)
- 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)
- 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
- 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)
- SUB_MUTEZ :: Instr ('TMutez ': ('TMutez ': s)) ('TOption 'TMutez ': 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 :: (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 -> 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)
- SAPLING_EMPTY_STATE :: Sing n -> Instr s ('TSaplingState n ': s)
- SAPLING_VERIFY_UPDATE :: Instr ('TSaplingTransaction n ': ('TSaplingState n ': s)) ('TOption ('TPair 'TInt ('TSaplingState n)) ': s)
- castInstr :: forall inp1 out1 inp2 out2. (SingI inp1, SingI out1, SingI inp2, SingI out2) => Instr inp1 out1 -> Maybe (Instr inp2 out2)
- pattern (:#) :: Instr a b -> Instr b c -> Instr a c
- data ExtInstr s
- data CommentType
- data StackRef (st :: [T]) where
- StackRef :: RequireLongerThan st idx => PeanoNatural idx -> StackRef st
- mkStackRef :: forall (gn :: Nat) st n. (n ~ ToPeano gn, SingIPeano gn, RequireLongerThan st n) => StackRef st
- newtype PrintComment (st :: [T]) = PrintComment {
- unPrintComment :: [Either Text (StackRef st)]
- data TestAssert (s :: [T]) where
- TestAssert :: Text -> PrintComment inp -> Instr inp ('TBool ': out) -> TestAssert inp
- data SomeMeta where
- pattern CAR :: () => (i ~ ('TPair a b ': s), o ~ (a ': s)) => Instr i o
- pattern CDR :: () => (i ~ ('TPair a b ': s), o ~ (b ': s)) => Instr i o
- pattern LEFT :: () => (SingI b, i ~ (a ': s), o ~ ('TOr a b ': s)) => Instr i o
- pattern PAIR :: () => (i ~ (a ': (b ': s)), o ~ ('TPair a b ': s)) => Instr i o
- pattern RIGHT :: () => (SingI a, i ~ (b ': s), o ~ ('TOr a b ': s)) => Instr i o
- pattern UNPAIR :: () => (i ~ ('TPair a b ': s), o ~ (a ': (b ': s))) => Instr i o
- type ConstraintDUPN n inp out a = ConstraintDUPN' T n inp out a
- 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 ConstraintDIPN n inp out s s' = ConstraintDIPN' T n inp out s s'
- 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 ConstraintDIG n inp out a = ConstraintDIG' T n inp out a
- type ConstraintDIG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (KnownList inp, RequireLongerThan inp n, inp ~ (Take n inp ++ (a ': Drop ('S n) inp)), out ~ (a ': (Take n inp ++ Drop ('S n) inp)))
- type ConstraintDUG n inp out a = ConstraintDUG' T n inp out a
- 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 ConstraintPairN (n :: Peano) (inp :: [T]) = (RequireLongerOrSameLength inp n, TypeErrorUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n \8805 2"))
- type PairN (n :: Peano) (s :: [T]) = RightComb (Take n s) ': Drop n s
- type family RightComb (s :: [T]) :: T where ...
- type ConstraintUnpairN (n :: Peano) (pair :: T) = (TypeErrorUnless (n >= ToPeano 2) ('Text "'UNPAIR n' expects n \8805 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)))
- type family UnpairN (n :: Peano) (s :: T) :: [T] where ...
- 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))
- type family GetN (ix :: Peano) (pair :: T) :: T where ...
- 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))
- type family UpdateN (ix :: Peano) (val :: T) (pair :: T) :: T where ...
Documentation
data Instr (inp :: [T]) (out :: [T]) where Source #
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.
WithLoc :: InstrCallStack -> Instr a b -> Instr a b | A wrapper carrying original source location of the instruction. TODO [#283]: replace this wrapper with something more clever and abstract. |
Meta :: SomeMeta -> Instr a b -> Instr a b | A wrapper allowing arbitrary user metadata to be stored by some instruction.
TODO [#689]: Use this instead of |
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, 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] |
InstrWithVarNotes :: NonEmpty VarAnn -> Instr a b -> Instr a b | 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] |
InstrWithVarAnns :: VarAnns -> 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] |
FrameInstr :: forall a b s. (KnownList a, KnownList b) => Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s) | 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 |
Seq :: Instr a b -> Instr b c -> Instr a c | |
Nop :: Instr s s | Nop operation. Missing in Michelson spec, added to parse construction like `IF {} { SWAP; DROP; }`. |
Ext :: ExtInstr s -> Instr s s | |
Nested :: Instr inp out -> Instr inp out | 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. |
DocGroup :: DocGrouping -> Instr inp out -> Instr inp out | Places documentation generated for given instruction under some group.
This is not part of |
Fn :: Text -> StackFn -> Instr inp out -> Instr inp out | Deprecated: Morley let macros are deprecated Represents a typed stack function.
This is not part of |
AnnCAR :: VarAnn -> FieldAnn -> Instr ('TPair a b ': s) (a ': s) | CAR and CDR's original annotations must be retained inside the instruction's constructor. See: Note [Annotations - Exceptional scenarios]. |
AnnCDR :: VarAnn -> FieldAnn -> Instr ('TPair a b ': s) (b ': s) | |
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' | |
AnnPAIR :: TypeAnn -> FieldAnn -> FieldAnn -> Instr (a ': (b ': s)) ('TPair a b ': s) | PAIR'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)) | UNPAIR's original annotations must be retained inside the instruction's constructor. See: Note [Annotations - Exceptional scenarios]. |
PAIRN :: forall n inp. ConstraintPairN n inp => PeanoNatural n -> Instr inp (PairN n inp) |
|
UNPAIRN :: forall (n :: Peano) (pair :: T) (s :: [T]). ConstraintUnpairN n pair => PeanoNatural n -> Instr (pair ': s) (UnpairN n pair ++ s) |
|
AnnLEFT :: SingI b => TypeAnn -> FieldAnn -> FieldAnn -> Instr (a ': s) ('TOr a b ': s) | LEFT and RIGHT's original annotations must be retained inside the instruction's constructor. See: Note [Annotations - Exceptional scenarios]. |
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) | |
GETN :: forall (ix :: Peano) (pair :: T) (s :: [T]). ConstraintGetN ix pair => PeanoNatural ix -> Instr (pair ': s) (GetN ix pair ': s) | Get the node at index For example, a pair with 3 elements pair / \ a pair / \ b c Where the nodes are numbered as follows: 0 / \ 1 2 / \ 3 4
Note that
|
UPDATE :: UpdOp c => Instr (UpdOpKey c ': (UpdOpParams c ': (c ': s))) (c ': s) | |
UPDATEN :: forall (ix :: Peano) (val :: T) (pair :: T) (s :: [T]). ConstraintUpdateN ix pair => PeanoNatural ix -> Instr (val ': (pair ': s)) (UpdateN ix val pair ': s) | Update the node at index
Note that
|
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 | |
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) | |
SUB_MUTEZ :: Instr ('TMutez ': ('TMutez ': s)) ('TOption 'TMutez ': 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 :: (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 -> 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) | |
SAPLING_EMPTY_STATE :: Sing n -> Instr s ('TSaplingState n ': s) | |
SAPLING_VERIFY_UPDATE :: Instr ('TSaplingTransaction n ': ('TSaplingState n ': s)) ('TOption ('TPair 'TInt ('TSaplingState n)) ': s) |
Instances
castInstr :: forall inp1 out1 inp2 out2. (SingI inp1, SingI out1, SingI inp2, SingI out2) => Instr inp1 out1 -> Maybe (Instr inp2 out2) Source #
pattern (:#) :: Instr a b -> Instr b c -> Instr a c infixr 8 Source #
Right-associative operator for Seq
.
>>>
Debug.show (DROP :# UNIT :# Nop) == Debug.show (DROP :# (UNIT :# Nop))
True
TEST_ASSERT (TestAssert s) | |
PRINT (PrintComment s) | |
DOC_ITEM SomeDocItem | |
COMMENT_ITEM CommentType | |
STACKTYPE StackTypePattern |
Instances
data CommentType Source #
FunctionStarts Text | |
FunctionEnds Text | |
StatementStarts Text | |
StatementEnds Text | |
JustComment Text | |
StackTypeComment (Maybe [T]) |
|
Instances
data StackRef (st :: [T]) where Source #
A reference into the stack of a given type.
StackRef :: RequireLongerThan st idx => PeanoNatural idx -> StackRef st | Keeps 0-based index to a stack element counting from the top. |
mkStackRef :: forall (gn :: Nat) st n. (n ~ ToPeano gn, SingIPeano gn, RequireLongerThan st n) => StackRef st Source #
Create a stack reference, performing checks at compile time.
newtype PrintComment (st :: [T]) Source #
A print format with references into the stack
PrintComment | |
|
Instances
data TestAssert (s :: [T]) where Source #
TestAssert :: Text -> PrintComment inp -> Instr inp ('TBool ': out) -> TestAssert inp |
Instances
SingI s => Eq (TestAssert s) Source # | |
Defined in Morley.Michelson.Typed.Convert (==) :: TestAssert s -> TestAssert s -> Bool # (/=) :: TestAssert s -> TestAssert s -> Bool # | |
Show (TestAssert s) Source # | |
Defined in Morley.Michelson.Typed.Instr showsPrec :: Int -> TestAssert s -> ShowS # show :: TestAssert s -> String # showList :: [TestAssert s] -> ShowS # | |
NFData (TestAssert s) Source # | |
Defined in Morley.Michelson.Typed.Instr rnf :: TestAssert s -> () # |
type ConstraintDUPN n inp out a = ConstraintDUPN' T n inp out a Source #
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)) Source #
Constraint that is used in DUPN, we want to share it with typechecking code and eDSL code.
type ConstraintDIPN n inp out s s' = ConstraintDIPN' T n inp out s s' Source #
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) Source #
Constraint that is used in DIPN, we want to share it with typechecking code and eDSL code.
type ConstraintDIG n inp out a = ConstraintDIG' T n inp out a Source #
type ConstraintDIG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = (KnownList inp, RequireLongerThan inp n, inp ~ (Take n inp ++ (a ': Drop ('S n) inp)), out ~ (a ': (Take n inp ++ Drop ('S n) inp))) Source #
Constraint that is used in DIG, we want to share it with typechecking code and eDSL code.
type ConstraintDUG n inp out a = ConstraintDUG' T n inp out a Source #
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))) Source #
Constraint that is used in DUG, we want to share it with typechecking code and eDSL code.
type ConstraintPairN (n :: Peano) (inp :: [T]) = (RequireLongerOrSameLength inp n, TypeErrorUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n \8805 2")) Source #
type family RightComb (s :: [T]) :: T where ... Source #
Folds a stack into a right-combed pair.
RightComb '[ 'TInt, 'TString, 'TUnit ] ~ 'TPair 'TInt ('TPair 'TString 'TUnit)
type ConstraintUnpairN (n :: Peano) (pair :: T) = (TypeErrorUnless (n >= ToPeano 2) ('Text "'UNPAIR n' expects n \8805 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))) Source #
type family UnpairN (n :: Peano) (s :: T) :: [T] where ... Source #
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 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)) Source #
type family GetN (ix :: Peano) (pair :: T) :: T where ... Source #
Get the node at index ix
of a right-combed pair.
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)) Source #