-- Uebungen zur Gleichungslogik, SS 2000
-- Rahmen fuer Aufgabe 7, Blatt 5
--
-- 30.05.2000 G.K.

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

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

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

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


-- matching
data Unifier = Result Subst | Error

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

matchs ([],s)           = ...
matchs ((V x, t):s', s) = ...
matchs ((t, V x):s', s) = ...
matchs ((T(f,ts),T(g,us)):s', s)
                        = ...

-- embedding of matchs
match :: (Term,Term) -> Unifier
match (pat, obj) = matchs ...

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

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