| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
PlutusCore.TypeCheck
Description
Kindtype inferencechecking.
Synopsis
- class ToKind (uni :: Type -> Type)
- type MonadKindCheck err term (uni :: Type -> Type) fun ann (m :: Type -> Type) = (MonadError err m, ToKind uni)
- type MonadTypeCheck err term (uni :: Type -> Type) fun ann (m :: Type -> Type) = (MonadKindCheck err term uni fun ann m, MonadNormalizeType uni m, AnnotateCaseBuiltin uni, GEq uni, Ix fun)
- type TypeErrorPlc (uni :: Type -> Type) fun ann = TypeError (Term TyName Name uni fun ()) uni fun ann
- type Typecheckable (uni :: Type -> Type) fun = (ToKind uni, HasUniApply uni, ToBuiltinMeaning uni fun, AnnotateCaseBuiltin uni)
- newtype BuiltinTypes (uni :: Type -> Type) fun = BuiltinTypes {
- unBuiltinTypes :: Array fun (Dupable (Normalized (Type TyName uni ())))
- newtype KindCheckConfig = KindCheckConfig {}
- data TypeCheckConfig (uni :: Type -> Type) fun = TypeCheckConfig {
- _tccKindCheckConfig :: KindCheckConfig
- _tccBuiltinTypes :: BuiltinTypes uni fun
- tccBuiltinTypes :: HasTypeCheckConfig cfg uni fun => Lens' cfg (BuiltinTypes uni fun)
- defKindCheckConfig :: KindCheckConfig
- builtinMeaningsToTypes :: forall term (uni :: Type -> Type) fun ann m. (MonadKindCheck (TypeError term uni fun ann) term uni fun ann m, Typecheckable uni fun) => BuiltinSemanticsVariant fun -> ann -> m (BuiltinTypes uni fun)
- getDefTypeCheckConfig :: forall term (uni :: Type -> Type) fun ann m. (MonadKindCheck (TypeError term uni fun ann) term uni fun ann m, Typecheckable uni fun) => ann -> m (TypeCheckConfig uni fun)
- inferKind :: forall term (uni :: Type -> Type) fun ann m. MonadKindCheck (TypeError term uni fun ann) term uni fun ann m => KindCheckConfig -> Type TyName uni ann -> m (Kind ())
- checkKind :: forall term (uni :: Type -> Type) fun ann m. MonadKindCheck (TypeError term uni fun ann) term uni fun ann m => KindCheckConfig -> ann -> Type TyName uni ann -> Kind () -> m ()
- inferType :: forall (uni :: Type -> Type) fun ann m. MonadTypeCheckPlc uni fun ann m => TypeCheckConfig uni fun -> Term TyName Name uni fun ann -> m (Normalized (Type TyName uni ()))
- checkType :: forall (uni :: Type -> Type) fun ann m. MonadTypeCheckPlc uni fun ann m => TypeCheckConfig uni fun -> ann -> Term TyName Name uni fun ann -> Normalized (Type TyName uni ()) -> m ()
- inferTypeOfProgram :: forall (uni :: Type -> Type) fun ann m. MonadTypeCheckPlc uni fun ann m => TypeCheckConfig uni fun -> Program TyName Name uni fun ann -> m (Normalized (Type TyName uni ()))
- checkTypeOfProgram :: forall (uni :: Type -> Type) fun ann m. MonadTypeCheckPlc uni fun ann m => TypeCheckConfig uni fun -> ann -> Program TyName Name uni fun ann -> Normalized (Type TyName uni ()) -> m ()
Documentation
class ToKind (uni :: Type -> Type) Source #
For computing the Plutus kind of a built-in type. See kindOfBuiltinType.
Minimal complete definition
Instances
| ToKind DefaultUni Source # | |
Defined in PlutusCore.Default.Universe Methods toSingKind :: forall k (a :: k). DefaultUni (Esc a) -> SingKind k Source # | |
type MonadKindCheck err term (uni :: Type -> Type) fun ann (m :: Type -> Type) = (MonadError err m, ToKind uni) Source #
The constraints that are required for kind checking.
type MonadTypeCheck err term (uni :: Type -> Type) fun ann (m :: Type -> Type) = (MonadKindCheck err term uni fun ann m, MonadNormalizeType uni m, AnnotateCaseBuiltin uni, GEq uni, Ix fun) Source #
The general constraints that are required for type checking a Plutus AST.
type TypeErrorPlc (uni :: Type -> Type) fun ann = TypeError (Term TyName Name uni fun ()) uni fun ann Source #
The PLC type error type.
type Typecheckable (uni :: Type -> Type) fun = (ToKind uni, HasUniApply uni, ToBuiltinMeaning uni fun, AnnotateCaseBuiltin uni) Source #
The constraint for built-in types/functions are kind/type-checkable.
We keep this separate from MonadKindCheck/MonadTypeCheck, because those mainly constrain the
monad and Typecheckable constraints only the builtins. In particular useful when the monad gets
instantiated and builtins don't. Another reason is that Typecheckable is not required during
type checking, since it's only needed for computing BuiltinTypes, which is passed as a regular
argument to the worker of the type checker.
Configuration.
newtype BuiltinTypes (uni :: Type -> Type) fun Source #
Mapping from Builtins to their Normalized Types.
Constructors
| BuiltinTypes | |
Fields
| |
newtype KindCheckConfig Source #
Configuration of the kind checker.
Constructors
| KindCheckConfig | |
Instances
data TypeCheckConfig (uni :: Type -> Type) fun Source #
Configuration of the type checker.
Constructors
| TypeCheckConfig | |
Fields
| |
Instances
| HasKindCheckConfig (TypeCheckConfig uni fun) Source # | |
Defined in PlutusCore.TypeCheck.Internal Methods kindCheckConfig :: Lens' (TypeCheckConfig uni fun) KindCheckConfig Source # kccHandleNameMismatches :: Lens' (TypeCheckConfig uni fun) HandleNameMismatches Source # | |
| HasTypeCheckConfig (TypeCheckConfig uni fun) uni fun Source # | |
Defined in PlutusCore.TypeCheck.Internal Methods typeCheckConfig :: Lens' (TypeCheckConfig uni fun) (TypeCheckConfig uni fun) Source # tccKindCheckConfig :: Lens' (TypeCheckConfig uni fun) KindCheckConfig Source # tccBuiltinTypes :: Lens' (TypeCheckConfig uni fun) (BuiltinTypes uni fun) Source # | |
tccBuiltinTypes :: HasTypeCheckConfig cfg uni fun => Lens' cfg (BuiltinTypes uni fun) Source #
defKindCheckConfig :: KindCheckConfig Source #
The default kind checking config.
builtinMeaningsToTypes :: forall term (uni :: Type -> Type) fun ann m. (MonadKindCheck (TypeError term uni fun ann) term uni fun ann m, Typecheckable uni fun) => BuiltinSemanticsVariant fun -> ann -> m (BuiltinTypes uni fun) Source #
Extract the TypeScheme from a BuiltinMeaning and convert it to the
corresponding Type for each built-in function.
getDefTypeCheckConfig :: forall term (uni :: Type -> Type) fun ann m. (MonadKindCheck (TypeError term uni fun ann) term uni fun ann m, Typecheckable uni fun) => ann -> m (TypeCheckConfig uni fun) Source #
Get the default type checking config.
Kindtype inferencechecking.
inferKind :: forall term (uni :: Type -> Type) fun ann m. MonadKindCheck (TypeError term uni fun ann) term uni fun ann m => KindCheckConfig -> Type TyName uni ann -> m (Kind ()) Source #
Infer the kind of a type.
checkKind :: forall term (uni :: Type -> Type) fun ann m. MonadKindCheck (TypeError term uni fun ann) term uni fun ann m => KindCheckConfig -> ann -> Type TyName uni ann -> Kind () -> m () Source #
Check a type against a kind.
Infers the kind of the type and checks that it's equal to the given kind
throwing a TypeError (annotated with the value of the ann argument) otherwise.
inferType :: forall (uni :: Type -> Type) fun ann m. MonadTypeCheckPlc uni fun ann m => TypeCheckConfig uni fun -> Term TyName Name uni fun ann -> m (Normalized (Type TyName uni ())) Source #
Infer the type of a term.
checkType :: forall (uni :: Type -> Type) fun ann m. MonadTypeCheckPlc uni fun ann m => TypeCheckConfig uni fun -> ann -> Term TyName Name uni fun ann -> Normalized (Type TyName uni ()) -> m () Source #
Check a term against a type.
Infers the type of the term and checks that it's equal to the given type
throwing a TypeError (annotated with the value of the ann argument) otherwise.
inferTypeOfProgram :: forall (uni :: Type -> Type) fun ann m. MonadTypeCheckPlc uni fun ann m => TypeCheckConfig uni fun -> Program TyName Name uni fun ann -> m (Normalized (Type TyName uni ())) Source #
Infer the type of a program.
checkTypeOfProgram :: forall (uni :: Type -> Type) fun ann m. MonadTypeCheckPlc uni fun ann m => TypeCheckConfig uni fun -> ann -> Program TyName Name uni fun ann -> Normalized (Type TyName uni ()) -> m () Source #
Check a program against a type.
Infers the type of the program and checks that it's equal to the given type
throwing a TypeError (annotated with the value of the ann argument) otherwise.