fix: Evaluation

src/prolog/builtins/control.kt

@@ -1,18 +1,16 @@
 package prolog.builtins
 
-import prolog.Substitution
+import prolog.Substituted
 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(): Sequence<Substitution> = emptySequence()
+    override fun prove(subs: Substituted): Sequence<Substituted> = emptySequence()
 }
 
 /**
@@ -24,7 +22,7 @@ typealias False = Fail
  * Always succeed.
  */
 class True: Atom("true"), Body {
-    override fun prove(): Sequence<Substitution> = sequenceOf(emptyMap())
+    override fun prove(subs: Substituted): Sequence<Substituted> = sequenceOf(emptyMap())
 }
 
 // TODO Repeat/0
@@ -35,15 +33,15 @@ 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(): Sequence<Substitution> = sequence {
+    override fun prove(subs: Substituted): Sequence<Substituted> = sequence {
         if (leftOperand != null) {
-            leftOperand.prove().forEach { left ->
-                rightOperand.prove().forEach { right ->
+            leftOperand.prove(subs).forEach { left ->
+                rightOperand.prove(subs + left).forEach { right ->
                     yield(left + right)
                 }
             }
         } else {
-            yieldAll(rightOperand.prove())
+            yieldAll(rightOperand.prove(subs))
         }
     }
 }
@@ -52,10 +50,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(): Sequence<Substitution> = sequence {
+    override fun prove(subs: Substituted): Sequence<Substituted> = sequence {
         if (leftOperand != null) {
-            yieldAll(leftOperand.prove())
+            yieldAll(leftOperand.prove(subs))
         }
-        yieldAll(rightOperand.prove())
+        yieldAll(rightOperand.prove(subs))
     }
 }

src/prolog/builtins/other.kt

@@ -1,10 +1,10 @@
 package prolog.builtins
 
-import prolog.Substitution
+import prolog.Substituted
 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(): Sequence<Substitution> = rightOperand.prove()
+    override fun prove(subs: Substituted): Sequence<Substituted> = rightOperand.prove(subs)
 }

src/prolog/builtins/unification.kt

@@ -0,0 +1,20 @@
+package prolog.builtins
+
+import prolog.components.terms.Atom
+import prolog.components.terms.Structure
+import prolog.components.terms.Term
+import prolog.components.terms.Variable
+
+/**
+ * True if Term1 is equivalent to Term2. A variable is only identical to a sharing variable.
+ */
+fun equivalent(term1: Term, term2: Term): Boolean {
+    return when {
+        term1 is Variable && term2 is Variable -> term1 == term2
+        term1 is Variable -> term1.alias().isPresent && equivalent(term1.alias().get(), term2)
+        term2 is Variable -> term2.alias().isPresent && equivalent(term2.alias().get(), term1)
+        term1 is Atom && term2 is Atom -> term1.compareTo(term2) == 0
+        term1 is Structure && term2 is Structure -> term1.compareTo(term2) == 0
+        else -> false
+    }
+}

src/prolog/components/Program.kt

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

src/prolog/components/Provable.kt

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

src/prolog/components/Resolvent.kt

@@ -1,6 +1,6 @@
 package prolog.components
 
-import prolog.Substitution
+import prolog.Substituted
 import prolog.components.terms.Goal
 
 /**
@@ -13,5 +13,5 @@ interface Resolvent {
      * @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>
+    fun solve(goal: Goal, subs: Substituted): Sequence<Substituted>
 }

src/prolog/components/expressions/Clause.kt

@@ -1,6 +1,8 @@
 package prolog.components.expressions
 
-import prolog.Substitution
+import prolog.Substituted
+import prolog.builtins.True
+import prolog.builtins.equivalent
 import prolog.components.Resolvent
 import prolog.components.terms.*
 import prolog.unifyLazy
@@ -13,31 +15,29 @@ import prolog.unifyLazy
  * @see [prolog.components.terms.Variable]
  * @see [Predicate]
  */
-abstract class Clause(private val head: Head, private val body: Body? = null) : Resolvent {
+abstract class Clause(private val head: Head, private val body: Body) : Resolvent {
     val functor: Functor = head.functor
 
-    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)
-                }
+    override fun solve(goal: Goal, subs: Substituted): Sequence<Substituted> = sequence {
+        // 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, subs).forEach { newHeadSubs ->
+            // If the body can be proven, yield the (combined) substitutions
+            body.prove(subs + newHeadSubs).forEach { newBodySubs ->
+                yield(newHeadSubs + newBodySubs)
+                // Unbind the newly bound variables, so they can be reused.
+                newBodySubs.keys.forEach { it.unbind() }
             }
+            // Unbind the newly bound variables, so they can be reused.
+            newHeadSubs.keys.forEach { it.unbind() }
         }
     }
 
     override fun toString(): String {
         return when {
-            body == null -> head.toString()
-            else -> "$head :- $body"
+            body == True() -> head.toString()
+            else           -> "$head :- $body"
         }
     }
 }

src/prolog/components/expressions/Operator.kt

@@ -1,6 +1,6 @@
 package prolog.components.expressions
 
-import prolog.Substitution
+import prolog.Substituted
 import prolog.components.Provable
 import prolog.components.terms.Atom
 import prolog.components.terms.CompoundTerm
@@ -13,7 +13,7 @@ abstract class Operator(
     val leftOperand: Operand? = null,
     val rightOperand: Operand
 ) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)), Provable {
-    abstract override fun prove(): Sequence<Substitution>
+    abstract override fun prove(subs: Substituted): Sequence<Substituted>
 
     override fun toString(): String {
         return when (leftOperand) {

src/prolog/components/expressions/Predicate.kt

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

src/prolog/components/terms/Atom.kt

@@ -1,29 +1,24 @@
 package prolog.components.terms
 
-import prolog.Substitution
+import prolog.Substituted
 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): Sequence<Substitution> = unifyLazy(goal, this)
+    override fun solve(goal: Goal, subs: Substituted): Sequence<Substituted> = unifyLazy(goal, this, subs)
+
+    override fun compareTo(other: Term): Int {
+        return when (other) {
+            is Variable  -> 1
+            is Atom      -> name.compareTo(other.name)
+            is Structure -> -1
+            else         -> throw IllegalArgumentException("Cannot compare $this with $other")
+        }
+    }
 
     override fun toString(): String {
         return name
     }
-
-    override fun equals(other: Any?): Boolean {
-        if (this === other) return true
-        if (other !is Atom) return false
-
-        if (name != other.name) return false
-
-        return true
-    }
-
-    override fun hashCode(): Int {
-        return javaClass.hashCode()
-    }
 }

src/prolog/components/terms/Goal.kt

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

src/prolog/components/terms/Structure.kt

@@ -1,6 +1,7 @@
 package prolog.components.terms
 
-import prolog.Substitution
+import prolog.Substituted
+import prolog.builtins.equivalent
 import prolog.components.Resolvent
 import prolog.unifyLazy
 
@@ -9,8 +10,26 @@ 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): Sequence<Substitution> {
-        return unifyLazy(goal, this)
+    override fun solve(goal: Goal, subs: Substituted): Sequence<Substituted> {
+        return unifyLazy(goal, this, subs)
+    }
+
+    override fun compareTo(other: Term): Int {
+        when (other) {
+            is Structure -> {
+                val arityComparison = arguments.size.compareTo(other.arguments.size)
+                if (arityComparison != 0) return arityComparison
+                val nameComparison = name.compareTo(other.name)
+                if (nameComparison != 0) return nameComparison
+                arguments.zip(other.arguments).forEach { (arg1, arg2) ->
+                    val argsComparison = equivalent(arg1, arg2)
+                    if (!argsComparison) return arg1.compareTo(arg2)
+                }
+                return 0
+            }
+            // Structure is always greater than other terms
+            else -> return 1
+        }
     }
 
     override fun toString(): String {

src/prolog/components/terms/Term.kt

@@ -6,7 +6,7 @@ package prolog.components.terms
  * A [Term] is either a [Variable], [Atom], integer, float or [CompoundTerm].
  * In addition, SWI-Prolog also defines the type string.
  */
-interface Term
+interface Term : Comparable<Term>
 
 /*
 <program> ::= <clause list> <query> | <query>

src/prolog/components/terms/Variable.kt

@@ -21,18 +21,18 @@ data class Variable(val name: String) : Term {
         alias = Optional.empty()
     }
 
-    override fun toString(): String {
-        return when {
-            alias.isPresent -> "$name = ${alias.get()}"
-            else -> name
+    override fun compareTo(other: Term): Int {
+        return when (other) {
+            is Variable  -> name.compareTo(other.name)
+            // Variables are always less than atoms
+            else         -> -1
         }
     }
 
-    override fun equals(other: Any?): Boolean {
-        return if (alias.isPresent) {
-            alias.get() == other
-        } else {
-            name == other.toString()
+    override fun toString(): String {
+        return when {
+            alias.isPresent -> "$name: ${alias.get()}"
+            else -> name
         }
     }
 }

src/prolog/unify.kt

@@ -2,17 +2,18 @@ package prolog
 
 import prolog.builtins.atomic
 import prolog.builtins.compound
+import prolog.builtins.equivalent
 import prolog.builtins.variable
 import prolog.components.terms.Term
 import prolog.components.terms.Variable
 import prolog.components.terms.Structure
 import java.util.*
 
-typealias Substitution = Map<Variable, Term>
+typealias Substituted = Map<Variable, Term>
 
 // Apply substitutions to a term
-private fun applySubstitution(term: Term, substitution: Substitution): Term = when {
-    variable(term) -> (term as Variable).alias().map { applySubstitution(it, substitution) }.orElse(term)
+private fun applySubstitution(term: Term, substitution: Substituted): Term = when {
+    variable(term) -> substitution[(term as Variable)] ?: term
     atomic(term)   -> term
     compound(term) -> {
         val structure = term as Structure
@@ -33,33 +34,31 @@ private fun occurs(variable: Variable, term: Term): Boolean = when {
 }
 
 // Generate possible substitutions
-private fun generateSubstitutions(term1: Term, term2: Term, substitution: Substitution): Sequence<Substitution> = sequence {
-    val t1 = applySubstitution(term1, substitution)
-    val t2 = applySubstitution(term2, substitution)
+private fun generateSubstitutions(term1: Term, term2: Term, subs: Substituted): Sequence<Substituted> = sequence {
+    val t1 = applySubstitution(term1, subs)
+    val t2 = applySubstitution(term2, subs)
 
     when {
-        t1 == t2      -> yield(substitution)
+        equivalent(t1, t2) -> yield(subs)
         variable(t1) -> {
             val variable = t1 as Variable
             if (!occurs(variable, t2)) {
-//                variable.bind(t2)
-                yield(substitution + (variable to t2))
-//                variable.unbind()
+                variable.bind(t2)
+                yield(subs + (variable to t2))
             }
         }
         variable(t2) -> {
             val variable = t2 as Variable
             if (!occurs(variable, t1)) {
-//                variable.bind(t1)
-                yield(substitution + (variable to t1))
-//                variable.unbind()
+                variable.bind(t1)
+                yield(subs + (variable to t1))
             }
         }
         compound(t1) && compound(t2) -> {
             val structure1 = t1 as Structure
             val structure2 = t2 as Structure
             if (structure1.functor == structure2.functor) {
-                val newSubstitution = structure1.arguments.zip(structure2.arguments).fold(substitution) { acc, (arg1, arg2) ->
+                val newSubstitution = structure1.arguments.zip(structure2.arguments).fold(subs) { acc, (arg1, arg2) ->
                     generateSubstitutions(arg1, arg2, acc).firstOrNull() ?: return@sequence
                 }
                 yield(newSubstitution)
@@ -70,15 +69,15 @@ private fun generateSubstitutions(term1: Term, term2: Term, substitution: Substi
 }
 
 // Unify two terms with backtracking and lazy evaluation
-fun unifyLazy(term1: Term, term2: Term, substitution: Substitution = emptyMap()): Sequence<Substitution> = sequence {
-    generateSubstitutions(term1, term2, substitution).forEach { newSubstitution ->
+fun unifyLazy(term1: Term, term2: Term, subs: Substituted): Sequence<Substituted> = sequence {
+    generateSubstitutions(term1, term2, subs).forEach { newSubs ->
         // Return the new substitution
-        yield(newSubstitution)
+        yield(newSubs)
     }
 }
 
-fun unify(term1: Term, term2: Term): Optional<Substitution> {
-    val substitutions = unifyLazy(term1, term2).toList()
+fun unify(term1: Term, term2: Term): Optional<Substituted> {
+    val substitutions = unifyLazy(term1, term2, emptyMap()).toList()
     return if (substitutions.isNotEmpty()) {
         Optional.of(substitutions.first())
     } else {