| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
PlutusIR.TypeCheck
Description
Kind type inference checking, mirroring PlutusCore.TypeCheck
Synopsis
-
newtype
BuiltinTypes
uni fun =
BuiltinTypes
{
- unBuiltinTypes :: Maybe ( Array fun ( Dupable ( Normalized ( Type TyName uni ()))))
-
data
PirTCConfig
uni fun =
PirTCConfig
{
- _pirConfigTCConfig :: TypeCheckConfig uni fun
- _pirConfigAllowEscape :: AllowEscape
- tccBuiltinTypes :: HasTypeCheckConfig c uni fun => Lens' c ( BuiltinTypes uni fun)
- getDefTypeCheckConfig :: forall uni fun m err ann. ( MonadError err m, AsTypeError err ( Term TyName Name uni fun ()) uni fun ann, Typecheckable uni fun) => ann -> m ( PirTCConfig uni fun)
- inferType :: ( AsTypeError e ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann, MonadError e m, MonadQuote m, GEq uni, Ix fun) => PirTCConfig uni fun -> Term TyName Name uni fun ann -> m ( Normalized ( Type TyName uni ()))
- checkType :: ( AsTypeError e ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann, MonadError e m, MonadQuote m, GEq uni, Ix fun) => PirTCConfig uni fun -> ann -> Term TyName Name uni fun ann -> Normalized ( Type TyName uni ()) -> m ()
- inferTypeOfProgram :: ( AsTypeError e ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann, MonadError e m, MonadQuote m, GEq uni, Ix fun) => PirTCConfig uni fun -> Program TyName Name uni fun ann -> m ( Normalized ( Type TyName uni ()))
- checkTypeOfProgram :: ( AsTypeError e ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann, MonadError e m, MonadQuote m, GEq uni, Ix fun) => PirTCConfig uni fun -> ann -> Program TyName Name uni fun ann -> Normalized ( Type TyName uni ()) -> m ()
Configuration.
newtype BuiltinTypes uni fun Source #
Constructors
| BuiltinTypes | |
|
Fields
|
|
data PirTCConfig uni fun Source #
extending the plc typecheck config with AllowEscape
Constructors
| PirTCConfig | |
|
Fields
|
|
tccBuiltinTypes :: HasTypeCheckConfig c uni fun => Lens' c ( BuiltinTypes uni fun) Source #
getDefTypeCheckConfig :: forall uni fun m err ann. ( MonadError err m, AsTypeError err ( Term TyName Name uni fun ()) uni fun ann, Typecheckable uni fun) => ann -> m ( PirTCConfig uni fun) Source #
The default
TypeCheckConfig
.
Type checking, extending the plc typechecker
inferType :: ( AsTypeError e ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann, MonadError e m, MonadQuote m, GEq uni, Ix fun) => 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 :: ( AsTypeError e ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann, MonadError e m, MonadQuote m, GEq uni, Ix fun) => 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 :: ( AsTypeError e ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann, MonadError e m, MonadQuote m, GEq uni, Ix fun) => 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 :: ( AsTypeError e ( Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann, MonadError e m, MonadQuote m, GEq uni, Ix fun) => 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]