module Unification where

import Types ( Type(..), typeVars, typeSubst )

type Unifier = [(Type, Type)]

-- unification algorithm of martelli montanari
unify :: Unifier -> Maybe Unifier
unify [] = Just []
-- (delete)
unify ((TypeVar x, TypeVar y) : rest) | x == y = unify rest
-- (decomp)
unify ((Arrow t1 t2, Arrow t1' t2') : rest) = unify $ [(t1, t1'), (t2, t2')] ++ rest
unify ((BaseType b1, BaseType b2) : rest) | b1 == b2 = unify rest
-- (conflict)
unify ((BaseType b1, BaseType b2) : _) | b1 /= b2 = Nothing
-- (orient)
unify ((Arrow t1 t2, TypeVar x) : rest) = unify $ (TypeVar x, Arrow t1 t2) : rest
unify ((BaseType b, TypeVar x) : rest) = unify $ (TypeVar x, BaseType b) : rest
-- (occurs)
unify ((TypeVar x, t) : _) | x `elem` typeVars t && TypeVar x /= t = Nothing
-- (elim)
unify ((TypeVar x, t) : rest) | notElem x (typeVars t) && x `elem` concatMap (\(t1, t2) -> typeVars t1 ++ typeVars t2) rest = unify $ (TypeVar x, t) : map (\(t1, t2) -> (typeSubst t1 x t, typeSubst t2 x t)) rest
-- descent
unify ((t, s) : rest) = do
    rest' <- unify rest
    return $ (t, s) : rest'

-- apply a mgu to some type
applyMgu :: Type -> Unifier -> Type
applyMgu (TypeVar x) [] = TypeVar x
applyMgu (TypeVar x) ((TypeVar y, tp) : rest) = if x == y then tp else applyMgu (TypeVar x) rest
applyMgu (BaseType b) _ = BaseType b
applyMgu (Arrow t1 t2) mgu = Arrow (applyMgu t1 mgu) (applyMgu t2 mgu)
applyMgu _ (tp : _) = error $ "Non primitive type '" ++ show tp ++ "' on left side of mgu"