morley-1.20.0: Developer tools for the Michelson Language
Safe HaskellSafe-Inferred
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) => (SingT x, Dict (WellTyped x)) -> HST xs -> HST (x ': xs) infixr 7 

Instances

Instances details
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 -> () #

Eq (HST ts) Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

Methods

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

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

Buildable (HST ts) Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

Methods

build :: HST ts -> Doc

buildList :: [HST ts] -> Doc

(-:&) :: (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.

data SomeHST where Source #

No-argument type wrapper for HST data type.

Constructors

SomeHST :: SingI ts => HST ts -> SomeHST 

Instances

Instances details
Show SomeHST Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

Methods

showsPrec :: Int -> SomeHST -> ShowS #

show :: SomeHST -> String #

showList :: [SomeHST] -> ShowS #

NFData SomeHST Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

Methods

rnf :: SomeHST -> () #

Eq SomeHST Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

Methods

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

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

data SomeTcInstrOut 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 -> SomeTcInstrOut 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) -> SomeTcInstrOut 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 (SomeTcInstrOut inp) Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

Methods

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

show :: SomeTcInstrOut inp -> String #

showList :: [SomeTcInstrOut inp] -> ShowS #

Buildable (SomeTcInstrOut inp) Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

Methods

build :: SomeTcInstrOut inp -> Doc

buildList :: [SomeTcInstrOut inp] -> Doc

data SomeTcInstr inp where Source #

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

Constructors

(:/) :: HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp infix 8 

Instances

Instances details
Show (SomeTcInstr inp) Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

Methods

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

show :: SomeTcInstr inp -> String #

showList :: [SomeTcInstr inp] -> ShowS #

Buildable (SomeTcInstr inp) Source # 
Instance details

Defined in Morley.Michelson.TypeCheck.Types

Methods

build :: SomeTcInstr inp -> Doc

buildList :: [SomeTcInstr inp] -> Doc

data BoundVars Source #

Set of variables defined in a let-block.

Constructors

BoundVars (Map Var Ty) (Maybe SomeHST) 

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) -> SomeTcInstr inp -> SomeTcInstr inp Source #

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

noBoundVars :: BoundVars Source #