refactor: Rework

src/prolog/Program.kt

@@ -1,6 +1,5 @@
 package prolog
 
-import prolog.logic.Substituted
 import prolog.ast.logic.Clause
 import prolog.ast.logic.Predicate
 import prolog.ast.logic.Resolvent
@@ -29,9 +28,9 @@ object Program: Resolvent {
      * Queries the program with a goal.
      * @return true if the goal can be proven, false otherwise.
      */
-    fun query(goal: Goal): Sequence<Substituted> = solve(goal, emptyMap())
+    fun query(goal: Goal): Answers = solve(goal, emptyMap())
 
-    override fun solve(goal: Goal, subs: Substituted): Sequence<Substituted> {
+    override fun solve(goal: Goal, subs: Substitutions): Answers {
         val functor = goal.functor
         // If the predicate does not exist, return false
         val predicate = predicates[functor] ?: return emptySequence()

src/prolog/Substitution.kt

@@ -0,0 +1,11 @@
+package prolog
+
+import prolog.ast.terms.Term
+
+abstract class Substitution(val from: Term, val to: Term) {
+    val mapped: Pair<Term, Term>? = if (from != to) from to to else null
+    override fun toString(): String = "$from -> $to"
+}
+typealias Substitutions = Map<Term, Term>
+typealias Answer = Result<Substitutions>
+typealias Answers = Sequence<Answer>

src/prolog/ast/arithmetic/ArithmeticOperator.kt

@@ -2,11 +2,6 @@ package prolog.ast.arithmetic
 
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Operator
-import prolog.ast.terms.Term
-import prolog.logic.Substituted
 
 abstract class ArithmeticOperator(symbol: Atom, leftOperand: Expression, rightOperand: Expression) :
-    Operator(symbol, leftOperand, rightOperand), Expression {
-    // Operators should overload the evaluate method to perform the operation
-    abstract override fun evaluate(subs: Substituted): Pair<Term, Substituted>
-}
+    Operator(symbol, leftOperand, rightOperand), Expression

src/prolog/ast/arithmetic/Expression.kt

@@ -1,5 +1,11 @@
 package prolog.ast.arithmetic
 
+import prolog.Substitutions
 import prolog.ast.terms.Term
 
-interface Expression : Term
+interface Expression : Term {
+    /**
+     * Returns the term that this expression evaluates to. (All the way down.)
+     */
+    fun simplify(subs: Substitutions): Simplification
+}

src/prolog/ast/arithmetic/Simplification.kt

@@ -0,0 +1,6 @@
+package prolog.ast.arithmetic
+
+import prolog.Substitution
+import prolog.ast.terms.Term
+
+class Simplification(from: Expression, to: Term) : Substitution(from, to)

src/prolog/ast/logic/Clause.kt

@@ -1,6 +1,7 @@
 package prolog.ast.logic
 
-import prolog.logic.Substituted
+import prolog.Answers
+import prolog.Substitutions
 import prolog.ast.terms.Body
 import prolog.ast.terms.Functor
 import prolog.ast.terms.Goal
@@ -19,26 +20,26 @@ import prolog.logic.unifyLazy
 abstract class Clause(private val head: Head, private val body: Body) : Resolvent {
     val functor: Functor = head.functor
 
-    override fun solve(goal: Goal, subs: Substituted): Sequence<Substituted> = sequence {
+    override fun solve (goal: Goal, subs: Substitutions): Answers = 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() }
+        unifyLazy(goal, head, subs).forEach { headAnswer ->
+            headAnswer.map { newHeadSubs ->
+                // If the body can be proven, yield the (combined) substitutions
+                body.satisfy(subs + newHeadSubs).forEach { bodyAnswer ->
+                    bodyAnswer.map { newBodySubs ->
+                        yield(Result.success(newHeadSubs + newBodySubs))
+                    }
+                }
             }
-            // Unbind the newly bound variables, so they can be reused.
-            newHeadSubs.keys.forEach { it.unbind() }
         }
     }
 
     override fun toString(): String {
         return when {
             body is True -> head.toString()
-            else         -> "$head :- $body"
+            else -> "$head :- $body"
         }
     }
 }

src/prolog/ast/logic/LogicOperand.kt

@@ -2,4 +2,4 @@ package prolog.ast.logic
 
 import prolog.ast.terms.Operand
 
-abstract class LogicOperand : Operand, Provable
+abstract class LogicOperand : Operand, Satisfiable

src/prolog/ast/logic/LogicOperator.kt

@@ -1,13 +1,14 @@
 package prolog.ast.logic
 
+import prolog.Answers
+import prolog.Substitutions
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Operator
-import prolog.logic.Substituted
 
 abstract class LogicOperator(
     symbol: Atom,
     leftOperand: LogicOperand? = null,
     rightOperand: LogicOperand
-) : Operator(symbol, leftOperand, rightOperand), Provable {
-    abstract override fun prove(subs: Substituted): Sequence<Substituted>
+) : Operator(symbol, leftOperand, rightOperand), Satisfiable {
+    abstract override fun satisfy(subs: Substitutions): Answers
 }

src/prolog/ast/logic/Predicate.kt

@@ -1,6 +1,7 @@
 package prolog.ast.logic
 
-import prolog.logic.Substituted
+import prolog.Answers
+import prolog.Substitutions
 import prolog.ast.terms.Functor
 import prolog.ast.terms.Goal
 
@@ -48,7 +49,7 @@ class Predicate : Resolvent {
         this.clauses.addAll(clauses)
     }
 
-    override fun solve(goal: Goal, subs: Substituted): Sequence<Substituted> = sequence {
+    override fun solve(goal: Goal, subs: Substitutions): Answers = sequence {
         require(goal.functor == functor) { "Goal functor does not match predicate functor" }
         // Try to unify the goal with the clause
         // If the unification is successful, yield the substitutions

src/prolog/ast/logic/Provable.kt

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

src/prolog/ast/logic/Resolvent.kt

@@ -1,6 +1,7 @@
 package prolog.ast.logic
 
-import prolog.logic.Substituted
+import prolog.Answers
+import prolog.Substitutions
 import prolog.ast.terms.Goal
 
 /**
@@ -13,5 +14,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, subs: Substituted): Sequence<Substituted>
+    fun solve(goal: Goal, subs: Substitutions): Answers
 }

src/prolog/ast/logic/Satisfiable.kt

@@ -0,0 +1,14 @@
+package prolog.ast.logic
+
+import prolog.Answers
+import prolog.Substitutions
+
+interface Satisfiable {
+    /**
+     * Proves the current [Satisfiable] instance.
+     *
+     * @return a sequence of [Substitutions] instances representing the results of the proof.
+     * If the proof fails, an empty sequence is returned.
+     */
+    fun satisfy(subs: Substitutions): Answers
+}

src/prolog/ast/terms/Atom.kt

@@ -1,27 +1,14 @@
 package prolog.ast.terms
 
+import prolog.Answers
+import prolog.Substitutions
 import prolog.ast.logic.Resolvent
-import prolog.logic.Substituted
 import prolog.logic.unifyLazy
 
 open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
     override val functor: Functor = "$name/_"
 
-    override fun solve(goal: Goal, subs: Substituted): Sequence<Substituted> = unifyLazy(goal, this, subs)
-
-    override fun evaluate(subs: Substituted): Pair<Term, Substituted> = Pair(this, emptyMap())
-
-    /**
-     * See also [SWI Prolog Standard Order of Terms](https://www.swi-prolog.org/pldoc/man?section=standardorder)
-     */
-    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 solve(goal: Goal, subs: Substitutions): Answers = unifyLazy(goal, this, subs)
 
     override fun toString(): String {
         return name

src/prolog/ast/terms/Body.kt

@@ -1,5 +1,5 @@
 package prolog.ast.terms
 
-import prolog.ast.logic.Provable
+import prolog.ast.logic.Satisfiable
 
-interface Body : Provable
+interface Body : Satisfiable

src/prolog/ast/terms/Goal.kt

@@ -1,8 +1,9 @@
 package prolog.ast.terms
 
+import prolog.Answers
 import prolog.Program
+import prolog.Substitutions
 import prolog.ast.logic.LogicOperand
-import prolog.logic.Substituted
 
 /**
  * Ask the Prolog engine.
@@ -14,5 +15,5 @@ import prolog.logic.Substituted
 abstract class Goal : LogicOperand(), Term {
     abstract val functor: Functor
 
-    override fun prove(subs: Substituted): Sequence<Substituted> = Program.solve(this, subs)
+    override fun satisfy(subs: Substitutions): Answers = Program.solve(this, subs)
 }

src/prolog/ast/terms/Integer.kt

@@ -1,22 +1,12 @@
 package prolog.ast.terms
 
+import prolog.Substitutions
 import prolog.ast.arithmetic.Expression
-import prolog.logic.Substituted
-
-data class Integer(val value: Int): Term, Expression {
-    /**
-     * See also [SWI Prolog Standard Order of Terms](https://www.swi-prolog.org/pldoc/man?section=standardorder)
-     */
-    override fun compareTo(other: Term): Int {
-        return when (other) {
-            is Variable -> 1
-            is Integer -> value.compareTo(other.value)
-            else -> -1
-        }
-    }
+import prolog.ast.arithmetic.Simplification
 
+data class Integer(val value: Int): Expression {
     // Integers are already evaluated
-    override fun evaluate(subs: Substituted): Pair<Term, Substituted> = Pair(this, emptyMap())
+    override fun simplify(subs: Substitutions): Simplification = Simplification(this, this)
 
     override fun toString(): String {
         return value.toString()

src/prolog/ast/terms/Operator.kt

@@ -1,5 +1,7 @@
 package prolog.ast.terms
 
+import prolog.ast.arithmetic.Expression
+
 typealias Operand = Term
 
 abstract class Operator(

src/prolog/ast/terms/Structure.kt

@@ -1,8 +1,8 @@
 package prolog.ast.terms
 
+import prolog.Answers
+import prolog.Substitutions
 import prolog.ast.logic.Resolvent
-import prolog.logic.equivalent
-import prolog.logic.Substituted
 import prolog.logic.unifyLazy
 
 typealias Argument = Term
@@ -12,34 +12,10 @@ typealias CompoundTerm = Structure
 open class Structure(val name: Atom, var arguments: List<Argument>) : Goal(), Head, Body, Resolvent {
     override val functor: Functor = "${name.name}/${arguments.size}"
 
-    override fun solve(goal: Goal, subs: Substituted): Sequence<Substituted> {
+    override fun solve(goal: Goal, subs: Substitutions): Answers {
         return unifyLazy(goal, this, subs)
     }
 
-    // A structure does not need to be evaluated, so return an empty sequence.
-    override fun evaluate(subs: Substituted): Pair<Term, Substituted> = Pair(this, emptyMap())
-
-    /**
-     * See also [SWI Prolog Standard Order of Terms](https://www.swi-prolog.org/pldoc/man?section=standardorder)
-     */
-    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 {
         return when {
             arguments.isEmpty() -> name.name

src/prolog/ast/terms/Term.kt

@@ -1,16 +1,13 @@
 package prolog.ast.terms
 
-import prolog.logic.Substituted
+import prolog.logic.compare
 
 /**
  * Value in Prolog.
  *
- * A [Term] is either a [Variable], [Atom], integer, float or [CompoundTerm].
+ * A [Term] is either a [Variable], [Atom], [Integer], float or [CompoundTerm].
  * In addition, SWI-Prolog also defines the type string.
  */
 interface Term : Comparable<Term> {
-    /**
-     * Returns the term that this expression evaluates to. (All the way down.)
-     */
-    fun evaluate(subs: Substituted): Pair<Term, Substituted>
+    override fun compareTo(other: Term): Int = compare(this, other, emptyMap())
 }

src/prolog/ast/terms/Variable.kt

@@ -1,50 +1,20 @@
 package prolog.ast.terms
 
+import prolog.Substitutions
 import prolog.ast.arithmetic.Expression
-import prolog.logic.Substituted
-import java.util.*
+import prolog.ast.arithmetic.Simplification
 
 data class Variable(val name: String) : Term, Expression {
-    private var alias: Optional<Term> = Optional.empty()
-
-    fun alias(): Optional<Term> {
-        return alias
-    }
-
-    fun bind(term: Term): Optional<Term> {
-        if (alias.isEmpty) {
-            alias = Optional.of(term)
-        }
-
-        return alias
-    }
-
-    fun unbind() {
-        alias = Optional.empty()
-    }
-
-    override fun evaluate(subs: Substituted): Pair<Term, Substituted> {
+    override fun simplify(subs: Substitutions): Simplification {
         // If the variable is bound, return the value of the binding
         // If the variable is not bound, return the variable itself
-        return if (alias.isPresent) {
-            alias.get().evaluate(subs)
-        } else {
-            Pair(this, emptyMap())
+        var result = this as Term
+        if (this in subs) {
+            val boundTerm = subs[this]!!
+            result = if (boundTerm is Expression) boundTerm.simplify(subs).to else boundTerm
         }
+        return Simplification(this, result)
     }
 
-    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 toString(): String {
-        return when {
-            alias.isPresent -> "$name: ${alias.get()}"
-            else -> name
-        }
-    }
+    override fun toString(): String = name
 }

src/prolog/ast/terms/VariableBinding.kt

@@ -0,0 +1,5 @@
+package prolog.ast.terms
+
+import prolog.Substitution
+
+class VariableBinding(from: Variable, to: Term) : Substitution(from, to)

src/prolog/builtins/arithmeticOperators.kt

@@ -1,10 +1,11 @@
 package prolog.builtins
 
+import prolog.Answers
+import prolog.Substitutions
 import prolog.ast.arithmetic.ArithmeticOperator
 import prolog.ast.arithmetic.Expression
-import prolog.ast.logic.LogicOperand
-import prolog.ast.logic.LogicOperator
-import prolog.ast.logic.Provable
+import prolog.ast.arithmetic.Simplification
+import prolog.ast.logic.Satisfiable
 import prolog.ast.terms.*
 import prolog.logic.*
 
@@ -20,20 +21,20 @@ import prolog.logic.*
  * True if expression Expr1 evaluates to a number non-equal to Expr2.
  */
 class EvaluatesToDifferent(private val left: Expression, private val right: Expression) :
-    ArithmeticOperator(Atom("=\\="), left, right) {
-    override fun evaluate(subs: Substituted): Pair<Term, Substituted> {
-        val t1 = left.evaluate(subs)
-        val t2 = right.evaluate(subs)
+    Operator(Atom("=\\="), left, right), Satisfiable {
+    override fun satisfy(subs: Substitutions): Answers {
+        val t1 = left.simplify(subs)
+        val t2 = right.simplify(subs)
 
         // Should both be instantiated
-        if (!atomic(t1.first) || !atomic(t2.first)) {
-            throw IllegalArgumentException("Both operands must be instantiated")
+        if (!atomic(t1.to, subs) || !atomic(t2.to, subs)) {
+            return sequenceOf(Result.failure(IllegalArgumentException("Both operands must be instantiated")))
         }
 
-        return if (equivalent(t1.first, t2.first)) {
-            Pair(False, emptyMap())
+        return if (equivalent(t1.to, t2.to, subs)) {
+            emptySequence()
         } else {
-            Pair(True, t1.second + t2.second)
+            sequenceOf(Result.success(emptyMap()))
         }
     }
 
@@ -43,21 +44,17 @@ class EvaluatesToDifferent(private val left: Expression, private val right: Expr
  * True if Expr1 evaluates to a number equal to Expr2.
  */
 class EvaluatesTo(private val left: Expression, private val right: Expression) :
-    ArithmeticOperator(Atom("=:="), left, right) {
-    override fun evaluate(subs: Substituted): Pair<Term, Substituted> {
-        val t1 = left.evaluate(subs)
-        val t2 = right.evaluate(subs)
+    Operator(Atom("=:="), left, right) {
+    override fun satisfy(subs: Substitutions): Answers {
+        val t1 = left.simplify(subs)
+        val t2 = right.simplify(subs)
 
         // Should both be instantiated
-        if (!atomic(t1.first) || !atomic(t2.first)) {
-            throw IllegalArgumentException("Both operands must be instantiated")
+        if (!atomic(t1.to, subs) || !atomic(t2.to, subs)) {
+            return sequenceOf(Result.failure(IllegalArgumentException("Both operands must be instantiated")))
         }
 
-        return if (equivalent(t1.first, t2.first)) {
-            Pair(True, t1.second + t2.second)
-        } else {
-            Pair(False, emptyMap())
-        }
+        return if (equivalent(t1.to, t2.to, subs)) sequenceOf(Result.success(emptyMap())) else emptySequence()
     }
 }
 
@@ -65,16 +62,20 @@ class EvaluatesTo(private val left: Expression, private val right: Expression) :
  * True when Number is the value to which Expr evaluates.
  */
 class Is(private val left: Expression, private val right: Expression) :
-    Operator(Atom("is"), left, right), Provable {
-    override fun prove(subs: Substituted): Sequence<Substituted> {
-        val t1 = left.evaluate(subs)
-        val t2 = right.evaluate(subs)
+    Operator(Atom("is"), left, right), Satisfiable {
+    override fun satisfy(subs: Substitutions): Answers {
+        val t1 = left.simplify(subs)
+        val t2 = right.simplify(subs)
 
-        if (!atomic(t2.first)) {
-            throw IllegalArgumentException("Arguments are not sufficiently instantiated")
+        if (!atomic(t2.to, subs)) {
+            return sequenceOf(Result.failure(IllegalArgumentException("Right operand must be instantiated")))
         }
 
-        return unifyLazy(t1.first, t2.first, subs).map{ it + t1.second + t2.second }
+        if (!variable(t1.to, subs) && equivalent(t1.to, t2.to, subs + listOfNotNull(t1.mapped, t2.mapped))) {
+            return sequenceOf(Result.success(emptyMap()))
+        }
+
+        return unifyLazy(t1.to, t2.to, subs)
     }
 }
 
@@ -93,10 +94,11 @@ class Positive(operand: Expression) : Add(Integer(0), operand)
  */
 open class Add(private val expr1: Expression, private val expr2: Expression) :
     ArithmeticOperator(Atom("+"), expr1, expr2) {
-    override fun evaluate(subs: Substituted): Pair<Term, Substituted> {
+    override fun simplify(subs: Substitutions): Simplification {
         val result = Variable("Result")
         val map = plus(expr1, expr2, result, subs)
-        return result.evaluate(map.first().getOrThrow())
+        val simplification = result.simplify(map.first().getOrThrow())
+        return Simplification(this, simplification.to)
     }
 }
 
@@ -105,10 +107,11 @@ open class Add(private val expr1: Expression, private val expr2: Expression) :
  */
 open class Subtract(private val expr1: Expression, private val expr2: Expression) :
     ArithmeticOperator(Atom("-"), expr1, expr2) {
-    override fun evaluate(subs: Substituted): Pair<Term, Substituted> {
+    override fun simplify(subs: Substitutions): Simplification {
         val result = Variable("Result")
         val map = plus(expr2, result, expr1, subs)
-        return result.evaluate(map.first().getOrThrow())
+        val simplification = result.simplify(map.first().getOrThrow())
+        return Simplification(this, simplification.to)
     }
 }
 
@@ -118,10 +121,11 @@ open class Subtract(private val expr1: Expression, private val expr2: Expression
  */
 class Multiply(private val expr1: Expression, private val expr2: Expression) :
     ArithmeticOperator(Atom("*"), expr1, expr2) {
-    override fun evaluate(subs: Substituted): Pair<Term, Substituted> {
+    override fun simplify(subs: Substitutions): Simplification {
         val result = Variable("Result")
         val map = mul(expr1, expr2, result, subs)
-        return result.evaluate(map.first().getOrThrow())
+        val simplification = result.simplify(map.first().getOrThrow())
+        return Simplification(this, simplification.to)
     }
 }
 
@@ -133,20 +137,24 @@ class Multiply(private val expr1: Expression, private val expr2: Expression) :
 
 class Between(private val expr1: Expression, private val expr2: Expression, private val expr3: Expression) :
     Operator(Atom("between"), expr1, expr2) {
-    override fun prove(subs: Substituted): Sequence<Substituted> {
-        val e1 = expr1.evaluate(subs)
-        val e2 = expr2.evaluate(subs)
-        val e3 = expr3.evaluate(subs)
+    override fun satisfy(subs: Substitutions): Answers {
+        val e1 = expr1.simplify(subs)
+        val e2 = expr2.simplify(subs)
+        val e3 = expr3.simplify(subs)
 
-        require(e1.first is Integer && e2.first is Integer) { "Arguments must be integers" }
+        require(e1.to is Integer && e2.to is Integer) { "Arguments must be integers" }
 
-        val v1 = e1.first as Integer
-        val v2 = e2.first as Integer
+        val v1 = e1.to as Integer
+        val v2 = e2.to as Integer
 
-        return if (variable(e3.first)) {
-            between(v1, v2, e3.first as Variable).map { it + e1.second + e2.second }
+        return if (variable(e3.to, subs)) {
+            between(v1, v2, e3.to as Variable).map { answer ->
+                answer.mapCatching { it + listOfNotNull(e1.mapped, e2.mapped) }
+            }
         } else {
-            between(v1, v2, e3.first as Integer).map { it + e1.second + e2.second }
+            between(v1, v2, e3.to as Integer).map { answer ->
+                answer.mapCatching { it + listOfNotNull(e1.mapped, e2.mapped) }
+            }
         }
     }
 }

src/prolog/builtins/controlOperators.kt

@@ -1,17 +1,18 @@
 package prolog.builtins
 
+import prolog.Answers
+import prolog.Substitutions
 import prolog.ast.logic.LogicOperand
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Body
 import prolog.ast.terms.Goal
 import prolog.ast.logic.LogicOperator
-import prolog.logic.Substituted
 
 /**
  * Always fail.
  */
 object Fail : Atom("fail"), Body {
-    override fun prove(subs: Substituted): Sequence<Substituted> = emptySequence()
+    override fun satisfy(subs: Substitutions): Answers = emptySequence()
 }
 
 /**
@@ -23,7 +24,7 @@ typealias False = Fail
  * Always succeed.
  */
 object True : Atom("true"), Body {
-    override fun prove(subs: Substituted): Sequence<Substituted> = sequenceOf(emptyMap())
+    override fun satisfy(subs: Substitutions): Answers = sequenceOf(Result.success(emptyMap()))
 }
 
 // TODO Repeat/0
@@ -34,10 +35,14 @@ object True : Atom("true"), Body {
  * Conjunction (and). True if both Goal1 and Goal2 are true.
  */
 class Conjunction(private val left: LogicOperand, private val right: LogicOperand) : LogicOperator(Atom(","), left, right) {
-    override fun prove(subs: Substituted): Sequence<Substituted> = sequence {
-        left.prove(subs).forEach { left ->
-            right.prove(subs + left).forEach { right ->
-                yield(left + right)
+    override fun satisfy(subs: Substitutions): Answers = sequence {
+        left.satisfy(subs).forEach { leftResult ->
+            leftResult.mapCatching { left ->
+                right.satisfy(subs + left).forEach { rightResult ->
+                    rightResult.map { right ->
+                        yield(Result.success(left + right))
+                    }
+                }
             }
         }
     }
@@ -48,9 +53,9 @@ class Conjunction(private val left: LogicOperand, private val right: LogicOperan
  */
 open class Disjunction(private val left: LogicOperand, private val right: LogicOperand) :
     LogicOperator(Atom(";"), left, right) {
-    override fun prove(subs: Substituted): Sequence<Substituted> = sequence {
-        yieldAll(left.prove(subs))
-        yieldAll(right.prove(subs))
+    override fun satisfy(subs: Substitutions): Answers = sequence {
+        yieldAll(left.satisfy(subs))
+        yieldAll(right.satisfy(subs))
     }
 }
 
@@ -65,12 +70,12 @@ class Bar(leftOperand: LogicOperand, rightOperand: LogicOperand) : Disjunction(l
  * True if 'Goal' cannot be proven.
  */
 class Not(private val goal: Goal) : LogicOperator(Atom("\\+"), rightOperand = goal) {
-    override fun prove(subs: Substituted): Sequence<Substituted> {
+    override fun satisfy(subs: Substitutions): Answers {
         // If the goal can be proven, return an empty sequence
-        if (goal.prove(subs).toList().isNotEmpty()) {
+        if (goal.satisfy(subs).toList().isNotEmpty()) {
             return emptySequence()
         }
         // If the goal cannot be proven, return a sequence with an empty map
-        return sequenceOf(emptyMap())
+        return sequenceOf(Result.success(emptyMap()))
     }
 }

src/prolog/builtins/other.kt

@@ -1,10 +1,11 @@
 package prolog.builtins
 
+import prolog.Answers
+import prolog.Substitutions
 import prolog.ast.logic.LogicOperand
 import prolog.ast.terms.Atom
 import prolog.ast.logic.LogicOperator
-import prolog.logic.Substituted
 
 class Query(private val query: LogicOperand) : LogicOperator(Atom("?-"), null, query) {
-    override fun prove(subs: Substituted): Sequence<Substituted> = query.prove(subs)
+    override fun satisfy(subs: Substitutions): Answers = query.satisfy(subs)
 }

src/prolog/builtins/unificationOperators.kt

@@ -5,20 +5,21 @@
  */
 package prolog.builtins
 
+import prolog.Answers
+import prolog.Substitutions
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Operator
 import prolog.ast.terms.Term
-import prolog.logic.Substituted
 import prolog.logic.applySubstitution
 import prolog.logic.equivalent
 
 class Equivalent(private val term1: Term, private val term2: Term) : Operator(Atom("=="), term1, term2) {
-    override fun prove(subs: Substituted): Sequence<Substituted> = sequence {
+    override fun satisfy(subs: Substitutions): Answers = sequence {
         val t1 = applySubstitution(term1, subs)
         val t2 = applySubstitution(term2, subs)
 
-        if (equivalent(t1, t2)) {
-            yield(emptyMap())
+        if (equivalent(t1, t2, subs)) {
+            yield(Result.success(emptyMap()))
         }
     }
 }

src/prolog/logic/arithmetic.kt

@@ -1,10 +1,12 @@
 package prolog.logic
 
+import prolog.Answers
+import prolog.Substitution
+import prolog.Substitutions
 import prolog.ast.arithmetic.Expression
 import prolog.ast.terms.Integer
+import prolog.ast.terms.Term
 import prolog.ast.terms.Variable
-import prolog.builtins.Is
-import java.util.*
 
 /**
  * Low and High are integers, High ≥Low.
@@ -18,9 +20,9 @@ fun between(
     low: Integer,
     high: Integer,
     value: Integer
-): Sequence<Substituted> {
+): Answers {
     return if (value.value in low.value..high.value) {
-        sequenceOf(emptyMap())
+        sequenceOf(Result.success(emptyMap()))
     } else {
         emptySequence()
     }
@@ -30,10 +32,10 @@ fun between(
     low: Integer,
     high: Integer,
     variable: Variable
-): Sequence<Substituted> {
+): Answers {
     return sequence {
         for (i in low.value..high.value) {
-            yield(mapOf(variable to Integer(i)))
+            yield(Result.success(mapOf(variable to Integer(i))))
         }
     }
 }
@@ -46,24 +48,26 @@ fun between(
  * @throws IllegalArgumentException the domain error not_less_than_zero if called with a negative integer.
  * E.g. succ(X, 0) fails silently and succ(X, -1) raises a domain error.125
  */
-fun succ(term1: Expression, term2: Expression, subs: Substituted): Sequence<Result<Substituted>> {
+fun succ(term1: Expression, term2: Expression, subs: Substitutions): Answers {
     if (term2 is Integer) {
         require(term2.value >= 0) { "Domain error: not_less_than_zero" }
     }
-    val result = plus(term1, Integer(1), term2, subs)
     // If term1 is a variable, we need to check if it is bound to a negative integer
     return sequence {
-        result.forEach { newSubs ->
-            if (newSubs.isSuccess) {
-                val t1 = applySubstitution(term1, newSubs.getOrNull()!!)
-                if (t1 is Variable && t1.alias().isPresent) {
-                    val e1 = t1.evaluate(subs)
-                    if (e1.first is Integer && (e1.first as Integer).value < 0) {
-                        return@sequence
+        plus(term1, Integer(1), term2, subs).forEach {
+            it.fold(
+                onSuccess = { result ->
+                    val t1 = applySubstitution(term1, result)
+                    if (t1 in result) {
+                        val e1 = t1.simplify(result)
+                        if (e1.to is Integer && e1.to.value < 0) {
+                            return@sequence
+                        }
                     }
-                }
-            }
-            yield(newSubs)
+                    yield(Result.success(result))
+                },
+                onFailure = { yield(Result.success(emptyMap())) }
+            )
         }
     }
 }
@@ -73,55 +77,56 @@ fun succ(term1: Expression, term2: Expression, subs: Substituted): Sequence<Resu
  *
  * At least two of the three arguments must be instantiated to integers.
  */
-fun plus(term1: Expression, term2: Expression, term3: Expression, subs: Substituted): Sequence<Result<Substituted>> =
+fun plus(term1: Expression, term2: Expression, term3: Expression, subs: Substitutions): Answers =
     operate(term1, term2, term3, subs, Integer::plus, Integer::minus)
 
-fun mul(term1: Expression, term2: Expression, term3: Expression, subs: Substituted): Sequence<Result<Substituted>> =
+fun mul(term1: Expression, term2: Expression, term3: Expression, subs: Substitutions): Answers =
     operate(term1, term2, term3, subs, Integer::times, Integer::div)
 
 fun operate(
     term1: Expression,
     term2: Expression,
     term3: Expression,
-    subs: Substituted,
+    subs: Substitutions,
     op: (Integer, Integer) -> Integer,
     inverseOp: (Integer, Integer) -> Integer
-): Sequence<Result<Substituted>> = sequence {
+): Answers = sequence {
     val t1 = applySubstitution(term1, subs)
     val t2 = applySubstitution(term2, subs)
     val t3 = applySubstitution(term3, subs)
 
     when {
-        nonvariable(t1) && nonvariable(t2) && nonvariable(t3) -> {
-            val e1 = t1.evaluate(subs)
-            val e2 = t2.evaluate(subs)
-            val e3 = t3.evaluate(subs)
+        nonvariable(t1, subs) && nonvariable(t2, subs) && nonvariable(t3, subs) -> {
+            val e1 = t1.simplify(subs)
+            val e2 = t2.simplify(subs)
+            val e3 = t3.simplify(subs)
 
-            val int3Value = op(e1.first as Integer, e2.first as Integer)
-            if (int3Value == e3.first as Integer) {
-                yield(Result.success(e1.second + e2.second + e3.second))
+            val int3Value = op(e1.to as Integer, e2.to as Integer)
+            if (int3Value == e3.to as Integer) {
+                val opSubs: Substitutions = listOfNotNull(e1.mapped, e2.mapped, e3.mapped)
+                    .filter{ pair: Pair<Term, Term>? -> pair != null && !subs.contains(pair.first) }
+                    .toMap()
+                yield(Result.success(opSubs))
             }
         }
 
-        nonvariable(t1) && nonvariable(t2) && variable(t3) -> {
-            val e1 = t1.evaluate(subs)
-            val e2 = t2.evaluate(subs)
+        nonvariable(t1, subs) && nonvariable(t2, subs) && variable(t3, subs) -> {
+            val e1 = t1.simplify(subs)
+            val e2 = t2.simplify(subs)
 
-            val int3Value = op(e1.first as Integer, e2.first as Integer)
+            val int3Value = op(e1.to as Integer, e2.to as Integer)
             val int3 = t3 as Variable
-            int3.bind(int3Value)
-            yield(Result.success(mapOf(int3 to int3Value) + e1.second + e2.second))
+            yield(Result.success(mapOf(int3 to int3Value) + listOfNotNull(e1.mapped, e2.mapped)))
         }
 
-        ((nonvariable(t1) && variable(t2)) || (variable(t1) && nonvariable(t2))) && nonvariable(t3) -> {
-            val t = if (nonvariable(t1)) t2 else t1
-            val e = if (nonvariable(t1)) t1.evaluate(subs) else t2.evaluate(subs)
-            val e3 = t3.evaluate(subs)
+        ((nonvariable(t1, subs) && variable(t2, subs)) || (variable(t1, subs) && nonvariable(t2, subs))) && nonvariable(t3, subs) -> {
+            val t = if (nonvariable(t1, subs)) t2 else t1
+            val e = if (nonvariable(t1, subs)) t1.simplify(subs) else t2.simplify(subs)
+            val e3 = t3.simplify(subs)
 
-            val value = inverseOp(e3.first as Integer, e.first as Integer)
+            val value = inverseOp(e3.to as Integer, e.to as Integer)
             val int = t as Variable
-            int.bind(value)
-            yield(Result.success(mapOf(int to value) + e.second + e3.second))
+            yield(Result.success(mapOf(int to value) + listOfNotNull(e.mapped, e3.mapped)))
         }
 
         else -> {

src/prolog/logic/unification.kt

@@ -1,26 +1,27 @@
 package prolog.logic
 
+import prolog.Answer
+import prolog.Answers
+import prolog.Substitutions
 import prolog.ast.arithmetic.Expression
 import prolog.ast.logic.LogicOperator
 import prolog.ast.terms.*
-import java.util.*
-
-typealias Substituted = Map<Variable, Term>
+import kotlin.NoSuchElementException
 
 // Apply substitutions to a term
-fun applySubstitution(term: Term, subs: Substituted): Term = when {
-    variable(term) -> subs[(term as Variable)] ?: term
-    atomic(term)   -> term
-    compound(term) -> {
+fun applySubstitution(term: Term, subs: Substitutions): Term = when {
+    variable(term, emptyMap()) -> subs[(term as Variable)] ?: term
+    atomic(term, subs)   -> term
+    compound(term, subs) -> {
         val structure = term as Structure
         Structure(structure.name, structure.arguments.map { applySubstitution(it, subs) })
     }
     else -> term
 }
-
-fun applySubstitution(expr: Expression, subs: Substituted): Expression = when {
-    variable(expr) -> applySubstitution(expr as Term, subs) as Expression
-    atomic(expr)   -> expr
+//TODO Combine with the other applySubstitution function
+fun applySubstitution(expr: Expression, subs: Substitutions): Expression = when {
+    variable(expr, subs) -> applySubstitution(expr as Term, subs) as Expression
+    atomic(expr, subs)   -> expr
     expr is LogicOperator -> {
         expr.arguments = expr.arguments.map { applySubstitution(it, subs) }
         expr
@@ -29,71 +30,138 @@ fun applySubstitution(expr: Expression, subs: Substituted): Expression = when {
 }
 
 // Check if a variable occurs in a term
-private fun occurs(variable: Variable, term: Term): Boolean = when {
-    variable(term) -> term == variable
-    atomic(term) -> false
-    compound(term) -> {
+private fun occurs(variable: Variable, term: Term, subs: Substitutions): Boolean = when {
+    variable(term, subs) -> term == variable
+    atomic(term, subs) -> false
+    compound(term, subs) -> {
         val structure = term as Structure
-        structure.arguments.any { occurs(variable, it) }
+        structure.arguments.any { occurs(variable, it, subs) }
     }
     else -> false
 }
 
 // Unify two terms with backtracking and lazy evaluation
-fun unifyLazy(term1: Term, term2: Term, subs: Substituted): Sequence<Substituted> = sequence {
+fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence {
     val t1 = applySubstitution(term1, subs)
     val t2 = applySubstitution(term2, subs)
 
     when {
-        equivalent(t1, t2) -> yield(subs)
-        variable(t1) -> {
+        equivalent(t1, t2, subs) -> yield(Result.success(subs))
+        variable(t1, subs) -> {
             val variable = t1 as Variable
-            if (!occurs(variable, t2)) {
-                variable.bind(t2)
-                yield(subs + (variable to t2))
+            if (!occurs(variable, t2, subs)) {
+                yield(Result.success(subs + (variable to t2)))
             }
         }
-        variable(t2) -> {
+        variable(t2, subs) -> {
             val variable = t2 as Variable
-            if (!occurs(variable, t1)) {
-                variable.bind(t1)
-                yield(subs + (variable to t1))
+            if (!occurs(variable, t1, subs)) {
+                yield(Result.success(subs + (variable to t1)))
             }
         }
-        compound(t1) && compound(t2) -> {
+        compound(t1, subs) && compound(t2, subs) -> {
             val structure1 = t1 as Structure
             val structure2 = t2 as Structure
             if (structure1.functor == structure2.functor) {
-                val newSubstitution = structure1.arguments.zip(structure2.arguments).fold(subs) { acc, (arg1, arg2) ->
-                    unifyLazy(arg1, arg2, acc).firstOrNull() ?: return@sequence
+                // Unify each argument at the same time, and yield the result
+                val args1 = structure1.arguments
+                val args2 = structure2.arguments
+                if (args1.size == args2.size) {
+                    val results = args1.zip(args2).map { (arg1, arg2) ->
+                        unifyLazy(arg1, arg2, subs)
+                    }
+                    // Combine the results of all unifications
+                    val combinedResults = results.reduce { acc, result ->
+                        acc.flatMap { a -> result.map { b ->
+                            if (a.isSuccess && b.isSuccess) a.getOrThrow() + b.getOrThrow() else emptyMap()
+                        } }.map { Result.success(it) }
+                    }
+                    yieldAll(combinedResults)
                 }
-                yield(newSubstitution)
             }
         }
         else -> {}
     }
 }
 
-fun unify(term1: Term, term2: Term): Optional<Substituted> {
+fun unify(term1: Term, term2: Term): Answer {
     val substitutions = unifyLazy(term1, term2, emptyMap()).toList()
     return if (substitutions.isNotEmpty()) {
-        Optional.of(substitutions.first())
+        substitutions.first()
     } else {
-        Optional.empty()
+        Result.failure(NoSuchElementException())
     }
 }
 
 /**
  * True if Term1 is equivalent to Term2. A variable is only identical to a sharing variable.
  */
-fun equivalent(term1: Term, term2: Term): Boolean {
+fun equivalent(term1: Term, term2: Term, subs: Substitutions): Boolean {
     return when {
-        term1 is Atom && term2 is Atom -> term1.compareTo(term2) == 0
-        term1 is Structure && term2 is Structure -> term1.compareTo(term2) == 0
-        term1 is Integer && term2 is Integer -> term1.compareTo(term2) == 0
+        term1 is Atom && term2 is Atom -> compare(term1, term2, subs) == 0
+        term1 is Structure && term2 is Structure -> compare(term1, term2, subs) == 0
+        term1 is Integer && term2 is Integer -> compare(term1, term2, subs) == 0
         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 Variable -> term1 in subs && equivalent(subs[term1]!!, term2, subs)
+        term2 is Variable -> term2 in subs && equivalent(subs[term2]!!, term1, subs)
         else -> false
     }
 }
+
+/**
+ * See also [SWI Prolog Standard Order of Terms](https://www.swi-prolog.org/pldoc/man?section=standardorder)
+ */
+fun compare(term1: Term, term2: Term, subs: Substitutions): Int {
+    val t1 = applySubstitution(term1, subs)
+    val t2 = applySubstitution(term2, subs)
+
+    return when (t1) {
+        is Variable -> {
+            when (t2) {
+                is Variable  -> t1.name.compareTo(t2.name)
+                is Integer   -> -1
+                is Atom      -> -1
+                is Structure -> -1
+                else -> throw IllegalArgumentException("Cannot compare $t1 with $t2")
+            }
+        }
+        is Integer -> {
+            when (t2) {
+                is Variable  -> 1
+                is Integer   -> t1.value.compareTo(t2.value)
+                is Atom      -> -1
+                is Structure -> -1
+                else -> throw IllegalArgumentException("Cannot compare $t1 with $t2")
+            }
+        }
+        is Atom -> {
+            when (t2) {
+                is Variable  -> 1
+                is Integer   -> 1
+                is Atom      -> t1.name.compareTo(t2.name)
+                is Structure -> -1
+                else -> throw IllegalArgumentException("Cannot compare $t1 with $t2")
+            }
+        }
+        is Structure -> {
+            when (t2) {
+                is Variable -> 1
+                is Integer  -> 1
+                is Atom     -> 1
+                is Structure -> {
+                    val arityComparison = t1.arguments.size.compareTo(t2.arguments.size)
+                    if (arityComparison != 0) return arityComparison
+                    val nameComparison = t1.name.compareTo(t2.name)
+                    if (nameComparison != 0) return nameComparison
+                    t1.arguments.zip(t2.arguments).forEach { (arg1, arg2) ->
+                        val argsComparison = equivalent(arg1, arg2, emptyMap())
+                        if (!argsComparison) return compare(arg1, arg2, subs)
+                    }
+                    return 0
+                }
+                else -> throw IllegalArgumentException("Cannot compare $t1 with $t2")
+            }
+        }
+        else -> throw IllegalArgumentException("Cannot compare $t1 with $t2")
+    }
+}

src/prolog/logic/verification.kt

@@ -1,5 +1,6 @@
 package prolog.logic
 
+import prolog.Substitutions
 import prolog.ast.terms.CompoundTerm
 import prolog.ast.terms.Term
 import prolog.ast.terms.Variable
@@ -12,29 +13,29 @@ import prolog.ast.terms.Variable
  *         nonvar(Term),
  *         \+ compound(Term).
  */
-fun atomic(term: Term): Boolean = nonvariable(term) && !compound(term)
+fun atomic(term: Term, subs: Substitutions = emptyMap()): Boolean = nonvariable(term, subs) && !compound(term, subs)
 
 /**
  * True if [Term] is bound to a compound term.
  * See also functor/3 =../2, compound_name_arity/3 and compound_name_arguments/3.
  */
-fun compound(term: Term): Boolean {
+fun compound(term: Term, subs: Substitutions = emptyMap()): Boolean {
     val isCompound = term is CompoundTerm
-    val isVariableCompound = term is Variable && term.alias().isPresent && compound(term.alias().get())
+    val isVariableCompound = term is Variable && term in subs && compound(subs[term]!!, subs)
     return isCompound || isVariableCompound
 }
 
 /**
  * True if [Term] currently is not a free variable.
  */
-fun nonvariable(term: Term): Boolean = !variable(term)
+fun nonvariable(term: Term, subs: Substitutions = emptyMap()): Boolean = !variable(term, subs)
 
 /**
  * True if [Term] currently is a free variable.
  */
-fun variable(term: Term): Boolean {
+fun variable(term: Term, subs: Substitutions = emptyMap()): Boolean {
     if (term is Variable) {
-        return term.alias().isEmpty || term.alias().get() === term || variable(term.alias().get())
+        return term !in subs || subs[term] === term || variable(subs[term]!!, subs)
     }
 
     return false