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 tuples. First element of tuple is a structure, holding field and type annotations for a given type. Second element of tuple is an optional variable annotation for the stack element. Additionally constructor keeps SingI constraint for the current type.

Constructors

SNil :: HST '[]

(::&) :: (Typeable xs, KnownT x) => (Notes x, Dict (WellTyped 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

NFData (HST ts)

Defined in Michelson.TypeCheck.Types

Methods

rnf :: HST ts -> ()

Buildable (HST ts)

Defined in Michelson.TypeCheck.Types

Methods

build :: HST ts -> Builder

(-:&) :: (Typeable xs, WellTyped 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.

pattern (::&+) :: () => (ys ~ (x ': xs), KnownT x, Typeable xs) => (Sing x, Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST ys infixr 7

Extended pattern-match - adds Sing x argument.

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

NFData SomeHST

Defined in Michelson.TypeCheck.Types

Methods

rnf :: SomeHST -> ()

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

Constructors

SomeContract :: Contract cp st -> SomeContract

Instances

Show SomeContract

Defined in Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> SomeContract -> ShowS

show :: SomeContract -> String

showList :: [SomeContract] -> ShowS

NFData SomeContract

Defined in Michelson.TypeCheck.Types

Methods

rnf :: SomeContract -> ()

data SomeContractAndStorage where

Represents a typed contract & a storage value of the type expected by the contract.

Constructors

SomeContractAndStorage :: forall cp st. (StorageScope st, ParameterScope cp) => Contract cp st -> Value st -> SomeContractAndStorage

Instances

Show SomeContractAndStorage

Defined in Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> SomeContractAndStorage -> ShowS

show :: SomeContractAndStorage -> String

showList :: [SomeContractAndStorage] -> ShowS

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

data NotWellTyped

Error type for when a value is not well-typed.

Constructors

NotWellTyped T

Instances

Buildable NotWellTyped

Defined in Michelson.TypeCheck.Types

Methods

build :: NotWellTyped -> Builder

getWTP :: forall t. SingI t => Either NotWellTyped (Dict (WellTyped t))

Given a type, provide evidence that it is well typed w.r.t to the Michelson rules regarding where comparable types are required.

withWTPm :: forall t m a. (MonadFail m, SingI t) => (WellTyped t => m a) -> m a

Given a type and an action that requires evidence that the type is well typed, generate the evidence and execute the action, or else fail with an error.

unsafeWithWTP :: forall t a. SingI t => (WellTyped t => a) -> a

Similar to withWTPm but is mean to be used within tests.

mapSomeContract :: (forall inp out. Instr inp out -> Instr inp out) -> SomeContract -> SomeContract

mapSomeInstr :: (forall out. Instr inp out -> Instr inp out) -> SomeInstr inp -> SomeInstr inp

mapSomeInstrOut :: (forall out. Instr inp out -> Instr inp' out) -> SomeInstrOut inp -> SomeInstrOut inp'

noBoundVars :: BoundVars