-- Uebungen zur Gleichungslogik, SS 2000
-- Rahmenprogramm fuer Aufgabe 6, Blatt 6
--
-- 06.06.2000 G.K.

-- variable names 
type VName = (String, Int)

-- terms
data Term = V VName | T (String,[Term])

-- define == on Term
instance Eq Term where (==) = curry isequal

-- substitutions
type Subst = [(VName,Term)]


-- finite forall/exists on lists

exists :: (a -> Bool) -> [a] -> Bool
exists p []     = False
exists p (x:xs) = if p x then True else exists p xs

forall :: (a -> Bool) -> [a] -> Bool
forall p []     = True
forall p (x:xs) = if p x then forall p xs else False


-- equality for terms
isequal :: (Term,Term) -> Bool
isequal (V x, V y)         = x == y
isequal (T(f,ts), T(g,us)) = f == g && forall isequal (zip ts us)
isequal (_,_)              = False


-- is variable x in the domain of substitution s?
indom :: VName -> Subst -> Bool
indom x s = exists (\(y,_) -> x==y) s 

-- applies substitution to variable
app :: Subst -> VName -> Term
app ((y,t):s) x = if x == y then t else app s x

-- applies substition to term
lift :: Subst -> Term -> Term
lift s (V x)      = if indom x s then app s x else V x
lift s (T (f,ts)) = T(f, map (lift s) ts)

-- does variable x occur in a term?
occurs :: VName -> Term -> Bool
occurs x (V y)     = x == y
occurs x (T(_,ts)) = exists (occurs x) ts


-- unification

data Unifier = Result Subst | Error

solve :: ([(Term,Term)], Subst) -> Unifier
solve ([], s)                  = Result s
solve ((V x, V y) : s', s)     = if x == y then solve(s',s) else elim(x,V y,s',s)
solve ((V x, t) : s', s)       = elim(x,t,s',s)
solve ((t, V x) : s', s)       = elim(x,t,s',s)
solve ((T(f,ts),T(g,us)):s',s) = if f == g then solve((zip ts us) ++ s', s) else Error

elim :: (VName, Term, [(Term,Term)], Subst) -> Unifier
elim (x,t,s',s) = if occurs x t then 
                    Error 
                  else
                    solve( (map (\(t1,t2) -> (xt t1, xt t2)) s'), 
                           ((x,t):(map (\(y,u) -> (y, xt u)) s)) )
                    where xt = lift [(x,t)]


-- embedding of solve
unify :: (Term, Term) -> Unifier
unify (t1,t2) = solve([(t1,t2)], [])



--
-- some terms for testing:

-- building blocks
x     = V("x",0)
y     = V("y",0)
z     = V("z",0)
f a b = T("f", [a,b])
g a b = T("g", [a,b])
 
a x1 x2 x3 x4 x5 x6 = T("a", [x1,x2,x3,x4,x5,x6])
b x1 x2 x3 x4 x5 x6 = T("b", [x1,x2,x3,x4,x5,x6])

x1 = V("x",1)
x2 = V("x",2)
x3 = V("x",3)
x4 = V("x",4)
x5 = V("x",5)
x6 = V("x",6)
x7 = V("x",7)

-- terms
t1 = f x y
t2 = f (T("h", [T("a",[])])) x
t3 = f x (T("b",[]))
t4 = f (T("h",[y])) (V("z",0))

t5 = f (g y y) (g z z)

t6 = a x1 x2 x3 x4 x5 x6
t7 = a (b x2 x2 x2 x2 x2 x2) (b x3 x3 x3 x3 x3 x3) (b x4 x4 x4 x4 x4 x4)
       (b x5 x5 x5 x5 x5 x5) (b x6 x6 x6 x6 x6 x6) (b x7 x7 x7 x7 x7 x7 )