| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
PlutusIR.TypeCheck
Description
Kindtype inferencechecking, mirroring PlutusCore.TypeCheck
Synopsis
- newtype BuiltinTypes (uni ∷ Type → Type) fun = BuiltinTypes {
- unBuiltinTypes ∷ Array fun (Dupable (Normalized (Type TyName uni ())))
- data PirTCConfig uni fun = PirTCConfig {}
- tccBuiltinTypes ∷ HasTypeCheckConfig cfg uni fun ⇒ Lens' cfg (BuiltinTypes uni fun)
- getDefTypeCheckConfig ∷ (MonadKindCheck err term uni fun ann m, Typecheckable uni fun) ⇒ ann → m (PirTCConfig uni fun)
- inferType ∷ MonadTypeCheckPir err uni fun ann m ⇒ PirTCConfig uni fun → Term TyName Name uni fun ann → m (Normalized (Type TyName uni ()))
- checkType ∷ MonadTypeCheckPir err uni fun ann m ⇒ PirTCConfig uni fun → ann → Term TyName Name uni fun ann → Normalized (Type TyName uni ()) → m ()
- inferTypeOfProgram ∷ MonadTypeCheckPir err uni fun ann m ⇒ PirTCConfig uni fun → Program TyName Name uni fun ann → m (Normalized (Type TyName uni ()))
- checkTypeOfProgram ∷ MonadTypeCheckPir err uni fun ann m ⇒ PirTCConfig uni fun → ann → Program TyName Name uni fun ann → Normalized (Type TyName uni ()) → m ()
- type MonadTypeCheckPir err uni fun ann m = (MonadTypeCheck err (Term TyName Name uni fun ()) uni fun ann m, AsTypeErrorExt err uni ann)
Configuration.
newtype BuiltinTypes (uni ∷ Type → Type) fun Source #
Mapping from Builtins to their Normalized Kinds.
Constructors
| BuiltinTypes | |
Fields
| |
data PirTCConfig uni fun Source #
extending the plc typecheck config with AllowEscape
Constructors
| PirTCConfig | |
Fields | |
Instances
| HasKindCheckConfig (PirTCConfig uni fun) Source # | |
Defined in PlutusIR.Compiler.Types Methods kindCheckConfig ∷ Lens' (PirTCConfig uni fun) KindCheckConfig Source # kccHandleNameMismatches ∷ Lens' (PirTCConfig uni fun) HandleNameMismatches Source # | |
| HasTypeCheckConfig (PirTCConfig uni fun) uni fun Source # | |
Defined in PlutusIR.Compiler.Types Methods typeCheckConfig ∷ Lens' (PirTCConfig uni fun) (TypeCheckConfig uni fun) Source # tccKindCheckConfig ∷ Lens' (PirTCConfig uni fun) KindCheckConfig Source # tccBuiltinTypes ∷ Lens' (PirTCConfig uni fun) (BuiltinTypes uni fun) Source # | |
tccBuiltinTypes ∷ HasTypeCheckConfig cfg uni fun ⇒ Lens' cfg (BuiltinTypes uni fun) Source #
getDefTypeCheckConfig ∷ (MonadKindCheck err term uni fun ann m, Typecheckable uni fun) ⇒ ann → m (PirTCConfig uni fun) Source #
The default TypeCheckConfig.
Type checking, extending the plc typechecker
inferType ∷ MonadTypeCheckPir err uni fun ann m ⇒ PirTCConfig uni fun → Term TyName Name uni fun ann → m (Normalized (Type TyName uni ())) Source #
Infer the type of a term. Note: The "inferred type" can escape its scope if YesEscape config is passed, see [PIR vs Paper Escaping Types Difference]
checkType ∷ MonadTypeCheckPir err uni fun ann m ⇒ PirTCConfig 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.
Note: this may allow witnessing a type that escapes its scope, see
[PIR vs Paper Escaping Types Difference]
inferTypeOfProgram ∷ MonadTypeCheckPir err uni fun ann m ⇒ PirTCConfig uni fun → Program TyName Name uni fun ann → m (Normalized (Type TyName uni ())) Source #
Infer the type of a program. Note: The "inferred type" can escape its scope if YesEscape config is passed, see [PIR vs Paper Escaping Types Difference]
checkTypeOfProgram ∷ MonadTypeCheckPir err uni fun ann m ⇒ PirTCConfig 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.
Note: this may allow witnessing a type that escapes its scope, see
[PIR vs Paper Escaping Types Difference]
type MonadTypeCheckPir err uni fun ann m = (MonadTypeCheck err (Term TyName Name uni fun ()) uni fun ann m, AsTypeErrorExt err uni ann) Source #
The constraints that are required for type checking Plutus IR.