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

step2 :: [Equ] -> StepResult
step2 = undefined

step3 :: [Equ] -> StepResult
step3 = undefined

step4 :: [Equ] -> StepResult
step4 = undefined

step5 :: [Equ] -> StepResult
step5 = undefined

-- candidates for "x=t" in step 6 of the algorithm
step6cand :: [Equ] -> [Equ]
step6cand es = undefined

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

step6 :: [Equ] -> StepResult
step6 es = undefined
                
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