--
-- Hilfsfunktionen auf Listen
--

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


--
-- Terme
--

-- Variablennamen
-- (luxorioese Darstellung mit Name und Index, also z.B. x0)

type VName = (String, Int)

-- Terme

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


-- Gleichheit von Termen, ueberladen auf "=="

instance Eq Term where (==) = curry isequal

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

--
-- Substitutionen
--

-- Substitutionen
-- als Liste von Ersetzungspaaren VName->Term

type Subst = [(VName,Term)]

-- Ist die Variable x im Domain der Substitution s?

indom :: VName -> Subst -> Bool
indom x s = exists (\(y,_) -> x==y) s 

-- Anwenden einer Substitution auf eine Variable
-- app s x liefert den Term s(x) zurueck

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

-- Anwenden einer Substitution auf einen Term
-- apply s t liefert den Term s(t) zurueck

apply :: Subst -> Term -> Term
apply s (V x)      = if indom x s then app s x else V x
apply s (T (f,ts)) = T(f, map (apply s) ts)

-- Kommt die Variable x occur in einem Term vor?

occurs :: VName -> Term -> Bool
occurs x (V y)     = x == y
occurs x (T(_,ts)) = exists (occurs x) ts

-- Der Rueckgabewert ist entweder eine Substitution oder ein Fehler

data Unifier = Result Subst | Error

-- Verzoegerte Anwendung von Substitutionen

chase :: Term -> Subst -> Term
chase (V x) s      = if indom x s then chase (app s x) s else V x
chase (T(f,ts)) s  = T(f,ts)

-- Fallunterscheidung

cases :: Term -> Term -> [(Term,Term)] -> Subst -> Unifier
cases (V x) (V y) s' s         = if x == y then 
                                   solve (s', s) 
                                 else 
                                   solve (s', (x,V y):s)

cases (V x) t s' s             = if occurs x t then 
                                   Error 
                                 else 
                                   solve (s', (x,t):s)

cases t (V x) s' s             = cases (V x) t s' s

cases (T(f,ts)) (T(g,gs)) s' s = if f == g then 
                                   solve ( (zip ts gs)++s', s ) 
                                 else 
                                   Error

-- Die neue Funktion solve

solve :: ([(Term,Term)], Subst) -> Unifier
solve ([], s)         = Result s
solve ((t1,t2):s', s) = cases (chase t1 s) (chase t2 s) s' s

-- Front-end zu solve
-- unify (t1, t2) berechnet den Unifikator von t1 und t2

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])
h x   = T("h",[x])
i x   = T("i",[x])
 
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 )
t8 = f x z
t9 = f (h y) (i x)

-- unification problems

u1 = unify (t1, t2)
u2 = unify (t1, t3)
u3 = unify (t1, t4)
u4 = unify (t1, t5)
u5 = unify (t3, t1)
u6 = unify (t6, t7)
u7 = unify (t8, t9)
u8 = solve ([(x,h y),(h z, x)],[])
u9 = solve ([(x,h y),(z,x),(y,z)],[])