Michelson.Typed.Haskell.Instr.Sum

Instructions working on sum types derived from Haskell ones.

Documentation

type InstrWrapC dt name = (GenericIsoValue dt, GInstrWrap (Rep dt) (LnrBranch (GetNamed name dt)) (LnrFieldType (GetNamed name dt)))

type InstrWrapOneC dt name = (InstrWrapC dt name, GetCtorField dt name ~ 'OneField (CtorOnlyField name dt))

type InstrCaseC dt = (GenericIsoValue dt, GInstrCase (Rep dt))

type InstrUnwrapC dt name = (GenericIsoValue dt, GInstrUnwrap (Rep dt) (LnrBranch (GetNamed name dt)) (CtorOnlyField name dt))

instrWrap :: forall dt name st. InstrWrapC dt name => Label name -> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt ': st)

Wrap given element into a constructor with the given name.

Mentioned constructor must have only one field.

Since labels interpretable by OverloadedLabels extension cannot start with capital latter, prepend constructor name with letter "c" (see examples below).

instrWrapOne :: forall dt name st. InstrWrapOneC dt name => Label name -> Instr (ToT (CtorOnlyField name dt) ': st) (ToT dt ': st)

Like instrWrap but only works for contructors with a single field. Results in a type error if a constructor with no field is used instead.

hsWrap :: forall dt name. InstrWrapC dt name => Label name -> ExtractCtorField (GetCtorField dt name) -> dt

Wrap a haskell value into a constructor with the given name.

This is symmetric to instrWrap.

instrCase :: forall dt out inp. InstrCaseC dt => Rec (CaseClause inp out) (CaseClauses dt) -> RemFail Instr (ToT dt ': inp) out

Pattern-match on the given datatype.

(//->) :: Label ("c" `AppendSymbol` ctor) -> RemFail Instr (AppendCtorField x inp) out -> CaseClause inp out ('CaseClauseParam ctor x) infixr 8

Lift an instruction to case clause.

You should write out constructor name corresponding to the clause explicitly. Prefix constructor name with "c" letter, otherwise your label will not be recognized by Haskell parser. Passing constructor name can be circumvented but doing so is not recomended as mentioning contructor name improves readability and allows avoiding some mistakes.

instrUnwrapUnsafe :: forall dt name st. InstrUnwrapC dt name => Label name -> Instr (ToT dt ': st) (ToT (CtorOnlyField name dt) ': st)

Unwrap a constructor with the given name.

Rules which apply to instrWrap function work here as well. Although, unlike instrWrap, this function does not work for nullary constructors.

hsUnwrap :: forall dt name. InstrUnwrapC dt name => Label name -> dt -> Maybe (CtorOnlyField name dt)

Try to unwrap a constructor with the given name.

data CaseClauseParam

In what different case branches differ - related constructor name and input stack type which the branch starts with.

Constructors

CaseClauseParam Symbol CtorField

data CaseClause (inp :: [T]) (out :: [T]) (param :: CaseClauseParam) where

Type information about single case clause.

Constructors

CaseClause :: RemFail Instr (AppendCtorField x inp) out -> CaseClause inp out ('CaseClauseParam ctor x)

type CaseClauses a = GCaseClauses (Rep a)

List of CaseClauseParams required to pattern match on the given type.

type family GCaseClauses x :: [CaseClauseParam]

Instances

type GCaseClauses (x :+: y)

Defined in Michelson.Typed.Haskell.Instr.Sum

type GCaseClauses (x :+: y) = GCaseClauses x ++ GCaseClauses y

type GCaseClauses (D1 i x)

Defined in Michelson.Typed.Haskell.Instr.Sum

type GCaseClauses (D1 i x) = GCaseClauses x

type GCaseClauses (C1 ('MetaCons ctor _1 _2) x)

Defined in Michelson.Typed.Haskell.Instr.Sum

type GCaseClauses (C1 ('MetaCons ctor _1 _2) x) = '[GCaseBranchInput ctor x]

type family GCaseBranchInput ctor x :: CaseClauseParam

Instances

type GCaseBranchInput ctor (U1 :: Type -> Type)

Defined in Michelson.Typed.Haskell.Instr.Sum

type GCaseBranchInput ctor (U1 :: Type -> Type) = 'CaseClauseParam ctor 'NoFields

type GCaseBranchInput ctor (Rec0 a)

Defined in Michelson.Typed.Haskell.Instr.Sum

type GCaseBranchInput ctor (Rec0 a) = 'CaseClauseParam ctor ('OneField a)

type GCaseBranchInput ctor (S1 i x)

Defined in Michelson.Typed.Haskell.Instr.Sum

type GCaseBranchInput ctor (S1 i x) = GCaseBranchInput ctor x

type GCaseBranchInput ctor (x :*: y)

Defined in Michelson.Typed.Haskell.Instr.Sum

type GCaseBranchInput ctor (x :*: y) = 'CaseClauseParam ctor 'NoFields

data Branch

Which branch to choose in generic tree representation: left, straight or right. S is used when there is one constructor with one field (something newtype-like).

The reason why we need S can be explained by this example: data A = A1 B | A2 Integer data B = B Bool Now we may search for A1 constructor or B constructor. Without S in both cases path will be the same ([L]).

Constructors

L

S

R

type Path = [Branch]

Path to a leaf (some field or constructor) in generic tree representation.

data CtorField

We support only two scenarious - constructor with one field and without fields. Nonetheless, it's not that sad since for sum types we can't even assign names to fields if there are many (the style guide prohibits partial records).

Constructors

OneField Type

NoFields

type family ExtractCtorField (cf :: CtorField) where ...

Get something as field of the given constructor.

Equations

ExtractCtorField ('OneField t) = t

ExtractCtorField 'NoFields = ()

type family AppendCtorField (cf :: CtorField) (l :: [k]) :: [k] where ...

Push field to stack, if any.

Equations

AppendCtorField ('OneField t) (l :: [T]) = ToT t ': l

AppendCtorField ('OneField t) (l :: [Type]) = t ': l

AppendCtorField 'NoFields (l :: [T]) = l

AppendCtorField 'NoFields (l :: [Type]) = l

type AppendCtorFieldAxiom (cf :: CtorField) (st :: [Type]) = ToTs (AppendCtorField cf st) ~ AppendCtorField cf (ToTs st)

To use AppendCtorField not only here for T-based stacks, but also later in Lorentz with Type-based stacks we need the following property.

appendCtorFieldAxiom :: (AppendCtorFieldAxiom ('OneField Word) '[Int], AppendCtorFieldAxiom 'NoFields '[Int]) => Dict (AppendCtorFieldAxiom cf st)

Proof of AppendCtorFieldAxiom.

type GetCtorField dt ctor = LnrFieldType (GetNamed ctor dt)

Get type of constructor fields (one or zero) referred by given datatype and name.

type CtorHasOnlyField ctor dt f = GetCtorField dt ctor ~ 'OneField f

Expect referred constructor to have only one field (in form of constraint) and extract its type.

type CtorOnlyField name dt = RequireOneField name (GetCtorField dt name)

Expect referred constructor to have only one field (otherwise compile error is raised) and extract its type.

data MyCompoundType

Instances

Generic MyCompoundType

Defined in Michelson.Typed.Haskell.Instr.Sum

Associated Types

type Rep MyCompoundType :: Type -> Type

Methods

from :: MyCompoundType -> Rep MyCompoundType x

to :: Rep MyCompoundType x -> MyCompoundType

IsoValue MyCompoundType

Defined in Michelson.Typed.Haskell.Instr.Sum

Associated Types

type ToT MyCompoundType :: T

Methods

toVal :: MyCompoundType -> Value (ToT MyCompoundType)

fromVal :: Value (ToT MyCompoundType) -> MyCompoundType

type Rep MyCompoundType

Defined in Michelson.Typed.Haskell.Instr.Sum

type Rep MyCompoundType

type ToT MyCompoundType

Defined in Michelson.Typed.Haskell.Instr.Sum

type ToT MyCompoundType = GValueType (Rep MyCompoundType)

Helpers

type family IsPrimitiveValue (x :: Type) :: Bool where ...

Whether given type represents an atomic Michelson value.

Equations

IsPrimitiveValue (Maybe _) = 'True

IsPrimitiveValue (NamedF _ _ _) = 'True

IsPrimitiveValue Integer = 'True

IsPrimitiveValue Natural = 'True

IsPrimitiveValue Text = 'True

IsPrimitiveValue MText = 'True

IsPrimitiveValue Bool = 'True

IsPrimitiveValue ByteString = 'True

IsPrimitiveValue Mutez = 'True

IsPrimitiveValue Address = 'True

IsPrimitiveValue EpAddress = 'True

IsPrimitiveValue KeyHash = 'True

IsPrimitiveValue Timestamp = 'True

IsPrimitiveValue PublicKey = 'True

IsPrimitiveValue Signature = 'True

IsPrimitiveValue (ContractRef _) = 'True

IsPrimitiveValue (BigMap _ _) = 'True

IsPrimitiveValue (Map _ _) = 'True

IsPrimitiveValue (Set _) = 'True

IsPrimitiveValue [_] = 'True

IsPrimitiveValue (Operation' _) = 'True

IsPrimitiveValue ChainId = 'True

IsPrimitiveValue _ = 'False