module Base.KindSubst
( module Base.KindSubst, idSubst, singleSubst, bindSubst, compose
) where
import Base.Kinds
import Base.Subst
import Base.TopEnv
import Env.TypeConstructor
type KindSubst = Subst Int Kind
class SubstKind a where
subst :: KindSubst -> a -> a
bindVar :: Int -> Kind -> KindSubst -> KindSubst
bindVar :: Int -> Kind -> KindSubst -> KindSubst
bindVar kv :: Int
kv k :: Kind
k = KindSubst -> KindSubst -> KindSubst
forall v e. Ord v => Subst v e -> Subst v e -> Subst v e
compose (Int -> Kind -> KindSubst -> KindSubst
forall v e. Ord v => v -> e -> Subst v e -> Subst v e
bindSubst Int
kv Kind
k KindSubst
forall a b. Subst a b
idSubst)
substVar :: KindSubst -> Int -> Kind
substVar :: KindSubst -> Int -> Kind
substVar = (Int -> Kind)
-> (KindSubst -> Kind -> Kind) -> KindSubst -> Int -> Kind
forall v e.
Ord v =>
(v -> e) -> (Subst v e -> e -> e) -> Subst v e -> v -> e
substVar' Int -> Kind
KindVariable KindSubst -> Kind -> Kind
forall a. SubstKind a => KindSubst -> a -> a
subst
instance SubstKind Kind where
subst :: KindSubst -> Kind -> Kind
subst _ KindStar = Kind
KindStar
subst sigma :: KindSubst
sigma (KindVariable kv :: Int
kv) = KindSubst -> Int -> Kind
substVar KindSubst
sigma Int
kv
subst sigma :: KindSubst
sigma (KindArrow k1 :: Kind
k1 k2 :: Kind
k2) = Kind -> Kind -> Kind
KindArrow (KindSubst -> Kind -> Kind
forall a. SubstKind a => KindSubst -> a -> a
subst KindSubst
sigma Kind
k1) (KindSubst -> Kind -> Kind
forall a. SubstKind a => KindSubst -> a -> a
subst KindSubst
sigma Kind
k2)
instance SubstKind TypeInfo where
subst :: KindSubst -> TypeInfo -> TypeInfo
subst theta :: KindSubst
theta (DataType tc :: QualIdent
tc k :: Kind
k cs :: [DataConstr]
cs) = QualIdent -> Kind -> [DataConstr] -> TypeInfo
DataType QualIdent
tc (KindSubst -> Kind -> Kind
forall a. SubstKind a => KindSubst -> a -> a
subst KindSubst
theta Kind
k) [DataConstr]
cs
subst theta :: KindSubst
theta (RenamingType tc :: QualIdent
tc k :: Kind
k nc :: DataConstr
nc) = QualIdent -> Kind -> DataConstr -> TypeInfo
RenamingType QualIdent
tc (KindSubst -> Kind -> Kind
forall a. SubstKind a => KindSubst -> a -> a
subst KindSubst
theta Kind
k) DataConstr
nc
subst theta :: KindSubst
theta (AliasType tc :: QualIdent
tc k :: Kind
k n :: Int
n ty :: Type
ty) = QualIdent -> Kind -> Int -> Type -> TypeInfo
AliasType QualIdent
tc (KindSubst -> Kind -> Kind
forall a. SubstKind a => KindSubst -> a -> a
subst KindSubst
theta Kind
k) Int
n Type
ty
subst theta :: KindSubst
theta (TypeClass cls :: QualIdent
cls k :: Kind
k ms :: [ClassMethod]
ms) = QualIdent -> Kind -> [ClassMethod] -> TypeInfo
TypeClass QualIdent
cls (KindSubst -> Kind -> Kind
forall a. SubstKind a => KindSubst -> a -> a
subst KindSubst
theta Kind
k) [ClassMethod]
ms
subst theta :: KindSubst
theta (TypeVar k :: Kind
k) = Kind -> TypeInfo
TypeVar (KindSubst -> Kind -> Kind
forall a. SubstKind a => KindSubst -> a -> a
subst KindSubst
theta Kind
k)
instance SubstKind a => SubstKind (TopEnv a) where
subst :: KindSubst -> TopEnv a -> TopEnv a
subst = (a -> a) -> TopEnv a -> TopEnv a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> TopEnv a -> TopEnv a)
-> (KindSubst -> a -> a) -> KindSubst -> TopEnv a -> TopEnv a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KindSubst -> a -> a
forall a. SubstKind a => KindSubst -> a -> a
subst