plutus-core-0.1.0.0: Language library for Plutus Core
Safe HaskellNone
LanguageHaskell2010

PlutusIR.TypeCheck

Description

Kindtype inferencechecking, mirroring PlutusCore.TypeCheck

Synopsis

Configuration.

newtype BuiltinTypes uni fun Source #

Mapping from Builtins to their Types.

Constructors

BuiltinTypes 

Fields

data PirTCConfig uni fun Source #

extending the plc typecheck config with AllowEscape

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]