| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
PlutusCore.TypeCheck.Internal
Description
The internal module of the type checker that defines the actual algorithms, but not the user-facing API.
Synopsis
- normalizeTypeM :: forall (uni :: Type -> Type) (m :: Type -> Type) ann fun cfg. MonadNormalizeType uni m => Type TyName uni ann -> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
- substNormalizeTypeM :: forall (uni :: Type -> Type) (m :: Type -> Type) fun cfg. MonadNormalizeType uni m => Normalized (Type TyName uni ()) -> TyName -> Type TyName uni () -> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
- type MonadKindCheck err term (uni :: Type -> Type) fun ann (m :: Type -> Type) = (MonadError err m, ToKind uni)
- type MonadTypeCheck err term (uni :: Type -> Type) fun ann (m :: Type -> Type) = (MonadKindCheck err term uni fun ann m, MonadNormalizeType uni m, AnnotateCaseBuiltin uni, GEq uni, Ix fun)
- type TypeErrorPlc (uni :: Type -> Type) fun ann = TypeError (Term TyName Name uni fun ()) uni fun ann
- newtype BuiltinTypes (uni :: Type -> Type) fun = BuiltinTypes {
- unBuiltinTypes :: Array fun (Dupable (Normalized (Type TyName uni ())))
- newtype KindCheckConfig = KindCheckConfig {}
- data TypeCheckConfig (uni :: Type -> Type) fun = TypeCheckConfig {
- _tccKindCheckConfig :: KindCheckConfig
- _tccBuiltinTypes :: BuiltinTypes uni fun
- class HasKindCheckConfig cfg => HasTypeCheckConfig cfg (uni :: Type -> Type) fun | cfg -> uni fun where
- typeCheckConfig :: Lens' cfg (TypeCheckConfig uni fun)
- tccKindCheckConfig :: Lens' cfg KindCheckConfig
- tccBuiltinTypes :: Lens' cfg (BuiltinTypes uni fun)
- checkTypeM :: forall (uni :: Type -> Type) fun ann (m :: Type -> Type) cfg. (MonadTypeCheckPlc uni fun ann m, HasTypeCheckConfig cfg uni fun) => ann -> Term TyName Name uni fun ann -> Normalized (Type TyName uni ()) -> TypeCheckT uni fun cfg m ()
- type TyVarKinds = UniqueMap TypeUnique (Named (Kind ()))
- type VarTypes (uni :: Type -> Type) = UniqueMap TermUnique (Named (Dupable (Normalized (Type TyName uni ()))))
- data HandleNameMismatches
- class HasKindCheckConfig c where
- data TypeCheckEnv (uni :: Type -> Type) fun cfg = TypeCheckEnv {
- _tceTypeCheckConfig :: cfg
- _tceTyVarKinds :: TyVarKinds
- _tceVarTypes :: VarTypes uni
- type TypeCheckT (uni :: Type -> Type) fun cfg (m :: Type -> Type) = ReaderT (TypeCheckEnv uni fun cfg) m
- type MonadTypeCheckPlc (uni :: Type -> Type) fun ann (m :: Type -> Type) = MonadTypeCheck (TypeErrorPlc uni fun ann) (Term TyName Name uni fun ()) uni fun ann m
- runTypeCheckM :: forall cfg (uni :: Type -> Type) fun m a. cfg -> TypeCheckT uni fun cfg m a -> m a
- withTyVar :: forall (uni :: Type -> Type) fun cfg (m :: Type -> Type) a. TyName -> Kind () -> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
- tceTyVarKinds :: forall (uni :: Type -> Type) fun1 cfg fun2 f. Functor f => (TyVarKinds -> f TyVarKinds) -> TypeCheckEnv uni fun1 cfg -> f (TypeCheckEnv uni fun2 cfg)
- lookupBuiltinM :: forall term (uni :: Type -> Type) fun ann (m :: Type -> Type) cfg. (MonadTypeCheck (TypeError term uni fun ann) term uni fun ann m, HasTypeCheckConfig cfg uni fun) => ann -> fun -> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
- tceTypeCheckConfig :: forall (uni :: Type -> Type) fun1 cfg1 fun2 cfg2 f. Functor f => (cfg1 -> f cfg2) -> TypeCheckEnv uni fun1 cfg1 -> f (TypeCheckEnv uni fun2 cfg2)
- withVar :: forall (uni :: Type -> Type) fun cfg (m :: Type -> Type) a. Name -> Normalized (Type TyName uni ()) -> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
- tceVarTypes :: forall (uni1 :: Type -> Type) fun1 cfg (uni2 :: Type -> Type) fun2 f. Functor f => (VarTypes uni1 -> f (VarTypes uni2)) -> TypeCheckEnv uni1 fun1 cfg -> f (TypeCheckEnv uni2 fun2 cfg)
- lookupTyVarM :: forall term (uni :: Type -> Type) fun ann (m :: Type -> Type) cfg. (MonadKindCheck (TypeError term uni fun ann) term uni fun ann m, HasKindCheckConfig cfg) => ann -> TyName -> TypeCheckT uni fun cfg m (Kind ())
- lookupVarM :: forall term (uni :: Type -> Type) fun ann (m :: Type -> Type) cfg. (MonadTypeCheck (TypeError term uni fun ann) term uni fun ann m, HasTypeCheckConfig cfg uni fun) => ann -> Name -> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
- inferKindM :: forall term (uni :: Type -> Type) fun ann (m :: Type -> Type) cfg. (MonadKindCheck (TypeError term uni fun ann) term uni fun ann m, HasKindCheckConfig cfg) => Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ())
- checkKindM :: forall term (uni :: Type -> Type) fun ann (m :: Type -> Type) cfg. (MonadKindCheck (TypeError term uni fun ann) term uni fun ann m, HasKindCheckConfig cfg) => ann -> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
- unfoldIFixOf :: forall (uni :: Type -> Type) (m :: Type -> Type) fun cfg. MonadNormalizeType uni m => Normalized (Type TyName uni ()) -> Normalized (Type TyName uni ()) -> Kind () -> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
- inferTypeM :: forall (uni :: Type -> Type) fun ann (m :: Type -> Type) cfg. (MonadTypeCheckPlc 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 :: Type -> Type) (m :: Type -> Type) = (MonadQuote m, HasUniApply uni)
Documentation
normalizeTypeM :: forall (uni :: Type -> Type) (m :: Type -> Type) ann fun cfg. MonadNormalizeType uni m => Type TyName uni ann -> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann)) Source #
Normalize a Type.
Arguments
| :: forall (uni :: Type -> Type) (m :: Type -> Type) fun cfg. 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.
type MonadKindCheck err term (uni :: Type -> Type) fun ann (m :: Type -> Type) = (MonadError err m, 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, AnnotateCaseBuiltin uni, GEq uni, Ix fun) Source #
The general constraints that are required for type checking a Plutus AST.
type TypeErrorPlc (uni :: Type -> Type) fun ann = TypeError (Term TyName Name uni fun ()) uni fun ann Source #
The PLC type error type.
newtype BuiltinTypes (uni :: Type -> Type) fun Source #
Mapping from Builtins to their Normalized Types.
Constructors
| BuiltinTypes | |
Fields
| |
newtype KindCheckConfig Source #
Configuration of the kind checker.
Constructors
| KindCheckConfig | |
Instances
data TypeCheckConfig (uni :: Type -> Type) fun Source #
Configuration of the type checker.
Constructors
| TypeCheckConfig | |
Fields
| |
Instances
| HasKindCheckConfig (TypeCheckConfig uni fun) Source # | |
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 Source # | |
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 # | |
class HasKindCheckConfig cfg => HasTypeCheckConfig cfg (uni :: Type -> Type) 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.
Minimal complete definition
Methods
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 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 # | |
checkTypeM :: forall (uni :: Type -> Type) fun ann (m :: Type -> Type) cfg. (MonadTypeCheckPlc 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.
type TyVarKinds = UniqueMap TypeUnique (Named (Kind ())) Source #
type VarTypes (uni :: Type -> Type) = 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 0th 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.
Constructors
| DetectNameMismatches | Throw upon encountering such a name. |
| IgnoreNameMismatches | Ignore it. |
Instances
| Show HandleNameMismatches Source # | |
Defined in PlutusCore.TypeCheck.Internal | |
| Eq HandleNameMismatches Source # | |
Defined in PlutusCore.TypeCheck.Internal Methods (==) :: HandleNameMismatches -> HandleNameMismatches -> Bool Source # (/=) :: HandleNameMismatches -> HandleNameMismatches -> Bool Source # | |
class HasKindCheckConfig c where Source #
Minimal complete definition
Methods
kindCheckConfig :: Lens' c KindCheckConfig Source #
kccHandleNameMismatches :: Lens' c HandleNameMismatches Source #
Instances
| HasKindCheckConfig KindCheckConfig Source # | |
| HasKindCheckConfig (TypeCheckConfig uni fun) Source # | |
Defined in PlutusCore.TypeCheck.Internal Methods kindCheckConfig :: Lens' (TypeCheckConfig uni fun) KindCheckConfig Source # kccHandleNameMismatches :: Lens' (TypeCheckConfig uni fun) HandleNameMismatches Source # | |
data TypeCheckEnv (uni :: Type -> Type) fun cfg Source #
The environment that the type checker runs in.
Constructors
| TypeCheckEnv | |
Fields
| |
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 MonadTypeCheckPlc (uni :: Type -> Type) fun ann (m :: Type -> Type) = MonadTypeCheck (TypeErrorPlc uni fun ann) (Term TyName Name uni fun ()) uni fun ann m Source #
The constraints that are required for type checking Plutus Core.
runTypeCheckM :: forall cfg (uni :: Type -> Type) fun m a. 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 :: forall (uni :: Type -> Type) fun cfg (m :: Type -> Type) a. 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 :: forall (uni :: Type -> Type) fun1 cfg fun2 f. Functor f => (TyVarKinds -> f TyVarKinds) -> TypeCheckEnv uni fun1 cfg -> f (TypeCheckEnv uni fun2 cfg) Source #
lookupBuiltinM :: forall term (uni :: Type -> Type) fun ann (m :: Type -> Type) cfg. (MonadTypeCheck (TypeError term uni fun ann) 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 :: forall (uni :: Type -> Type) fun1 cfg1 fun2 cfg2 f. Functor f => (cfg1 -> f cfg2) -> TypeCheckEnv uni fun1 cfg1 -> f (TypeCheckEnv uni fun2 cfg2) Source #
withVar :: forall (uni :: Type -> Type) fun cfg (m :: Type -> Type) a. 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.
tceVarTypes :: forall (uni1 :: Type -> Type) fun1 cfg (uni2 :: Type -> Type) fun2 f. Functor f => (VarTypes uni1 -> f (VarTypes uni2)) -> TypeCheckEnv uni1 fun1 cfg -> f (TypeCheckEnv uni2 fun2 cfg) Source #
lookupTyVarM :: forall term (uni :: Type -> Type) fun ann (m :: Type -> Type) cfg. (MonadKindCheck (TypeError term uni fun ann) 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 :: forall term (uni :: Type -> Type) fun ann (m :: Type -> Type) cfg. (MonadTypeCheck (TypeError term uni fun ann) 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 :: forall term (uni :: Type -> Type) fun ann (m :: Type -> Type) cfg. (MonadKindCheck (TypeError term uni fun ann) 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 :: forall term (uni :: Type -> Type) fun ann (m :: Type -> Type) cfg. (MonadKindCheck (TypeError term uni fun ann) term uni fun ann m, HasKindCheckConfig cfg) => ann -> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m () Source #
Arguments
| :: forall (uni :: Type -> Type) (m :: Type -> Type) fun cfg. 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 :: forall (uni :: Type -> Type) fun ann (m :: Type -> Type) cfg. (MonadTypeCheckPlc 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 :: Type -> Type) (m :: Type -> Type) = (MonadQuote m, HasUniApply uni) Source #
The constraints that type normalization requires.