{- |
    Module      :  $Header$
    Description :  Kind substitution
    Copyright   :  (c) 2016      Finn Teegen
    License     :  BSD-3-clause

    Maintainer  :  bjp@informatik.uni-kiel.de
    Stability   :  experimental
    Portability :  portable

   This module implements substitutions on kinds.
-}

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