{-+
This module defines the represenation of types, qualified types, type schemes,
substitution and various auxiliary types.
-}
module TiTypes(module TiTypes,HsTypeI(..),HsIdentI(..),Kind) where
import Syntax(HsTypeI(..),TI(..),HsIdentI(..),HsFunDeps,
              hsTyFun,hsTyApp,hsTyTuple,hsTyCon,hsTyVar,
              kstar,base,mapTI,accT)
import List(nub,(\\))
import Maybe(fromMaybe)
import MUtils(collectByFst)
--import TiEnv(Env,range)
import TiKinds(Kind)
import TiNames
import Debug.Trace(trace) -- for debugging

type Type i = HsTypeI i
type Pred i = Type i
data Qual i t = [Pred i] :=> t deriving (Eq,Show,Read)
type QType i = Qual i (Type i)

data Scheme v = Forall [Kinded v] [Kinded v] (QType v)
              deriving (Eq,Show,Read) -- Eq??

unQual t = []:=>t
forall' = Forall []
mono t = forall' [] (unQual t)
--uscheme qt = fakeForall (tv qt) qt --  temporary hack!!!
--  where fakeForall vs qt = Forall (map (:>:kstar) vs) qt --  temporary hack!!!
--upscheme t = uscheme (unQual t) --  temporary hack!!!
kuscheme ks qt = forall' (kinded ks (tv qt)) qt
kupscheme ks t = kuscheme ks (unQual t)

funT ts = foldr1 hsTyFun ts -- :: Type
appT ts = foldl1 hsTyApp ts -- :: Type
tupleT ts = hsTyTuple ts -- :: Type
tyvar v = hsTyVar v -- :: Tyvar -> Type
ty (HsVar v) = tyvar v
ty (HsCon c) = hsTyCon c -- :: Type

isVarT (Typ (HsTyVar v)) = Just v
isVarT _ = Nothing

isFunT (Typ (HsTyFun t1 t2)) = Just (t1,t2)
isFunT _ = Nothing

flatAppT t = flat t []
  where
    flat (Typ (HsTyApp t1 t2)) ts = flat t1 (t2:ts)
    flat t ts = (t,ts)


flatConAppT ty =
  case flatAppT ty of
    (Typ (HsTyCon c),ts) -> Just (HsCon c,ts)
    _ -> Nothing

--instName (SrcLoc f l c) = HsVar (Qual (Module "i") (show l++"_"++show c))
--dictName n = HsVar (Qual (Module "d") n) :: QId
--vvar = unqual :: String->VarId

infix 1 :>:
data Typing x t = x :>: t deriving (Eq,Show,Read)
type Assump i = Typing (HsIdentI i) (Scheme i)
type Typed i x = Typing x (Type i)

emap f (e :>: t) = f e:>:t
tdom xts = [x|x:>:_<-xts]

unzipTyped :: [Typing x t] -> Typing [x] [t]
unzipTyped ets = uncurry (:>:) $ unzip [(e,t)|e:>:t<-ets]

zipTyped :: Typing [x] [t] -> [Typing x t]
zipTyped (xs:>:ts) = zipWith (:>:) xs ts

--collectTyped :: Ord x => [Typing x t] -> [Typing x [t]]
collectTyped xts = map (uncurry (:>:)) $ collectByFst [(x,t)|x:>:t<-xts]


type Kinded x = Typing x Kind
kinded1 ks v = v:>:head' [k|HsVar v':>:k<-ks,v'==v] -- not very efficient...
  where head' [] = trace ("Bug in TiTypes.kinded1: missing kind info for "++show v) kstar
        head' (k:_) = k
kinded ks = map (kinded1 ks)
--type KAssump = Typing Id Kind

type KInfo i = [Typing (HsIdentI i) (TypeInfo i)]

data TypeInfo i
  = Data
  | Newtype
  | Class [Pred i]        -- superclasses
          [Kinded i]      -- parameters
          (HsFunDeps Int) -- fun deps (0-based parameter positions)
          [Assump i]      -- methods
  | Synonym [i] (Type i)
  | Tyvar
  deriving ({-Eq,-}Show,Read)

newtype Subst i = S [(i,Type i)] deriving (Show)

idS = S []
infix 5 +->
v+-> t = S [(v,t)]
extS v t s = compS (v+->t) s
compS s1@(S s1') s2 = S (s1'++s2')
   where S s2' = apply s1 s2
domS (S s) = map fst s

varSubst s@(S s') v = fromMaybe (tyvar v) (lookup v s')

applySubst s@(S s') ty@(Typ t) =
    case t of
      HsTyVar v -> fromMaybe ty (lookup v s')
      _ -> base $ mapTI id (applySubst s) t

class TypeVar v => Types v t | t->v where
  tmap :: (Type v->Type v) -> t -> t
  apply :: Subst v -> t -> t
  tv :: t -> Set v

  apply = tmap . applySubst

type Set a = [a]

occurs v t = v `elem` tv t

instance Types v t => Types v [t] where
  tmap = map . tmap
  tv = nub . concatMap tv

instance TypeVar v => Types v (Subst v) where
  tmap f (S s') = S [(v,tmap f t)|(v,t)<-s'] -- hmm
  tv (S s') = tv (map snd s') -- hmm

instance (Types v t1,Types v t2) => Types v (t1,t2) where
  tmap f (t1,t2) = (tmap f t1,tmap f t2)
  tv (t1,t2) = nub (tv t1++tv t2)

instance (Types v t1,Types v t2,Types v t3) => Types v (t1,t2,t3) where
  tmap f (t1,t2,t3) = (tmap f t1,tmap f t2,tmap f t3)
  tv (t1,t2,t3) = nub (tv t1++tv t2++tv t3)

instance Types v t => Types v (Typing x t) where
  tmap f (x:>:t) = x:>:tmap f t
  tv (x:>:t) = tv t

instance Functor (Typing x) where
  fmap f (x:>:t) = x:>:f t -- hmm

instance TypeVar v => Types v (Type v) where
  tmap = id
  tv (Typ t) =
    case t of
      HsTyVar v -> [v]
      HsTyForall vs ps t -> tv (ps,t) \\ vs
      _ -> nub $ accT ((++) . tv) t []

instance TypeVar v => Types v (Scheme v) where
  apply s (Forall ags gs qt) = Forall ags gs (apply (restrict s (tdom (ags++gs))) qt)
  tmap f (Forall ags gs qt) = Forall ags gs (tmap f qt) -- hmm
  tv (Forall ags gs qt) = tv qt \\ tdom (ags++gs)

restrict (S s) gs = S [s1|s1@(v,_)<-s,v `notElem` gs]

instance Types v t => Types v (Qual v t) where
  tmap f (ps:=>t) = tmap f ps:=>tmap f t
  tv (ps:=>t) = tv (ps,t)
{-
instance Types v info => Types v (Env key info) where
  tmap = fmap . tmap
  tv = tv . range
-}