{- 
   Robinson's unification algorithm for first order terms
   Pedro Vasconcelos, 2009
   pbv@dcc.fc.up.pt
 -}
module Unify(unifyEqs) where

import FOL  
import qualified Data.Map as Map

-- unification algorithm
-- the inputs are the current unifier substitution
-- and a list of pairs of terms to unify (i.e. equations)
unifyEqs :: Subst -> [(Term,Term)] -> Maybe Subst
unifyEqs s [] = return s 
unifyEqs s ((t,t'):eqs) = unifyEqs' s (subst s t) (subst s t') eqs

-- auxiliary function
-- pre-condition: the unifying substitution has already been applyed
unifyEqs' :: Subst -> Term -> Term -> [(Term,Term)] -> Maybe Subst
unifyEqs' s (Var x) (Var y) eqs 
    | x==y      = unifyEqs s eqs
    | x<y       = unifyEqs (s `extend` (y,Var x)) eqs
    | otherwise = unifyEqs (s `extend` (x,Var y)) eqs
unifyEqs' s (Var x) t eqs 
    | x`notElem`fv t = unifyEqs (s `extend` (x,t)) eqs
    | otherwise      = fail "occur check failed"

unifyEqs' s t (Var x) eqs = unifyEqs' s (Var x) t eqs

unifyEqs' s (Fun f ts) (Fun f' ts') eqs
    | f==f' && length ts==length ts' = unifyEqs s (zip ts ts' ++ eqs)
    | otherwise                      = fail "unification failed" 

-- note that "fail" for the Maybe monad is Nothing


-- extend a substitution
extend :: Subst -> (Var,Term) -> Subst
s `extend` (v,t) = Map.insert v t s 

-- compose two substitutions
-- note that Map.union is left-biased
-- compose :: Subst -> Subst -> Subst
-- compose s2 s1 = Map.map (subst s2) s1 `Map.union` s2


-- restrict a substitution
-- remove bindings for a list of variables
-- restrict :: Subst -> [Var] -> Subst
-- s `restrict` vs = foldr Map.delete s vs