Michelson.TypeCheck

Documentation

typeCheckContract :: Contract -> TypeCheckOptions -> Either TCError SomeContract

typeCheckContractAndStorage :: Contract -> Value -> Either TCError SomeContractAndStorage

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

typeCheckExt :: forall s. Typeable s => TcInstrHandler -> ExpandedExtInstr -> HST s -> TypeCheckInstrNoExcept (TypeCheckedSeq s)

typeCheckInstr :: TcInstrHandler

Function typeCheckInstr converts a single Michelson instruction given in representation from 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 neccessary.

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 :: Typeable inp => [ExpandedOp] -> HST inp -> TypeCheck (SomeInstr inp)

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.

typeCheckListNoExcept :: Typeable inp => [ExpandedOp] -> HST inp -> TypeCheckNoExcept (TypeCheckedSeq inp)

Function typeCheckListNoExcept converts list of Michelson instructions given in representation from 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 -> Type -> Value -> Either TCError 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 :: Type -> Value -> Either TCError SomeValue

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

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

Function typeCheckValue converts a single Michelson value given in representation from 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.

typeVerifyParameter :: SingI t => TcOriginatedContracts -> Value -> Either TCError (Value t)

typeVerifyStorage :: SingI t => Value -> Either TCError (Value t)

module Michelson.TypeCheck.Error

module Michelson.TypeCheck.Types

module Michelson.TypeCheck.TypeCheck

eqType :: forall (a :: T) (b :: T). Each '[KnownT] [a, b] => Either TCTypeError (a :~: b)

Function eqType is a simple wrapper around Data.Typeable.eqT suited for use within Either TCTypeError a applicative.

matchTypes :: forall t1 t2. Each '[KnownT] [t1, t2] => Notes t1 -> Notes t2 -> Either TCTypeError (t1 :~: t2, Notes t1)

Check whether given types are structurally equal and annotations converge.