-- Uebungen zur Gleichungslogik, WS 2007/08
-- Rahmen fuer Uebungsblatt 7, Aufgabe 5
--
-- 06.06.2000 G.K.
-- 16.05.2003 C.B.
-- 03.12.2004 C.B.
-- 27.11.2006 N.S.

--
-- Bitte ergaenzen Sie die fehlenden Programmstuecke!
--


--
-- 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

-- !!! Bitte selbst programmieren !!!

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

apply :: Subst -> Term -> Term

-- !!! Bitte selbst programmieren !!!

-- 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

--
-- Unifikation
--

-- Der Rueckgabewert ist entweder eine Substitution oder ein Fehler

data Unifier = Result Subst | Error

-- Inkrementelle Implementierung des Unifikations-Algorithmus
-- solve (ps, s) loest das Unifikations-Problem, wobei
--   ps das verbleibende Unifikations-Problem ist, und
--   s  die bereits berechnete Substitution

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 = apply [(x,t)]


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

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



--
-- Einige Testeingaben
--

-- Bausteine
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)

-- Terme
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)
u7 = unify (t8, t9)
u8 = solve ([(x,h y),(h z, x)],[])
u9 = solve ([(x,h y),(z,x),(y,z)],[])

--
-- Geben Sie mit Ihrer Loesung die Ergebnisse der folgenden Anfragen ab!
--

-- unify (t1, t2)
-- unify (t1, t3)
-- unify (t1, t4)
-- unify (t1, t5)
-- unify (t3, t1)
-- unify (t6, t7) -- Ohne Optimierung nicht praktikabel