data Term = Variable String | FuncSymb String [Term]
    deriving (Eq, Show)

union2 :: (Eq a) => [a] -> [a] -> [a]
union2 x y = x ++ [z | z <- y, notElem z x]
    
union :: (Eq a) => [[a]] -> [a]
union = foldr union2 []

-- returns all variables of a term
var :: Term -> [String]
var (Variable x) = [x]
var (FuncSymb f ts) = union (map var ts)

-- substitutes, in a term, a variable by another term
subst :: Term -> String -> Term -> Term
subst (Variable x) y t | x == y = t
subst (Variable x) _ _ = Variable x
subst (FuncSymb f ts) y t = FuncSymb f (map (\u -> subst u y t) ts)

data Equ = Equ Term Term
    deriving Show

-- returns all variables of an equation
varEq :: Equ -> [String]
varEq (Equ t s) = union2 (var t) (var s)

data StepResult = FailureStep | SetStep [Equ] | Inapplicable
    deriving Show

step1 :: [Equ] -> StepResult
step1 [] = Inapplicable
step1 ((Equ (FuncSymb f ss) (FuncSymb g ts)):es) | f == g = SetStep ((zipWith Equ ss ts) ++ es)
step1 (e:es) = case (step1 es) of
                    Inapplicable -> Inapplicable
                    SetStep fs -> SetStep (e:fs)

step2 :: [Equ] -> StepResult
step2 [] = Inapplicable
step2 ((Equ (FuncSymb f ss) (FuncSymb g ts)):es) | f /= g = FailureStep
step2 (e:es) = step2 es

step3 :: [Equ] -> StepResult
step3 [] = Inapplicable
step3 ((Equ (Variable x) (Variable y)):es) | x == y = SetStep es
step3 (e:es) = case (step3 es) of
                    Inapplicable -> Inapplicable
                    SetStep fs -> SetStep (e:fs)

step4 :: [Equ] -> StepResult
step4 [] = Inapplicable
step4 ((Equ (FuncSymb f ss) (Variable x)):es) = SetStep ((Equ (Variable x) (FuncSymb f ss)):es)
step4 (e:es) = case (step4 es) of
                    Inapplicable -> Inapplicable
                    SetStep fs -> SetStep (e:fs)

step5 :: [Equ] -> StepResult
step5 [] = Inapplicable
step5 ((Equ (Variable x) (FuncSymb f ss)):es) | elem x (var (FuncSymb f ss)) = FailureStep
step5 (e:es) = step5 es

-- candidates for "x=t" in step 6 of the algorithm
step6cand :: [Equ] -> [Equ]
step6cand es = [Equ (Variable x) t | Equ (Variable x) t <- es, not (elem x (var t)), length [1 | e <- es, elem x (varEq e)] > 1]

-- substitutes in a list of equations a variable by a term EXCEPT for the equation "variable=term" (as used in step 6 of the algorithm)
substeq :: [Equ] -> String -> Term -> [Equ]
substeq [] _ _ = []
substeq ((Equ s u):es) x t | (s == Variable x) && (u == t) = (Equ s u):(substeq es x t)
substeq ((Equ s u):es) x t = (Equ (subst s x t) (subst u x t)):(substeq es x t)

step6 :: [Equ] -> StepResult
step6 es = case (step6cand es) of
                [] -> Inapplicable
                (Equ (Variable x) t):_ -> SetStep (substeq es x t)
                
onestep :: [Equ] -> StepResult
onestep es = case (step1 es) of
              SetStep fs -> SetStep fs
              Inapplicable -> case (step2 es) of
                          FailureStep -> FailureStep
                          Inapplicable -> case (step3 es) of
                                      SetStep fs -> SetStep fs
                                      Inapplicable -> case (step4 es) of
                                                  SetStep fs -> SetStep fs
                                                  Inapplicable -> case (step5 es) of
                                                              FailureStep -> FailureStep
                                                              Inapplicable ->  case (step6 es) of
                                                                           SetStep fs -> SetStep fs
                                                                           Inapplicable -> Inapplicable

data AllResult = Failure | Set [Equ]
    deriving Show

unify :: [Equ] -> AllResult
unify es = case (onestep es) of
                    Inapplicable -> Set es
                    FailureStep -> Failure
                    SetStep fs -> unify fs
                    
eqset1 = [Equ (Variable "z") (FuncSymb "f" [Variable "x"]), Equ (FuncSymb "f" [Variable "t"]) (Variable "y")]
         -- z=f(x), f(t)=y  --> should have z=f(x), y=f(t)

eqset2 = [Equ (FuncSymb "f" [Variable "x", FuncSymb "g" [Variable "y"]]) (FuncSymb "f" [FuncSymb "g" [Variable "z"], Variable "z"])]
         -- f(x,g(y))=f(g(z),z) --> should have x=g(g(y)), z=g(y)

eqset3 = [Equ (FuncSymb "f" [Variable "x", FuncSymb "g" [Variable "x"], FuncSymb "b" []]) (FuncSymb "f" [FuncSymb "a" [], FuncSymb "g" [Variable "z"], Variable "z"])]
          -- f(x,g(x),b)=f(a,g(z),z) --> should return failure