Checkpoint

src/prolog/Program.kt

@@ -48,4 +48,10 @@ object Program : Resolvent {
 
         correspondingDBs.forEach { it.clear() }
     }
+
+    fun reset() {
+        clear()
+        variableRenamingStart = 0
+        storeNewLine = false
+    }
 }

src/prolog/ast/arithmetic/Integer.kt

@@ -1,11 +1,15 @@
 package prolog.ast.arithmetic
 
+import prolog.Answers
 import prolog.Substitutions
+import prolog.ast.logic.LogicOperand
 
-data class Integer(override val value: Int) : Number {
+data class Integer(override val value: Int) : Number, LogicOperand() {
     // Integers are already evaluated
     override fun simplify(subs: Substitutions): Simplification = Simplification(this, this)
 
+    override fun satisfy(subs: Substitutions): Answers = sequenceOf(Result.success(emptyMap()))
+
     override fun toString(): String = value.toString()
 
     override operator fun plus(other: Number): Number = when (other) {

src/prolog/ast/logic/Clause.kt

@@ -8,6 +8,7 @@ import prolog.builtins.True
 import prolog.flags.AppliedCut
 import prolog.logic.applySubstitution
 import prolog.logic.numbervars
+import prolog.logic.occurs
 import prolog.logic.unifyLazy
 
 /**
@@ -46,7 +47,7 @@ abstract class Clause(val head: Head, val body: Body) : Resolvent {
                                 .mapValues { reverse[it.value] ?: it.value }
                             result = result.map { it.key to applySubstitution(it.value, result) }
                                 .toMap()
-                                .filterNot { it.key in renamed.keys }
+                                .filterNot { it.key in renamed.keys && !occurs(it.key as Variable, goal, emptyMap())}
                             yield(Result.success(result))
                         },
                         onFailure = { error ->

src/prolog/ast/terms/Variable.kt

@@ -4,8 +4,9 @@ import prolog.Answers
 import prolog.Substitutions
 import prolog.ast.arithmetic.Expression
 import prolog.ast.arithmetic.Simplification
+import prolog.ast.logic.LogicOperand
 
-data class Variable(val name: String) : Term, Body, Expression {
+data class Variable(val name: String) : Term, Body, Expression, LogicOperand() {
     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

src/prolog/builtins/io.kt

@@ -18,7 +18,12 @@ import prolog.logic.unifyLazy
  */
 class Write(private val term: Term) : Operator(Atom("write"), null, term), Satisfiable {
     override fun satisfy(subs: Substitutions): Answers {
-        val t = applySubstitution(term, subs)
+        var t = term
+        var temp = applySubstitution(t, subs)
+        while (t != temp) {
+            t = temp
+            temp = applySubstitution(t, subs)
+        }
 
         Terminal().say(t.toString())