Backtracking fixed

src/prolog/ast/arithmetic/Float.kt

@@ -32,6 +32,8 @@ class Float(override val value: kotlin.Float): Number {
         else -> throw IllegalArgumentException("Cannot multiply $this and $other")
     }
 
+    override fun applySubstitution(subs: Substitutions): Float = this
+
     override fun equals(other: Any?): Boolean {
         if (this === other) return true
         if (other !is Float) return false

src/prolog/ast/arithmetic/Integer.kt

@@ -33,6 +33,7 @@ data class Integer(override val value: Int) : Number, LogicOperand() {
                 Float(value / other.value.toFloat())
             }
         }
+
         else -> throw IllegalArgumentException("Cannot divide $this and $other")
     }
 
@@ -41,4 +42,6 @@ data class Integer(override val value: Int) : Number, LogicOperand() {
         is Integer -> Integer(value * other.value)
         else -> throw IllegalArgumentException("Cannot multiply $this and $other")
     }
+
+    override fun applySubstitution(subs: Substitutions): Integer = this
 }

src/prolog/ast/logic/Clause.kt

@@ -27,27 +27,23 @@ 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.
 
-        // Since we are only interested in substitutions in the goal (as opposed to the head of this clause),
+        val (headEnd, headRenaming) = numbervars(head, Program.variableRenamingStart, subs)
-        //  we can use variable renaming and filter out the substitutions that are not in the goal.
+        Program.variableRenamingStart = headEnd
-        val (end, renamed: Substitutions) = numbervars(head, Program.variableRenamingStart, subs)
 
-        val reverse = renamed.entries.associate { (a, b) -> b to a }
+        val renamedHead = applySubstitution(head, subs + headRenaming)
-        Program.variableRenamingStart = end
+        val renamedBody = applySubstitution(body, subs + headRenaming) as Body
 
-        var newSubs: Substitutions = subs + renamed
+        unifyLazy(goal, renamedHead, subs).forEach { headAnswer ->
-        unifyLazy(applySubstitution(goal, subs), head, newSubs).forEach { headAnswer ->
             headAnswer.map { headSubs ->
-                // If the body can be proven, yield the (combined) substitutions
+                val subsNotInGoal = headSubs.filterNot { occurs(it.key as Variable, goal, emptyMap()) }
-                newSubs = subs + renamed + headSubs
+                renamedBody.satisfy(subsNotInGoal).forEach { bodyAnswer ->
-                body.satisfy(newSubs).forEach { bodyAnswer ->
                     bodyAnswer.fold(
+                        // If the body can be proven, yield the (combined) substitutions
                         onSuccess = { bodySubs ->
-                            var result = (headSubs + bodySubs)
+                            var result = headSubs + bodySubs
-                                .mapKeys { applySubstitution(it.key, reverse)}
+                            result = result
-                                .mapValues { applySubstitution(it.value, reverse) }
+                                .mapValues { applySubstitution(it.value, result) }
-                            result = result.map { it.key to applySubstitution(it.value, result) }
+                                .filterKeys { it !is AnonymousVariable && occurs(it as Variable, goal, emptyMap()) }
-                                .toMap()
-                                .filterNot { it.key in renamed.keys && !occurs(it.key as Variable, goal, emptyMap())}
                             yield(Result.success(result))
                         },
                         onFailure = { error ->
@@ -81,7 +77,5 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
         return true
     }
 
-    override fun hashCode(): Int {
+    override fun hashCode(): Int = super.hashCode()
-        return super.hashCode()
-    }
 }

src/prolog/ast/logic/Fact.kt

@@ -1,6 +1,10 @@
 package prolog.ast.logic
 
+import prolog.Substitutions
 import prolog.ast.terms.Head
 import prolog.builtins.True
+import prolog.logic.applySubstitution
 
-class Fact(head: Head) : Clause(head, True)
+class Fact(head: Head) : Clause(head, True) {
+    override fun applySubstitution(subs: Substitutions): Fact = Fact(applySubstitution(head, subs) as Head)
+}

src/prolog/ast/logic/Rule.kt

@@ -1,6 +1,13 @@
 package prolog.ast.logic
 
+import prolog.Substitutions
 import prolog.ast.terms.Body
 import prolog.ast.terms.Head
+import prolog.logic.applySubstitution
 
-class Rule(head: Head, body: Body) : Clause(head, body)
+class Rule(head: Head, body: Body) : Clause(head, body) {
+    override fun applySubstitution(subs: Substitutions): Rule = Rule(
+        head = applySubstitution(head, subs) as Head,
+        body = applySubstitution(body, subs) as Body
+    )
+}

src/prolog/ast/terms/AnonymousVariable.kt

@@ -1,8 +1,9 @@
 package prolog.ast.terms
 
 import io.Logger
+import prolog.Substitutions
 
-class AnonymousVariable(id: Int) : Variable("_$id") {
+class AnonymousVariable(private val id: Int) : Variable("_$id") {
     companion object {
         private var counter = 0
         fun create(): AnonymousVariable {
@@ -13,5 +14,7 @@ class AnonymousVariable(id: Int) : Variable("_$id") {
         }
     }
 
+    override fun applySubstitution(subs: Substitutions): AnonymousVariable = this
+
     override fun toString(): String = "_"
 }

src/prolog/ast/terms/Atom.kt

@@ -10,6 +10,8 @@ open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
 
     override fun solve(goal: Goal, subs: Substitutions): Answers = unifyLazy(goal, this, subs)
 
+    override fun applySubstitution(subs: Substitutions): Atom = Atom(name)
+
     override fun toString(): String {
         return name
     }

src/prolog/ast/terms/Body.kt

@@ -2,4 +2,4 @@ package prolog.ast.terms
 
 import prolog.ast.logic.Satisfiable
 
-interface Body : Satisfiable
+interface Body : Term, Satisfiable

src/prolog/ast/terms/Structure.kt

@@ -3,6 +3,7 @@ package prolog.ast.terms
 import prolog.Answers
 import prolog.Substitutions
 import prolog.ast.logic.Resolvent
+import prolog.logic.applySubstitution
 import prolog.logic.unifyLazy
 
 typealias Argument = Term
@@ -23,6 +24,11 @@ open class Structure(val name: Atom, var arguments: List<Argument>) : Goal(), He
         }
     }
 
+    override fun applySubstitution(subs: Substitutions): Structure = Structure(
+        name,
+        arguments.map { applySubstitution(it, subs) }
+    )
+
     override fun equals(other: Any?): Boolean {
         if (this === other) return true
         if (other !is Structure) return false

src/prolog/ast/terms/Term.kt

@@ -1,14 +1,18 @@
 package prolog.ast.terms
 
+import prolog.Substitutions
+import prolog.ast.arithmetic.Float
+import prolog.ast.arithmetic.Integer
 import prolog.logic.compare
 
 /**
  * Value in Prolog.
  *
- * A [Term] is either a [Variable], [Atom], [Integer][prolog.ast.arithmetic.Integer],
+ * A [Term] is either a [Variable], [Atom], [Integer],
- * [Float][prolog.ast.arithmetic.Float] or [CompoundTerm].
+ * [Float] or [CompoundTerm].
  * In addition, SWI-Prolog also defines the type TODO string.
  */
 interface Term : Comparable<Term> {
     override fun compareTo(other: Term): Int = compare(this, other, emptyMap())
+    fun applySubstitution(subs: Substitutions): Term
 }

src/prolog/ast/terms/Variable.kt

@@ -34,6 +34,8 @@ open class Variable(val name: String) : Term, Body, Expression, LogicOperand() {
         return name == other.name
     }
 
+    override fun applySubstitution(subs: Substitutions): Variable = this
+
     override fun hashCode(): Int {
         return name.hashCode()
     }

src/prolog/builtins/arithmeticOperators.kt

@@ -39,6 +39,10 @@ class EvaluatesToDifferent(private val left: Expression, private val right: Expr
         }
     }
 
+    override fun applySubstitution(subs: Substitutions): EvaluatesToDifferent = EvaluatesToDifferent(
+        left.applySubstitution(subs) as Expression,
+        right.applySubstitution(subs) as Expression
+    )
 }
 
 /**
@@ -57,6 +61,11 @@ class EvaluatesTo(private val left: Expression, private val right: Expression) :
 
         return if (equivalent(t1.to, t2.to, subs)) sequenceOf(Result.success(emptyMap())) else emptySequence()
     }
+
+    override fun applySubstitution(subs: Substitutions): EvaluatesTo = EvaluatesTo(
+        left.applySubstitution(subs) as Expression,
+        right.applySubstitution(subs) as Expression
+    )
 }
 
 /**
@@ -78,6 +87,11 @@ class Is(val number: Expression, val expr: Expression) :
 
         return unifyLazy(t1.to, t2.to, subs)
     }
+
+    override fun applySubstitution(subs: Substitutions): Is = Is(
+        number.applySubstitution(subs) as Expression,
+        expr.applySubstitution(subs) as Expression
+    )
 }
 
 /**
@@ -101,6 +115,11 @@ open class Add(private val expr1: Expression, private val expr2: Expression) :
         val simplification = result.simplify(map.first().getOrThrow())
         return Simplification(this, simplification.to)
     }
+
+    override fun applySubstitution(subs: Substitutions): Add = Add(
+        expr1.applySubstitution(subs) as Expression,
+        expr2.applySubstitution(subs) as Expression
+    )
 }
 
 /**
@@ -114,6 +133,11 @@ open class Subtract(private val expr1: Expression, private val expr2: Expression
         val simplification = result.simplify(map.first().getOrThrow())
         return Simplification(this, simplification.to)
     }
+
+    override fun applySubstitution(subs: Substitutions): Subtract = Subtract(
+        expr1.applySubstitution(subs) as Expression,
+        expr2.applySubstitution(subs) as Expression
+    )
 }
 
 /**
@@ -127,6 +151,11 @@ class Multiply(val expr1: Expression, val expr2: Expression) :
         val simplification = result.simplify(map.first().getOrThrow())
         return Simplification(this, simplification.to)
     }
+
+    override fun applySubstitution(subs: Substitutions): Multiply = Multiply(
+        expr1.applySubstitution(subs) as Expression,
+        expr2.applySubstitution(subs) as Expression
+    )
 }
 
 class Divide(private val expr1: Expression, private val expr2: Expression) :
@@ -137,6 +166,11 @@ class Divide(private val expr1: Expression, private val expr2: Expression) :
         val simplification = result.simplify(map.first().getOrThrow())
         return Simplification(this, simplification.to)
     }
+
+    override fun applySubstitution(subs: Substitutions): Divide = Divide(
+        expr1.applySubstitution(subs) as Expression,
+        expr2.applySubstitution(subs) as Expression
+    )
 }
 
 // TODO Expr mod Expr
@@ -166,5 +200,11 @@ class Between(private val expr1: Expression, private val expr2: Expression, priv
         }
     }
 
+    override fun applySubstitution(subs: Substitutions): Between = Between(
+        expr1.applySubstitution(subs) as Expression,
+        expr2.applySubstitution(subs) as Expression,
+        expr3.applySubstitution(subs) as Expression
+    )
+
     override fun toString(): String = "$expr1..$expr3..$expr2"
 }

src/prolog/builtins/controlOperators.kt

@@ -7,13 +7,16 @@ import prolog.ast.logic.LogicOperator
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Body
 import prolog.ast.terms.Goal
+import prolog.ast.terms.Structure
 import prolog.flags.AppliedCut
+import prolog.logic.applySubstitution
 
 /**
  * Always fail.
  */
 object Fail : Atom("fail"), Body {
     override fun satisfy(subs: Substitutions): Answers = emptySequence()
+    override fun applySubstitution(subs: Substitutions): Fail = Fail
 }
 
 /**
@@ -26,6 +29,7 @@ typealias False = Fail
  */
 object True : Atom("true"), Body {
     override fun satisfy(subs: Substitutions): Answers = sequenceOf(Result.success(emptyMap()))
+    override fun applySubstitution(subs: Substitutions): True = True
 }
 
 // TODO Repeat/0
@@ -34,6 +38,8 @@ class Cut() : Atom("!") {
     override fun satisfy(subs: Substitutions): Answers {
         return sequenceOf(Result.failure(AppliedCut(emptyMap())))
     }
+
+    override fun applySubstitution(subs: Substitutions): Cut = Cut()
 }
 
 /**
@@ -94,6 +100,11 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
             )
         }
     }
+
+    override fun applySubstitution(subs: Substitutions): Conjunction = Conjunction(
+        applySubstitution(left, subs) as LogicOperand,
+        applySubstitution(right, subs) as LogicOperand
+    )
 }
 
 /**
@@ -105,6 +116,11 @@ open class Disjunction(private val left: LogicOperand, private val right: LogicO
         yieldAll(left.satisfy(subs))
         yieldAll(right.satisfy(subs))
     }
+
+    override fun applySubstitution(subs: Substitutions): Disjunction = Disjunction(
+        applySubstitution(left, subs) as LogicOperand,
+        applySubstitution(right, subs) as LogicOperand
+    )
 }
 
 @Deprecated("Use Disjunction instead")
@@ -127,4 +143,6 @@ class Not(private val goal: Goal) : LogicOperator(Atom("\\+"), rightOperand = go
         // If the goal cannot be proven, return a sequence with an empty map
         return sequenceOf(Result.success(emptyMap()))
     }
+
+    override fun applySubstitution(subs: Substitutions): Not = Not(applySubstitution(goal, subs) as Goal)
 }

src/prolog/builtins/databaseOperators.kt

@@ -42,6 +42,8 @@ class Dynamic(private val dynamicFunctor: Functor): Goal(), Body {
     }
 
     override fun hashCode(): Int = super.hashCode()
+
+    override fun applySubstitution(subs: Substitutions): Dynamic = Dynamic(dynamicFunctor)
 }
 
 class Assert(clause: Clause) : AssertZ(clause) {
@@ -59,6 +61,8 @@ class AssertA(val clause: Clause) : Operator(Atom("asserta"), null, clause) {
 
         return sequenceOf(Result.success(emptyMap()))
     }
+
+    override fun applySubstitution(subs: Substitutions): AssertA = AssertA(applySubstitution(clause, subs) as Clause)
 }
 
 /**
@@ -72,6 +76,8 @@ open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause)
 
         return sequenceOf(Result.success(emptyMap()))
     }
+
+    override fun applySubstitution(subs: Substitutions): AssertZ = AssertZ(applySubstitution(clause, subs) as Clause)
 }
 
 /**
@@ -110,4 +116,6 @@ class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
             }
         }
     }
+
+    override fun applySubstitution(subs: Substitutions): Retract = Retract(applySubstitution(term, subs))
 }

src/prolog/builtins/ioOperators.kt

@@ -27,6 +27,8 @@ class Write(private val term: Term) : Operator(Atom("write"), null, term), Satis
         return sequenceOf(Result.success(emptyMap()))
     }
 
+    override fun applySubstitution(subs: Substitutions): Write = Write(applySubstitution(term, subs))
+
     override fun toString(): String = "write($term)"
 }
 
@@ -39,6 +41,8 @@ object Nl : Atom("nl"), Satisfiable {
         Program.storeNewLine = false
         return sequenceOf(Result.success(emptyMap()))
     }
+
+    override fun applySubstitution(subs: Substitutions): Nl = this
 }
 
 /**
@@ -72,4 +76,6 @@ class Read(private val term: Term) : Operator(Atom("read"), null, term), Satisfi
 
         yieldAll(unifyLazy(t1, t2, subs))
     }
+
+    override fun applySubstitution(subs: Substitutions): Read = Read(applySubstitution(term, subs))
 }

src/prolog/builtins/unificationOperators.kt

@@ -24,11 +24,20 @@ class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="
 
         yieldAll(unifyLazy(t1, t2, subs))
     }
+
+    override fun applySubstitution(subs: Substitutions): Unify = Unify(
+        applySubstitution(term1, subs),
+        applySubstitution(term2, subs)
+    )
 }
 
-class NotUnify(term1: Term, term2: Term) : Operator(Atom("\\="), term1, term2) {
+class NotUnify(private val term1: Term, private val term2: Term) : Operator(Atom("\\="), term1, term2) {
     private val not = Not(Unify(term1, term2))
     override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs)
+    override fun applySubstitution(subs: Substitutions): NotUnify = NotUnify(
+        applySubstitution(term1, subs),
+        applySubstitution(term2, subs)
+    )
 }
 
 class Equivalent(private val term1: Term, private val term2: Term) : Operator(Atom("=="), term1, term2) {
@@ -40,4 +49,9 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator(At
             yield(Result.success(emptyMap()))
         }
     }
+
+    override fun applySubstitution(subs: Substitutions): Equivalent = Equivalent(
+        applySubstitution(term1, subs),
+        applySubstitution(term2, subs)
+    )
 }

src/prolog/logic/unification.kt

@@ -15,19 +15,15 @@ import prolog.ast.terms.*
 
 // Apply substitutions to a term
 fun applySubstitution(term: Term, subs: Substitutions): Term = when {
-    term is Fact -> {
+    term is Fact -> term.applySubstitution(subs)
-        Fact(applySubstitution(term.head, subs) as Head)
-    }
 
     variable(term, emptyMap()) -> {
         val variable = term as Variable
         subs[variable]?.let { applySubstitution(term = it, subs = subs) } ?: term
     }
+
     atomic(term, subs) -> term
-    compound(term, subs) -> {
+    compound(term, subs) -> term.applySubstitution(subs)
-        val structure = term as Structure
-        Structure(structure.name, structure.arguments.map { applySubstitution(it, subs) })
-    }
 
     else -> term
 }

tests/prolog/EvaluationTests.kt

@@ -14,6 +14,8 @@ import prolog.ast.terms.Atom
 import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable
 import prolog.ast.Database.Program
+import prolog.ast.arithmetic.Integer
+import prolog.ast.terms.AnonymousVariable
 
 class EvaluationTests {
     @BeforeEach
@@ -108,8 +110,8 @@ class EvaluationTests {
         val variable2 = Variable("Y")
 
         val parent = Rule(
-            Structure(Atom("parent"), listOf(variable1, variable2)),
+            Structure(Atom("parent"), listOf(variable1, variable2)), /* :- */
-            /* :- */ Disjunction(
+            Disjunction(
                 Structure(Atom("father"), listOf(variable1, variable2)),
                 /* ; */
                 Structure(Atom("mother"), listOf(variable1, variable2))
@@ -118,10 +120,14 @@ class EvaluationTests {
 
         Program.load(listOf(father, mother, parent))
 
-        val result1 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy"))))
+        val result1 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy")))).toList()
-        assertTrue(result1.toList().isNotEmpty())
+        assertEquals(1, result1.size, "Expected 1 result")
-        val result2 = Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy"))))
+        assertTrue(result1[0].isSuccess, "Expected success")
-        assertTrue(result2.toList().isNotEmpty())
+        assertTrue(result1[0].getOrNull()!!.isEmpty(), "Expected no substitutions")
+        val result2 = Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy")))).toList()
+        assertEquals(1, result2.size, "Expected 1 result")
+        assertTrue(result2[0].isSuccess, "Expected success")
+        assertTrue(result2[0].getOrNull()!!.isEmpty(), "Expected no substitutions")
 
         val result3 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jane"))))
         assertFalse(result3.any())
@@ -414,4 +420,63 @@ class EvaluationTests {
             assertEquals(Atom("bob"), subs5[Variable("Person")], "Expected bob")
         }
     }
+
+    @Test
+    fun `leq Peano`() {
+        val fact = Fact(Structure(Atom("leq"), listOf(Integer(0), AnonymousVariable.create())))
+        val rule = Rule(
+            Structure(
+                Atom("leq"),
+                listOf(Structure(Atom("s"), listOf(Variable("X"))), Structure(Atom("s"), listOf(Variable("Y"))))
+            ),
+            Structure(Atom("leq"), listOf(Variable("X"), Variable("Y"))),
+        )
+
+        Program.db.load(listOf(fact, rule))
+
+        val result1 = Program.query(Structure(Atom("leq"), listOf(Variable("X"), Integer(0)))).toList()
+
+        assertEquals(1, result1.size, "Expected 1 result")
+        assertTrue(result1[0].isSuccess, "Expected success")
+        val subs = result1[0].getOrNull()!!
+        assertEquals(1, subs.size, "Expected 1 substitution")
+        assertEquals(Integer(0), subs[Variable("X")], "Expected X to be 0")
+
+        val result2 =
+            Program.query(Structure(Atom("leq"), listOf(Variable("X"), Structure(Atom("s"), listOf(Integer(0))))))
+                .toList()
+
+        assertEquals(2, result2.size, "Expected 2 results")
+
+        assertTrue(result2[0].isSuccess, "Expected success")
+        val subs2a = result2[0].getOrNull()!!
+        assertEquals(1, subs2a.size, "Expected 1 substitution")
+        assertEquals(Integer(0), subs2a[Variable("X")], "Expected X to be 0")
+
+        assertTrue(result2[1].isSuccess, "Expected success")
+        val subs2b = result2[1].getOrNull()!!
+        assertEquals(1, subs2b.size, "Expected 1 substitution")
+        assertEquals(Structure(Atom("s"), listOf(Integer(0))), subs2b[Variable("X")], "Expected X to be s(0)")
+
+        val result3 = Program.query(
+            Structure(
+                Atom("leq"),
+                listOf(Variable("X"), Structure(Atom("s"), listOf(Structure(Atom("s"), listOf(Integer(0))))))
+            )
+        ).toList()
+
+        assertEquals(3, result3.size, "Expected 3 results")
+        assertTrue(result3[0].isSuccess, "Expected success")
+        val subs3a = result3[0].getOrNull()!!
+        assertEquals(1, subs3a.size, "Expected 1 substitution")
+        assertEquals(Integer(0), subs3a[Variable("X")], "Expected X to be 0")
+        assertTrue(result3[1].isSuccess, "Expected success")
+        val subs3b = result3[1].getOrNull()!!
+        assertEquals(1, subs3b.size, "Expected 1 substitution")
+        assertEquals(Structure(Atom("s"), listOf(Integer(0))), subs3b[Variable("X")], "Expected X to be s(0)")
+        assertTrue(result3[2].isSuccess, "Expected success")
+        val subs3c = result3[2].getOrNull()!!
+        assertEquals(1, subs3c.size, "Expected 1 substitution")
+        assertEquals(Structure(Atom("s"), listOf(Structure(Atom("s"), listOf(Integer(0))))), subs3c[Variable("X")], "Expected X to be s(s(0))")
+    }
 }