Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- data HST (ts :: [T]) where
- (-:&) :: (Typeable xs, WellTyped x) => Sing x -> HST xs -> HST (x ': xs)
- pattern (::&+) :: () => (ys ~ (x ': xs), KnownT x, Typeable xs) => (Sing x, Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST ys
- data SomeHST where
- data SomeInstrOut inp where
- (:::) :: Typeable out => Instr inp out -> HST out -> SomeInstrOut inp
- AnyOutInstr :: (forall out. Instr inp out) -> SomeInstrOut inp

- data SomeInstr inp where
- (:/) :: HST inp -> SomeInstrOut inp -> SomeInstr inp

- data SomeContract where
- SomeContract :: Contract cp st -> SomeContract

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

- data BoundVars = BoundVars (Map Var Type) (Maybe SomeHST)
- type TcExtFrames = [BoundVars]
- data NotWellTyped = NotWellTyped T
- getWTP :: forall t. SingI t => Either NotWellTyped (Dict (WellTyped t))
- withWTPm :: forall t m a. (MonadFail m, SingI t) => (WellTyped t => m a) -> m a
- unsafeWithWTP :: forall t a. SingI t => (WellTyped t => a) -> a
- mapSomeContract :: (forall inp out. Instr inp out -> Instr inp out) -> SomeContract -> SomeContract
- noBoundVars :: BoundVars

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

SNil :: HST '[] | |

(::&) :: (Typeable xs, KnownT x) => (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x ': xs) infixr 7 |

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

No-argument type wrapper for `HST`

data type.

data SomeInstrOut inp where Source #

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

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

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 |

#### Instances

Show (ExtInstr inp) => Show (SomeInstrOut inp) Source # | |

Defined in Michelson.TypeCheck.Types showsPrec :: Int -> SomeInstrOut inp -> ShowS # show :: SomeInstrOut inp -> String # showList :: [SomeInstrOut inp] -> ShowS # |

data SomeInstr inp where Source #

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

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

data SomeContract where Source #

SomeContract :: Contract cp st -> SomeContract |

#### Instances

Show SomeContract Source # | |

Defined in Michelson.TypeCheck.Types showsPrec :: Int -> SomeContract -> ShowS # show :: SomeContract -> String # showList :: [SomeContract] -> ShowS # | |

NFData SomeContract Source # | |

Defined in Michelson.TypeCheck.Types rnf :: SomeContract -> () # |

data SomeContractAndStorage where Source #

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

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

#### Instances

Show SomeContractAndStorage Source # | |

Defined in Michelson.TypeCheck.Types showsPrec :: Int -> SomeContractAndStorage -> ShowS # show :: SomeContractAndStorage -> String # showList :: [SomeContractAndStorage] -> ShowS # |

Set of variables defined in a let-block.

type TcExtFrames = [BoundVars] Source #

State for type checking `nop`

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 #