Safe Haskell	None
Language	Haskell2010

PlutusIR.TypeCheck

Contents

Configuration.
Type checking, extending the plc typechecker

Description

Kindtype inferencechecking, 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 #

Mapping from Builtins to their Types.

Constructors

BuiltinTypes
Fields unBuiltinTypes :: Maybe (Array fun (Dupable (Normalized (Type TyName uni ()))))

data PirTCConfig uni fun Source #

extending the plc typecheck config with AllowEscape

Constructors

PirTCConfig
Fields _pirConfigTCConfig :: TypeCheckConfig uni fun _pirConfigAllowEscape :: 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]