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
- 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.
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
data NotWellTyped Source #
Error type for when a value is not well-typed.
Constructors
NotWellTyped T |
Instances
Buildable NotWellTyped Source # | |
Defined in Michelson.TypeCheck.Types Methods 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 mean 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 #