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
- type MonadKindCheck err term uni fun ann m = (MonadError err m, AsTypeError err term uni fun ann, ToKind uni)
- type MonadTypeCheck err term uni fun ann m = (MonadKindCheck err term uni fun ann m, MonadNormalizeType uni m, GEq uni, Ix fun)
- newtype BuiltinTypes uni fun = BuiltinTypes {
- unBuiltinTypes ∷ Array fun (Dupable (Normalized (Type TyName uni ())))
- newtype KindCheckConfig = KindCheckConfig {}
- data TypeCheckConfig uni fun = TypeCheckConfig {}
- type TyVarKinds = UniqueMap TypeUnique (Named (Kind ()))
- type VarTypes uni = UniqueMap TermUnique (Named (Dupable (Normalized (Type TyName uni ()))))
- data HandleNameMismatches
- class HasKindCheckConfig c where
- class HasKindCheckConfig cfg ⇒ HasTypeCheckConfig cfg uni fun | cfg → uni fun where
- typeCheckConfig ∷ Lens' cfg (TypeCheckConfig uni fun)
- tccKindCheckConfig ∷ Lens' cfg KindCheckConfig
- tccBuiltinTypes ∷ Lens' cfg (BuiltinTypes uni fun)
- data TypeCheckEnv uni fun cfg = TypeCheckEnv {
- _tceTypeCheckConfig ∷ cfg
- _tceTyVarKinds ∷ TyVarKinds
- _tceVarTypes ∷ VarTypes uni
- type TypeCheckT uni fun cfg m = ReaderT (TypeCheckEnv uni fun cfg) m
- type MonadTypeCheckPlc err uni fun ann m = MonadTypeCheck err (Term TyName Name uni fun ()) uni fun ann m
- withVar ∷ Name → Normalized (Type TyName uni ()) → TypeCheckT uni fun cfg m a → TypeCheckT uni fun cfg m a
- normalizeTypeM ∷ MonadNormalizeType uni m ⇒ Type TyName uni ann → TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
- substNormalizeTypeM ∷ MonadNormalizeType uni m ⇒ Normalized (Type TyName uni ()) → TyName → Type TyName uni () → TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
- checkTypeM ∷ (MonadTypeCheckPlc err uni fun ann m, HasTypeCheckConfig cfg uni fun) ⇒ ann → Term TyName Name uni fun ann → Normalized (Type TyName uni ()) → TypeCheckT uni fun cfg m ()
- runTypeCheckM ∷ cfg → TypeCheckT uni fun cfg m a → m a
- withTyVar ∷ TyName → Kind () → TypeCheckT uni fun cfg m a → TypeCheckT uni fun cfg m a
- tceTyVarKinds ∷ ∀ uni fun cfg fun. Lens (TypeCheckEnv uni fun cfg) (TypeCheckEnv uni fun cfg) TyVarKinds TyVarKinds
- lookupBuiltinM ∷ (MonadTypeCheck err term uni fun ann m, HasTypeCheckConfig cfg uni fun) ⇒ ann → fun → TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
- tceTypeCheckConfig ∷ ∀ uni fun cfg fun cfg. Lens (TypeCheckEnv uni fun cfg) (TypeCheckEnv uni fun cfg) cfg cfg
- tceVarTypes ∷ ∀ uni fun cfg uni fun. Lens (TypeCheckEnv uni fun cfg) (TypeCheckEnv uni fun cfg) (VarTypes uni) (VarTypes uni)
- lookupTyVarM ∷ (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) ⇒ ann → TyName → TypeCheckT uni fun cfg m (Kind ())
- lookupVarM ∷ (MonadTypeCheck err term uni fun ann m, HasTypeCheckConfig cfg uni fun) ⇒ ann → Name → TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
- inferKindM ∷ (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) ⇒ Type TyName uni ann → TypeCheckT uni fun cfg m (Kind ())
- checkKindM ∷ (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) ⇒ ann → Type TyName uni ann → Kind () → TypeCheckT uni fun cfg m ()
- unfoldIFixOf ∷ MonadNormalizeType uni m ⇒ Normalized (Type TyName uni ()) → Normalized (Type TyName uni ()) → Kind () → TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
- inferTypeM ∷ (MonadTypeCheckPlc err uni fun ann m, HasTypeCheckConfig cfg uni fun) ⇒ Term TyName Name uni fun ann → TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
- type MonadNormalizeType uni m = (MonadQuote m, HasUniApply uni)
Documentation
type MonadKindCheck err term uni fun ann m = (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 fun ann m = (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.
newtype BuiltinTypes uni fun Source #
Mapping from Builtin
s to their Normalized
Kind
s.
BuiltinTypes | |
|
newtype KindCheckConfig Source #
Configuration of the kind checker.
data TypeCheckConfig uni fun Source #
Configuration of the type checker.
Instances
HasKindCheckConfig (TypeCheckConfig uni fun) Source # | |
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 Source # | |
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 TyVarKinds = UniqueMap TypeUnique (Named (Kind ())) Source #
type VarTypes uni = UniqueMap TermUnique (Named (Dupable (Normalized (Type TyName uni ())))) Source #
data HandleNameMismatches Source #
Decides what to do upon encountering a variable whose name doesn't match the name of the variable with the same unique that is currently in the scope. Consider for example this type:
(a_0 :: *) (b_0 :: *) -> a_0
here b_0
shadows a_0
and so any variable having the 0
th unique within the body of the
lambda references b_0
, but we have a_0
there and so there's a name mismatch. Technically,
it's not a type error to have a name mismatch, because uniques are the single source of truth,
however a name mismatch is deeply suspicious and is likely to be caused by a bug somewhere.
We perform the same check for term-level variables too.
DetectNameMismatches | Throw upon encountering such a name. |
IgnoreNameMismatches | Ignore it. |
Instances
class HasKindCheckConfig c where Source #
kindCheckConfig ∷ Lens' c KindCheckConfig Source #
kccHandleNameMismatches ∷ Lens' c HandleNameMismatches Source #
Instances
HasKindCheckConfig KindCheckConfig Source # | |
HasKindCheckConfig (TypeCheckConfig uni fun) Source # | |
Defined in PlutusCore.TypeCheck.Internal kindCheckConfig ∷ Lens' (TypeCheckConfig uni fun) KindCheckConfig Source # kccHandleNameMismatches ∷ Lens' (TypeCheckConfig uni fun) HandleNameMismatches Source # |
class HasKindCheckConfig cfg ⇒ HasTypeCheckConfig cfg uni fun | cfg → uni fun where Source #
We want HasKindCheckConfig
to be a superclass of HasTypeCheckConfig
for being able to
seamlessly call the kind checker from the type checker, hence we're rolling out our own
makeClassy
here just to add the constraint.
typeCheckConfig ∷ Lens' cfg (TypeCheckConfig uni fun) Source #
tccKindCheckConfig ∷ Lens' cfg KindCheckConfig Source #
tccBuiltinTypes ∷ Lens' cfg (BuiltinTypes uni fun) Source #
Instances
HasTypeCheckConfig (TypeCheckConfig uni fun) uni fun Source # | |
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 # |
data TypeCheckEnv uni fun cfg Source #
The environment that the type checker runs in.
TypeCheckEnv | |
|
type TypeCheckT uni fun cfg m = 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 MonadTypeCheckPlc err uni fun ann m = MonadTypeCheck err (Term TyName Name uni fun ()) uni fun ann m Source #
The constraints that are required for type checking Plutus Core.
withVar ∷ Name → Normalized (Type TyName uni ()) → TypeCheckT uni fun cfg m a → TypeCheckT uni fun cfg m a Source #
Extend the context of a TypeCheckM
computation with a typed variable.
normalizeTypeM ∷ MonadNormalizeType uni m ⇒ Type TyName uni ann → TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann)) Source #
Normalize a Kind
.
∷ MonadNormalizeType uni m | |
⇒ Normalized (Type TyName uni ()) | ty |
→ TyName | name |
→ Type TyName uni () | body |
→ TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())) |
Substitute a type for a variable in a type and normalize the result.
checkTypeM ∷ (MonadTypeCheckPlc err uni fun ann m, HasTypeCheckConfig cfg uni fun) ⇒ ann → Term TyName Name uni fun ann → Normalized (Type TyName uni ()) → TypeCheckT uni fun cfg m () Source #
Check a Term
against a NormalizedType
.
runTypeCheckM ∷ cfg → TypeCheckT uni fun cfg m a → m a Source #
Run a TypeCheckM
computation by supplying a TypeCheckConfig
to it.
Used for both type and kind checking, because we need to do kind checking during type checking
and so it makes sense to keep a single monad. However type checking requires a TypeCheckConfig
,
while kind checking doesn't, hence we keep the kind checker fully polymorphic over the type of
config, so that the kinder checker can be run with an empty config (such as ()
) and access to
a TypeCheckConfig
is not needed.
withTyVar ∷ TyName → Kind () → TypeCheckT uni fun cfg m a → TypeCheckT uni fun cfg m a Source #
Extend the context of a TypeCheckM
computation with a kinded variable.
tceTyVarKinds ∷ ∀ uni fun cfg fun. Lens (TypeCheckEnv uni fun cfg) (TypeCheckEnv uni fun cfg) TyVarKinds TyVarKinds Source #
lookupBuiltinM ∷ (MonadTypeCheck err term uni fun ann m, HasTypeCheckConfig cfg uni fun) ⇒ ann → fun → TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())) Source #
Look up the type of a built-in function.
tceTypeCheckConfig ∷ ∀ uni fun cfg fun cfg. Lens (TypeCheckEnv uni fun cfg) (TypeCheckEnv uni fun cfg) cfg cfg Source #
tceVarTypes ∷ ∀ uni fun cfg uni fun. Lens (TypeCheckEnv uni fun cfg) (TypeCheckEnv uni fun cfg) (VarTypes uni) (VarTypes uni) Source #
lookupTyVarM ∷ (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) ⇒ ann → TyName → TypeCheckT uni fun cfg m (Kind ()) Source #
Look up a type variable in the current context.
lookupVarM ∷ (MonadTypeCheck err term uni fun ann m, HasTypeCheckConfig cfg uni fun) ⇒ ann → Name → TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())) Source #
Look up a term variable in the current context.
inferKindM ∷ (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) ⇒ Type TyName uni ann → TypeCheckT uni fun cfg m (Kind ()) Source #
Infer the kind of a type.
checkKindM ∷ (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) ⇒ ann → Type TyName uni ann → Kind () → TypeCheckT uni fun cfg m () Source #
∷ MonadNormalizeType uni m | |
⇒ Normalized (Type TyName uni ()) | vPat |
→ Normalized (Type TyName uni ()) | vArg |
→ Kind () | k |
→ TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())) |
unfoldIFixOf pat arg k = NORM (vPat ((a :: k) -> ifix vPat a) arg)
inferTypeM ∷ (MonadTypeCheckPlc err uni fun ann m, HasTypeCheckConfig cfg uni fun) ⇒ Term TyName Name uni fun ann → TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())) Source #
Synthesize the type of a term, returning a normalized type.
type MonadNormalizeType uni m = (MonadQuote m, HasUniApply uni) Source #
The constraints that type normalization requires.