morley-1.7.0: Developer tools for the Michelson Language
Safe HaskellNone
LanguageHaskell2010

Michelson.TypeCheck.Types

Synopsis

Documentation

data HST (ts :: [T]) where Source #

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

Instances details
Eq (HST ts) Source # 
Instance details

Defined in Michelson.TypeCheck.Types

Methods

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

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

Show (HST ts) Source # 
Instance details

Defined in Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> HST ts -> ShowS #

show :: HST ts -> String #

showList :: [HST ts] -> ShowS #

NFData (HST ts) Source # 
Instance details

Defined in Michelson.TypeCheck.Types

Methods

rnf :: HST ts -> () #

Buildable (HST ts) Source # 
Instance details

Defined in Michelson.TypeCheck.Types

Methods

build :: HST ts -> Builder #

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

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

Extended pattern-match - adds Sing x argument.

data SomeHST where Source #

No-argument type wrapper for HST data type.

Constructors

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

Instances

Instances details
Eq SomeHST Source # 
Instance details

Defined in Michelson.TypeCheck.Types

Methods

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

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

Show SomeHST Source # 
Instance details

Defined in Michelson.TypeCheck.Types

NFData SomeHST Source # 
Instance details

Defined in Michelson.TypeCheck.Types

Methods

rnf :: SomeHST -> () #

data SomeInstrOut inp where Source #

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

Instances details
Show (ExtInstr inp) => Show (SomeInstrOut inp) Source # 
Instance details

Defined in Michelson.TypeCheck.Types

data SomeInstr inp where Source #

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

Instances details
Show (ExtInstr inp) => Show (SomeInstr inp) Source # 
Instance details

Defined in Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> SomeInstr inp -> ShowS #

show :: SomeInstr inp -> String #

showList :: [SomeInstr inp] -> ShowS #

data SomeContract where Source #

Constructors

SomeContract :: Contract cp st -> SomeContract 

Instances

Instances details
Show SomeContract Source # 
Instance details

Defined in Michelson.TypeCheck.Types

NFData SomeContract Source # 
Instance details

Defined in Michelson.TypeCheck.Types

Methods

rnf :: SomeContract -> () #

data SomeContractAndStorage where Source #

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 

data BoundVars Source #

Set of variables defined in a let-block.

Constructors

BoundVars (Map Var Type) (Maybe SomeHST) 

type TcExtFrames = [BoundVars] Source #

State for type checking nop

data NotWellTyped Source #

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

Constructors

NotWellTyped T 

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

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

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

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

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