Michelson.TypeCheck

Documentation

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

typeCheckValue :: Value -> (Sing t, Notes t) -> TypeCheckInstr SomeValue

Function typeCheckValue converts a single Michelson value given in representation from Michelson.Type module to representation in strictly typed GADT.

As a second argument, typeCheckValue 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.

typeVerifyValue :: forall t. (Typeable t, SingI t) => Value -> TypeCheckInstr (Value t)

Like typeCheckValue, but returns value of a desired type.

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.

typeCheckCValue :: Value' op -> CT -> Either (Value' op, TCTypeError) SomeCValue

typeCheckExt :: forall s. Typeable s => TypeCheckListHandler s -> ExpandedExtInstr -> HST s -> TypeCheckInstr (SomeInstr s)

module Michelson.TypeCheck.Error

module Michelson.TypeCheck.Types

module Michelson.TypeCheck.TypeCheck

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

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

compareTypes :: forall t. (Typeable t, SingI t) => (Sing t, Notes t) -> Type -> Either TCTypeError ()

Check whether typed and untyped types converge