Michelson.TypeCheck.Types

Documentation

data HST (ts :: [T]) where

Data type holding type information for stack (Heterogeneous Stack Type).

This data type is used along with instruction data type Instr to carry information about its input and output stack types.

That is, if there is value instr :: Instr inp out, along with this instr one may carry inpHST :: HST inp and outHST :: HST out which will contain whole information about input and output stack types for instr.

Data type HST is very similar to Data.Vinyl.Rec, but is specialized for a particular purpose. In particular, definition of HST (t1 ': t2 ': ... tn ': '[]) requires constraints (Typeable t1, Typeable t2, ..., Typeable tn) as well as constraints (Typeable '[ t1 ], Typeable '[ t1, t2 ], ...). These applications of Typeable class are required for convenient usage of type encoded by HST ts with some functions from Data.Typeable.

Data type HST (Heterogeneous Stack Type) is a heterogenuous list of triples. First element of triple is a type singleton which is due to main motivation behind HST, namely for it to be used as representation of Instr type data for pattern-matching. Second element of triple is a structure, holding field and type annotations for a given type. Third element of triple is an optional variable annotation for the stack element.

Constructors

SNil :: HST '[]

(::&) :: (Typeable xs, Typeable x, SingI x) => (Sing x, Notes x, VarAnn) -> HST xs -> HST (x ': xs) infixr 7

Instances

Eq (HST ts)

Defined in Michelson.TypeCheck.Types

Methods

(==) :: HST ts -> HST ts -> Bool

(/=) :: HST ts -> HST ts -> Bool

Show (HST ts)

Defined in Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> HST ts -> ShowS

show :: HST ts -> String

showList :: [HST ts] -> ShowS

(-:&) :: (Typeable xs, Typeable x, SingI x) => Sing x -> HST xs -> HST (x ': xs) infixr 7

Append a type to HST, assuming that notes and annotations for this type are unknown.

data SomeHST where

No-argument type wrapper for HST data type.

Constructors

SomeHST :: Typeable ts => HST ts -> SomeHST

Instances

Eq SomeHST

Defined in Michelson.TypeCheck.Types

Methods

(==) :: SomeHST -> SomeHST -> Bool

(/=) :: SomeHST -> SomeHST -> Bool

Show SomeHST

Defined in Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> SomeHST -> ShowS

show :: SomeHST -> String

showList :: [SomeHST] -> ShowS

data SomeInstrOut inp where

This data type keeps part of type check result - instruction and corresponding output stack.

Constructors

(:::) :: Typeable out => Instr inp out -> HST out -> SomeInstrOut inp infix 9

Type-check result with concrete output stack, most common case.

Output stack type is wrapped inside the type and Typeable constraint is provided to allow convenient unwrapping.

AnyOutInstr :: (forall out. Instr inp out) -> SomeInstrOut inp

Type-check result which matches against arbitrary output stack. Information about annotations in the output stack is absent.

This case is only possible when the corresponding code terminates with FAILWITH instruction in all possible executions. The opposite may be not true though (example: you push always-failing lambda and immediatelly execute it - stack type is known).

Instances

Show (ExtInstr inp) => Show (SomeInstrOut inp)

Defined in Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> SomeInstrOut inp -> ShowS

show :: SomeInstrOut inp -> String

showList :: [SomeInstrOut inp] -> ShowS

data SomeInstr inp where

Data type keeping the whole type check result: instruction and type representations of instruction's input and output.

Constructors

(:/) :: HST inp -> SomeInstrOut inp -> SomeInstr inp infix 8

Instances

Show (ExtInstr inp) => Show (SomeInstr inp)

Defined in Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> SomeInstr inp -> ShowS

show :: SomeInstr inp -> String

showList :: [SomeInstr inp] -> ShowS

data SomeValue where

Data type, holding strictly-typed Michelson value along with its type singleton.

Constructors

(::::) :: (SingI t, Typeable t) => Value t -> (Sing t, Notes t) -> SomeValue

data SomeContract where

Constructors

SomeContract :: (Each [Typeable, SingI, HasNoOp] [st, cp], HasNoBigMap cp, BigMapConstraint st) => Contract cp st -> HST (ContractInp cp st) -> HST (ContractOut st) -> SomeContract

Instances

Show SomeContract

Defined in Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> SomeContract -> ShowS

show :: SomeContract -> String

showList :: [SomeContract] -> ShowS

data SomeCValue where

Data type, holding strictly-typed Michelson value along with its type singleton.

Constructors

(:--:) :: (SingI t, Typeable t) => CValue t -> Sing t -> SomeCValue

data BoundVars

Set of variables defined in a let-block.

Constructors

BoundVars (Map Var Type) (Maybe SomeHST)

type TcExtFrames = [BoundVars]

State for type checking nop

noBoundVars :: BoundVars