| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
PlutusIR.TypeCheck.Internal
Description
The internal module of the type checker that defines the actual algorithms, but not the user-facing API.
Synopsis
- newtype BuiltinTypes (uni ∷ Type → Type) fun = BuiltinTypes {
- unBuiltinTypes ∷ Array fun (Dupable (Normalized (Type TyName uni ())))
- data TypeCheckConfig (uni ∷ Type → Type) fun = TypeCheckConfig {}
- type TypeCheckT (uni ∷ Type → Type) fun cfg (m ∷ Type → Type) = ReaderT (TypeCheckEnv uni fun cfg) m
- type MonadKindCheck err term (uni ∷ Type → Type) fun ann (m ∷ Type → Type) = (MonadError err m, AsTypeError err term uni fun ann, ToKind uni)
- type MonadTypeCheck err term (uni ∷ Type → Type) fun ann (m ∷ Type → Type) = (MonadKindCheck err term uni fun ann m, MonadNormalizeType uni m, GEq uni, Ix fun)
- type MonadTypeCheckPir err uni fun ann m = (MonadTypeCheck err (Term TyName Name uni fun ()) uni fun ann m, AsTypeErrorExt err uni ann)
- tccBuiltinTypes ∷ HasTypeCheckConfig cfg uni fun ⇒ Lens' cfg (BuiltinTypes uni fun)
- data PirTCConfig uni fun = PirTCConfig {}
- data AllowEscape
- inferTypeM ∷ ∀ err m uni fun ann. MonadTypeCheckPir err uni fun ann m ⇒ Term TyName Name uni fun ann → PirTCEnv uni fun m (Normalized (Type TyName uni ()))
- checkTypeM ∷ MonadTypeCheckPir err uni fun ann m ⇒ ann → Term TyName Name uni fun ann → Normalized (Type TyName uni ()) → PirTCEnv uni fun m ()
- runTypeCheckM ∷ PirTCConfig uni fun → PirTCEnv uni fun m a → m a
Documentation
newtype BuiltinTypes (uni ∷ Type → Type) fun Source #
Mapping from Builtins to their Normalized Kinds.
Constructors
| BuiltinTypes | |
Fields
| |
data TypeCheckConfig (uni ∷ Type → Type) fun Source #
Configuration of the type checker.
Constructors
| TypeCheckConfig | |
Fields | |
Instances
| HasKindCheckConfig (TypeCheckConfig uni fun) | |
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 | |
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 # | |
type TypeCheckT (uni ∷ Type → Type) fun cfg (m ∷ Type → Type) = ReaderT (TypeCheckEnv uni fun cfg) m Source #
The type checking monad that the type checker runs in.
In contains a TypeCheckEnv and allows to throw TypeErrors.
type MonadKindCheck err term (uni ∷ Type → Type) fun ann (m ∷ Type → Type) = (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 ∷ Type → Type) fun ann (m ∷ Type → Type) = (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 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.
tccBuiltinTypes ∷ HasTypeCheckConfig cfg uni fun ⇒ Lens' cfg (BuiltinTypes uni fun) Source #
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 # | |
data AllowEscape Source #
Extra flag to be passed in the TypeCheckM Reader context, to signal if the PIR expression currently being typechecked is at the top-level and thus its type can escape, or nested and thus not allowed to escape.
inferTypeM ∷ ∀ err m uni fun ann. MonadTypeCheckPir err uni fun ann m ⇒ Term TyName Name uni fun ann → PirTCEnv uni fun m (Normalized (Type TyName uni ())) Source #
Synthesize the type of a term, returning a normalized type.
checkTypeM ∷ MonadTypeCheckPir err uni fun ann m ⇒ ann → Term TyName Name uni fun ann → Normalized (Type TyName uni ()) → PirTCEnv uni fun m () Source #
Check a Term against a NormalizedType.
runTypeCheckM ∷ PirTCConfig uni fun → PirTCEnv uni fun m a → m a Source #
Run a TypeCheckM computation by supplying a TypeCheckConfig to it.
Differs from its PLC version in that is passes an extra env flag YesEscape.