Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- typeCheckContract :: TcOriginatedContracts -> Contract -> Either TCError SomeContract
- typeCheckTopLevelType :: HasCallStack => TcOriginatedContracts -> Type -> Value -> Either TCError SomeValue
- typeVerifyTopLevelType :: (Typeable t, SingI t, HasCallStack) => TcOriginatedContracts -> Value -> Either TCError (Value t)
- typeCheckValue :: Value -> (Sing t, Notes t) -> TypeCheckInstr SomeNotedValue
- typeVerifyValue :: forall t. (Typeable t, SingI t) => Value -> TypeCheckInstr (Value t)
- typeCheckList :: Typeable inp => [ExpandedOp] -> HST inp -> TypeCheck (SomeInstr inp)
- 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)
- matchTypes :: forall t1 t2. Each [Typeable, SingI] [t1, t2] => Notes t1 -> Notes t2 -> Either TCTypeError (t1 :~: t2, Notes t1)
Documentation
typeCheckTopLevelType :: HasCallStack => TcOriginatedContracts -> Type -> Value -> Either TCError SomeValue Source #
typeVerifyTopLevelType :: (Typeable t, SingI t, HasCallStack) => TcOriginatedContracts -> Value -> Either TCError (Value t) Source #
typeCheckValue :: Value -> (Sing t, Notes t) -> TypeCheckInstr SomeNotedValue Source #
Function typeCheckValue
converts a single Michelson value
given in representation from Michelson.Untyped
module hierarchy 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) Source #
Like typeCheckValue
, but returns value of a desired type.
typeCheckList :: Typeable inp => [ExpandedOp] -> HST inp -> TypeCheck (SomeInstr inp) Source #
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 Source #
typeCheckExt :: forall s. Typeable s => TypeCheckListHandler s -> ExpandedExtInstr -> HST s -> TypeCheckInstr (SomeInstr s) Source #
module Michelson.TypeCheck.Error
module Michelson.TypeCheck.Types