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

Morley.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 '[] 
(::&) :: (SingI x, SingI xs) => (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x ': xs) infixr 7 

Instances

Instances details
Eq (HST ts) Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

Methods

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

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

Show (HST ts) Source # 
Instance details

Defined in Morley.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 Morley.Michelson.TypeCheck.Types

Methods

rnf :: HST ts -> () #

Buildable (HST ts) Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

Methods

build :: HST ts -> Builder #

RenderDoc (HST ts) Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

(-:&) :: (WellTyped x, SingI xs) => 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), SingI x, SingI 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 :: SingI ts => HST ts -> SomeHST 

Instances

Instances details
Eq SomeHST Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

Methods

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

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

Show SomeHST Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

NFData SomeHST Source # 
Instance details

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

(:::) :: SingI 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 Morley.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 Morley.Michelson.TypeCheck.Types

Methods

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

show :: SomeInstr inp -> String #

showList :: [SomeInstr inp] -> ShowS #

data BoundVars Source #

Set of variables defined in a let-block.

Constructors

BoundVars (Map Var Ty) (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 

Instances

Instances details
Buildable NotWellTyped Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

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.

getWTP' :: Sing t -> Either NotWellTyped (Dict (WellTyped t)) Source #

Version of getWTP that accepts Sing at term-level.

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 meant to be used within tests.

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

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

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