fix: Satisfy clause

examples/basics/backtracking.pl

@@ -4,6 +4,6 @@ leq(s(X), s(Y)) :- leq(X, Y).
 :- initialization(main).
 
 main :-
-    leq(X, s(s(s(0)))),
+    leq(A, s(s(s(0)))),
-    write(X), nl,
+    write(A), nl,
     fail.

src/prolog/ast/logic/Clause.kt

@@ -27,30 +27,31 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
         // Only if the body can be proven, the substitutions should be returned.
         // Do this in a lazy way.
 
-        val (headEnd, headRenaming) = numbervars(head, Program.variableRenamingStart, subs)
+        // Since we are only interested in substitutions in the goal (as opposed to the head of this clause),
+        //  we can use variable renaming and filter out the substitutions that are not in the goal.
+        val (headEnd, headRenaming) = numbervars(head, Program.variableRenamingStart, emptyMap())
         Program.variableRenamingStart = headEnd
 
-        val renamedHead = applySubstitution(head, subs + headRenaming)
+        val renamedHead = applySubstitution(head, headRenaming)
-        val renamedBody = applySubstitution(body, subs + headRenaming) as Body
+        val simplifiedGoal = applySubstitution(goal, subs)
-
+        unifyLazy(simplifiedGoal, renamedHead, emptyMap()).forEach { headAnswer ->
-        unifyLazy(goal, renamedHead, subs).forEach { headAnswer ->
+            headAnswer.map { headAndGoalSubs ->
-            headAnswer.map { headSubs ->
+                // Filter the substitutions to only include those that map from head to goal
-                val subsNotInGoal = headSubs.filterNot { occurs(it.key as Variable, goal, emptyMap()) }
+                val headToGoalSubs = headAndGoalSubs.filterKeys { it in headRenaming.values }
-                renamedBody.satisfy(subsNotInGoal).forEach { bodyAnswer ->
+                val goalToHeadSubs = headAndGoalSubs.filterKeys { occurs(it as Variable, simplifiedGoal) }
+                val newSubs = headRenaming + headToGoalSubs
+                body.satisfy(newSubs).forEach { bodyAnswer ->
                     bodyAnswer.fold(
-                        // If the body can be proven, yield the (combined) substitutions
                         onSuccess = { bodySubs ->
-                            var result = headSubs + bodySubs
+                            // If the body can be proven, yield the (combined) substitutions
-                            result = result
+                            var result = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
-                                .mapValues { applySubstitution(it.value, result) }
-                                .filterKeys { it !is AnonymousVariable && occurs(it as Variable, goal, emptyMap()) }
                             yield(Result.success(result))
                         },
                         onFailure = { error ->
                             if (error is AppliedCut) {
                                 // Find single solution and return immediately
                                 if (error.subs != null) {
-                                    yield(Result.failure(AppliedCut(headSubs + error.subs)))
+                                    yield(Result.failure(AppliedCut(headAndGoalSubs + error.subs)))
                                 } else {
                                     yield(Result.failure(AppliedCut()))
                                 }

src/prolog/logic/unification.kt

@@ -41,7 +41,7 @@ fun applySubstitution(expr: Expression, subs: Substitutions): Expression = when
 }
 
 // Check if a variable occurs in a term
-fun occurs(variable: Variable, term: Term, subs: Substitutions): Boolean = when {
+fun occurs(variable: Variable, term: Term, subs: Substitutions = emptyMap()): Boolean = when {
     variable(term, subs) -> term == variable
     atomic(term, subs) -> false
     compound(term, subs) -> {