-- Uebungen zur Gleichungslogik, WS 2004/05
-- Rahmen fuer Uebungsblatt 6, Aufgabe 5
--
-- 30.05.2000 G.K.
-- 12.05.2003 C.B.
-- 22.11.2004 C.B.

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

--
-- Matching
--

-- Der Rueckgabewert ist entweder eine Substitution oder ein Fehler

data Unifier = Result Subst | Error

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

matchs :: ([(Term,Term)],Subst) -> Unifier

-- !!! Bitte selbst programmieren !!!

-- Front-end zu matchs
-- match (pat, obj) berechnet die Loesung zu pat < obj

match :: (Term,Term) -> Unifier
match (pat, obj) = matchs([(pat,obj)],[])

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

-- Terme
t1 = f x y
t2 = f (T("h", [T("a",[])])) x
t3 = f x (T("b",[]))
t4 = f (T("h",[y])) z
t5 = f (g y y) (g z z)

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

-- match (t1, t2)
-- match (t1, t3)
-- match (t1, t4)
-- match (t1, t5)
-- match (t3, t1)