Quick and dirty unification algorithm

gistfile1.hs

-- simple unification for predicate logic

data AtomicFormula = Variable String |  -- single variable 
                     Function String [AtomicFormula] -- function with some args

instance Show AtomicFormula where       
         show (Variable a) = a
         show (Function f l) = f ++ (show l)

data Formula = And Formula Formula -- conjunction, not needed
               | Or Formula Formula -- disjunction, not needed
               | Neg Formula -- negation
               | Predicate String [AtomicFormula] -- predicate with name and arguments
               deriving (Show)

data UnificationResult = Success [(String, AtomicFormula)] | Error [(AtomicFormula, AtomicFormula)]

instance Show UnificationResult where
         show (Error l) = show l
         show (Success []) = ""
         show (Success ((x1, x2):xs)) = "[" ++ (x1) ++ "/" ++ (show x2) ++ "] " ++ (show (Success xs))

unify (Predicate p1 args1) (Predicate p2 args2) = 
      if p1 == p2 then unifyArgumentLists args1 args2
      else Error []  

-- eliminate variable from formula
substituteVariable v expr [] = []
substituteVariable (Variable v) expr ((Variable y):xs) = if v==y then expr:(substituteVariable (Variable v) expr xs)
                                                         else (Variable y):(substituteVariable (Variable v) expr xs)
substituteVariable v expr ((Function f a):xs) = (Function f (substituteVariable v expr a)) : (substituteVariable v expr xs)

-- occurs-check
occurs _ [] = False
occurs (Variable x) ((Variable y):ys) = if x==y then True else occurs (Variable x) ys
occurs (Variable x) ((Function f l):ys) = (occurs (Variable x) l) || (occurs (Variable x) ys)

-- unify argument lists - central part
unifyArgumentLists [] [] = Success []

unifyArgumentLists ((Variable v):xs) ((Variable y):ys) = 
                   let Success l = unifyArgumentLists (substituteVariable (Variable v) (Variable y) xs) (substituteVariable (Variable v) (Variable y) ys) 
                   in Success ((v, Variable y):l) 
                   
unifyArgumentLists ((Function f v):xs) ((Function g y):ys) = 
                   if f == g then
                      let Success l = unifyArgumentLists v y in
                          let Success k = unifyArgumentLists xs ys in
                      Success (l++k)
                   else Error [(Function f [], Function g [])]


unifyArgumentLists ((Variable v):xs) (y:ys) = let Success rem = if occurs (Variable v) [y] then Error []
                                                                else unifyArgumentLists xs ys in Success ((v, y):rem)
unifyArgumentLists (y:ys) ((Variable v):xs) = unifyArgumentLists ((Variable v):xs) (y:ys)

unifyArgumentLists _ _ = Error []