Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data HST (ts :: [T]) where
- (-:&) :: (WellTyped x, SingI xs) => Sing x -> HST xs -> HST (x ': xs)
- pattern (::&+) :: () => (ys ~ (x ': xs), SingI x, SingI xs) => (Sing x, Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST ys
- data SomeHST where
- data SomeInstrOut inp where
- (:::) :: SingI 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 BoundVars = BoundVars (Map Var Ty) (Maybe SomeHST)
- type TcExtFrames = [BoundVars]
- data NotWellTyped = NotWellTyped {}
- getWTP :: forall t. SingI t => Either NotWellTyped (Dict (WellTyped t))
- getWTP_ :: forall t. Sing 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
- 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
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 '[] | |
(::&) :: (SingI x, SingI xs) => (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x ': xs) infixr 7 |
(-:&) :: (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.
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.
(:::) :: 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 |
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 |
Set of variables defined in a let-block.
type TcExtFrames = [BoundVars] Source #
State for type checking nop
data NotWellTyped Source #
Error type for when a value is not well-typed.
Instances
Buildable NotWellTyped Source # | |
Defined in Michelson.TypeCheck.Types build :: NotWellTyped -> Builder # |
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 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 #