| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Morley.Michelson.TypeCheck.Instr
Description
Module, providing functions for conversion from
instruction and value representation from Morley.Michelson.Type module
to strictly-typed GADT-based representation from Morley.Michelson.Value module.
This conversion is labeled as type check because that's what we are obliged to do on our way.
Type check algorithm relies on the property of Michelson language that each instruction on a given input stack type produces a definite output stack type. Michelson contract defines concrete types for storage and parameter, from which input stack type is deduced. Then this type is being combined with each subsequent instruction, producing next stack type after each application.
Function typeCheck takes list of instructions and returns value of type
Instr inp out along with HST inp and HST out all wrapped into
SomeTcInstr data type. This wrapping is done to satisfy Haskell type
system (which has no support for dependent types).
Functions typeCheckInstr, typeCheckValue behave similarly.
When a recursive call is made within typeCheck, typeCheckInstr or
typeCheckValue, result of a call is unwrapped from SomeTcInstr and type
information from HST inp and HST out is being used to assert that
recursive call returned instruction of expected type
(error is thrown otherwise).
Synopsis
- typeCheckContract :: Contract -> TypeCheckResult ExpandedOp SomeContract
- typeCheckContract' :: TcInstrBase op -> Contract' op -> TypeCheckResult op SomeContract
- typeCheckContractAndStorage :: Contract -> Value -> TypeCheckResult ExpandedOp SomeContractAndStorage
- typeCheckContractAndStorage' :: IsInstrOp op => TcInstrBase op -> Contract' op -> Value' [] op -> TypeCheckResult op SomeContractAndStorage
- typeCheckInstr :: forall op. IsInstrOp op => TcInstrBase op -> TcInstr op (InstrAbstract [] op)
- typeCheckList :: SingI inp => [ExpandedOp] -> HST inp -> TypeCheck ExpandedOp (SomeTcInstr inp)
- tcList :: IsInstrOp op => TcInstrBase op -> TcInstr op [op]
- typeCheckListNoExcept :: (SingI inp, IsInstrOp op) => TcInstrBase op -> [op] -> HST inp -> TypeCheckNoExcept op (TypeCheckedSeq op inp)
- typeCheckParameter :: TcOriginatedContracts -> Ty -> Value -> TypeCheckResult ExpandedOp SomeValue
- typeCheckStorage :: Ty -> Value -> TypeCheckResult ExpandedOp SomeValue
- typeCheckTopLevelType :: Maybe TcOriginatedContracts -> Ty -> Value -> TypeCheckResult ExpandedOp SomeValue
- typeCheckTopLevelType' :: IsInstrOp op => TcInstrBase op -> Maybe TcOriginatedContracts -> Ty -> Value' [] op -> TypeCheckResult op SomeValue
- typeCheckViews :: WellTyped st => Contract' (TypeCheckedOp ExpandedOp) -> Notes st -> ViewsSet ExpandedOp -> TypeCheck ExpandedOp (ViewsSet st)
- typeCheckView' :: WellTyped st => TcInstrBase op -> Notes st -> View' op -> TypeCheck op (SomeView st)
- typeCheckViews' :: forall st op. WellTyped st => TcInstrBase op -> Contract' (TypeCheckedOp op) -> Notes st -> ViewsSet op -> TypeCheck op (ViewsSet st)
- typeCheckValue :: forall t. SingI t => Value -> TypeCheckResult ExpandedOp (Value t)
- typeCheckValueRunCodeCompat :: forall t. SingI t => BigMapFinder -> Value -> TypeCheckResult ExpandedOp (Value t)
- typeCheckExpandedOp :: TcInstrBase ExpandedOp
- typeVerifyContract :: forall cp st. (SingI cp, SingI st) => Contract -> TypeCheckResult ExpandedOp (Contract cp st)
- typeVerifyContract' :: forall cp st op. (SingI cp, SingI st) => TcInstrBase op -> Contract' op -> TypeCheckResult op (Contract cp st)
- typeVerifyParameter :: SingI t => TcOriginatedContracts -> Value -> TypeCheckResult ExpandedOp (Value t)
- typeVerifyStorage :: SingI t => Value -> TypeCheckResult ExpandedOp (Value t)
- typeVerifyTopLevelType :: forall t. SingI t => Maybe TcOriginatedContracts -> Value -> TypeCheckResult ExpandedOp (Value t)
- typeVerifyView :: forall arg ret st. (SingI arg, SingI ret, WellTyped st) => Notes st -> View -> TypeCheckResult ExpandedOp (View arg st ret)
- typeVerifyView' :: forall arg ret st op. (SingI arg, SingI ret, WellTyped st) => TcInstrBase op -> Notes st -> View' op -> TypeCheckResult op (View arg st ret)
Documentation
typeCheckContract' :: TcInstrBase op -> Contract' op -> TypeCheckResult op SomeContract Source #
typeCheckContractAndStorage :: Contract -> Value -> TypeCheckResult ExpandedOp SomeContractAndStorage Source #
Type check a contract and verify that the given storage is of the type expected by the contract.
typeCheckContractAndStorage' :: IsInstrOp op => TcInstrBase op -> Contract' op -> Value' [] op -> TypeCheckResult op SomeContractAndStorage Source #
typeCheckInstr :: forall op. IsInstrOp op => TcInstrBase op -> TcInstr op (InstrAbstract [] op) 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 ExpandedOp (SomeTcInstr 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.
tcList :: IsInstrOp op => TcInstrBase op -> TcInstr op [op] Source #
Alias for typeCheckImpl.
typeCheckListNoExcept :: (SingI inp, IsInstrOp op) => TcInstrBase op -> [op] -> HST inp -> TypeCheckNoExcept op (TypeCheckedSeq op 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 ExpandedOp 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 ExpandedOp SomeValue Source #
Like typeCheckValue, but for values to be used as storage.
typeCheckTopLevelType :: Maybe TcOriginatedContracts -> Ty -> Value -> TypeCheckResult ExpandedOp SomeValue Source #
typeCheckTopLevelType' :: IsInstrOp op => TcInstrBase op -> Maybe TcOriginatedContracts -> Ty -> Value' [] op -> TypeCheckResult op SomeValue Source #
typeCheckViews :: WellTyped st => Contract' (TypeCheckedOp ExpandedOp) -> Notes st -> ViewsSet ExpandedOp -> TypeCheck ExpandedOp (ViewsSet st) Source #
typeCheckView' :: WellTyped st => TcInstrBase op -> Notes st -> View' op -> TypeCheck op (SomeView st) Source #
typeCheckViews' :: forall st op. WellTyped st => TcInstrBase op -> Contract' (TypeCheckedOp op) -> Notes st -> ViewsSet op -> TypeCheck op (ViewsSet st) Source #
typeCheckValue :: forall t. SingI t => Value -> TypeCheckResult ExpandedOp (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.
typeCheckValueRunCodeCompat :: forall t. SingI t => BigMapFinder -> Value -> TypeCheckResult ExpandedOp (Value t) Source #
Simulates the typechecking behavior of the RPC's /run_code endpoint.
If an integer is found where a big_map is expected, we check if a big_map exists with that ID. If it does, and if the big_map's value and key have the expected types, we replace the big_map ID with the corresponding big_map value.
typeVerifyContract :: forall cp st. (SingI cp, SingI st) => Contract -> TypeCheckResult ExpandedOp (Contract cp st) Source #
typeVerifyContract' :: forall cp st op. (SingI cp, SingI st) => TcInstrBase op -> Contract' op -> TypeCheckResult op (Contract cp st) Source #
typeVerifyParameter :: SingI t => TcOriginatedContracts -> Value -> TypeCheckResult ExpandedOp (Value t) Source #
typeVerifyStorage :: SingI t => Value -> TypeCheckResult ExpandedOp (Value t) Source #
typeVerifyTopLevelType :: forall t. SingI t => Maybe TcOriginatedContracts -> Value -> TypeCheckResult ExpandedOp (Value t) Source #
typeVerifyView :: forall arg ret st. (SingI arg, SingI ret, WellTyped st) => Notes st -> View -> TypeCheckResult ExpandedOp (View arg st ret) Source #
typeVerifyView' :: forall arg ret st op. (SingI arg, SingI ret, WellTyped st) => TcInstrBase op -> Notes st -> View' op -> TypeCheckResult op (View arg st ret) Source #