Checkpoint

src/prolog/builtins/control.kt

@@ -1,15 +1,18 @@
 package prolog.builtins
 
+import prolog.Substitution
 import prolog.components.expressions.Operand
 import prolog.components.expressions.Operator
 import prolog.components.terms.Atom
 import prolog.components.terms.Body
+import prolog.components.terms.Term
+import prolog.components.terms.Variable
 
 /**
  * Always fail.
  */
 class Fail: Atom("fail"), Body {
-    override fun prove(): Boolean = false
+    override fun prove(): Sequence<Substitution> = emptySequence()
 }
 
 /**
@@ -21,7 +24,7 @@ typealias False = Fail
  * Always succeed.
  */
 class True: Atom("true"), Body {
-    override fun prove(): Boolean = true
+    override fun prove(): Sequence<Substitution> = sequenceOf(emptyMap())
 }
 
 // TODO Repeat/0
@@ -32,10 +35,16 @@ class True: Atom("true"), Body {
  * Conjunction (and). True if both Goal1 and Goal2 are true.
  */
 class Conjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(","), leftOperand, rightOperand) {
-    override fun prove(): Boolean {
-        val left = leftOperand?.prove() ?: true
-        val right = rightOperand.prove()
-        return left && right
+    override fun prove(): Sequence<Substitution> = sequence {
+        if (leftOperand != null) {
+            leftOperand.prove().forEach { left ->
+                rightOperand.prove().forEach { right ->
+                    yield(left + right)
+                }
+            }
+        } else {
+            yieldAll(rightOperand.prove())
+        }
     }
 }
 
@@ -43,9 +52,10 @@ class Conjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom("
  * Disjunction (or). True if either Goal1 or Goal2 succeeds.
  */
 class Disjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(";"), leftOperand, rightOperand) {
-    override fun prove(): Boolean {
-        val left = leftOperand?.prove() ?: false
-        val right = rightOperand.prove()
-        return left || right
+    override fun prove(): Sequence<Substitution> = sequence {
+        if (leftOperand != null) {
+            yieldAll(leftOperand.prove())
+        }
+        yieldAll(rightOperand.prove())
     }
 }

src/prolog/builtins/other.kt

@@ -1,9 +1,10 @@
 package prolog.builtins
 
+import prolog.Substitution
 import prolog.components.expressions.Operand
 import prolog.components.expressions.Operator
 import prolog.components.terms.Atom
 
 class Query(rightOperand: Operand) : Operator(Atom("?-"), null, rightOperand) {
-    override fun prove(): Boolean = rightOperand.prove()
+    override fun prove(): Sequence<Substitution> = rightOperand.prove()
 }

src/prolog/components/Program.kt

@@ -1,5 +1,6 @@
 package prolog.components
 
+import prolog.Substitution
 import prolog.builtins.True
 import prolog.components.expressions.Clause
 import prolog.components.expressions.Fact
@@ -24,16 +25,20 @@ object Program: Resolvent {
         ))
     }
 
-    fun query(goal: Goal): Boolean {
+    /**
+     * Queries the program with a goal.
+     * @return true if the goal can be proven, false otherwise.
+     */
+    fun query(goal: Goal): Boolean = solve(goal).any()
+
+    override fun solve(goal: Goal): Sequence<Substitution> {
         val functor = goal.functor
         // If the predicate does not exist, return false
-        val predicate = predicates[functor] ?: return false
+        val predicate = predicates[functor] ?: return emptySequence()
         // If the predicate exists, evaluate the goal against it
         return predicate.solve(goal)
     }
 
-    override fun solve(goal: Goal): Boolean = query(goal)
-
     /**
      * Loads a list of clauses into the program.
      */

src/prolog/components/Provable.kt

@@ -1,5 +1,13 @@
 package prolog.components
 
+import prolog.Substitution
+
 interface Provable {
-    fun prove(): Boolean
+    /**
+     * Proves the current [Provable] instance.
+     *
+     * @return a sequence of [Substitution] instances representing the results of the proof.
+     * If the proof fails, an empty sequence is returned.
+     */
+    fun prove(): Sequence<Substitution>
 }

src/prolog/components/Resolvent.kt

@@ -1,10 +1,17 @@
 package prolog.components
 
+import prolog.Substitution
 import prolog.components.terms.Goal
 
 /**
  * Can be instructed to solve a goal.
  */
 interface Resolvent {
-    fun solve(goal: Goal): Boolean
+    /**
+     * Attempts to solve the given goal.
+     *
+     * @return A sequence of substitutions that can be applied to the goal to unify it with this resolvent.
+     * If the goal cannot be unified with this resolvent, an empty sequence is returned.
+     */
+    fun solve(goal: Goal): Sequence<Substitution>
 }

src/prolog/components/expressions/Clause.kt

@@ -1,8 +1,9 @@
 package prolog.components.expressions
 
+import prolog.Substitution
 import prolog.components.Resolvent
 import prolog.components.terms.*
-import prolog.unify
+import prolog.unifyLazy
 
 /**
  * ‘Sentence’ of a Prolog program.
@@ -15,20 +16,22 @@ import prolog.unify
 abstract class Clause(private val head: Head, private val body: Body? = null) : Resolvent {
     val functor: Functor = head.functor
 
-    override fun solve(goal: Goal): Boolean {
-        val unification = unify(goal, head)
-
-        if (unification.isEmpty) {
-            return false
+    override fun solve(goal: Goal): Sequence<Substitution> = sequence {
+        if (body == null) {
+            // If the clause is a fact, unify the goal with the head, and return the substitutions.
+            // Do this in a lazy way.
+            yieldAll(unifyLazy(goal, head))
+        } else {
+            // If the clause is a rule, unify the goal with the head and then try to prove the body.
+            // Only if the body can be proven, the substitutions should be returned.
+            // Do this in a lazy way.
+            unifyLazy(goal, head).forEach { subs ->
+                // If the body can be proven, yield the (combined) substitutions
+                body.prove().forEach { bodySubs ->
+                    yield(subs + bodySubs)
+                }
+            }
         }
-
-        val substitutions = unification.get()
-
-        val proven = body == null || body.prove()
-
-        substitutions.forEach { (variable, _) -> variable.unbind() }
-
-        return proven
     }
 
     override fun toString(): String {

src/prolog/components/expressions/Operator.kt

@@ -1,5 +1,6 @@
 package prolog.components.expressions
 
+import prolog.Substitution
 import prolog.components.Provable
 import prolog.components.terms.Atom
 import prolog.components.terms.CompoundTerm
@@ -8,11 +9,11 @@ import prolog.components.terms.Goal
 typealias Operand = Goal
 
 abstract class Operator(
-    val symbol: Atom,
+    private val symbol: Atom,
     val leftOperand: Operand? = null,
     val rightOperand: Operand
 ) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)), Provable {
-    abstract override fun prove(): Boolean
+    abstract override fun prove(): Sequence<Substitution>
 
     override fun toString(): String {
         return when (leftOperand) {

src/prolog/components/expressions/Predicate.kt

@@ -1,5 +1,6 @@
 package prolog.components.expressions
 
+import prolog.Substitution
 import prolog.components.Resolvent
 import prolog.components.terms.Functor
 import prolog.components.terms.Goal
@@ -48,8 +49,12 @@ class Predicate : Resolvent {
         this.clauses.addAll(clauses)
     }
 
-    override fun solve(goal: Goal): Boolean {
+    override fun solve(goal: Goal): Sequence<Substitution> = sequence {
         require(goal.functor == functor) { "Goal functor does not match predicate functor" }
-        return clauses.any { it.solve(goal) }
+        for (clause in clauses) {
+            // Try to unify the goal with the clause
+            // If the unification is successful, yield the substitutions
+            yieldAll(clause.solve(goal))
+        }
     }
 }

src/prolog/components/terms/Atom.kt

@@ -1,12 +1,14 @@
 package prolog.components.terms
 
+import prolog.Substitution
 import prolog.components.Resolvent
 import prolog.unify
+import prolog.unifyLazy
 
 open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
     override val functor: Functor = "$name/_"
 
-    override fun solve(goal: Goal): Boolean = unify(goal, this).isEmpty
+    override fun solve(goal: Goal): Sequence<Substitution> = unifyLazy(goal, this)
 
     override fun toString(): String {
         return name

src/prolog/components/terms/Goal.kt

@@ -1,5 +1,6 @@
 package prolog.components.terms
 
+import prolog.Substitution
 import prolog.components.Program
 import prolog.components.Provable
 
@@ -13,5 +14,5 @@ import prolog.components.Provable
 abstract class Goal : Term, Provable {
     abstract val functor: Functor
 
-    override fun prove(): Boolean = Program.query(this)
+    override fun prove(): Sequence<Substitution> = Program.solve(this)
 }

src/prolog/components/terms/Structure.kt

@@ -1,15 +1,16 @@
 package prolog.components.terms
 
+import prolog.Substitution
 import prolog.components.Resolvent
-import prolog.unify
+import prolog.unifyLazy
 
 typealias Argument = Term
 
 open class Structure(val name: Atom, val arguments: List<Argument>): Goal(), Head, Body, Resolvent {
     override val functor: Functor = "${name.name}/${arguments.size}"
 
-    override fun solve(goal: Goal): Boolean {
-        return unify(goal, this).isEmpty
+    override fun solve(goal: Goal): Sequence<Substitution> {
+        return unifyLazy(goal, this)
     }
 
     override fun toString(): String {

src/prolog/unify.kt

@@ -11,7 +11,7 @@ import java.util.*
 typealias Substitution = Map<Variable, Term>
 
 // Apply substitutions to a term
-fun applySubstitution(term: Term, substitution: Substitution): Term = when {
+private fun applySubstitution(term: Term, substitution: Substitution): Term = when {
     variable(term) -> (term as Variable).alias().map { applySubstitution(it, substitution) }.orElse(term)
     atomic(term)   -> term
     compound(term) -> {
@@ -22,7 +22,7 @@ fun applySubstitution(term: Term, substitution: Substitution): Term = when {
 }
 
 // Check if a variable occurs in a term
-fun occurs(variable: Variable, term: Term): Boolean = when {
+private fun occurs(variable: Variable, term: Term): Boolean = when {
     variable(term) -> term == variable
     atomic(term) -> false
     compound(term) -> {
@@ -33,7 +33,7 @@ fun occurs(variable: Variable, term: Term): Boolean = when {
 }
 
 // Generate possible substitutions
-fun generateSubstitutions(term1: Term, term2: Term, substitution: Substitution): Sequence<Substitution> = sequence {
+private fun generateSubstitutions(term1: Term, term2: Term, substitution: Substitution): Sequence<Substitution> = sequence {
     val t1 = applySubstitution(term1, substitution)
     val t2 = applySubstitution(term2, substitution)
 
@@ -42,15 +42,17 @@ fun generateSubstitutions(term1: Term, term2: Term, substitution: Substitution):
         variable(t1) -> {
             val variable = t1 as Variable
             if (!occurs(variable, t2)) {
-                variable.bind(t2)
+//                variable.bind(t2)
                 yield(substitution + (variable to t2))
+//                variable.unbind()
             }
         }
         variable(t2) -> {
             val variable = t2 as Variable
             if (!occurs(variable, t1)) {
-                variable.bind(t1)
+//                variable.bind(t1)
                 yield(substitution + (variable to t1))
+//                variable.unbind()
             }
         }
         compound(t1) && compound(t2) -> {
@@ -68,8 +70,11 @@ fun generateSubstitutions(term1: Term, term2: Term, substitution: Substitution):
 }
 
 // Unify two terms with backtracking and lazy evaluation
-fun unifyLazy(term1: Term, term2: Term, substitution: Substitution = emptyMap()): Sequence<Substitution> {
-    return generateSubstitutions(term1, term2, substitution)
+fun unifyLazy(term1: Term, term2: Term, substitution: Substitution = emptyMap()): Sequence<Substitution> = sequence {
+    generateSubstitutions(term1, term2, substitution).forEach { newSubstitution ->
+        // Return the new substitution
+        yield(newSubstitution)
+    }
 }
 
 fun unify(term1: Term, term2: Term): Optional<Substitution> {

tests/prolog/EvaluationTest.kt

@@ -1,7 +1,6 @@
 package prolog
 
-import org.junit.jupiter.api.Assertions.assertFalse
-import org.junit.jupiter.api.Assertions.assertTrue
+import org.junit.jupiter.api.Assertions.*
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
 import prolog.builtins.Conjunction
@@ -11,6 +10,7 @@ import prolog.components.expressions.Fact
 import prolog.components.expressions.Rule
 import prolog.components.terms.Atom
 import prolog.components.terms.Structure
+import prolog.components.terms.Variable
 
 class EvaluationTest {
     @BeforeEach
@@ -23,7 +23,9 @@ class EvaluationTest {
         val fact = Fact(Atom("a"))
         Program.load(listOf(fact))
 
-        assertTrue(Program.query(Atom("a")))
+        val result = Program.query(Atom("a"))
+
+        assertTrue(result)
     }
 
     @Test
@@ -75,14 +77,14 @@ class EvaluationTest {
         val mother = Fact(Structure(Atom("mother"), listOf(Atom("jane"), Atom("jimmy"))))
 
         val parent1 = Rule(
-            Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))),
+            Structure(Atom("parent"), listOf(Variable("X"), Variable("Y"))),
             /* :- */
-            Structure(Atom("father"), listOf(Atom("X"), Atom("Y")))
+            Structure(Atom("father"), listOf(Variable("X"), Variable("Y")))
         )
         val parent2 = Rule(
-            Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))),
+            Structure(Atom("parent"), listOf(Variable("X"), Variable("Y"))),
             /* :- */
-            Structure(Atom("mother"), listOf(Atom("X"), Atom("Y")))
+            Structure(Atom("mother"), listOf(Variable("X"), Variable("Y")))
         )
 
         Program.load(listOf(father, mother, parent1, parent2))
@@ -100,11 +102,11 @@ class EvaluationTest {
         val mother = Fact(Structure(Atom("mother"), listOf(Atom("jane"), Atom("jimmy"))))
 
         val parent = Rule(
-            Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))),
+            Structure(Atom("parent"), listOf(Variable("X"), Variable("Y"))),
             /* :- */ Disjunction(
-            Structure(Atom("father"), listOf(Atom("X"), Atom("Y"))),
+            Structure(Atom("father"), listOf(Variable("X"), Variable("Y"))),
             /* ; */
-            Structure(Atom("mother"), listOf(Atom("X"), Atom("Y")))
+            Structure(Atom("mother"), listOf(Variable("X"), Variable("Y")))
             ))
 
         Program.load(listOf(father, mother, parent))
@@ -129,17 +131,17 @@ class EvaluationTest {
         val parent2 = Fact(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy"))))
 
         val isFather = Rule(
-            Structure(Atom("isFather"), listOf(Atom("X"), Atom("Y"))),
+            Structure(Atom("isFather"), listOf(Variable("X"), Variable("Y"))),
             Conjunction(
-                Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))),
-                Structure(Atom("male"), listOf(Atom("X")))
+                Structure(Atom("parent"), listOf(Variable("X"), Variable("Y"))),
+                Structure(Atom("male"), listOf(Variable("X")))
             )
         )
         val isMother = Rule(
-            Structure(Atom("isMother"), listOf(Atom("X"), Atom("Y"))),
+            Structure(Atom("isMother"), listOf(Variable("X"), Variable("Y"))),
             Conjunction(
-                Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))),
-                Structure(Atom("female"), listOf(Atom("X")))
+                Structure(Atom("parent"), listOf(Variable("X"), Variable("Y"))),
+                Structure(Atom("female"), listOf(Variable("X")))
             )
         )