module Subst where 

import Types 
import List (intersect)
import Control.Applicative


type Subst = [(Var, Type)]


nullSubst :: Subst
nullSubst = []


(+->) :: Var -> Type -> Subst
u +-> t = [(u, t)]


apply :: Subst -> Type -> Type
apply s v@(TVar u)     = case lookup u s of
                             Just t -> t
                             Nothing -> v
apply s (TList t)        = TList (apply s t)
apply s (TFunc t1 t2)    = TFunc (apply s t1) (apply s t2)
apply s (TPair t1 t2)    = TPair (apply s t1) (apply s t2)
apply s (TAppl t1 t2)    = TAppl (apply s t1) (apply s t2)
apply s t                = t


merge :: Subst -> Subst -> Subst
merge s1 s2 | agree     = s1 ++ s2
            | otherwise = error "merge fails"
  where agree = all (\v -> apply s1 (TVar v) == apply s2 (TVar v)) (map fst s1 `intersect` map fst s2)


match :: Type -> Type -> Subst
match (TList t) (TList t') = match t t'
match (TFunc t1 t2) (TFunc t1' t2') = merge (match t1 t1') (match t2 t2')
match (TPair t1 t2) (TPair t1' t2') = merge (match t1 t1') (match t2 t2')
match (TAppl t1 t2) (TAppl t1' t2') = merge (match t1 t1') (match t2 t2')
match t1@(TVar u) t2 | kind t1 == kind t2 = u +-> t2
match (TCtor tc1 _) (TCtor tc2 _) | tc1 == tc2 = nullSubst
match t1 t2 = error $ "types do not match: '" ++ show t1 ++ "', '" ++ show t2 ++ "'"