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
                    
-- This is where the new stuff starts

-- an endless reservoir of variables
freshvarlist :: [String]
freshvarlist = map ("x" ++) (map show [0..])

-- a list of equations in solved form acting as a substitution
substitute :: [Equ] -> Term -> Term
substitute [] t = t
substitute ((Equ (Variable x) s):es) t = substitute es (subst t x s)

--substitute repeatedly through a series of solved forms, from beginning to end
substituter :: [[Equ]] -> Term -> Term
substituter [] t = t
substituter (es:ess) t = substituter ess (substitute es t)

data AtomicRel = AtomicRel String [Term]
    deriving (Eq, Show)

-- variables of a relational atomic formula
vara :: AtomicRel -> [String]
vara (AtomicRel p ts) = union (map var ts)

-- substitution for an atomic formula
substitutea :: [Equ] -> AtomicRel -> AtomicRel
substitutea es (AtomicRel p ts) = AtomicRel p (map (substitute es) ts)

-- unification for two atomic formulas
unifya :: AtomicRel -> AtomicRel -> AllResult
unifya (AtomicRel p ts) (AtomicRel q us) | p == q = unify (zipWith Equ ts us)
unifya _ _ = Failure

data Clause = Clause AtomicRel [AtomicRel]
    deriving (Eq, Show)

-- variables of a clause
varcl :: Clause -> [String]
varcl (Clause at ats) = union (map vara (at:ats)) 

-- substitution for a clause
substitutecl :: [Equ] -> Clause -> Clause
substitutecl es (Clause at ats) = Clause (substitutea es at) (map (substitutea es) ats)

data Goal = Goal [AtomicRel]
    deriving (Eq, Show)

-- variables of a goal
vargl :: Goal -> [String]
vargl (Goal ats) = union (map vara ats)

-- fresh variables that are not in a clause and not in a goal
freshFor :: Clause -> Goal -> [String]
freshFor c g = [x | x <- freshvarlist, notElem x (varcl c), notElem x (vargl g)]

-- renaming of a clause according to a goal
renclause :: Goal -> Clause -> Clause
renclause g c = substitutecl [Equ (Variable x) (Variable y) | (x, y) <- zip (varcl c) (freshFor c g)] c

-- substitution for a goal
substitutegl :: [Equ] -> Goal -> Goal
substitutegl es (Goal ats) = Goal (map (substitutea es) ats)

-- evaluates (one step) a goal in a clause (assuming the clause is already renamed)
evaluategc :: Goal -> Clause -> Maybe (Goal, [Equ])
evaluategc (Goal (at:ats)) (Clause bt bts) = case (unifya at bt) of
                                                Failure -> Nothing
                                                Set es -> Just (substitutegl es (Goal (bts ++ ats)), es)
                                                
-- evaluates (one step) a program and a goal (also renaming the clauses)
evaluatep :: [Clause] -> Goal -> [(Goal, [Equ])]
evaluatep p (Goal []) = []
evaluatep p g = [x | Just x <- map ((evaluategc g) . (renclause g)) p]

data ResTree = ResTree (Goal, [Equ]) [ResTree]
    deriving Show

-- the resolution tree of a program and a (Goal, [Equ])
restree :: [Clause] -> (Goal, [Equ]) -> ResTree
restree p (g, es) = ResTree (g, es) (map (restree p) (evaluatep p g))

-- branches of a resolution tree (a branch is a list of nodes from the root to a leaf)
branches :: ResTree -> [[(Goal, [Equ])]]
branches (ResTree p []) = [[p]]
branches (ResTree p ts) = map (p:) (concatMap branches ts)

-- branches where the goal of the leaf is empty
validBranches :: ResTree -> [[(Goal, [Equ])]]
validBranches t = filter (\x -> fst (last x) == Goal []) (branches t)

-- the values of the variables after running a program with a goal (one list per valid branch)
evaluate :: [Clause] -> Goal -> [[(String, Term)]] 
evaluate p g = [[(v, substituter (map snd b) (Variable v)) | v <- vargl g] | b <- validBranches (restree p (g, []))]

-- zero term
termz :: Term
termz = FuncSymb "z" []

-- successor
terms :: Term -> Term
terms t = FuncSymb "s" [t]

-- variables
vx :: Term
vx = Variable "x"

vy :: Term
vy = Variable "y"

vz :: Term
vz = Variable "z"

vw :: Term
vw = Variable "w"

-- addition predicate
vadd :: Term -> Term -> Term -> AtomicRel
vadd t s u = AtomicRel "add" [t, s, u]

-- multiplication predicate
vmul :: Term -> Term -> Term -> AtomicRel
vmul t s u = AtomicRel "mul" [t, s, u]

-- term for natural number
termn :: Int -> Term
termn 0 = termz
termn n = terms (termn (n-1))

-- recovering the natural number from a term
backp :: Term -> Int
backp (FuncSymb "z" []) = 0
backp (FuncSymb "s" [t]) = (backp t) + 1

extr :: [[(String, Term)]] -> Int
extr ((("x", t):_):_) = backp t

proga = [Clause (vadd vx termz vx) [], Clause (vadd vx (terms vy) (terms vz)) [vadd vx vy vz]]
progm = [Clause (vmul vx termz termz) [], Clause (vmul vx (terms vy) vz) [vadd vw vx vz, vmul vx vy vw]]
prog  = proga ++ progm
goal1 = Goal [vadd (termn 3) (termn 4) vx]
goal2 = Goal [vmul (termn 3) (termn 4) vx]
goal3 = Goal [vmul vx (termn 7) (termn 21)]
test1 = extr (evaluate prog goal1)
test2 = extr (evaluate prog goal2)
test3 = extr (evaluate prog goal3)