Checkpoint

build.gradle.kts

@@ -28,20 +28,26 @@ sourceSets {
     }
 }
 
-tasks {
+tasks.named<Test>("test") {
-    withType<Jar> {
+    useJUnitPlatform()
-        manifest {
+    testLogging {
-            attributes["Main-Class"] = "MainKt"
+        events("passed", "skipped", "failed")
-        }
+    }
-        from(configurations.runtimeClasspath.get().map {
+}
-            if (it.isDirectory) it else zipTree(it)
+
-        })
+tasks.register<Jar>("fatJar") {
-    }
+    manifest {
-
+        attributes["Main-Class"] = "MainKt"
-    test {
+    }
-        useJUnitPlatform()
+    duplicatesStrategy = DuplicatesStrategy.EXCLUDE
-        testLogging {
+    from(configurations.runtimeClasspath.get().map {
-            events("passed", "skipped", "failed")
+        if (it.isDirectory) it else zipTree(it)
-        }
+    })
+    with(tasks.jar.get() as CopySpec)
+}
+
+tasks {
+    build {
+        dependsOn("fatJar")
     }
 }

examples/scratchpad.pl

@@ -1 +1,23 @@
-choice(X) :- X = 1, !; X = 2.
+% choice(X) :- X = 1, !; X = 2.
+grade(alice, a).
+grade(bob, b).
+grade(carol, a).
+grade(dave, c).
+
+got_an_a(Student) :-
+    grade(Student, Grade),
+    Grade = a.
+
+did_not_get_an_a(Student) :-
+    grade(Student, Grade),
+    Grade \= a.
+
+:- initialization(main).
+
+main :-
+    write("While "),
+    got_an_a(X),
+    write(X), write(" got an A, "), fail;
+    write("but "),
+    did_not_get_an_a(Y),
+    write(Y), write(" did not get an A, "), fail; write("unfortunately."), nl.

src/Main.kt

@@ -5,7 +5,7 @@ import io.GhentPrologArgParser
 import io.Logger
 import repl.Repl
 
-fun main(args: Array<String>) = mainBody {
+fun main(args: Array<String>) {
     // Parse command line arguments
     val parsedArgs = ArgParser(args).parseInto(::GhentPrologArgParser)
 
@@ -22,21 +22,9 @@ fun main(args: Array<String>) = mainBody {
 
         // Check if REPL was requested
         if (repl) {
-            Repl().start()
+            Repl()
         } else {
             Logger.warn("REPL not started. Use -r or --repl to start the REPL.")
         }
     }
 }
-
-fun help() {
-    println("""
-        Ghent Prolog: A Prolog interpreter in Kotlin
-        
-        Options:
-        -s, --source <file>  Specify the source file to load
-        -r, --repl           Start the REPL (default)
-        -v, --verb
-        -h, --help           Show this help message
-    """.trimIndent())
-}

src/gpl

@@ -20,7 +20,7 @@ fi
 if [ ! -f "${JAR_PATH}" ]; then
     printf 'Info: JAR file not found at "%s"\n' "${JAR_PATH}"
     printf 'Info: Building the project...\n'
-    ./gradlew build
+    ./gradlew fatJar
     if [ "${?}" -ne 0 ]; then
         printf 'Error: Build failed\n'
         exit 1

src/interpreter/FileLoader.kt

@@ -2,22 +2,27 @@ package interpreter
 
 import io.Logger
 import parser.ScriptParser
+import prolog.ast.Database
 import prolog.Program
 import prolog.ast.logic.Clause
 
 class FileLoader {
     private val parser = ScriptParser()
 
-    fun load(filePath: String): () -> Unit {
+    fun load(filePath: String) {
+        Logger.info("Loading file: $filePath")
+
         val input = readFile(filePath)
 
         Logger.debug("Parsing content of $filePath")
         val clauses: List<Clause> = parser.parse(input)
 
-        Program.load(clauses)
+        val db = Database(filePath)
+        db.load(clauses)
+        Program.add(db)
+        db.initialize()
 
-        // TODO Pass next commands to execute
+        Logger.debug("Finished loading file: $filePath")
-        return {}
     }
 
     fun readFile(filePath: String): String {

src/interpreter/Preprocessor.kt

@@ -47,7 +47,7 @@ open class Preprocessor {
         }
     }
 
-    protected open fun preprocess(term: Term): Term {
+    protected open fun preprocess(term: Term, nested: Boolean = false): Term {
         val prepped = when (term) {
             Atom("true") -> True
             Structure(Atom("true"), emptyList()) -> True
@@ -61,7 +61,7 @@ open class Preprocessor {
             Atom("nl") -> Nl
             is Structure -> {
                 // Preprocess the arguments first to recognize builtins
-                val args = term.arguments.map { preprocess(it) }
+                val args = term.arguments.map { preprocess(it, nested = true) }
 
                 when {
                     // TODO Remove hardcoding by storing the functors as constants in operators?
@@ -77,7 +77,7 @@ open class Preprocessor {
                     term.functor == "\\+/1" -> {
                         Not(args[0] as Goal)
                     }
-                    // Arithmetic
+
                     term.functor == "=\\=/2" && args.all { it is Expression } -> {
                         EvaluatesToDifferent(args[0] as Expression, args[1] as Expression)
                     }
@@ -90,6 +90,16 @@ open class Preprocessor {
                         Is(args[0] as Expression, args[1] as Expression)
                     }
 
+                    // Arithmetic
+
+                    term.functor == "=/2" && args.all { it is Expression } -> {
+                        Unify(args[0] as Expression, args[1] as Expression)
+                    }
+
+                    term.functor == "\\=/2" && args.all { it is Expression } -> {
+                        NotUnify(args[0] as Expression, args[1] as Expression)
+                    }
+
                     term.functor == "-/1" && args.all { it is Expression } -> {
                         Negate(args[0] as Expression)
                     }
@@ -121,6 +131,7 @@ open class Preprocessor {
                     // Other
                     term.functor == "write/1" -> Write(args[0])
                     term.functor == "read/1" -> Read(args[0])
+                    term.functor == "initialization/1" -> Initialization(args[0] as Goal)
 
                     else -> term
                 }
@@ -129,9 +140,10 @@ open class Preprocessor {
             else -> term
         }
 
-        if (prepped != term || prepped::class != term::class) {
+        Logger.debug(
-            Logger.debug("Preprocessed term: $term -> $prepped (is ${prepped::class.simpleName})")
+            "Preprocessed term $term into $prepped (kind ${prepped::class.simpleName})",
-        }
+            !nested && (prepped != term || prepped::class != term::class)
+        )
 
         return prepped
     }

src/io/Logger.kt

@@ -8,17 +8,18 @@ object Logger {
     val defaultLevel: Level = Level.WARN
     var level: Level = defaultLevel
 
-    private val io: IoHandler = Terminal()
+    private val io = Terminal()
 
-    fun log(message: String, messageLevel: Level = defaultLevel) {
+    fun log(message: String, messageLevel: Level = defaultLevel, onlyIf: Boolean) {
-        if (level <= messageLevel) {
+        if (level <= messageLevel && onlyIf) {
+            io.checkNewLine()
             val text = "$messageLevel: $message\n"
             io.say(text)
         }
     }
 
-    fun debug(message: String) = log(message, Level.DEBUG)
+    fun debug(message: String, onlyIf: Boolean = true) = log(message, Level.DEBUG, onlyIf)
-    fun info(message: String) = log(message, Level.INFO)
+    fun info(message: String, onlyIf: Boolean = true) = log(message, Level.INFO, onlyIf)
-    fun warn(message: String) = log(message, Level.WARN)
+    fun warn(message: String, onlyIf: Boolean = true) = log(message, Level.WARN, onlyIf)
-    fun error(message: String) = log(message, Level.ERROR)
+    fun error(message: String, onlyIf: Boolean = true) = log(message, Level.ERROR, onlyIf)
 }

src/io/Terminal.kt

@@ -1,5 +1,6 @@
 package io
 
+import prolog.Program
 import java.io.BufferedReader
 import java.io.BufferedWriter
 import java.io.InputStream
@@ -60,4 +61,11 @@ class Terminal(
         error.close()
         System.exit(0)
     }
+
+    fun checkNewLine() {
+        if (Program.storeNewLine) {
+            say("\n")
+            Program.storeNewLine = false
+        }
+    }
 }

src/parser/ScriptParser.kt

@@ -2,11 +2,17 @@ package parser
 
 import com.github.h0tk3y.betterParse.grammar.Grammar
 import com.github.h0tk3y.betterParse.grammar.parseToEnd
+import interpreter.Preprocessor
+import io.Logger
 import parser.grammars.LogicGrammar
 import prolog.ast.logic.Clause
 
 class ScriptParser: Parser {
     private val grammar: Grammar<List<Clause>> = LogicGrammar() as Grammar<List<Clause>>
+    private val preprocessor = Preprocessor()
 
-    override fun parse(input: String): List<Clause> = grammar.parseToEnd(input)
+    override fun parse(input: String): List<Clause> {
+        val raw = grammar.parseToEnd(input)
+        return preprocessor.preprocess(raw)
+    }
 }

src/parser/grammars/LogicGrammar.kt

@@ -1,22 +1,21 @@
 package parser.grammars
 
-import com.github.h0tk3y.betterParse.combinators.oneOrMore
+import com.github.h0tk3y.betterParse.combinators.*
-import com.github.h0tk3y.betterParse.combinators.or
-import com.github.h0tk3y.betterParse.combinators.separated
-import com.github.h0tk3y.betterParse.combinators.times
-import com.github.h0tk3y.betterParse.combinators.unaryMinus
-import com.github.h0tk3y.betterParse.combinators.use
 import com.github.h0tk3y.betterParse.parser.Parser
 import prolog.ast.logic.Clause
 import prolog.ast.logic.Fact
 import prolog.ast.logic.Rule
+import prolog.ast.terms.Atom
 
 class LogicGrammar : TermsGrammar() {
+    protected val constraint: Parser<Rule> by (-neck * body) use {
+        Rule(Atom(""), this)
+    }
     protected val rule: Parser<Rule> by (head * -neck * body) use { Rule(t1, t2) }
     protected val fact: Parser<Fact> by head use { Fact(this) }
 
-    protected val clause: Parser<Clause> by ((rule or fact) * -dot)
+    protected val clause: Parser<Clause> by ((rule or constraint or fact) * -dot)
     protected val clauses: Parser<List<Clause>> by oneOrMore(clause)
 
     override val rootParser: Parser<Any> by clauses
-}
+}

src/parser/grammars/TermsGrammar.kt

@@ -1,16 +1,10 @@
 package parser.grammars
 
-import com.github.h0tk3y.betterParse.combinators.or
+import com.github.h0tk3y.betterParse.combinators.*
-import com.github.h0tk3y.betterParse.combinators.separated
-import com.github.h0tk3y.betterParse.combinators.times
-import com.github.h0tk3y.betterParse.combinators.unaryMinus
-import com.github.h0tk3y.betterParse.combinators.use
 import com.github.h0tk3y.betterParse.grammar.parser
 import com.github.h0tk3y.betterParse.parser.Parser
-import prolog.ast.arithmetic.Expression
 import prolog.ast.arithmetic.Float
 import prolog.ast.arithmetic.Integer
-import prolog.ast.logic.LogicOperand
 import prolog.ast.terms.*
 
 open class TermsGrammar : Tokens() {
@@ -37,42 +31,32 @@ open class TermsGrammar : Tokens() {
     protected val float: Parser<Float> by floatToken use { Float(text.toFloat()) }
 
     // Operators
-    protected val logOps: Parser<String> by (dummy
+    protected val ops: Parser<String> by (dummy
+            // Logic
             or comma
             or semicolon
+            // Arithmetic
+            or plus
+            or equals
+            or notEquals
             ) use { this.text }
-    protected val simpleLogicOperand: Parser<LogicOperand> by (dummy
+    protected val simpleOperand: Parser<Operand> by (dummy
+            // Logic
             or compound
             or atom
-            )
+            or variable
-    protected val logicOperand: Parser<LogicOperand> by (dummy
+            // Arithmetic
-            or parser(::logicOperator)
-            or simpleLogicOperand
-            )
-    protected val logicOperator: Parser<CompoundTerm> by (simpleLogicOperand * logOps * logicOperand) use {
-        CompoundTerm(Atom(t2), listOf(t1, t3))
-    }
-
-    protected val arithmeticOps: Parser<String> by (dummy
-            or plus
-            ) use { this.text }
-    protected val simpleArithmeticOperand: Parser<Expression> by (dummy
             or int
             or float
             )
-    protected val arithmeticOperand: Parser<Expression> by (dummy
+    protected val operand: Parser<Operand> by (dummy
-            or parser(::arithmeticOperator)
+        or parser(::operator)
-            or simpleArithmeticOperand
+        or simpleOperand
-            ) use { this as Expression }
+    )
-    protected val arithmeticOperator: Parser<CompoundTerm> by (simpleArithmeticOperand * arithmeticOps * arithmeticOperand) use {
+    protected val operator: Parser<CompoundTerm> by (simpleOperand * ops * operand) use {
         CompoundTerm(Atom(t2), listOf(t1, t3))
     }
 
-    protected val operator: Parser<CompoundTerm> by (dummy
-            or logicOperator
-            or arithmeticOperator
-            )
-
     // Parts
     protected val head: Parser<Head> by (dummy
             or compound
@@ -81,6 +65,7 @@ open class TermsGrammar : Tokens() {
     protected val body: Parser<Body> by (dummy
             or operator
             or head
+            or variable
             ) use { this as Body }
 
     protected val term: Parser<Term> by (dummy

src/parser/grammars/Tokens.kt

@@ -22,6 +22,8 @@ abstract class Tokens : Grammar<Any>() {
     protected val rightParenthesis: Token by literalToken(")")
     protected val comma: Token by literalToken(",")
     protected val semicolon: Token by literalToken(";")
+    protected val equals: Token by literalToken("=")
+    protected val notEquals: Token by literalToken("\\=")
     protected val plus: Token by literalToken("+")
     protected val dot by literalToken(".")
 

src/prolog/Program.kt

@@ -1,32 +1,25 @@
 package prolog
 
 import io.Logger
+import prolog.ast.Database
 import prolog.ast.logic.Clause
-import prolog.ast.logic.Predicate
 import prolog.ast.logic.Resolvent
-import prolog.ast.terms.Functor
 import prolog.ast.terms.Goal
 
-typealias Database = Program
-
 /**
- * Prolog Program or database.
+ * Object to handle execution
+ *
+ * This object is a singleton that manages a list of databases.
  */
-object Program: Resolvent {
+object Program : Resolvent {
-    var predicates: Map<Functor, Predicate> = emptyMap()
+    private val internalDb = Database("")
+    private val databases: MutableList<Database> = mutableListOf(internalDb)
 
-    init {
+    var storeNewLine: Boolean = false
-        Logger.debug("Initializing ${this::class.java.simpleName}")
+    var variableRenamingStart: Int = 0
-        setup()
-        Logger.debug("Initialization of ${this::class.java.simpleName} complete")
-    }
 
-    private fun setup() {
+    fun add(database: Database) {
-        Logger.debug("Setting up ${this::class.java.simpleName}")
+        databases.add(database)
-
-        // Initialize the program with built-in predicates
-        load(listOf(
-        ))
     }
 
     /**
@@ -35,51 +28,24 @@ object Program: Resolvent {
      */
     fun query(goal: Goal): Answers = solve(goal, emptyMap())
 
-    override fun solve(goal: Goal, subs: Substitutions): Answers {
+    override fun solve(goal: Goal, subs: Substitutions): Answers = sequence {
         Logger.debug("Solving goal $goal")
-        val functor = goal.functor
+        for (database in databases) {
-        // If the predicate does not exist, return false
+            yieldAll(database.solve(goal, subs))
-        val predicate = predicates[functor] ?: return emptySequence()
-        // If the predicate exists, evaluate the goal against it
-        return predicate.solve(goal, subs)
-    }
-
-    /**
-     * Loads a list of clauses into the program.
-     */
-    fun load(clauses: List<Clause>) {
-        for (clause in clauses) {
-            val functor = clause.functor
-            val predicate = predicates[functor]
-
-            if (predicate != null) {
-                // If the predicate already exists, add the clause to it
-                predicate.add(clause)
-            } else {
-                // If the predicate does not exist, create a new one
-                predicates += Pair(functor, Predicate(listOf(clause)))
-            }
-
-            Logger.debug("Loaded clause $clause into predicate $functor")
         }
     }
 
-    fun load(predicate: Predicate) {
+    fun load(clauses: List<Clause>) = internalDb.load(clauses)
-        val functor = predicate.functor
-        val existingPredicate = predicates[functor]
-
-        if (existingPredicate != null) {
-            // If the predicate already exists, add the clauses to it
-            existingPredicate.addAll(predicate.clauses)
-        } else {
-            // If the predicate does not exist, create a new one
-            predicates += Pair(functor, predicate)
-        }
-    }
 
     fun clear() {
-        Logger.debug("Clearing ${this::class.java.simpleName}")
+        databases.forEach { it.clear() }
-        predicates = emptyMap()
+    }
-        setup()
+
+    fun clear(filePath: String) {
+        val correspondingDBs = databases.filter { it.sourceFile == filePath }
+
+        require(correspondingDBs.isNotEmpty()) { "No database found for file: $filePath" }
+
+        correspondingDBs.forEach { it.clear() }
     }
 }

src/prolog/Substitution.kt

@@ -4,7 +4,7 @@ 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"
+    override fun toString(): String = "$from |-> $to"
 }
 typealias Substitutions = Map<Term, Term>
 typealias Answer = Result<Substitutions>

src/prolog/ast/Database.kt

@@ -0,0 +1,76 @@
+package prolog.ast
+
+import io.Logger
+import prolog.Program
+import prolog.Answers
+import prolog.Substitutions
+import prolog.ast.logic.Clause
+import prolog.ast.logic.Predicate
+import prolog.ast.logic.Resolvent
+import prolog.ast.terms.Functor
+import prolog.ast.terms.Goal
+
+/**
+ * Prolog Program or Database
+ */
+class Database(val sourceFile: String): Resolvent {
+    private var predicates: Map<Functor, Predicate> = emptyMap()
+
+    fun initialize() {
+        Logger.info("Initializing database from $sourceFile")
+        if (predicates.contains("/_")) {
+            Logger.debug("Loading clauses from /_ predicate")
+            predicates["/_"]?.clauses?.forEach {
+                Logger.debug("Loading clause $it")
+                val goal = it.body as Goal
+                goal.satisfy(emptyMap()).toList()
+            }
+        }
+    }
+
+    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()
+        // If the predicate exists, evaluate the goal against it
+        return predicate.solve(goal, subs)
+    }
+
+    /**
+     * Loads a list of clauses into the program.
+     */
+    fun load(clauses: List<Clause>) {
+        for (clause in clauses) {
+            val functor = clause.functor
+            val predicate = predicates[functor]
+
+            if (predicate != null) {
+                // If the predicate already exists, add the clause to it
+                predicate.add(clause)
+            } else {
+                // If the predicate does not exist, create a new one
+                predicates += Pair(functor, Predicate(listOf(clause)))
+            }
+
+            Logger.debug("Loaded clause $clause into predicate $functor")
+        }
+    }
+
+    fun load(predicate: Predicate) {
+        val functor = predicate.functor
+        val existingPredicate = predicates[functor]
+
+        if (existingPredicate != null) {
+            // If the predicate already exists, add the clauses to it
+            existingPredicate.addAll(predicate.clauses)
+        } else {
+            // If the predicate does not exist, create a new one
+            predicates += Pair(functor, predicate)
+        }
+    }
+
+    fun clear() {
+        Logger.debug("Clearing ${this::class.java.simpleName}")
+        predicates = emptyMap()
+    }
+}

src/prolog/ast/arithmetic/Float.kt

@@ -31,4 +31,15 @@ class Float(override val value: kotlin.Float): Number {
         is Integer -> Float(value * other.value.toFloat())
         else -> throw IllegalArgumentException("Cannot multiply $this and $other")
     }
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (other !is Float) return false
+        if (value != other.value) return false
+        return true
+    }
+
+    override fun hashCode(): Int {
+        return super.hashCode()
+    }
 }

src/prolog/ast/logic/Clause.kt

@@ -1,13 +1,13 @@
 package prolog.ast.logic
 
 import prolog.Answers
+import prolog.Program
 import prolog.Substitutions
-import prolog.ast.terms.Body
+import prolog.ast.terms.*
-import prolog.ast.terms.Functor
-import prolog.ast.terms.Goal
-import prolog.ast.terms.Head
 import prolog.builtins.True
 import prolog.flags.AppliedCut
+import prolog.logic.applySubstitution
+import prolog.logic.numbervars
 import prolog.logic.unifyLazy
 
 /**
@@ -21,23 +21,39 @@ import prolog.logic.unifyLazy
 abstract class Clause(val head: Head, val body: Body) : Resolvent {
     val functor: Functor = head.functor
 
-    override fun solve (goal: Goal, subs: Substitutions): Answers = 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 { headAnswer ->
+
-            headAnswer.map { newHeadSubs ->
+        // Since we are only interested in substitutions in the goal (as opposed to the head of this clause),
+        //  we can use variable renaming and filter out the substitutions that are not in the goal.
+        val (end, renamed: Substitutions) = numbervars(head, Program.variableRenamingStart, subs)
+
+        val reverse = renamed.entries.associate { (a, b) -> b to a }
+        Program.variableRenamingStart = end
+
+        var newSubs: Substitutions = subs + renamed
+        unifyLazy(goal, head, newSubs).forEach { headAnswer ->
+            headAnswer.map { headSubs ->
                 // If the body can be proven, yield the (combined) substitutions
-                body.satisfy(subs + newHeadSubs).forEach { bodyAnswer ->
+                newSubs = subs + renamed + headSubs
+                body.satisfy(newSubs).forEach { bodyAnswer ->
                     bodyAnswer.fold(
-                        onSuccess = { newBodySubs ->
+                        onSuccess = { bodySubs ->
-                            yield(Result.success(newHeadSubs + newBodySubs))
+                            var result = (headSubs + bodySubs)
+                                .mapKeys { reverse[it.key] ?: it.key }
+                                .mapValues { reverse[it.value] ?: it.value }
+                            result = result.map { it.key to applySubstitution(it.value, result) }
+                                .toMap()
+                                .filterNot { it.key in renamed.keys }
+                            yield(Result.success(result))
                         },
                         onFailure = { error ->
                             if (error is AppliedCut) {
                                 // Find single solution and return immediately
                                 if (error.subs != null) {
-                                    yield(Result.failure(AppliedCut(newHeadSubs + error.subs)))
+                                    yield(Result.failure(AppliedCut(headSubs + error.subs)))
                                 } else {
                                     yield(Result.failure(AppliedCut()))
                                 }
@@ -52,10 +68,5 @@ abstract class Clause(val head: Head, val body: Body) : Resolvent {
         }
     }
 
-    override fun toString(): String {
+    override fun toString(): String = if (body is True) head.toString() else "$head :- $body"
-        return when {
+}
-            body is True -> head.toString()
-            else -> "$head :- $body"
-        }
-    }
-}

src/prolog/ast/logic/Predicate.kt

@@ -51,6 +51,7 @@ class Predicate : Resolvent {
 
     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
         clauses.forEach { clause ->

src/prolog/ast/terms/Variable.kt

@@ -1,10 +1,11 @@
 package prolog.ast.terms
 
+import prolog.Answers
 import prolog.Substitutions
 import prolog.ast.arithmetic.Expression
 import prolog.ast.arithmetic.Simplification
 
-data class Variable(val name: String) : Term, Expression {
+data class Variable(val name: String) : Term, Body, Expression {
     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
@@ -16,5 +17,15 @@ data class Variable(val name: String) : Term, Expression {
         return Simplification(this, result)
     }
 
+    override fun satisfy(subs: Substitutions): Answers {
+        // If the variable is bound, satisfy the bound term
+        if (this in subs) {
+            val boundTerm = subs[this]!! as Body
+            return boundTerm.satisfy(subs)
+        }
+
+        return sequenceOf(Result.failure(IllegalArgumentException("Unbound variable: $this")))
+    }
+
     override fun toString(): String = name
 }

src/prolog/builtins/io.kt

@@ -4,6 +4,7 @@ import io.Logger
 import io.Terminal
 import parser.ReplParser
 import prolog.Answers
+import prolog.Program
 import prolog.Substitutions
 import prolog.ast.logic.Satisfiable
 import prolog.ast.terms.Atom
@@ -21,6 +22,8 @@ class Write(private val term: Term) : Operator(Atom("write"), null, term), Satis
 
         Terminal().say(t.toString())
 
+        Program.storeNewLine = true
+
         return sequenceOf(Result.success(emptyMap()))
     }
 }
@@ -31,6 +34,7 @@ class Write(private val term: Term) : Operator(Atom("write"), null, term), Satis
 object Nl : Atom("nl"), Satisfiable {
     override fun satisfy(subs: Substitutions): Answers {
         Terminal().say("\n")
+        Program.storeNewLine = false
         return sequenceOf(Result.success(emptyMap()))
     }
 }

src/prolog/builtins/other.kt

@@ -6,6 +6,10 @@ import prolog.ast.logic.LogicOperand
 import prolog.ast.terms.Atom
 import prolog.ast.logic.LogicOperator
 
+class Initialization(val goal: LogicOperand) : LogicOperator(Atom(":-"), null, goal) {
+    override fun satisfy(subs: Substitutions): Answers = goal.satisfy(subs).take(1)
+}
+
 class Query(val query: LogicOperand) : LogicOperator(Atom("?-"), null, query) {
     override fun satisfy(subs: Substitutions): Answers = query.satisfy(subs)
 }

src/prolog/builtins/unificationOperators.kt

@@ -26,6 +26,11 @@ class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="
     }
 }
 
+class NotUnify(term1: Term, term2: Term) : Operator(Atom("\\="), term1, term2) {
+    private val not = Not(Unify(term1, term2))
+    override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs)
+}
+
 class Equivalent(private val term1: Term, private val term2: Term) : Operator(Atom("=="), term1, term2) {
     override fun satisfy(subs: Substitutions): Answers = sequence {
         val t1 = applySubstitution(term1, subs)

src/prolog/logic/terms.kt

@@ -1,7 +1,10 @@
 package prolog.logic
 
+import prolog.Substitutions
 import prolog.ast.terms.Atom
+import prolog.ast.terms.Structure
 import prolog.ast.terms.Term
+import prolog.ast.terms.Variable
 
 /**
  * True when Term is a term with functor Name/Arity. If Term is a variable it is unified with a new term whose
@@ -20,3 +23,53 @@ fun functor(term: Term, name: Atom, arity: Int): Boolean {
     // TODO Implement
     return true
 }
+
+/**
+ * Unify the free variables in Term with a term $VAR(N), where N is the number of the variable.
+ * Counting starts at Start.
+ * End is unified with the number that should be given to the next variable.
+ *
+ * Source: [SWI-Prolog Predicate numbervars/3](https://www.swi-prolog.org/pldoc/man?predicate=numbervars/3)
+ *
+ * @return Pair of the next number and only the new substitutions of variables to $VAR(N)
+ */
+fun numbervars(
+    term: Term,
+    start: Int = 0,
+    subs: Substitutions = emptyMap(),
+    sessionSubs: Substitutions = emptyMap()
+): Pair<Int, Substitutions> {
+    when {
+        variable(term, subs) -> {
+            // All instances of the same variable are unified with the same term
+            if (term in sessionSubs) {
+                return Pair(start, emptyMap())
+            }
+
+            val from = term as Variable
+            var suggestedName = "${from.name}($start)"
+            // If the suggested name is already in use, find a new one
+            while ((subs + sessionSubs).filter { (it.key as Variable).name == suggestedName }.isNotEmpty()) {
+                val randomInfix = ((0..9) + ('a'..'z') + ('A'..'Z')).random()
+                suggestedName = "${from.name}_${randomInfix}_($start)"
+            }
+            return Pair(start + 1, mapOf(from to Variable(suggestedName)))
+        }
+
+        compound(term, subs) -> {
+            val from = term as Structure
+            var n = start
+            val s: MutableMap<Term, Term> = sessionSubs.toMutableMap()
+            from.arguments.forEach { arg ->
+                val (newN, newSubs) = numbervars(arg, n, subs, s)
+                n = newN
+                s += newSubs
+            }
+            return Pair(n, s)
+        }
+
+        else -> {
+            return Pair(start, emptyMap())
+        }
+    }
+}

src/prolog/logic/unification.kt

@@ -36,7 +36,7 @@ fun applySubstitution(expr: Expression, subs: Substitutions): Expression = when
 }
 
 // Check if a variable occurs in a term
-private fun occurs(variable: Variable, term: Term, subs: Substitutions): Boolean = when {
+fun occurs(variable: Variable, term: Term, subs: Substitutions): Boolean = when {
     variable(term, subs) -> term == variable
     atomic(term, subs) -> false
     compound(term, subs) -> {
@@ -53,18 +53,18 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
     val t2 = applySubstitution(term2, subs)
 
     when {
-        equivalent(t1, t2, subs) -> yield(Result.success(subs))
+        equivalent(t1, t2, subs) -> yield(Result.success(emptyMap()))
         variable(t1, subs) -> {
             val variable = t1 as Variable
             if (!occurs(variable, t2, subs)) {
-                yield(Result.success(subs + (variable to t2)))
+                yield(Result.success(mapOf(term1 to t2)))
             }
         }
 
         variable(t2, subs) -> {
             val variable = t2 as Variable
             if (!occurs(variable, t1, subs)) {
-                yield(Result.success(subs + (variable to t1)))
+                yield(Result.success(mapOf(term2 to t1)))
             }
         }
 

src/repl/Repl.kt

@@ -6,14 +6,15 @@ import io.Terminal
 import parser.ReplParser
 import prolog.Answer
 import prolog.Answers
+import prolog.Program
 
 class Repl {
     private val io = Terminal()
     private val parser = ReplParser()
     private val preprocessor = Preprocessor()
 
-    fun start() {
+    init {
-        io.say("Prolog REPL. Type '^D' to quit.\n")
+        welcome()
         while (true) {
             try {
                 printAnswers(query())
@@ -23,15 +24,19 @@ class Repl {
         }
     }
 
-    fun query(): Answers {
+    private fun welcome() {
+        io.checkNewLine()
+        io.say("Prolog REPL. Type '^D' to quit.\n")
+    }
+
+    private fun query(): Answers {
         val queryString = io.prompt("?-", { "|  " })
         val simpleQuery = parser.parse(queryString)
         val query = preprocessor.preprocess(simpleQuery)
-        Logger.debug("Satisfying query: $query")
         return query.satisfy(emptyMap())
     }
 
-    fun printAnswers(answers: Answers) {
+    private fun printAnswers(answers: Answers) {
         val knownCommands = setOf(";", "a", ".", "h")
 
         val iterator = answers.iterator()
@@ -68,7 +73,7 @@ class Repl {
         io.say("\n")
     }
 
-    fun help(): String {
+    private fun help(): String {
         io.say("Commands:\n")
         io.say("  ;   find next solution\n")
         io.say("  a   abort\n")
@@ -77,12 +82,13 @@ class Repl {
         return ""
     }
 
-    fun prettyPrint(result: Answer): String {
+    private fun prettyPrint(result: Answer): String {
         result.fold(
             onSuccess = {
                 val subs = result.getOrNull()!!
                 if (subs.isEmpty()) {
-                    return "true."
+                    io.checkNewLine()
+                    return "true.\n"
                 }
                 return subs.entries.joinToString(",\n") { "${it.key} = ${it.value}" }
             },

tests/compare.sh

@@ -0,0 +1,53 @@
+#!/usr/bin/env bash
+
+# This script is expected to be run from the root of the project.
+
+# Paths to the two implementations
+GPL="src/gpl"
+SPL="swipl"
+
+GPL_FLAGS=("--debug")
+SPL_FLAGS=("--quiet" "-t" "'true'")
+
+# Directory containing test files
+TEST_DIR="examples"
+
+# Temporary files for storing outputs
+GPL_OUT=$(mktemp)
+SPL_OUT=$(mktemp)
+
+# Flag to track if all tests pass
+PASSED=0
+FAILED=0
+
+# Iterate over all test files in the test directory
+#for TESTFILE in $(find ${TEST_DIR} -type f); do
+files=("examples/program.pl" "examples/basics/disjunction.pl" "examples/basics/fraternity.pl")
+for TESTFILE in "${files[@]}"; do
+    # Run both programs with the test file
+    "${SPL}" "${SPL_FLAGS[@]}" "$TESTFILE" > "${SPL_OUT}" 2>&1
+    "${GPL}" "${GPL_FLAGS[@]}" -s "$TESTFILE" > "${GPL_OUT}" 2>&1
+
+    # Compare the outputs
+    if diff -q "$SPL_OUT" "$GPL_OUT" > /dev/null; then
+        PASSED=$((PASSED + 1))
+    else
+        echo "Test failed! Outputs differ for $TESTFILE"
+        printf "\nTest:\n%s\n" "$(cat "$TESTFILE")"
+        printf "\nExpected:\n%s\n" "$(cat "$SPL_OUT")"
+        printf "\nGot:\n%s\n" "$(cat "$GPL_OUT")"
+        echo "-----------------------------------------"
+        FAILED=$((FAILED + 1))
+    fi
+done
+
+# Clean up temporary files
+rm "$SPL_OUT" "$GPL_OUT"
+
+# Final result, summary
+if [ $FAILED -eq 0 ]; then
+    echo "All tests passed!"
+else
+    printf "Tests passed: %d\nTests failed: %d\n" "$PASSED" "$FAILED"
+    exit 1
+fi

tests/e2e/myClass.kt

@@ -0,0 +1,4 @@
+package e2e
+
+class myClass {
+}

tests/interpreter/PreprocessorTests.kt

@@ -12,8 +12,8 @@ import prolog.builtins.*
 
 class PreprocessorTests {
     class OpenPreprocessor : Preprocessor() {
-        public override fun preprocess(input: Term): Term {
+        public override fun preprocess(term: Term, nested: Boolean): Term {
-            return super.preprocess(input)
+            return super.preprocess(term, nested)
         }
     }
 

tests/interpreter/SourceFileReaderTests.kt

@@ -16,8 +16,6 @@ class SourceFileReaderTests {
         val reader = FileLoader()
 
         reader.readFile(inputFile)
-
-        println(Program.predicates)
     }
 
     @Test
@@ -26,7 +24,5 @@ class SourceFileReaderTests {
         val reader = FileLoader()
 
         reader.readFile(inputFile)
-
-        println(Program.predicates)
     }
 }

tests/parser/OperatorParserTests.kt

@@ -26,4 +26,17 @@ class OperatorParserTests {
 
         assertEquals(Structure(Atom(","), listOf(Atom("a"), Atom("b"))), result, "Expected atom 'a, b'")
     }
+
+    class BodyParser : TermsGrammar() {
+        override val rootParser: Parser<Any> by body
+    }
+
+    @Test
+    fun `parse equality`() {
+        val input = "a = b"
+
+        val result = BodyParser().parseToEnd(input)
+
+        assertEquals(Structure(Atom("="), listOf(Atom("a"), Atom("b"))), result, "Expected atom 'a = b'")
+    }
 }

tests/parser/grammars/LogicGrammarTests.kt

@@ -129,4 +129,16 @@ class LogicGrammarTests {
         val conjunction = rule.body as CompoundTerm
         assertEquals("invited/2", (conjunction.arguments[0] as CompoundTerm).functor, "Expected functor 'invited/2'")
     }
+
+    @Test
+    fun `parse constraints`() {
+        val input = ":- a."
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(1, result.size, "Expected 1 rule")
+        assertTrue(result[0] is Rule, "Expected a rule")
+        val rule = result[0] as Rule
+        assertEquals("/_", rule.head.functor, "Expected a constraint")
+    }
 }

tests/parser/grammars/TermsGrammarTests.kt

@@ -2,9 +2,12 @@ package parser.grammars
 
 import com.github.h0tk3y.betterParse.grammar.Grammar
 import com.github.h0tk3y.betterParse.grammar.parseToEnd
+import com.github.h0tk3y.betterParse.parser.Parser
 import org.junit.jupiter.api.Assertions
+import org.junit.jupiter.api.Assertions.assertTrue
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.assertDoesNotThrow
 import org.junit.jupiter.params.ParameterizedTest
 import org.junit.jupiter.params.provider.ValueSource
 import prolog.ast.arithmetic.Float
@@ -14,6 +17,7 @@ import prolog.ast.terms.Structure
 import prolog.ast.terms.Term
 import prolog.ast.terms.Variable
 import prolog.logic.equivalent
+import kotlin.test.assertEquals
 
 class TermsGrammarTests {
     private lateinit var parser: Grammar<Term>
@@ -167,9 +171,12 @@ class TermsGrammarTests {
 
         val result = parser.parseToEnd(input)
 
-        Assertions.assertTrue(
+        assertEquals(Float(-42.0f), result, "Expected float '-42.0'")
-            equivalent(Float(-42.0f), result, emptyMap()),
+    }
-            "Expected float '-42.0'"
+
-        )
+    @ParameterizedTest
+    @ValueSource(strings = ["got_an_a(Student)", "grade(Student, Grade)"])
+    fun `parse unification`(input: String) {
+        assertDoesNotThrow { parser.parseToEnd(input) }
     }
 }

tests/prolog/EvaluationTests.kt

@@ -2,6 +2,7 @@ package prolog
 
 import org.junit.jupiter.api.Assertions.*
 import org.junit.jupiter.api.BeforeEach
+import org.junit.jupiter.api.Nested
 import org.junit.jupiter.api.Test
 import prolog.ast.logic.Fact
 import prolog.ast.logic.Rule
@@ -108,9 +109,9 @@ class EvaluationTests {
         val parent = Rule(
             Structure(Atom("parent"), listOf(variable1, variable2)),
             /* :- */ Disjunction(
-            Structure(Atom("father"), listOf(variable1, variable2)),
+                Structure(Atom("father"), listOf(variable1, variable2)),
-            /* ; */
+                /* ; */
-            Structure(Atom("mother"), listOf(variable1, variable2))
+                Structure(Atom("mother"), listOf(variable1, variable2))
             )
         )
 
@@ -212,7 +213,182 @@ class EvaluationTests {
         assertEquals(expectedResults.size, actualResults.size, "Number of results should match")
         for (i in expectedResults.indices) {
             assertEquals(expectedResults[i].size, actualResults[i].getOrNull()!!.size, "Substitution size should match")
-            assertTrue(expectedResults[i].all { actualResults[i].getOrNull()!![it.key]?.let { it1 -> equivalent(it.value, it1, emptyMap()) } ?: false }, "Substitution values should match")
+            assertTrue(expectedResults[i].all {
+                actualResults[i].getOrNull()!![it.key]?.let { it1 ->
+                    equivalent(
+                        it.value,
+                        it1,
+                        emptyMap()
+                    )
+                } ?: false
+            }, "Substitution values should match")
         }
     }
-}
+
+    @Test
+    fun `likes(alice, pizza)`() {
+        val fact = Fact(Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza"))))
+        val goal = Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza")))
+
+        Program.load(listOf(fact))
+
+        val result = Program.query(goal).toList()
+
+        assertEquals(1, result.size, "Expected 1 result")
+        assertTrue(result[0].isSuccess, "Expected success")
+        val subs = result[0].getOrNull()!!
+        assertEquals(0, subs.size, "Expected no substitutions")
+    }
+
+    @Test
+    fun `likes(Person, pizza)`() {
+        val fact = Fact(Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza"))))
+        val goal = Structure(Atom("likes"), listOf(Variable("Person"), Atom("pizza")))
+
+        Program.load(listOf(fact))
+
+        val result = Program.query(goal).toList()
+
+        assertEquals(1, result.size, "Expected 1 result")
+        assertTrue(result[0].isSuccess, "Expected success")
+        val subs = result[0].getOrNull()!!
+        assertEquals(1, subs.size, "Expected 1 substitution")
+        assertEquals(Atom("alice"), subs[Variable("Person")], "Expected Person to be alice")
+    }
+
+    @Test
+    fun `likes_food(alice)`() {
+        val fact = Fact(Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza"))))
+        val rule = Rule(
+            Structure(Atom("likes_food"), listOf(Variable("Person"))),
+            Structure(Atom("likes"), listOf(Variable("Person"), Atom("pizza")))
+        )
+
+        val goal = Structure(Atom("likes_food"), listOf(Atom("alice")))
+
+        Program.load(listOf(fact, rule))
+
+        val result = Program.query(goal).toList()
+
+        assertEquals(1, result.size, "Expected 1 result")
+        assertTrue(result[0].isSuccess, "Expected success")
+        val subs = result[0].getOrNull()!!
+        assertEquals(0, subs.size, "Expected no substitutions")
+    }
+
+    @Test
+    fun `likes_food(Person)`() {
+        val fact = Fact(Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza"))))
+        val rule = Rule(
+            Structure(Atom("likes_food"), listOf(Variable("Person"))),
+            Structure(Atom("likes"), listOf(Variable("Person"), Atom("pizza")))
+        )
+
+        val goal = Structure(Atom("likes"), listOf(Variable("X"), Atom("pizza")))
+
+        Program.load(listOf(fact, rule))
+
+        val result = Program.query(goal).toList()
+
+        assertEquals(1, result.size, "Expected 1 result")
+        assertTrue(result[0].isSuccess, "Expected success")
+        val subs = result[0].getOrNull()!!
+        assertEquals(1, subs.size, "Expected 1 substitution")
+        assertEquals(Atom("alice"), subs[Variable("X")], "Expected Person to be alice")
+    }
+
+    @Test
+    fun `requires querying exact`() {
+        val fact1 = Fact(Atom("a"))
+        val fact2 = Fact(Atom("b"))
+        val rule1 = Rule(
+            Atom("c"),
+            Conjunction(
+                Atom("a"),
+                Atom("b")
+            )
+        )
+
+        Program.load(listOf(fact1, fact2, rule1))
+
+        val result = Program.query(Atom("c")).toList()
+
+        assertEquals(1, result.size, "Expected 1 result")
+    }
+
+    @Test
+    fun `requires querying with variable`() {
+        val fact1 = Fact(Atom("a"))
+        val fact2 = Fact(Atom("b"))
+        val rule1 = Rule(
+            Structure(Atom("has fact"), listOf(Variable("X"))),
+            Variable("X")
+        )
+
+        Program.load(listOf(fact1, fact2, rule1))
+
+        val result = Program.query(Structure(Atom("has fact"), listOf(Atom("a")))).toList()
+
+        assertEquals(1, result.size, "Expected 1 result")
+        assertTrue(result[0].isSuccess, "Expected success")
+        val subs = result[0].getOrNull()!!
+        assertEquals(0, subs.size, "Expected no substitutions")
+    }
+
+    @Nested
+    class `requires querying with filled variable` {
+        @BeforeEach
+        fun setup() {
+            val fact1 = Fact(Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza"))))
+            val fact2 = Fact(Structure(Atom("likes"), listOf(Atom("alice"), Atom("pasta"))))
+            val fact3 = Fact(Structure(Atom("likes"), listOf(Atom("bob"), Atom("pasta"))))
+            val rule1 = Rule(
+                Structure(Atom("likes_italian_food"), listOf(Variable("Person"))),
+                Disjunction(
+                    Structure(Atom("likes"), listOf(Variable("Person"), Atom("pizza"))),
+                    Structure(Atom("likes"), listOf(Variable("Person"), Atom("pasta")))
+                )
+            )
+
+            Program.clear()
+            Program.load(listOf(fact1, fact2, fact3, rule1))
+        }
+
+        @Test
+        fun `likes_italian_food(alice)`() {
+            val result = Program.query(Structure(Atom("likes_italian_food"), listOf(Atom("alice")))).toList()
+
+            assertEquals(2, result.size, "Expected 2 results")
+
+            assertTrue(result[0].isSuccess, "Expected success")
+            val subs1 = result[0].getOrNull()!!
+            assertEquals(0, subs1.size, "Expected no substitutions")
+
+            assertTrue(result[1].isSuccess, "Expected success")
+            val subs2 = result[1].getOrNull()!!
+            assertEquals(0, subs2.size, "Expected no substitutions")
+        }
+
+        @Test
+        fun `likes_italian_food(X)`() {
+            val result = Program.query(Structure(Atom("likes_italian_food"), listOf(Variable("X")))).toList()
+
+            assertEquals(3, result.size, "Expected 3 results")
+
+            assertTrue(result[0].isSuccess, "Expected success")
+            val subs3 = result[0].getOrNull()!!
+            assertEquals(1, subs3.size, "Expected 1 substitution, especially without 'Person'")
+            assertEquals(Atom("alice"), subs3[Variable("X")], "Expected alice")
+
+            assertTrue(result[1].isSuccess, "Expected success")
+            val subs4 = result[1].getOrNull()!!
+            assertEquals(1, subs4.size, "Expected 1 substitution, especially without 'Person'")
+            assertEquals(Atom("alice"), subs4[Variable("X")], "Expected alice")
+
+            assertTrue(result[2].isSuccess, "Expected success")
+            val subs5 = result[2].getOrNull()!!
+            assertEquals(1, subs5.size, "Expected 1 substitution, especially without 'Person'")
+            assertEquals(Atom("bob"), subs5[Variable("X")], "Expected bob")
+        }
+    }
+}

tests/prolog/logic/TermsTests.kt

@@ -0,0 +1,109 @@
+package prolog.logic
+
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.Assertions.assertEquals
+import org.junit.jupiter.api.Assertions.assertTrue
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Structure
+import prolog.ast.terms.Variable
+
+class TermsTests {
+    @Test
+    fun `rename vars in atom`() {
+        val term = Atom("a")
+        val start = 0
+
+        val (end, subs) = numbervars(term, start)
+
+        assertEquals(start, end, "Expected end to still be at start")
+        assertTrue(subs.isEmpty(), "Expected no substitutions")
+    }
+
+    @Test
+    fun `rename vars in var`() {
+        val term = Variable("X")
+        val start = 0
+
+        val (end, subs) = numbervars(term, start)
+
+        assertEquals(start + 1, end, "Expected end to be incremented by 1")
+        assertEquals(1, subs.size, "Expected one substitution")
+        assertTrue(subs.containsKey(term), "Expected subs to contain the original term")
+        assertEquals(Variable("X($start)"), subs[term], "Expected subs to contain the new term")
+    }
+
+    @Test
+    fun `rename vars in compound term without vars`() {
+        val term = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
+        val start = 0
+
+        val (end, subs) = numbervars(term, start)
+
+        assertEquals(start, end, "Expected end to still be at start")
+        assertTrue(subs.isEmpty(), "Expected no substitutions")
+    }
+
+    @Test
+    fun `rename vars in compound term`() {
+        val term = Structure(Atom("f"), listOf(Variable("X"), Variable("Y")))
+        val start = 0
+
+        val (end, subs) = numbervars(term, start)
+
+        assertEquals(start + 2, end, "Expected end to be incremented by 2")
+        assertEquals(2, subs.size, "Expected two substitutions")
+        assertTrue(subs.containsKey(term.arguments[0]), "Expected subs to contain the first original term")
+        assertEquals(Variable("X($start)"), subs[term.arguments[0]], "Expected subs to contain the new term")
+        assertTrue(subs.containsKey(term.arguments[1]), "Expected subs to contain the second original term")
+        assertEquals(Variable("Y(${start + 1})"), subs[term.arguments[1]], "Expected subs to contain the new term")
+    }
+
+    @Test
+    fun `renaming identical vars should keep the same name`() {
+        val term = Structure(Atom("f"), listOf(Variable("X"), Variable("X")))
+        val start = 0
+
+        val (end, subs) = numbervars(term, start)
+
+        assertEquals(start + 1, end, "Expected end to be incremented by 1")
+        assertEquals(1, subs.size, "Expected one substitution")
+        assertTrue(subs.containsKey(term.arguments[0]), "Expected subs to contain the first original term")
+        assertEquals(Variable("X($start)"), subs[term.arguments[0]], "Expected subs to contain the new term")
+        assertTrue(subs.containsKey(term.arguments[1]), "Expected subs to contain the second original term")
+        assertEquals(Variable("X($start)"), subs[term.arguments[1]], "Expected subs to contain the new term")
+    }
+
+    @Test
+    fun `renaming identical vars should keep the same name in nested terms`() {
+        val term = Structure(Atom("f"), listOf(Variable("X"), Structure(Atom("g"), listOf(Variable("X")))))
+        val start = 0
+
+        val (end, subs) = numbervars(term, start)
+
+        assertEquals(start + 1, end, "Expected end to be incremented by 1")
+        assertEquals(1, subs.size, "Expected one substitution")
+        assertTrue(subs.containsKey(Variable("X")), "Expected subs to contain the variable")
+        assertEquals(Variable("X($start)"), subs[term.arguments[0]], "Expected subs to contain the new term")
+    }
+
+    @Test
+    fun `renaming multiple times`() {
+        val variable = Variable("X")
+        val term = Structure(Atom("f"), listOf(variable))
+        val start = 0
+
+        val (end1, subs1) = numbervars(term, start, emptyMap())
+
+        assertEquals(start + 1, end1, "Expected end to be incremented by 1")
+        assertEquals(1, subs1.size, "Expected one substitution")
+        assertTrue(subs1.containsKey(variable), "Expected subs to contain the variable")
+        assertEquals(Variable("X($start)"), subs1[variable], "Expected subs to contain the new term")
+
+        val (end2, subs2) = numbervars(term, end1, subs1)
+
+        assertEquals(start + 2, end2, "Expected end to be incremented by 2")
+        assertEquals(1, subs2.size, "Expected one substitution")
+        assertTrue(subs2.containsKey(variable), "Expected subs to contain the variable")
+        assertEquals(Variable("X($end1)"), subs2[variable], "Expected subs to contain the new term")
+    }
+}