| 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, AsTypeError err term uni fun ann, 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 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 err term uni fun ann m, Typecheckable uni fun) ⇒ BuiltinSemanticsVariant fun → ann → m (BuiltinTypes uni fun)
- getDefTypeCheckConfig ∷ (MonadKindCheck err term uni fun ann m, Typecheckable uni fun) ⇒ ann → m (TypeCheckConfig uni fun)
- inferKind ∷ MonadKindCheck err term uni fun ann m ⇒ KindCheckConfig → Type TyName uni ann → m (Kind ())
- checkKind ∷ MonadKindCheck err term uni fun ann m ⇒ KindCheckConfig → ann → Type TyName uni ann → Kind () → m ()
- inferType ∷ MonadTypeCheckPlc err uni fun ann m ⇒ TypeCheckConfig uni fun → Term TyName Name uni fun ann → m (Normalized (Type TyName uni ()))
- checkType ∷ MonadTypeCheckPlc err uni fun ann m ⇒ TypeCheckConfig uni fun → ann → Term TyName Name uni fun ann → Normalized (Type TyName uni ()) → m ()
- inferTypeOfProgram ∷ MonadTypeCheckPlc err uni fun ann m ⇒ TypeCheckConfig uni fun → Program TyName Name uni fun ann → m (Normalized (Type TyName uni ()))
- checkTypeOfProgram ∷ MonadTypeCheckPlc err 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, AsTypeError err term uni fun ann, 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 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 err 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 err term uni fun ann m, Typecheckable uni fun) ⇒ ann → m (TypeCheckConfig uni fun) Source #
Get the default type checking config.
Kindtype inferencechecking.
inferKind ∷ MonadKindCheck err term uni fun ann m ⇒ KindCheckConfig → Type TyName uni ann → m (Kind ()) Source #
Infer the kind of a type.
checkKind ∷ MonadKindCheck err 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 err 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 err 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 err 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 err 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.