Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- typeCheckContract :: ExtC => TcExtHandler -> UntypedContract -> Either TCError SomeContract
- typeCheckVal :: ExtC => UntypedValue -> T -> TypeCheckT SomeVal
- typeCheckList :: ExtC => [ExpandedOp] -> SomeHST -> TypeCheckT SomeInstr
- typeCheckCVal :: Value op -> CT -> Maybe SomeValC
- data HST (ts :: [T]) where
- data SomeHST where
- data SomeInstr where
- data SomeVal where
- data SomeContract where
- SomeContract :: (Typeable st, SingI st, SingI cp, Typeable cp) => Contract cp st -> HST (ContractInp cp st) -> HST (ContractOut st) -> SomeContract
- data SomeValC where
- data TCError
- type ExtC = (Show InstrExtT, Eq ExpandedInstrExtU, Typeable InstrExtT, Buildable ExpandedInstr, ConversibleExt)
- type TcInstrHandler = ExpandedInstr -> SomeHST -> TypeCheckT SomeInstr
- type TcExtHandler = ExpandedInstrExtU -> TcExtFrames -> SomeHST -> TypeCheckT (TcExtFrames, Maybe InstrExtT)
- type TcExtFrames = [(ExpandedInstrExtU, SomeHST)]
- type TcResult = Either TCError SomeInstr
- data TypeCheckEnv = TypeCheckEnv {}
- type TypeCheckT a = ExceptT TCError (State TypeCheckEnv) a
- runTypeCheckT :: TcExtHandler -> Type -> TypeCheckT a -> Either TCError a
- eqT' :: forall a b. (Typeable a, Typeable b) => Either Text (a :~: b)
Documentation
typeCheckContract :: ExtC => TcExtHandler -> UntypedContract -> Either TCError SomeContract Source #
typeCheckVal :: ExtC => UntypedValue -> T -> TypeCheckT SomeVal Source #
Function typeCheckVal
converts a single Michelson value
given in representation from Michelson.Type
module to representation
in strictly typed GADT.
As a second argument, typeCheckVal
accepts expected type of value.
Type checking algorithm pattern-matches on parse value representation,
expected type t
and constructs Val t
value.
If there was no match on a given pair of value and expected type, that is interpreted as input of wrong type and type check finishes with error.
typeCheckList :: ExtC => [ExpandedOp] -> SomeHST -> TypeCheckT SomeInstr Source #
Function typeCheckList
converts list of Michelson instructions
given in representation from Michelson.Type
module to representation
in strictly typed GADT.
Types are checked along the way which is neccessary to construct a strictly typed value.
As a second argument, typeCheckList
accepts input stack type representation.
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 triples.
First element of triple is a type singleton which is due to main motivation
behind HST
, namely for it to be used as representation of Instr
type
data for pattern-matching.
Second element of triple is a structure, holding field and type annotations
for a given type.
Third element of triple is an optional variable annotation for the stack
element.
No-argument type wrapper for HST
data type.
Data type holding both instruction and type representations of instruction's input and output.
Intput and output stack types are wrapped inside the type and Typeable
constraints are provided to allow convenient unwrapping.
Data type, holding strictly-typed Michelson value along with its type singleton.
data SomeContract where Source #
SomeContract :: (Typeable st, SingI st, SingI cp, Typeable cp) => Contract cp st -> HST (ContractInp cp st) -> HST (ContractOut st) -> SomeContract |
Instances
Show InstrExtT => Show SomeContract Source # | |
Defined in Michelson.TypeCheck.Types showsPrec :: Int -> SomeContract -> ShowS # show :: SomeContract -> String # showList :: [SomeContract] -> ShowS # |
Data type, holding strictly-typed Michelson value along with its type singleton.
Type check error
Instances
Buildable ExpandedInstr => Show TCError Source # | |
Buildable ExpandedInstr => Exception TCError Source # | |
Defined in Michelson.TypeCheck.Types toException :: TCError -> SomeException # fromException :: SomeException -> Maybe TCError # displayException :: TCError -> String # | |
Buildable TCError Source # | |
Defined in Michelson.TypeCheck.Types |
type ExtC = (Show InstrExtT, Eq ExpandedInstrExtU, Typeable InstrExtT, Buildable ExpandedInstr, ConversibleExt) Source #
Constraints on InstrExtT and untyped Instr which are required for type checking
type TcInstrHandler = ExpandedInstr -> SomeHST -> TypeCheckT SomeInstr Source #
type TcExtHandler = ExpandedInstrExtU -> TcExtFrames -> SomeHST -> TypeCheckT (TcExtFrames, Maybe InstrExtT) Source #
Function for typeChecking a nop
and updating state
TypeCheckT is used because inside
inside of TEST_ASSERT could be PRINTSTACKTYPEetc extended instructions.
type TcExtFrames = [(ExpandedInstrExtU, SomeHST)] Source #
State for type checking nop
data TypeCheckEnv Source #
The typechecking state
type TypeCheckT a = ExceptT TCError (State TypeCheckEnv) a Source #
runTypeCheckT :: TcExtHandler -> Type -> TypeCheckT a -> Either TCError a Source #