Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- typeCheckContract :: Contract -> TypeCheckResult SomeContract
- typeCheckContractAndStorage :: Contract -> Value -> TypeCheckResult SomeContractAndStorage
- typeCheckExt :: forall s. SingI s => TcInstrHandler -> ExpandedExtInstr -> HST s -> TypeCheckInstrNoExcept (TypeCheckedSeq s)
- typeCheckInstr :: TcInstrHandler
- typeCheckList :: SingI inp => [ExpandedOp] -> HST inp -> TypeCheck (SomeInstr inp)
- typeCheckListNoExcept :: SingI inp => [ExpandedOp] -> HST inp -> TypeCheckNoExcept (TypeCheckedSeq inp)
- typeCheckParameter :: TcOriginatedContracts -> Ty -> Value -> TypeCheckResult SomeValue
- typeCheckStorage :: Ty -> Value -> TypeCheckResult SomeValue
- typeCheckTopLevelType :: Maybe TcOriginatedContracts -> Ty -> Value -> TypeCheckResult SomeValue
- typeCheckValue :: forall t. SingI t => Value -> TypeCheckInstr (Value t)
- typeVerifyContract :: forall cp st. (SingI cp, SingI st) => Contract -> TypeCheckResult (Contract cp st)
- typeVerifyParameter :: SingI t => TcOriginatedContracts -> Value -> TypeCheckResult (Value t)
- typeVerifyStorage :: SingI t => Value -> TypeCheckResult (Value t)
- typeVerifyTopLevelType :: forall t. SingI t => Maybe TcOriginatedContracts -> Value -> TypeCheckResult (Value t)
- typeVerifyView :: forall arg ret st. (SingI arg, SingI ret, WellTyped st) => Notes st -> View -> TypeCheckResult (View arg st ret)
- module Morley.Michelson.TypeCheck.Error
- module Morley.Michelson.TypeCheck.Types
- module Morley.Michelson.TypeCheck.TypeCheck
- eqType :: forall (a :: T) (b :: T). Each '[SingI] [a, b] => Either TCTypeError (a :~: b)
Documentation
typeCheckContractAndStorage :: Contract -> Value -> TypeCheckResult SomeContractAndStorage Source #
Type check a contract and verify that the given storage is of the type expected by the contract.
typeCheckExt :: forall s. SingI s => TcInstrHandler -> ExpandedExtInstr -> HST s -> TypeCheckInstrNoExcept (TypeCheckedSeq s) Source #
typeCheckInstr :: TcInstrHandler Source #
Function typeCheckInstr
converts a single Michelson instruction
given in representation from Morley.Michelson.Type
module to representation
in strictly typed GADT.
As a second argument, typeCheckInstr
accepts input stack type representation.
Type checking algorithm pattern-matches on given instruction, input stack type and constructs strictly typed GADT value, checking necessary type equalities when necessary.
If there was no match on a given pair of instruction and input stack, that is interpreted as input of wrong type and type check finishes with error.
typeCheckList :: SingI inp => [ExpandedOp] -> HST inp -> TypeCheck (SomeInstr inp) Source #
Function typeCheckList
converts list of Michelson instructions
given in representation from Morley.Michelson.Type
module to representation
in strictly typed GADT.
Types are checked along the way which is necessary to construct a strictly typed value.
As a second argument, typeCheckList
accepts input stack type representation.
typeCheckListNoExcept :: SingI inp => [ExpandedOp] -> HST inp -> TypeCheckNoExcept (TypeCheckedSeq inp) Source #
Function typeCheckListNoExcept
converts list of Michelson instructions
given in representation from Morley.Michelson.Type
module to representation in a
partially typed tree. See TypeCheckedSeq
and TypeCheckedOp
.
Types are checked along the way. It is necessary to embed well typed node as well as type checking errors into the tree.
typeCheckParameter :: TcOriginatedContracts -> Ty -> Value -> TypeCheckResult SomeValue Source #
Like typeCheckValue
, but for values to be used as parameter.
Also accepts a TcOriginatedContracts
in order to be able to type-check
contract p
values (which can only be part of a parameter).
typeCheckStorage :: Ty -> Value -> TypeCheckResult SomeValue Source #
Like typeCheckValue
, but for values to be used as storage.
typeCheckTopLevelType :: Maybe TcOriginatedContracts -> Ty -> Value -> TypeCheckResult SomeValue Source #
typeCheckValue :: forall t. SingI t => Value -> TypeCheckInstr (Value t) Source #
Function typeCheckValue
converts a single Michelson value
given in representation from Morley.Michelson.Untyped
module hierarchy to
representation in strictly typed GADT.
typeCheckValue
is polymorphic in the expected type of value.
Type checking algorithm pattern-matches on parse value representation,
expected type t
and constructs Value 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.
typeVerifyContract :: forall cp st. (SingI cp, SingI st) => Contract -> TypeCheckResult (Contract cp st) Source #
typeVerifyParameter :: SingI t => TcOriginatedContracts -> Value -> TypeCheckResult (Value t) Source #
typeVerifyStorage :: SingI t => Value -> TypeCheckResult (Value t) Source #
typeVerifyTopLevelType :: forall t. SingI t => Maybe TcOriginatedContracts -> Value -> TypeCheckResult (Value t) Source #
typeVerifyView :: forall arg ret st. (SingI arg, SingI ret, WellTyped st) => Notes st -> View -> TypeCheckResult (View arg st ret) Source #