| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Michelson.TypeCheck.Types
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.
Constructors
| 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.
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 |
| 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 Methods 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.
Constructors
| (:/) :: HST inp -> SomeInstrOut inp -> SomeInstr inp infix 8 |
data SomeContract where Source #
Constructors
| SomeContract :: Contract cp st -> SomeContract |
Instances
| Show SomeContract Source # | |
Defined in Michelson.TypeCheck.Types Methods showsPrec :: Int -> SomeContract -> ShowS # show :: SomeContract -> String # showList :: [SomeContract] -> ShowS # | |
| NFData SomeContract Source # | |
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 |
Instances
| Show SomeContractAndStorage Source # | |
Defined in Michelson.TypeCheck.Types Methods 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 #