Morley.Michelson.TypeCheck

Documentation

typeCheckContract :: Contract -> TypeCheckResult ExpandedOp SomeContract

typeCheckContractAndStorage :: Contract -> Value -> TypeCheckResult ExpandedOp SomeContractAndStorage

Type check a contract and verify that the given storage is of the type expected by the contract.

typeCheckExt :: forall s op. (SingI s, IsInstrOp op) => TcInstrBase op -> ExtInstrAbstract op -> HST s -> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)

typeCheckInstr :: forall op. IsInstrOp op => TcInstrBase op -> TcInstr op (InstrAbstract op)

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)

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, IsInstrOp op) => TcInstrBase op -> [op] -> HST inp -> TypeCheckNoExcept op (TypeCheckedSeq op inp)

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

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

Like typeCheckValue, but for values to be used as storage.

typeCheckTopLevelType :: Maybe TcOriginatedContracts -> Ty -> Value -> TypeCheckResult ExpandedOp SomeValue

typeCheckValue :: forall t. SingI t => Value -> TypeCheckResult ExpandedOp (Value t)

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)

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.

typeCheckExpandedOp :: TcInstrBase ExpandedOp

typeVerifyContract :: forall cp st. (SingI cp, SingI st) => Contract -> TypeCheckResult ExpandedOp (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)

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)

Function eqType is a simple wrapper around Data.Singletons.decideEquality suited for use within Either TcTypeError a applicative.