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.

Constructors

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.

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 an instruction that also contains annotations for some of top types on the result stack.

As of now, when converting from untyped representation, we only preserve field annotations and type annotations in Notes. Variable annotations are preserved in InstrWithVarAnns.

This can wrap only instructions with at least one non-failing execution branch.

InstrWithVarNotes :: NonEmpty VarAnn -> Instr a b -> Instr a b

A wrapper for an instruction which produces variable annotations on the top stack element(s). See also: InstrWithVarAnns.

InstrWithVarAnns :: VarAnns -> Instr a b -> Instr a b

A wrapper for an instruction that also contains a variable annotation for the top type on the result stack.

This differs from InstrWithVarNotes in a subtle but significant way: that constructor is only present on instructions which explicitly produce variable annotations, while this constructor contains the annotation associated to an instruction after every type-checking phase, in the same manner as InstrWithNotes, which is useful during the interpreter phase.

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 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 behaviour of instruction put within it.

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

Variants of CAR/CDR to retain field annotations as they relate to the input stack, and hence won't be available from the annotation notes from the result stack we pack with the instructions during type check.

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

DROP :: Instr (a ': s) s

DROPN :: forall (n :: Peano) s. (SingI n, KnownPeano n, RequireLongerOrSameLength s n, NFData (Sing n)) => Sing n -> Instr s (Drop n s)

DUP :: Instr (a ': s) (a ': (a ': s))

DUPN :: forall (n :: Peano) inp out a. (ConstraintDUPN n inp out a, NFData (Sing n)) => Sing n -> Instr inp out

SWAP :: Instr (a ': (b ': s)) (b ': (a ': s))

DIG :: forall (n :: Peano) inp out a. (ConstraintDIG n inp out a, NFData (Sing n)) => Sing n -> Instr inp out

DUG :: forall (n :: Peano) inp out a. (ConstraintDUG n inp out a, NFData (Sing n)) => Sing 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. KnownT 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)

Annotations for PAIR instructions can be different from notes presented on the stack in case of special field annotations, so we carry annotations for instruction separately from notes.

PAIRN :: forall n inp. ConstraintPairN n inp => Sing n -> Instr inp (PairN n inp)

>>> :t PAIRN (peanoSing @3) :: Instr '[ 'TInt, 'TUnit, 'TString ] _
...
...:: Instr
...    '[ 'TInt, 'TUnit, 'TString]
...    '[ 'TPair 'TInt ('TPair 'TUnit 'TString)]

>>> PAIRN (peanoSing @1) :: Instr '[ 'TInt, 'TInt ] _
...
... 'PAIR n' expects n ≥ 2
...

>>> PAIRN (peanoSing @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 => Sing n -> Instr (pair ': s) (UnpairN n pair ++ s)

>>> :t UNPAIRN (peanoSing @3) :: Instr '[ 'TPair 'TInt ('TPair 'TUnit 'TString) ] _
...
...:: Instr
...   '[ 'TPair 'TInt ('TPair 'TUnit 'TString)]
...   '[ 'TInt, 'TUnit, 'TString]

>>> :t UNPAIRN (peanoSing @3) :: Instr '[ 'TPair 'TInt ('TPair 'TUnit ('TPair 'TString 'TNat)) ] _
...
...:: Instr
...   '[ 'TPair 'TInt ('TPair 'TUnit ('TPair 'TString 'TNat))]
...   '[ 'TInt, 'TUnit, 'TPair 'TString 'TNat]

>>> UNPAIRN (peanoSing @1) :: Instr '[ 'TPair 'TInt 'TUnit ] _
...
...'UNPAIR n' expects n ≥ 2
...

>>> UNPAIRN (peanoSing @2) :: Instr '[ 'TInt, 'TUnit, 'TString ] _
...
...Expected a pair at the top of the stack, but found: 'TInt
...

>>> UNPAIRN (peanoSing @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 :: KnownT b => TypeAnn -> FieldAnn -> FieldAnn -> Instr (a ': s) ('TOr a b ': s)

AnnRIGHT :: KnownT 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 :: KnownT 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 :: (KnownT e, Comparable e) => Instr s ('TSet e ': s)

EMPTY_MAP :: (KnownT a, KnownT b, Comparable a) => Instr s ('TMap a b ': s)

EMPTY_BIG_MAP :: (KnownT a, KnownT b, Comparable a) => Instr s ('TBigMap a b ': s)

MAP :: (MapOp c, KnownT 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, KnownT (GetOpVal c)) => Instr (GetOpKey c ': (c ': s)) ('TOption (GetOpVal c) ': s)

GETN :: forall (ix :: Peano) (pair :: T) (s :: [T]). ConstraintGetN ix pair => Sing 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 (peanoSing @1) :: Instr '[ 'TPair 'TInt 'TUnit] _
...
...:: Instr '[ 'TPair 'TInt 'TUnit] '[ 'TInt]

>>> GETN (peanoSing @1) :: Instr '[ 'TUnit ] _
...
...Expected a pair at the top of the stack, but found: 'TUnit
...

>>> GETN (peanoSing @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 (peanoSing @0) :: Instr '[ 'TInt ] _
...
...:: Instr '[ 'TInt] '[ 'TInt]

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 => Sing ix -> Instr (val ': (pair ': s)) (UpdateN ix val pair ': s)

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

>>> :t UPDATEN (peanoSing @1) :: Instr '[ 'TString, 'TPair 'TInt 'TUnit] _
...
...:: Instr
...     '[ 'TString, 'TPair 'TInt 'TUnit] '[ 'TPair 'TString 'TUnit]

>>> UPDATEN (peanoSing @1) :: Instr '[ 'TUnit, 'TInt ] _
...
...Expected the 2nd element of the stack to be a pair, but found: 'TInt
...

>>> UPDATEN (peanoSing @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 (peanoSing @0) :: Instr '[ 'TInt, 'TString ] _
...
...:: Instr '[ 'TInt, 'TString] '[ 'TInt]

GET_AND_UPDATE :: (GetOp c, UpdOp c, KnownT (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. (KnownT i, KnownT 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, KnownT 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', NFData (Sing n)) => Sing n -> Instr s s' -> Instr inp out

FAILWITH :: (KnownT 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, KnownT 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, KnownT c) => Instr ('TNat ': ('TNat ': (c ': s))) ('TOption c ': s)

ISNAT :: Instr ('TInt ': s) ('TOption 'TNat ': s)

ADD :: ArithOp Add n m => Instr (n ': (m ': s)) (ArithRes Add n m ': s)

SUB :: ArithOp Sub n m => Instr (n ': (m ': s)) (ArithRes Sub n m ': s)

MUL :: ArithOp Mul n m => Instr (n ': (m ': s)) (ArithRes Mul n m ': s)

EDIV :: EDivOp n m => Instr (n ': (m ': s)) ('TOption ('TPair (EDivOpRes n m) (EModOpRes 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, KnownT 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)

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

Instances

IsoValue Operation

Defined in Michelson.Typed.Haskell.Value

Associated Types

type ToT Operation :: T

Methods

toVal :: Operation -> Value (ToT Operation)

fromVal :: Value (ToT Operation) -> Operation

TypeHasDoc Operation

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

WellTyped t => IsoValue (Value t)

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

UnpackedValScope t => FromExpression (Value t)

Defined in Morley.Micheline.Class

Methods

fromExpression :: Expression -> Either FromExpressionError (Value t)

(SingI t, HasNoOp t) => ToExpression (Value t)

Defined in Morley.Micheline.Class

Methods

toExpression :: Value t -> Expression

Eq (Instr inp out)

Defined in Michelson.Typed.Convert

Methods

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

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

Show (Instr inp out)

Defined in Michelson.Typed.Instr

Methods

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

show :: Instr inp out -> String

showList :: [Instr inp out] -> ShowS

Semigroup (Instr s s)

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

Monoid (Instr s s)

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

NFData (Instr inp out)

Defined in Michelson.Typed.Instr

Methods

rnf :: Instr inp out -> ()

(SingI t, HasNoOp t) => Buildable (Value' Instr t)

Defined in Michelson.Typed.Convert

Methods

build :: Value' Instr t -> Builder

ContainsUpdateableDoc (Instr inp out)

Defined in Michelson.Typed.Doc

Methods

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

ContainsDoc (Instr inp out)

Defined in Michelson.Typed.Doc

Methods

buildDocUnfinalized :: Instr inp out -> ContractDoc

(KnownT inp, KnownT out) => FromExpression (Instr '[inp] '[out])

Defined in Morley.Micheline.Class

Methods

fromExpression :: Expression -> Either FromExpressionError (Instr '[inp] '[out])

ToExpression (Instr inp out)

Defined in Morley.Micheline.Class

Methods

toExpression :: Instr inp out -> Expression

type ToT Operation

Defined in Michelson.Typed.Haskell.Value

type ToT Operation = 'TOperation

type TypeDocFieldDescriptions Operation

Defined in Michelson.Typed.Haskell.Doc

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

type ToT (Value t)

Defined in Michelson.Typed.Haskell.Value

type ToT (Value t) = t

data ExtInstr s

Constructors

TEST_ASSERT (TestAssert s)

PRINT (PrintComment s)

DOC_ITEM SomeDocItem

COMMENT_ITEM CommentType

Instances

Show (ExtInstr s)

Defined in Michelson.Typed.Instr

Methods

showsPrec :: Int -> ExtInstr s -> ShowS

show :: ExtInstr s -> String

showList :: [ExtInstr s] -> ShowS

Generic (ExtInstr s)

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

NFData (ExtInstr s)

Defined in Michelson.Typed.Instr

Methods

rnf :: ExtInstr s -> ()

type Rep (ExtInstr s)

Defined in Michelson.Typed.Instr

type Rep (ExtInstr s) = D1 ('MetaData "ExtInstr" "Michelson.Typed.Instr" "morley-1.14.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))))

data CommentType

Constructors

FunctionStarts Text

FunctionEnds Text

StatementStarts Text

StatementEnds Text

JustComment Text

StackTypeComment (Maybe [T])

Nothing for any stack type

Instances

Show CommentType

Defined in Michelson.Typed.Instr

Methods

showsPrec :: Int -> CommentType -> ShowS

show :: CommentType -> String

showList :: [CommentType] -> ShowS

Generic CommentType

Defined in Michelson.Typed.Instr

Associated Types

type Rep CommentType :: Type -> Type

Methods

from :: CommentType -> Rep CommentType x

to :: Rep CommentType x -> CommentType

NFData CommentType

Defined in Michelson.Typed.Instr

Methods

rnf :: CommentType -> ()

type Rep CommentType

Defined in Michelson.Typed.Instr

type Rep CommentType = D1 ('MetaData "CommentType" "Michelson.Typed.Instr" "morley-1.14.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 :: (KnownPeano idx, SingI idx, RequireLongerThan st idx) => Sing (idx :: Peano) -> StackRef st

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

Instances

Eq (StackRef st)

Defined in Michelson.Typed.Instr

Methods

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

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

Show (StackRef st)

Defined in Michelson.Typed.Instr

Methods

showsPrec :: Int -> StackRef st -> ShowS

show :: StackRef st -> String

showList :: [StackRef st] -> ShowS

NFData (StackRef st)

Defined in Michelson.Typed.Instr

Methods

rnf :: StackRef st -> ()

mkStackRef :: forall (gn :: Nat) st n. (n ~ ToPeano gn, SingI n, KnownPeano n, 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

Eq (PrintComment st)

Defined in Michelson.Typed.Instr

Methods

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

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

Show (PrintComment st)

Defined in Michelson.Typed.Instr

Methods

showsPrec :: Int -> PrintComment st -> ShowS

show :: PrintComment st -> String

showList :: [PrintComment st] -> ShowS

IsString (PrintComment st)

Defined in Michelson.Typed.Instr

Methods

fromString :: String -> PrintComment st

Generic (PrintComment st)

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

Semigroup (PrintComment st)

Defined in Michelson.Typed.Instr

Methods

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

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

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

Monoid (PrintComment st)

Defined in Michelson.Typed.Instr

Methods

mempty :: PrintComment st

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

mconcat :: [PrintComment st] -> PrintComment st

NFData (PrintComment st)

Defined in Michelson.Typed.Instr

Methods

rnf :: PrintComment st -> ()

type Rep (PrintComment st)

Defined in Michelson.Typed.Instr

type Rep (PrintComment st) = D1 ('MetaData "PrintComment" "Michelson.Typed.Instr" "morley-1.14.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 :: Typeable out => Text -> PrintComment inp -> Instr inp ('TBool ': out) -> TestAssert inp

Instances

Typeable s => Eq (TestAssert s)

Defined in Michelson.Typed.Convert

Methods

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

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

Show (TestAssert s)

Defined in Michelson.Typed.Instr

Methods

showsPrec :: Int -> TestAssert s -> ShowS

show :: TestAssert s -> String

showList :: [TestAssert s] -> ShowS

NFData (TestAssert s)

Defined in Michelson.Typed.Instr

Methods

rnf :: TestAssert s -> ()

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

data Contract cp st

Typed contract and information about annotations which is not present in the contract code.

Constructors

(ParameterScope cp, StorageScope st) => Contract

Fields

• cCode :: ContractCode cp st
• cParamNotes :: ParamNotes cp
• cStoreNotes :: Notes st
• cEntriesOrder :: EntriesOrder

Instances

Eq (ContractCode cp st) => Eq (Contract cp st)

Defined in Michelson.Typed.Instr

Methods

(==) :: Contract cp st -> Contract cp st -> Bool

(/=) :: Contract cp st -> Contract cp st -> Bool

Show (Contract cp st)

Defined in Michelson.Typed.Instr

Methods

showsPrec :: Int -> Contract cp st -> ShowS

show :: Contract cp st -> String

showList :: [Contract cp st] -> ShowS

NFData (Contract cp st)

Defined in Michelson.Typed.Instr

Methods

rnf :: Contract cp st -> ()

ToExpression (Contract cp st)

Defined in Morley.Micheline.Class

Methods

toExpression :: Contract cp st -> Expression

defaultContract :: (ParameterScope cp, StorageScope st) => ContractCode cp st -> Contract cp st

mapContractCode :: (ContractCode cp st -> ContractCode cp st) -> Contract cp st -> Contract cp st

mapEntriesOrdered :: Contract cp st -> (ParamNotes cp -> a) -> (Notes st -> a) -> (ContractCode cp st -> a) -> [a]

Map each typed contract fields by the given function and sort the output based on the EntriesOrder.

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 :: () => (KnownT 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 :: () => (KnownT 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) = (SingI n, KnownPeano n, RequireLongerOrSameLength inp n, (n > 'Z) ~ 'True, inp ~ (Take (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]) = (SingI n, KnownPeano n, RequireLongerOrSameLength inp n, (Take n inp ++ s) ~ inp, (Take n inp ++ s') ~ 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) = (SingI n, KnownPeano n, RequireLongerThan inp n, inp ~ (Take n inp ++ (a ': Drop ('S n) inp)), out ~ (a ': (Take n inp ++ Drop ('S n) inp)))

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

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"), SingI n, KnownPeano n)

type PairN (n :: Peano) (s :: [T]) = RightComb (Take 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) = (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)), SingI n, KnownPeano n)

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) = (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)), SingI ix, KnownPeano ix)

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) = (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)), SingI ix, KnownPeano ix)

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)