| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
PlutusCore.TypeCheck
Description
Kindtype inferencechecking.
Synopsis
- class ToKind (uni ∷ Type → Type)
- type MonadKindCheck err term uni fun ann m = (MonadError err m, ToKind uni)
- type MonadTypeCheck err term uni fun ann m = (MonadKindCheck err term uni fun ann m, MonadNormalizeType uni m, GEq uni, Ix fun)
- type TypeErrorPlc uni fun ann = TypeError (Term TyName Name uni fun ()) uni fun ann
- type Typecheckable uni fun = (ToKind uni, HasUniApply uni, ToBuiltinMeaning uni fun)
- newtype BuiltinTypes uni fun = BuiltinTypes {
- unBuiltinTypes ∷ Array fun (Dupable (Normalized (Type TyName uni ())))
- newtype KindCheckConfig = KindCheckConfig {}
- data TypeCheckConfig uni fun = TypeCheckConfig {}
- tccBuiltinTypes ∷ HasTypeCheckConfig cfg uni fun ⇒ Lens' cfg (BuiltinTypes uni fun)
- defKindCheckConfig ∷ KindCheckConfig
- builtinMeaningsToTypes ∷ (MonadKindCheck (TypeError term uni fun ann) term uni fun ann m, Typecheckable uni fun) ⇒ BuiltinSemanticsVariant fun → ann → m (BuiltinTypes uni fun)
- getDefTypeCheckConfig ∷ (MonadKindCheck (TypeError term uni fun ann) term uni fun ann m, Typecheckable uni fun) ⇒ ann → m (TypeCheckConfig uni fun)
- inferKind ∷ MonadKindCheck (TypeError term uni fun ann) term uni fun ann m ⇒ KindCheckConfig → Type TyName uni ann → m (Kind ())
- checkKind ∷ MonadKindCheck (TypeError term uni fun ann) term uni fun ann m ⇒ KindCheckConfig → ann → Type TyName uni ann → Kind () → m ()
- inferType ∷ MonadTypeCheckPlc uni fun ann m ⇒ TypeCheckConfig uni fun → Term TyName Name uni fun ann → m (Normalized (Type TyName uni ()))
- checkType ∷ MonadTypeCheckPlc uni fun ann m ⇒ TypeCheckConfig uni fun → ann → Term TyName Name uni fun ann → Normalized (Type TyName uni ()) → m ()
- inferTypeOfProgram ∷ MonadTypeCheckPlc uni fun ann m ⇒ TypeCheckConfig uni fun → Program TyName Name uni fun ann → m (Normalized (Type TyName uni ()))
- checkTypeOfProgram ∷ 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 ∷ ∀ k (a ∷ k). DefaultUni (Esc a) → SingKind k Source # | |
type MonadKindCheck err term uni fun ann m = (MonadError err m, ToKind uni) Source #
The constraints that are required for kind checking.
type MonadTypeCheck err term uni fun ann m = (MonadKindCheck err term uni fun ann m, MonadNormalizeType uni m, GEq uni, Ix fun) Source #
The general constraints that are required for type checking a Plutus AST.
type TypeErrorPlc uni fun ann = TypeError (Term TyName Name uni fun ()) uni fun ann Source #
The PLC type error type.
type Typecheckable uni fun = (ToKind uni, HasUniApply uni, ToBuiltinMeaning uni fun) 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 fun Source #
Mapping from Builtins to their Normalized Kinds.
Constructors
| BuiltinTypes | |
Fields
| |
data TypeCheckConfig uni 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 ∷ (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 Kind for each built-in function.
getDefTypeCheckConfig ∷ (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 ∷ 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 ∷ 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 ∷ 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 ∷ 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 ∷ 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 ∷ 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.