Morley.Michelson.Typed.Instr

Module, containing data types for Michelson value.

Documentation

data Instr (inp :: [T]) (out :: [T]) where

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.

Constructors

WithLoc :: ErrorSrcPos -> 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 DOC_ITEM.

FrameInstr :: forall a b s. KnownList a => 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 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.

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 ExtInstr because it does not behave like Nop; instead, it inherits the behaviour of the instruction put within it.

AnnCAR :: Anns '[VarAnn, FieldAnn] -> Instr ('TPair a b ': s) (a ': s)

AnnCDR :: Anns '[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)

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

AnnPAIRN :: forall n inp. ConstraintPairN n inp => AnnVar -> PeanoNatural n -> Instr inp (PairN n inp)

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

UNPAIRN :: forall (n :: Peano) (pair :: T) (s :: [T]). ConstraintUnpairN n pair => PeanoNatural n -> Instr (pair ': s) (UnpairN n pair ++ s)

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

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)

AnnGETN :: forall (ix :: Peano) (pair :: T) (s :: [T]). ConstraintGetN ix pair => AnnVar -> PeanoNatural ix -> Instr (pair ': s) (GetN ix pair ': 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]

AnnUPDATE :: UpdOp c => AnnVar -> Instr (UpdOpKey c ': (UpdOpParams c ': (c ': s))) (c ': s)

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)

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]

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

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 :: (SingI arg, ViewableScope ret) => Anns '[VarAnn, Notes ret] -> ViewName -> Instr (arg ': ('TAddress ': s)) ('TOption ret ': s)

AnnSELF :: forall (arg :: T) s. (ParameterScope arg, IsNotInView) => AnnVar -> SomeEntrypointCallT arg -> Instr s ('TContract arg ': 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.

AnnCONTRACT :: ParameterScope p => Anns '[VarAnn, Notes p] -> EpName -> Instr ('TAddress ': s) ('TOption ('TContract p) ': 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.

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)

Bundled Patterns

pattern CAR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) ('TPair a b) s, out ~ '(:) a s) => Instr inp out

pattern CDR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) ('TPair a b) s, out ~ '(:) b s) => Instr inp out

pattern DUP :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a ('(:) a s), DupableScope a) => Instr inp out

pattern DUPN :: forall {inp} {out}. () => forall (n :: Peano) (inp :: [T]) (out :: [T]) (a :: T). (inp ~ inp, out ~ out, ConstraintDUPN n inp out a, DupableScope a) => PeanoNatural n -> Instr inp out

pattern PUSH :: forall {inp} {out}. () => forall (t :: T) (s :: [T]). (inp ~ s, out ~ '(:) t s, ConstantScope t) => Value' Instr t -> Instr inp out

pattern SOME :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) ('TOption a) s) => Instr inp out

pattern NONE :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TOption a) s, SingI a) => Instr inp out

pattern UNIT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TUnit s) => Instr inp out

pattern PAIR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) a ('(:) b s), out ~ '(:) ('TPair a b) s) => Instr inp out

pattern UNPAIR :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) ('TPair a b) s, out ~ '(:) a ('(:) b s)) => Instr inp out

pattern PAIRN :: forall {inp} {out}. () => forall (n :: Peano) (inp :: [T]). (inp ~ inp, out ~ PairN n inp, ConstraintPairN n inp) => PeanoNatural n -> Instr inp out

pattern LEFT :: forall {inp} {out}. () => forall (b :: T) (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) ('TOr a b) s, SingI b) => Instr inp out

pattern RIGHT :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ '(:) b s, out ~ '(:) ('TOr a b) s, SingI a) => Instr inp out

pattern NIL :: forall {inp} {out}. () => forall (p :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TList p) s, SingI p) => Instr inp out

pattern CONS :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a ('(:) ('TList a) s), out ~ '(:) ('TList a) s) => Instr inp out

pattern SIZE :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) c s, out ~ '(:) 'TNat s, SizeOp c) => Instr inp out

pattern EMPTY_SET :: forall {inp} {out}. () => forall (e :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TSet e) s, SingI e, Comparable e) => Instr inp out

pattern EMPTY_MAP :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TMap a b) s, SingI a, SingI b, Comparable a) => Instr inp out

pattern EMPTY_BIG_MAP :: forall {inp} {out}. () => forall (a :: T) (b :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TBigMap a b) s, SingI a, SingI b, Comparable a, HasNoBigMap b) => Instr inp out

pattern MAP :: forall {inp} {out}. () => forall (c :: T) (b :: T) (s :: [T]). (inp ~ '(:) c s, out ~ '(:) (MapOpRes c b) s, MapOp c, SingI b) => Instr ('(:) (MapOpInp c) s) ('(:) b s) -> Instr inp out

pattern MEM :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) (MemOpKey c) ('(:) c s), out ~ '(:) 'TBool s, MemOp c) => Instr inp out

pattern GET :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) (GetOpKey c) ('(:) c s), out ~ '(:) ('TOption (GetOpVal c)) s, GetOp c, SingI (GetOpVal c)) => Instr inp out

pattern GETN :: forall {inp} {out}. () => forall (ix :: Peano) (pair :: T) (s :: [T]). (inp ~ '(:) pair s, out ~ '(:) (GetN ix pair) s, ConstraintGetN ix pair) => PeanoNatural ix -> Instr inp out

pattern UPDATE :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) (UpdOpKey c) ('(:) (UpdOpParams c) ('(:) c s)), out ~ '(:) c s, UpdOp c) => Instr inp out

pattern UPDATEN :: forall {inp} {out}. () => forall (ix :: Peano) (val :: T) (pair :: T) (s :: [T]). (inp ~ '(:) val ('(:) pair s), out ~ '(:) (UpdateN ix val pair) s, ConstraintUpdateN ix pair) => PeanoNatural ix -> Instr inp out

pattern GET_AND_UPDATE :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) (UpdOpKey c) ('(:) (UpdOpParams c) ('(:) c s)), out ~ '(:) ('TOption (GetOpVal c)) ('(:) c s), GetOp c, UpdOp c, SingI (GetOpVal c), (~) (UpdOpKey c) (GetOpKey c)) => Instr inp out

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_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 EXEC :: forall {inp} {out}. () => forall (t1 :: T) (t2 :: T) (s :: [T]). (inp ~ '(:) t1 ('(:) ('TLambda t1 t2) s), out ~ '(:) t2 s) => Instr inp out

pattern APPLY :: forall {inp} {out}. () => forall (a :: T) (b :: T) (c :: T) (s :: [T]). (inp ~ '(:) a ('(:) ('TLambda ('TPair a b) c) s), out ~ '(:) ('TLambda b c) s, ConstantScope a, SingI b) => Instr inp out

pattern CAST :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a s, SingI a) => Instr inp out

pattern RENAME :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) a s) => Instr inp out

pattern PACK :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a s, out ~ '(:) 'TBytes s, PackedValScope a) => Instr inp out

pattern UNPACK :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) ('TOption a) s, UnpackedValScope a, SingI a) => Instr inp out

pattern CONCAT :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) c ('(:) c s), out ~ '(:) c s, ConcatOp c) => Instr inp out

pattern CONCAT' :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) ('TList c) s, out ~ '(:) c s, ConcatOp c) => Instr inp out

pattern SLICE :: forall {inp} {out}. () => forall (c :: T) (s :: [T]). (inp ~ '(:) 'TNat ('(:) 'TNat ('(:) c s)), out ~ '(:) ('TOption c) s, SliceOp c, SingI c) => Instr inp out

pattern ISNAT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TInt s, out ~ '(:) ('TOption 'TNat) s) => Instr inp out

pattern ADD :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Add n m) s, ArithOp Add n m) => Instr inp out

pattern SUB :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Sub n m) s, ArithOp Sub n m) => Instr inp out

pattern SUB_MUTEZ :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TMutez ('(:) 'TMutez s), out ~ '(:) ('TOption 'TMutez) s) => Instr inp out

pattern MUL :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Mul n m) s, ArithOp Mul n m) => Instr inp out

pattern EDIV :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes EDiv n m) s, ArithOp EDiv n m) => Instr inp out

pattern ABS :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Abs n) s, UnaryArithOp Abs n) => Instr inp out

pattern NEG :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Neg n) s, UnaryArithOp Neg n) => Instr inp out

pattern LSL :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Lsl n m) s, ArithOp Lsl n m) => Instr inp out

pattern LSR :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Lsr n m) s, ArithOp Lsr n m) => Instr inp out

pattern OR :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Or n m) s, ArithOp Or n m) => Instr inp out

pattern AND :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes And n m) s, ArithOp And n m) => Instr inp out

pattern XOR :: forall {inp} {out}. () => forall (n :: T) (m :: T) (s :: [T]). (inp ~ '(:) n ('(:) m s), out ~ '(:) (ArithRes Xor n m) s, ArithOp Xor n m) => Instr inp out

pattern NOT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Not n) s, UnaryArithOp Not n) => Instr inp out

pattern COMPARE :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n ('(:) n s), out ~ '(:) 'TInt s, Comparable n, SingI n) => Instr inp out

pattern EQ :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Eq' n) s, UnaryArithOp Eq' n) => Instr inp out

pattern NEQ :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Neq n) s, UnaryArithOp Neq n) => Instr inp out

pattern LT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Lt n) s, UnaryArithOp Lt n) => Instr inp out

pattern GT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Gt n) s, UnaryArithOp Gt n) => Instr inp out

pattern LE :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Le n) s, UnaryArithOp Le n) => Instr inp out

pattern GE :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) (UnaryArithRes Ge n) s, UnaryArithOp Ge n) => Instr inp out

pattern INT :: forall {inp} {out}. () => forall (n :: T) (s :: [T]). (inp ~ '(:) n s, out ~ '(:) 'TInt s, ToIntArithOp n) => Instr inp out

pattern VIEW :: forall {inp} {out}. () => forall (arg :: T) (ret :: T) (s :: [T]). (inp ~ '(:) arg ('(:) 'TAddress s), out ~ '(:) ('TOption ret) s, SingI arg, ViewableScope ret) => ViewName -> Instr inp out

pattern SELF :: forall {inp} {out}. () => forall (arg :: T) (s :: [T]). (inp ~ s, out ~ '(:) ('TContract arg) s, ParameterScope arg, IsNotInView) => SomeEntrypointCallT arg -> Instr inp out

pattern CONTRACT :: forall {inp} {out}. () => forall (p :: T) (s :: [T]). (inp ~ '(:) 'TAddress s, out ~ '(:) ('TOption ('TContract p)) s, ParameterScope p) => EpName -> Instr inp out

pattern TRANSFER_TOKENS :: forall {inp} {out}. () => forall (p :: T) (s :: [T]). (inp ~ '(:) p ('(:) 'TMutez ('(:) ('TContract p) s)), out ~ '(:) 'TOperation s, ParameterScope p, IsNotInView) => Instr inp out

pattern SET_DELEGATE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) ('TOption 'TKeyHash) s, out ~ '(:) 'TOperation s, IsNotInView) => Instr inp out

pattern CREATE_CONTRACT :: forall {inp} {out}. () => forall (p :: T) (g :: T) (s :: [T]). (inp ~ '(:) ('TOption 'TKeyHash) ('(:) 'TMutez ('(:) g s)), out ~ '(:) 'TOperation ('(:) 'TAddress s), ParameterScope p, StorageScope g, IsNotInView) => Contract' Instr p g -> Instr inp out

pattern IMPLICIT_ACCOUNT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKeyHash s, out ~ '(:) ('TContract 'TUnit) s) => Instr inp out

pattern NOW :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TTimestamp s) => Instr inp out

pattern AMOUNT :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TMutez s) => Instr inp out

pattern BALANCE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TMutez s) => Instr inp out

pattern VOTING_POWER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKeyHash s, out ~ '(:) 'TNat s) => Instr inp out

pattern TOTAL_VOTING_POWER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat s) => Instr inp out

pattern CHECK_SIGNATURE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKey ('(:) 'TSignature ('(:) 'TBytes s)), out ~ '(:) 'TBool s) => Instr inp out

pattern SHA256 :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out

pattern SHA512 :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out

pattern BLAKE2B :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out

pattern SHA3 :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out

pattern KECCAK :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TBytes s, out ~ '(:) 'TBytes s) => Instr inp out

pattern HASH_KEY :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TKey s, out ~ '(:) 'TKeyHash s) => Instr inp out

pattern PAIRING_CHECK :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) ('TList ('TPair 'TBls12381G1 'TBls12381G2)) s, out ~ '(:) 'TBool s) => Instr inp out

pattern SOURCE :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress s) => Instr inp out

pattern SENDER :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress s) => Instr inp out

pattern ADDRESS :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) ('TContract a) s, out ~ '(:) 'TAddress s) => Instr inp out

pattern CHAIN_ID :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TChainId s) => Instr inp out

pattern LEVEL :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat s) => Instr inp out

pattern SELF_ADDRESS :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TAddress s) => Instr inp out

pattern TICKET :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a ('(:) 'TNat s), out ~ '(:) ('TOption ('TTicket a)) s, Comparable a) => Instr inp out

pattern TICKET_DEPRECATED :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) a ('(:) 'TNat s), out ~ '(:) ('TTicket a) s, Comparable a) => Instr inp out

pattern READ_TICKET :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) ('TTicket a) s, out ~ '(:) (RightComb ('(:) 'TAddress ('(:) a ('(:) 'TNat ('[] :: [T]))))) ('(:) ('TTicket a) s)) => Instr inp out

pattern SPLIT_TICKET :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) ('TTicket a) ('(:) ('TPair 'TNat 'TNat) s), out ~ '(:) ('TOption ('TPair ('TTicket a) ('TTicket a))) s) => Instr inp out

pattern JOIN_TICKETS :: forall {inp} {out}. () => forall (a :: T) (s :: [T]). (inp ~ '(:) ('TPair ('TTicket a) ('TTicket a)) s, out ~ '(:) ('TOption ('TTicket a)) s) => Instr inp out

pattern OPEN_CHEST :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ '(:) 'TChestKey ('(:) 'TChest ('(:) 'TNat s)), out ~ '(:) ('TOr 'TBytes 'TBool) s) => Instr inp out

Deprecated: Due to a vulnerability discovered in time-lock protocol, OPEN_CHEST is temporarily deprecated since Lima

pattern SAPLING_EMPTY_STATE :: forall {inp} {out}. () => forall (n :: Peano) (s :: [T]). (inp ~ s, out ~ '(:) ('TSaplingState n) s) => Sing n -> Instr inp out

pattern SAPLING_VERIFY_UPDATE :: forall {inp} {out}. () => forall (n :: Peano) (s :: [T]). (inp ~ '(:) ('TSaplingTransaction n) ('(:) ('TSaplingState n) s), out ~ '(:) ('TOption ('TPair 'TBytes ('TPair 'TInt ('TSaplingState n)))) s) => Instr inp out

pattern MIN_BLOCK_TIME :: forall {inp} {out}. () => forall (s :: [T]). (inp ~ s, out ~ '(:) 'TNat s) => Instr inp out

pattern EMIT :: forall {inp} {out}. () => forall (t :: T) (s :: [T]). (inp ~ '(:) t s, out ~ '(:) 'TOperation s, PackedValScope t) => FieldAnn -> Maybe (Notes t) -> Instr inp out

Instances

HasRPCRepr Operation

Defined in Morley.AsRPC

Associated Types

type AsRPC Operation

WithClassifiedInstr Instr

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.WithClassifiedInstr

Associated Types

type WCIConstraint Instr cls'

Methods

withClassifiedInstr :: forall t (inp :: [T]) (out :: [T]) r. ClassifyInstr t => (forall (cls :: InstrClass). (SingI cls, WCIConstraint Instr cls) => Sing (GetClassified cls) -> ClassifiedInstr cls inp out -> r) -> Instr inp out -> r

TypeHasDoc Operation

Defined in Morley.Michelson.Typed.Haskell.Doc

Associated Types

type TypeDocFieldDescriptions Operation :: FieldDescriptions

Methods

typeDocName :: Proxy Operation -> Text

typeDocMdDescription :: Markdown

typeDocMdReference :: Proxy Operation -> WithinParens -> Markdown

typeDocDependencies :: Proxy Operation -> [SomeDocDefinitionItem]

typeDocHaskellRep :: TypeDocHaskellRep Operation

typeDocMichelsonRep :: TypeDocMichelsonRep Operation

IsoValue Operation

Defined in Morley.Michelson.Typed.Haskell.Value

Associated Types

type ToT Operation :: T

Methods

toVal :: Operation -> Value (ToT Operation)

fromVal :: Value (ToT Operation) -> Operation

(FromExp x Value, SingI t) => FromExp x (Value t)

Defined in Morley.Micheline.Class

Methods

fromExp :: Exp x -> Either (FromExpError x) (Value t)

(SingI inp, SingI out) => FromExp RegularExp (Instr '[inp] '[out])

Defined in Morley.Micheline.Class

Methods

fromExp :: Exp RegularExp -> Either (FromExpError RegularExp) (Instr '[inp] '[out])

HasRPCRepr (Value t)

Defined in Morley.AsRPC

Associated Types

type AsRPC (Value t)

HasNoOp t => ToExpression (Value t)

Defined in Morley.Micheline.Class

Methods

toExpression :: Value t -> Expression

(forall (t :: T). cs t => HasNoOp t) => RenderDoc (SomeConstrainedValue cs)

Defined in Morley.Michelson.Typed.Existential

Methods

renderDoc :: RenderContext -> SomeConstrainedValue cs -> Doc

isRenderable :: SomeConstrainedValue cs -> Bool

WellTyped t => IsoValue (Value t)

Defined in Morley.Michelson.Typed.Haskell.Value

Associated Types

type ToT (Value t) :: T

Methods

toVal :: Value t -> Value (ToT (Value t))

fromVal :: Value (ToT (Value t)) -> Value t

Monoid (Instr s s)

Defined in Morley.Michelson.Typed.Instr

Methods

mempty :: Instr s s

mappend :: Instr s s -> Instr s s -> Instr s s

mconcat :: [Instr s s] -> Instr s s

Semigroup (Instr s s)

Defined in Morley.Michelson.Typed.Instr

Methods

(<>) :: Instr s s -> Instr s s -> Instr s s

sconcat :: NonEmpty (Instr s s) -> Instr s s

stimes :: Integral b => b -> Instr s s -> Instr s s

Show (Instr inp out)

Defined in Morley.Michelson.Typed.Instr

Methods

showsPrec :: Int -> Instr inp out -> ShowS

show :: Instr inp out -> String

showList :: [Instr inp out] -> ShowS

NFData (Instr inp out)

Defined in Morley.Michelson.Typed.Instr

Methods

rnf :: Instr inp out -> ()

Buildable (Instr inp out)

Defined in Morley.Michelson.Typed.Convert

Methods

build :: Instr inp out -> Builder

Buildable (Value' Instr t)

Defined in Morley.Michelson.Typed.Convert

Methods

build :: Value' Instr t -> Builder

Eq (Instr inp out)

Defined in Morley.Michelson.Typed.Convert

Methods

(==) :: Instr inp out -> Instr inp out -> Bool

(/=) :: Instr inp out -> Instr inp out -> Bool

ToExpression (Contract cp st)

Defined in Morley.Micheline.Class

Methods

toExpression :: Contract cp st -> Expression

ToExpression (Instr inp out)

Defined in Morley.Micheline.Class

Methods

toExpression :: Instr inp out -> Expression

ContainsDoc (Contract cp st)

Defined in Morley.Michelson.Typed.Doc

Methods

buildDocUnfinalized :: Contract cp st -> ContractDoc

ContainsDoc (ContractCode inp out)

Defined in Morley.Michelson.Typed.Doc

Methods

buildDocUnfinalized :: ContractCode inp out -> ContractDoc

ContainsDoc (Instr inp out)

Defined in Morley.Michelson.Typed.Doc

Methods

buildDocUnfinalized :: Instr inp out -> ContractDoc

ContainsUpdateableDoc (Contract cp st)

Defined in Morley.Michelson.Typed.Doc

Methods

modifyDocEntirely :: (SomeDocItem -> SomeDocItem) -> Contract cp st -> Contract cp st

ContainsUpdateableDoc (ContractCode inp out)

Defined in Morley.Michelson.Typed.Doc

Methods

modifyDocEntirely :: (SomeDocItem -> SomeDocItem) -> ContractCode inp out -> ContractCode inp out

ContainsUpdateableDoc (Instr inp out)

Defined in Morley.Michelson.Typed.Doc

Methods

modifyDocEntirely :: (SomeDocItem -> SomeDocItem) -> Instr inp out -> Instr inp out

RenderDoc (Instr inp out)

Defined in Morley.Michelson.Typed.Convert

Methods

renderDoc :: RenderContext -> Instr inp out -> Doc

isRenderable :: Instr inp out -> Bool

HasNoOp t => RenderDoc (Value' Instr t)

Defined in Morley.Michelson.Typed.Convert

Methods

renderDoc :: RenderContext -> Value' Instr t -> Doc

isRenderable :: Value' Instr t -> Bool

type AsRPC Operation

Defined in Morley.AsRPC

type AsRPC Operation = Operation

type TypeDocFieldDescriptions Operation

Defined in Morley.Michelson.Typed.Haskell.Doc

type TypeDocFieldDescriptions Operation = '[] :: [(Symbol, (Maybe Symbol, [(Symbol, Symbol)]))]

type ToT Operation

Defined in Morley.Michelson.Typed.Haskell.Value

type ToT Operation = 'TOperation

type WCIConstraint Instr _1

Defined in Morley.Michelson.Typed.ClassifiedInstr.Internal.WithClassifiedInstr

type WCIConstraint Instr _1 = ()

type AsRPC (Value t)

Defined in Morley.AsRPC

type AsRPC (Value t) = Value (TAsRPC t)

type ToT (Value t)

Defined in Morley.Michelson.Typed.Haskell.Value

type ToT (Value t) = t

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

Right-associative operator for Seq.

>>> Debug.show (DROP :# UNIT :# Nop) == Debug.show (DROP :# (UNIT :# Nop))
True

data ExtInstr s

Constructors

TEST_ASSERT (TestAssert s)

PRINT (PrintComment s)

DOC_ITEM SomeDocItem

COMMENT_ITEM CommentType

STACKTYPE StackTypePattern

Instances

Generic (ExtInstr s)

Defined in Morley.Michelson.Typed.Instr

Associated Types

type Rep (ExtInstr s) :: Type -> Type

Methods

from :: ExtInstr s -> Rep (ExtInstr s) x

to :: Rep (ExtInstr s) x -> ExtInstr s

Show (ExtInstr s)

Defined in Morley.Michelson.Typed.Instr

Methods

showsPrec :: Int -> ExtInstr s -> ShowS

show :: ExtInstr s -> String

showList :: [ExtInstr s] -> ShowS

NFData (ExtInstr s)

Defined in Morley.Michelson.Typed.Instr

Methods

rnf :: ExtInstr s -> ()

type Rep (ExtInstr s)

Defined in Morley.Michelson.Typed.Instr

type Rep (ExtInstr s) = D1 ('MetaData "ExtInstr" "Morley.Michelson.Typed.Instr" "morley-1.19.0-inplace" 'False) ((C1 ('MetaCons "TEST_ASSERT" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (TestAssert s))) :+: C1 ('MetaCons "PRINT" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (PrintComment s)))) :+: (C1 ('MetaCons "DOC_ITEM" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 SomeDocItem)) :+: (C1 ('MetaCons "COMMENT_ITEM" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 CommentType)) :+: C1 ('MetaCons "STACKTYPE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 StackTypePattern)))))

data CommentType

Constructors

FunctionStarts Text

FunctionEnds Text

StatementStarts Text

StatementEnds Text

JustComment Text

StackTypeComment (Maybe [T])

Nothing for any stack type

Instances

IsString CommentType

Defined in Morley.Michelson.Typed.Instr

Methods

fromString :: String -> CommentType

Generic CommentType

Defined in Morley.Michelson.Typed.Instr

Associated Types

type Rep CommentType :: Type -> Type

Methods

from :: CommentType -> Rep CommentType x

to :: Rep CommentType x -> CommentType

Show CommentType

Defined in Morley.Michelson.Typed.Instr

Methods

showsPrec :: Int -> CommentType -> ShowS

show :: CommentType -> String

showList :: [CommentType] -> ShowS

NFData CommentType

Defined in Morley.Michelson.Typed.Instr

Methods

rnf :: CommentType -> ()

type Rep CommentType

Defined in Morley.Michelson.Typed.Instr

type Rep CommentType = D1 ('MetaData "CommentType" "Morley.Michelson.Typed.Instr" "morley-1.19.0-inplace" 'False) ((C1 ('MetaCons "FunctionStarts" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Text)) :+: (C1 ('MetaCons "FunctionEnds" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Text)) :+: C1 ('MetaCons "StatementStarts" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Text)))) :+: (C1 ('MetaCons "StatementEnds" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Text)) :+: (C1 ('MetaCons "JustComment" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Text)) :+: C1 ('MetaCons "StackTypeComment" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Maybe [T]))))))

data StackRef (st :: [T]) where

A reference into the stack of a given type.

Constructors

StackRef :: RequireLongerThan st idx => PeanoNatural idx -> StackRef st

Keeps 0-based index to a stack element counting from the top.

Instances

Show (StackRef st)

Defined in Morley.Michelson.Typed.Instr

Methods

showsPrec :: Int -> StackRef st -> ShowS

show :: StackRef st -> String

showList :: [StackRef st] -> ShowS

NFData (StackRef st)

Defined in Morley.Michelson.Typed.Instr

Methods

rnf :: StackRef st -> ()

Buildable (StackRef st)

Defined in Morley.Michelson.Typed.Instr

Methods

build :: StackRef st -> Builder

Eq (StackRef st)

Defined in Morley.Michelson.Typed.Instr

Methods

(==) :: StackRef st -> StackRef st -> Bool

(/=) :: StackRef st -> StackRef st -> Bool

mkStackRef :: forall (gn :: Nat) st n. (n ~ ToPeano gn, SingIPeano gn, RequireLongerThan st n) => StackRef st

Create a stack reference, performing checks at compile time.

newtype PrintComment (st :: [T])

A print format with references into the stack

Constructors

PrintComment

Fields

• unPrintComment :: [Either Text (StackRef st)]

Instances

IsString (PrintComment st)

Defined in Morley.Michelson.Typed.Instr

Methods

fromString :: String -> PrintComment st

Monoid (PrintComment st)

Defined in Morley.Michelson.Typed.Instr

Methods

mempty :: PrintComment st

mappend :: PrintComment st -> PrintComment st -> PrintComment st

mconcat :: [PrintComment st] -> PrintComment st

Semigroup (PrintComment st)

Defined in Morley.Michelson.Typed.Instr

Methods

(<>) :: PrintComment st -> PrintComment st -> PrintComment st

sconcat :: NonEmpty (PrintComment st) -> PrintComment st

stimes :: Integral b => b -> PrintComment st -> PrintComment st

Generic (PrintComment st)

Defined in Morley.Michelson.Typed.Instr

Associated Types

type Rep (PrintComment st) :: Type -> Type

Methods

from :: PrintComment st -> Rep (PrintComment st) x

to :: Rep (PrintComment st) x -> PrintComment st

Show (PrintComment st)

Defined in Morley.Michelson.Typed.Instr

Methods

showsPrec :: Int -> PrintComment st -> ShowS

show :: PrintComment st -> String

showList :: [PrintComment st] -> ShowS

NFData (PrintComment st)

Defined in Morley.Michelson.Typed.Instr

Methods

rnf :: PrintComment st -> ()

Eq (PrintComment st)

Defined in Morley.Michelson.Typed.Instr

Methods

(==) :: PrintComment st -> PrintComment st -> Bool

(/=) :: PrintComment st -> PrintComment st -> Bool

type Rep (PrintComment st)

Defined in Morley.Michelson.Typed.Instr

type Rep (PrintComment st) = D1 ('MetaData "PrintComment" "Morley.Michelson.Typed.Instr" "morley-1.19.0-inplace" 'True) (C1 ('MetaCons "PrintComment" 'PrefixI 'True) (S1 ('MetaSel ('Just "unPrintComment") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Either Text (StackRef st)])))

data TestAssert (s :: [T]) where

Constructors

TestAssert :: Text -> PrintComment inp -> Instr inp ('TBool ': out) -> TestAssert inp

Instances

Show (TestAssert s)

Defined in Morley.Michelson.Typed.Instr

Methods

showsPrec :: Int -> TestAssert s -> ShowS

show :: TestAssert s -> String

showList :: [TestAssert s] -> ShowS

NFData (TestAssert s)

Defined in Morley.Michelson.Typed.Instr

Methods

rnf :: TestAssert s -> ()

SingI s => Eq (TestAssert s)

Defined in Morley.Michelson.Typed.Convert

Methods

(==) :: TestAssert s -> TestAssert s -> Bool

(/=) :: TestAssert s -> TestAssert s -> Bool

data SomeMeta where

Constructors

SomeMeta :: forall meta. With [NFData, Show, Typeable] meta => meta -> SomeMeta

Instances

Show SomeMeta

Defined in Morley.Michelson.Typed.Instr

Methods

showsPrec :: Int -> SomeMeta -> ShowS

show :: SomeMeta -> String

showList :: [SomeMeta] -> ShowS

NFData SomeMeta

Defined in Morley.Michelson.Typed.Instr

Methods

rnf :: SomeMeta -> ()

pattern ConcreteMeta :: Typeable meta => meta -> Instr i o -> Instr i o

A convenience pattern synonym for Meta, matching on a concrete given type wrapped by SomeMeta, e.g.

\case { ContreteMeta (x :: Word) -> ... }

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

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'

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)

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

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

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

type ConstraintDUG' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = ConstraintDIG' kind n out inp a

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, FailUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n \8805 2"))

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

type family RightComb (s :: [T]) :: T where ...

Folds a stack into a right-combed pair.

RightComb '[ 'TInt,  'TString, 'TUnit ]
~
'TPair 'TInt ('TPair 'TString 'TUnit)

Equations

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 \8805 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)))

type family UnpairN (n :: Peano) (s :: T) :: [T] where ...

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]

Equations

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

type family GetN (ix :: Peano) (pair :: T) :: T where ...

Get the node at index ix of a right-combed pair.

Equations

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

type family UpdateN (ix :: Peano) (val :: T) (pair :: T) :: T where ...

Update the node at index ix of a right-combed pair.

Equations

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)