Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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 Builtin
s to their Normalized
Kind
s.
BuiltinTypes | |
|
data TypeCheckConfig (uni ∷ Type → Type) fun Source #
Configuration of the type checker.
Instances
HasKindCheckConfig (TypeCheckConfig uni fun) | |
Defined in PlutusCore.TypeCheck.Internal 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 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 TypeError
s.
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
Instances
HasKindCheckConfig (PirTCConfig uni fun) Source # | |
Defined in PlutusIR.Compiler.Types 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 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
.