Sync

.idea/2025LogProg-PrologInterpreter.iml

@@ -0,0 +1,8 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<module version="4">
+  <component name="AdditionalModuleElements">
+    <content url="file://$MODULE_DIR$" dumb="true">
+      <sourceFolder url="file://$MODULE_DIR$/examples" type="java-resource" />
+    </content>
+  </component>
+</module>

.idea/modules.xml

@@ -0,0 +1,8 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project version="4">
+  <component name="ProjectModuleManager">
+    <modules>
+      <module fileurl="file://$PROJECT_DIR$/.idea/2025LogProg-PrologInterpreter.iml" filepath="$PROJECT_DIR$/.idea/2025LogProg-PrologInterpreter.iml" />
+    </modules>
+  </component>
+</project>

build.gradle.kts

@@ -10,6 +10,8 @@ repositories {
 }
 
 dependencies {
+    // CLI argument parsing
+    implementation("com.xenomachina:kotlin-argparser:2.0.7")
     // Parser combinator library
     implementation("com.github.h0tk3y.betterParse:better-parse:0.4.4")
 
@@ -26,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,32 @@
-choice(X) :- X = 1, !; X = 2.
+% choice(X) :- X = 1, !; X = 2.
+:- dynamic declaration/1.
+
+add_declaration_first(NewDecl) :-
+    asserta(declaration(NewDecl)).
+
+add_declaration_last(NewDecl) :-
+    assertz(declaration(NewDecl)).
+
+database :-
+    add_declaration_first('Man is born free, and everywhere he is in chains.'),
+    retract(declaration(_)),
+    add_declaration_last('The revolution devours its own children.'),
+    add_declaration_first('I disapprove of what you say, but I will defend to the death your right to say it.'),
+    add_declaration_first('Give me Liberty, or give me Death!'),
+    add_declaration_last('So this is how liberty dies, with thunderous applause.').
+
+show_declarations :-
+    declaration(Decl),
+    write(Decl), nl,
+    fail.
+
+show_declarations.
+
+:- initialization(main).
+
+main :-
+    database,
+    show_declarations,
+    retractall(declaration(_)),
+    show_declarations.
+

src/Debug.kt

@@ -1,3 +0,0 @@
-data object Debug {
-    val on: Boolean = true
-}

src/Main.kt

@@ -1,98 +1,29 @@
-import better_parser.PrologParser
+import com.xenomachina.argparser.ArgParser
-import better_parser.SimpleReplParser
+import interpreter.FileLoader
-import interpreter.SourceFileReader
+import io.GhentPrologArgParser
-import prolog.Answer
+import io.Logger
-import prolog.Program
+import repl.Repl
-import prolog.ast.logic.Fact
-import prolog.ast.logic.Rule
-import prolog.ast.terms.Atom
-import prolog.ast.terms.CompoundTerm
-import prolog.ast.terms.Variable
-import prolog.builtins.Conjunction
 
-fun help(): String {
+fun main(args: Array<String>) {
-    println("Unknown command. Type 'h' for help.")
+    // Parse command line arguments
-    println("Commands:")
+    val parsedArgs = ArgParser(args).parseInto(::GhentPrologArgParser)
-    println("  ;   - find next solution")
-    println("  a   - abort")
-    println("  .   - end query")
-    println("  h   - help")
-    println("  exit - exit Prolog REPL")
-    return ""
-}
 
-fun say(message: String) {
+    parsedArgs.run {
-    println(message)
+        val loader = FileLoader()
-}
 
-fun prompt(message: String): String {
+        // Set the verbosity level
-    print("$message ")
+        Logger.level = verbosity
-    var input: String = readlnOrNull() ?: help()
-    while (input.isBlank()) {
-        input = readlnOrNull() ?: help()
-    }
-    return input
-}
 
-fun prettyResult(result: Answer): String {
+        // Check if script was provided
-    result.fold(
+        for (file in script) {
-        onSuccess = {
+            loader.load(file)
-            val subs = result.getOrNull()!!
-            if (subs.isEmpty()) {
-                return "true."
-            }
-            return subs.entries.joinToString(", ") { "${it.key} = ${it.value}" }
-        },
-        onFailure = {
-            return "Failure: ${result.exceptionOrNull()!!}"
         }
-    )
-}
 
-val knownCommands = setOf(";", "a", ".")
+        // Check if REPL was requested
-
+        if (repl) {
-fun main() {
+            Repl()
-    SourceFileReader().readFile("tests/better_parser/resources/parent.pl")
+        } else {
-
+            Logger.warn("REPL not started. Use -r or --repl to start the REPL.")
-    val parser = SimpleReplParser(debug = false)
-
-    say("Prolog REPL. Type 'exit' to quit.")
-
-    while (true) {
-        val queryString = prompt("?-")
-
-        try {
-            val query = parser.parse(queryString)
-            val answers = query.satisfy(emptyMap())
-
-            if (answers.none()) {
-                say("false.")
-            } else {
-                val iterator = answers.iterator()
-
-                var previous = iterator.next()
-
-                while (iterator.hasNext()) {
-                    var command = prompt(prettyResult(previous))
-
-                    while (command !in knownCommands) {
-                        say("Unknown action: $command (h for help)")
-                        command = prompt("Action?")
-                    }
-
-                    when (command) {
-                        ";" -> previous = iterator.next()
-                        "a" -> break
-                        "." -> break
-                    }
-                }
-
-                say(prettyResult(previous))
-            }
-
-        } catch (e: Exception) {
-            println("Error: ${e.message}")
         }
     }
-
 }

src/better_parser/PrologParser.kt

@@ -1,17 +0,0 @@
-package better_parser
-
-import com.github.h0tk3y.betterParse.grammar.Grammar
-import com.github.h0tk3y.betterParse.grammar.parseToEnd
-import prolog.Program
-import prolog.ast.logic.Clause
-import prolog.ast.terms.Atom
-
-class PrologParser {
-    private val parser: Grammar<List<Clause>> = SimpleSourceParser() as Grammar<List<Clause>>
-
-    public fun parse(input: String) {
-        val clauses: List<Clause> = parser.parseToEnd(input)
-
-        Program.load(clauses)
-    }
-}

src/better_parser/PrologSourceParser.kt

@@ -1,70 +0,0 @@
-package better_parser
-
-import com.github.h0tk3y.betterParse.combinators.*
-import com.github.h0tk3y.betterParse.grammar.Grammar
-import com.github.h0tk3y.betterParse.lexer.literalToken
-import com.github.h0tk3y.betterParse.lexer.regexToken
-import com.github.h0tk3y.betterParse.parser.Parser
-import prolog.ast.logic.Fact
-import prolog.ast.arithmetic.Integer
-import prolog.ast.arithmetic.Float
-import prolog.ast.logic.Clause
-import prolog.ast.logic.LogicOperand
-import prolog.ast.logic.Rule
-import prolog.ast.terms.*
-import prolog.builtins.Conjunction
-import prolog.builtins.Disjunction
-
-class PrologSourceParser : Grammar<List<Clause>>() {
-    // Define the tokens
-    private val atom by regexToken("[a-z][a-zA-Z0-9_]*")
-    private val variable by regexToken("[A-Z][a-zA-Z0-9_]*")
-    private val number by regexToken("-?[0-9]+(\\.[0-9]+)?")
-    private val whitespace by regexToken("\\s+", ignore = true)
-
-    private val comma by literalToken(",")
-    private val semicolon by literalToken(";")
-    private val neck by literalToken(":-")
-    private val lparen by literalToken("(")
-    private val rparen by literalToken(")")
-    private val dot by literalToken(".")
-
-    private val atomParser by atom use { Atom(text) }
-    private val variableParser by variable use { Variable(text) }
-    private val intParser by number use { Integer(text.toInt()) }
-    private val floatParser by number use { Float(text.toFloat()) }
-    private val numberParser by (intParser or floatParser)
-    private val compoundTermParser by (atomParser and skip(lparen) and separated(
-        atomParser or variableParser,
-        comma
-    ) and skip(rparen)) use {
-        CompoundTerm(t1, t2.terms)
-    }
-
-    private val termParser: Parser<Term> by (numberParser or variableParser or compoundTermParser or atomParser)
-
-    private val logicOperandParser: Parser<LogicOperand> by (termParser or compoundTermParser or atomParser) map {
-        it as LogicOperand
-    }
-
-    private val conjunctionParser: Parser<Conjunction> by (logicOperandParser and comma and logicOperandParser) use {
-        Conjunction(t1, t3)
-    }
-    private val disjunctionParser: Parser<Disjunction> by (logicOperandParser and semicolon and logicOperandParser) use {
-        Disjunction(t1, t3)
-    }
-
-    private val operatorParser: Parser<Operator> by (conjunctionParser or disjunctionParser)
-
-    private val headParser by (compoundTermParser or atomParser)
-    private val bodyParser by (operatorParser or compoundTermParser or atomParser)
-
-    private val factParser by (headParser and dot) use { Fact(t1 as Head) }
-    private val ruleParser by (headParser and neck and bodyParser and dot) use {
-        Rule(t1 as Head, t3 as Body)
-    }
-
-    private val clauseParser: Parser<Clause> by (factParser or ruleParser)
-
-    override val rootParser: Parser<List<Clause>> by zeroOrMore(clauseParser)
-}

src/better_parser/SimplePrologParser.kt

@@ -1,67 +0,0 @@
-package better_parser
-
-import com.github.h0tk3y.betterParse.combinators.*
-import com.github.h0tk3y.betterParse.grammar.Grammar
-import com.github.h0tk3y.betterParse.grammar.parser
-import com.github.h0tk3y.betterParse.lexer.Token
-import com.github.h0tk3y.betterParse.lexer.literalToken
-import com.github.h0tk3y.betterParse.lexer.regexToken
-import com.github.h0tk3y.betterParse.lexer.token
-import com.github.h0tk3y.betterParse.parser.Parser
-import prolog.ast.arithmetic.Float
-import prolog.ast.arithmetic.Integer
-import prolog.ast.terms.Atom
-import prolog.ast.terms.Structure
-import prolog.ast.terms.Term
-import prolog.ast.terms.Variable
-
-open class SimplePrologParser : Grammar<Any>() {
-    // Prolog tokens
-    protected val nameToken: Token by regexToken("[a-z][a-zA-Z0-9_]*")
-    protected val variableToken: Token by regexToken("[A-Z][a-zA-Z0-9_]*")
-
-    // Arithmetic tokens
-    private val floatToken: Token by regexToken("-?[1-9][0-9]*\\.[0-9]+")
-    private val integerToken: Token by regexToken("-?([1-9][0-9]*|0)")
-
-    // Special tokens
-    protected val neck by literalToken(":-")
-    protected val comma: Token by literalToken(",")
-    protected val leftParenthesis: Token by literalToken("(")
-    protected val rightParenthesis: Token by literalToken(")")
-    protected val dot by literalToken(".")
-
-    // Ignored tokens
-    protected val whitespace: Token by regexToken("\\s+", ignore = true)
-    protected val singleLineComment: Token by regexToken("%[^\\n]*", ignore = true)
-    protected val multiLineComment: Token by regexToken("/\\*.*?\\*/", ignore = true)
-
-    protected val dummy by token { _, _ -> -1 } use { throw IllegalStateException("This parser should not be used") }
-
-    // Prolog parsers
-    protected val variable: Parser<Variable> by variableToken use { Variable(text) }
-    protected val atom: Parser<Atom> by nameToken use { Atom(text) }
-    protected val compound: Parser<Structure> by (atom and skip(leftParenthesis) and separated(
-        parser(::term),
-        comma,
-        acceptZero = true
-    ) and skip(rightParenthesis)) use {
-        Structure(t1, t2.terms)
-    }
-
-    // Arithmetic parsers
-    private val int: Parser<Integer> by integerToken use { Integer(text.toInt()) }
-    private val float: Parser<Float> by floatToken use {
-        Float(text.toFloat())
-    }
-
-    protected val term: Parser<Term> by (dummy
-            or float
-            or int
-            or variable
-            or compound
-            or atom
-    ) map { it }
-
-    override val rootParser: Parser<Any> = term
-}

src/better_parser/SimpleReplParser.kt

@@ -1,27 +0,0 @@
-package better_parser
-
-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.parseToEnd
-import com.github.h0tk3y.betterParse.parser.Parser
-import prolog.ast.logic.LogicOperand
-import prolog.builtins.Query
-
-class SimpleReplParser(val debug: Boolean = false) : SimpleSourceParser() {
-    override val rootParser: Parser<Query> by (body * -dot) use { Query(this as LogicOperand) }
-
-    fun parse(input: String): Query {
-        if (debug) {
-            println("Parsing input: $input")
-        }
-
-        val query = parseToEnd(input) as Query
-
-        if (debug) {
-            println("Parsed query: $query")
-        }
-
-        return query
-    }
-}

src/better_parser/SimpleSourceParser.kt

@@ -1,48 +0,0 @@
-package better_parser
-
-import com.github.h0tk3y.betterParse.combinators.*
-import com.github.h0tk3y.betterParse.grammar.parser
-import com.github.h0tk3y.betterParse.lexer.literalToken
-import com.github.h0tk3y.betterParse.parser.Parser
-import prolog.ast.arithmetic.ArithmeticOperator
-import prolog.ast.logic.*
-import prolog.ast.terms.*
-import prolog.builtins.Conjunction
-import prolog.builtins.Disjunction
-
-open class SimpleSourceParser : SimplePrologParser() {
-    protected val simpleLogicOperand: Parser<LogicOperand> by (dummy
-            or compound
-            or atom
-            )
-    protected val logicOperand: Parser<LogicOperand> by (dummy
-        or parser(::operator)
-        or simpleLogicOperand
-    )
-
-    protected val arithmeticOperator: Parser<ArithmeticOperator> by dummy
-    protected val logicOperator: Parser<LogicOperator> by (simpleLogicOperand * comma * logicOperand) use {
-        Conjunction(t1, t3)
-    }
-
-    protected val operator: Parser<Operator> by (arithmeticOperator or logicOperator) use { this as Operator }
-
-    protected val head: Parser<Head> by (dummy
-            or compound
-            or atom
-            )
-    protected val body: Parser<Body> by (dummy
-            or operator
-            or head
-            ) use { this as Body }
-
-    // ----
-
-    private val rule: Parser<Rule> by (head * -neck * body) use { Rule(t1, t2) }
-    private val fact: Parser<Fact> by head use { Fact(this) }
-
-    private val clause: Parser<Clause> by ((rule or fact) * -dot)
-    private val clauses: Parser<List<Clause>> by zeroOrMore(clause)
-
-    override val rootParser: Parser<Any> by clauses
-}

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

@@ -0,0 +1,55 @@
+package interpreter
+
+import io.Logger
+import parser.ScriptParser
+import prolog.ast.Database
+import prolog.ast.Database.Program
+import prolog.ast.logic.Clause
+import prolog.ast.logic.Predicate
+
+class FileLoader {
+    private val parser = ScriptParser()
+
+    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)
+
+        Logger.debug("Adding clauses to program")
+        addToProgram(clauses, filePath)
+
+        Logger.debug("Finished loading file: $filePath")
+    }
+
+    fun readFile(filePath: String): String {
+        try {
+            Logger.debug("Reading $filePath")
+            val file = java.io.File(filePath)
+
+            if (!file.exists()) {
+                Logger.error("File $filePath does not exist")
+                throw IllegalArgumentException("File not found: $filePath")
+            }
+
+            return file.readText()
+        } catch (e: Exception) {
+            Logger.error("Error reading file: $filePath")
+            throw RuntimeException("Error reading file: $filePath", e)
+        }
+    }
+
+    fun addToProgram(clauses: List<Clause>, filePath: String) {
+        Logger.debug("Grouping clauses by functor")
+        val groupedClauses = clauses.groupBy { it.functor }
+        val predicates: List<Predicate> = groupedClauses.map { (_, clauses) ->
+            Predicate(clauses)
+        }
+
+        val database = Database(filePath)
+        predicates.forEach { database.load(it) }
+        Program.consult(database)
+    }
+}

src/interpreter/Preprocessor.kt

@@ -0,0 +1,141 @@
+package interpreter
+
+import io.Logger
+import prolog.ast.arithmetic.Expression
+import prolog.ast.arithmetic.Integer
+import prolog.ast.logic.Clause
+import prolog.ast.logic.Fact
+import prolog.ast.logic.LogicOperand
+import prolog.ast.logic.Rule
+import prolog.ast.terms.*
+import prolog.builtins.*
+
+/**
+ * Preprocessor for Prolog
+ *
+ * This class preprocesses Prolog code and applies various transformations such as recognizing builtins.
+ */
+open class Preprocessor {
+    /**
+     * Preprocesses the input Prolog code.
+     *
+     * @param input The already parsed Prolog code as a list of clauses.
+     * @return The preprocessed Prolog code as a list of clauses.
+     */
+    fun preprocess(input: List<Clause>): List<Clause> {
+        return input.map { preprocess(it) }
+    }
+
+    fun preprocess(input: Query): Query {
+        return Query(preprocess(input.query) as Goal)
+    }
+
+    private fun preprocess(clause: Clause): Clause {
+        return when (clause) {
+            is Fact -> {
+                Fact(preprocess(clause.head) as Head)
+            }
+
+            is Rule -> {
+                Rule(
+                    preprocess(clause.head) as Head,
+                    preprocess(clause.body as Term) as Body
+                )
+            }
+
+            else -> clause
+        }
+    }
+
+    protected open fun preprocess(term: Term, nested: Boolean = false): Term {
+        val prepped = when (term) {
+            Atom("true") -> True
+            Structure(Atom("true"), emptyList()) -> True
+            Atom("false") -> False
+            Structure(Atom("false"), emptyList()) -> False
+            Atom("fail") -> Fail
+            Structure(Atom("fail"), emptyList()) -> Fail
+            Atom("!") -> Cut()
+            Structure(Atom("!"), emptyList()) -> Cut()
+            Atom("inf") -> Integer(Int.MAX_VALUE)
+            Atom("nl") -> Nl
+            Variable("_") -> AnonymousVariable.create()
+            is Structure -> {
+                // Preprocess the arguments first to recognize builtins
+                val args = term.arguments.map { preprocess(it, nested = true) }
+
+                when {
+                    // TODO Remove hardcoding by storing the functors as constants in operators?
+
+                    term.functor == ":-/2" -> Rule( args[0] as Head, args[1] as Body )
+
+                    // Logic
+                    term.functor == "=/2" -> Unify(args[0], args[1])
+                    term.functor == "\\=/2" -> NotUnify(args[0], args[1])
+                    term.functor == ",/2" -> Conjunction(args[0] as LogicOperand, args[1] as LogicOperand)
+                    term.functor == ";/2" -> Disjunction(args[0] as LogicOperand, args[1] as LogicOperand)
+                    term.functor == "\\+/1" -> Not(args[0] as Goal)
+                    term.functor == "==/2" -> Equivalent(args[0], args[1])
+
+                    term.functor == "=\\=/2" && args.all { it is Expression } -> EvaluatesToDifferent(args[0] as Expression, args[1] as Expression)
+                    term.functor == "=:=/2" && args.all { it is Expression } -> EvaluatesTo(args[0] as Expression, args[1] as Expression)
+                    term.functor == "is/2" && args.all { it is Expression } -> Is(args[0] as Expression, args[1] as Expression)
+
+                    // Arithmetic
+
+                    term.functor == "-/1" && args.all { it is Expression } -> Negate(args[0] as Expression)
+                    term.functor == "-/2" && args.all { it is Expression } -> Subtract(args[0] as Expression, args[1] as Expression)
+                    term.functor == "+/1" && args.all { it is Expression } -> Positive(args[0] as Expression)
+                    term.functor == "+/2" && args.all { it is Expression } -> Add(args[0] as Expression, args[1] as Expression)
+                    term.functor == "*/2" && args.all { it is Expression } -> Multiply(args[0] as Expression, args[1] as Expression)
+                    term.functor == "//2" && args.all { it is Expression } -> Divide(args[0] as Expression, args[1] as Expression)
+                    term.functor == "between/3" && args.all { it is Expression } -> Between(args[0] as Expression, args[1] as Expression, args[2] as Expression)
+
+                    // Database
+                    term.functor == "dynamic/1" -> Dynamic((args[0] as Atom).name)
+                    term.functor == "retract/1" -> Retract(args[0])
+                    term.functor == "assert/1" -> {
+                        if (args[0] is Rule) {
+                            Assert(args[0] as Rule)
+                        } else {
+                            Assert(Fact(args[0] as Head))
+                        }
+                    }
+                    term.functor == "asserta/1" -> {
+                        if (args[0] is Rule) {
+                            AssertA(args[0] as Rule)
+                        } else {
+                            AssertA(Fact(args[0] as Head))
+                        }
+                    }
+                    term.functor == "assertz/1" -> {
+                        if (args[0] is Rule) {
+                            AssertZ(args[0] as Rule)
+                        } else {
+                            AssertZ(Fact(args[0] as Head))
+                        }
+                    }
+
+                    // 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.arguments = args
+                        term
+                    }
+                }
+            }
+
+            else -> term
+        }
+
+        Logger.debug(
+            "Preprocessed term $term into $prepped (kind ${prepped::class.simpleName})",
+            !nested && (prepped != term || prepped::class != term::class)
+        )
+
+        return prepped
+    }
+}

src/interpreter/SourceFileReader.kt

@@ -1,23 +0,0 @@
-package interpreter
-
-import better_parser.PrologParser
-
-class SourceFileReader {
-    private val parser = PrologParser()
-
-    fun readFile(filePath: String) {
-        return try {
-            val file = java.io.File(filePath)
-            if (!file.exists()) {
-                throw IllegalArgumentException("File not found: $filePath")
-            }
-
-            val content = file.readText()
-
-            // Parse the content using SimpleSourceParser
-            parser.parse(content)
-        } catch (e: Exception) {
-            throw RuntimeException("Error reading file: $filePath", e)
-        }
-    }
-}

src/io/GhentPrologArgParser.kt

@@ -0,0 +1,21 @@
+package io
+
+import com.xenomachina.argparser.ArgParser
+import com.xenomachina.argparser.default
+
+class GhentPrologArgParser(parser: ArgParser) {
+    val script by parser.adding("-s", "--script", help = "Script to run")
+    val repl by parser.flagging("-r", "--repl", help = "Start the REPL")
+
+    val verbosity by parser.mapping(
+        "--vvv" to Logger.Level.DEBUG,
+        "--debug" to Logger.Level.DEBUG,
+        "--vv" to Logger.Level.INFO,
+        "--verbose" to Logger.Level.INFO,
+        "--info" to Logger.Level.INFO,
+        "-v" to Logger.Level.WARN,
+        "--warn" to Logger.Level.WARN,
+        "--error" to Logger.Level.ERROR,
+        help = "Set the verbosity level (default: WARN)",
+    ).default(Logger.defaultLevel)
+}

src/io/IoHandler.kt

@@ -0,0 +1,10 @@
+package io
+
+interface IoHandler {
+    fun prompt(
+        message: String,
+        hint: () -> String = { "Please enter a valid input." }
+    ): String
+
+    fun say(message: String)
+}

src/io/Logger.kt

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

src/io/Terminal.kt

@@ -0,0 +1,71 @@
+package io
+
+import prolog.ast.Database.Program
+import java.io.BufferedReader
+import java.io.BufferedWriter
+import java.io.InputStream
+import java.io.OutputStream
+
+/**
+ * Handles input and output from a terminal.
+ */
+class Terminal(
+    inputStream: InputStream = System.`in`,
+    outputStream: OutputStream = System.`out`,
+    errorStream: OutputStream = System.err
+) : IoHandler {
+    val input: BufferedReader = inputStream.bufferedReader()
+    val output: BufferedWriter = outputStream.bufferedWriter()
+    val error: BufferedWriter = errorStream.bufferedWriter()
+
+    override fun prompt(
+        message: String,
+        hint: () -> String
+    ): String {
+        say("$message ")
+        var input: String = readLine()
+        while (input.isBlank()) {
+            say(hint(), error)
+            input = readLine()
+        }
+        return input
+    }
+
+    override fun say(message: String) {
+        output.write(message)
+        output.flush()
+    }
+
+    fun say(message: String, writer: BufferedWriter = output) {
+        writer.write(message)
+        writer.flush()
+    }
+
+    /**
+     * Reads a line from the input stream.
+     */
+    fun readLine(reader: BufferedReader = input): String {
+        val line = reader.readLine()
+        if (line == null) {
+            Logger.info("End of stream reached")
+            cleanup()
+        }
+        return line
+
+    }
+
+    fun cleanup() {
+        Logger.info("Closing terminal streams")
+        input.close()
+        output.close()
+        error.close()
+        System.exit(0)
+    }
+
+    fun checkNewLine() {
+        if (Program.storeNewLine) {
+            say("\n")
+            Program.storeNewLine = false
+        }
+    }
+}

src/lexer/Lexer.kt

@@ -1,127 +0,0 @@
-package lexer
-
-import lexer.errors.LexingError
-import lexer.errors.LexingErrorType
-import lexer.state.LexerPosition
-import lexer.state.TokenPosition
-
-class Lexer(private val source: String) {
-    private var tokens: List<Token> = emptyList()
-    private val position = LexerPosition(0, 0, -1)
-
-    /**
-     * Scans the source code and returns a list of tokens.
-     * @return List of [Token]s
-     */
-    fun scan(): List<Token> {
-        while (hasNext()) {
-            val char: Char = peek()
-            tokens += when {
-                char == '(' -> scanSymbol(TokenType.PARENTHESIS_LEFT)
-                char == ')' -> scanSymbol(TokenType.PARENTHESIS_RIGHT)
-                char == '.' -> scanSymbol(TokenType.DOT)
-                char == '"' -> scanQuotedString()
-                char == '%' -> { scanComment(); continue }
-                char.isLetterOrDigit() -> scanAlphanumeric()
-                char.isWhitespace()    -> { scanWhitespace(); continue }
-                else -> throw LexingError(LexingErrorType.UNKNOWN_TOKEN, "Did not recognize $char", position)
-            }
-        }
-        tokens += Token(TokenType.EOF, "EOF", getPosition(0))
-        return tokens
-    }
-
-    private fun hasNext(): Boolean {
-        // Check if the position is within the source length
-        return position.offset < source.length
-    }
-
-    private fun peek(): Char {
-        // Peek should only be called if there is a next character
-        require(hasNext()) {
-            LexingError(LexingErrorType.UNEXPECTED_END_OF_INPUT, "Expected additional character", position)
-        }
-
-        return source[position.offset]
-    }
-
-    private fun next(): Char {
-        // Advance the position and return the character
-        val char = peek()
-        position.offset++
-        position.column++
-        return char
-    }
-
-    private fun getPosition(length: Int = 1): TokenPosition {
-        // Return a new TokenPosition based on the current LexerPosition
-        return TokenPosition(position.line, position.column, length)
-    }
-
-    /* * * * * * *
-     * Scanners  *
-     * * * * * * */
-
-    /**
-     * Scans a symbol token, given the expected [TokenType].
-     * @param tokenType The expected [TokenType]
-     * @return The scanned [Token]
-     */
-    private fun scanSymbol(tokenType: TokenType): Token {
-        return Token(tokenType, next().toString(), getPosition(1))
-    }
-
-    private fun scanAlphanumeric(): Token {
-        // Scan all alphanumeric characters
-        var length = 0
-        while (hasNext() && peek().isLetterOrDigit()) {
-            next()
-            length++
-        }
-        val value = source.substring(position.offset - length, position.offset)
-        return Token(TokenType.ALPHANUMERIC, value, getPosition(length))
-    }
-
-    private fun scanQuotedString(): Token {
-        // "Assert" that the next character is the start of a quoted string
-        require(next() == '"') {
-            LexingError(LexingErrorType.UNEXPECTED_TOKEN, "Expected opening quote '('", position)
-        }
-
-        var length = 0
-        while (hasNext() && peek() != '"') {
-            next()
-            length++
-        }
-
-        // "Assert" that the next character is the end of the quoted string
-        require(next() == '"') {
-            LexingError(LexingErrorType.UNEXPECTED_TOKEN, "Expected closing quote ')'", position)
-        }
-
-        val value = source.substring(position.offset - length - 1, position.offset - 1)
-        return Token(TokenType.ALPHANUMERIC, value, getPosition(length))
-    }
-
-    private fun scanComment() {
-        // "Assert" that the next character is the start of a comment
-        require(next() == '%') {
-            LexingError(LexingErrorType.UNEXPECTED_TOKEN, "Expected opening comment '%'", position)
-        }
-
-        // Skip all characters until the end of the line
-        while (hasNext() && peek() != '\n') {
-            next()
-        }
-    }
-
-    private fun scanWhitespace() {
-        // Skip all whitespace characters
-        while (hasNext() && peek().isWhitespace()) {
-            if (next() == '\n') {
-                position.line++
-                position.column = 0
-            }
-        }
-    }
-}

src/lexer/Token.kt

@@ -1,9 +0,0 @@
-package lexer
-
-import lexer.state.TokenPosition
-
-data class Token(
-    val type: TokenType,
-    val value: String,
-    val position: TokenPosition
-)

src/lexer/TokenType.kt

@@ -1,15 +0,0 @@
-package lexer
-
-enum class TokenType {
-    ALPHANUMERIC,
-    // TODO Replace with SMALL_LETTER, CAPITAL_LETTER, DIGIT, HEX_DIGIT, ... ?
-
-    // Structure
-    COMMA,
-    DOT,
-    PARENTHESIS_LEFT, PARENTHESIS_RIGHT,
-
-    // Special
-
-    EOF
-}

src/lexer/errors/LexingError.kt

@@ -1,13 +0,0 @@
-package lexer.errors
-
-import lexer.state.LexerPosition
-
-data class LexingError(
-    val type: LexingErrorType,
-    override val message: String,
-    val position: LexerPosition
-) : Throwable(
-    """
-    ${position.line}:${position.column + 1} ${type}: $message
-""".trimIndent()
-)

src/lexer/errors/LexingErrorType.kt

@@ -1,7 +0,0 @@
-package lexer.errors
-
-enum class LexingErrorType {
-    UNKNOWN_TOKEN,
-    UNEXPECTED_TOKEN,
-    UNEXPECTED_END_OF_INPUT,
-}

src/lexer/state/LexerPosition.kt

@@ -1,3 +0,0 @@
-package lexer.state
-
-data class LexerPosition(var offset: Int, var line: Int, var column: Int)

src/lexer/state/TokenPosition.kt

@@ -1,3 +0,0 @@
-package lexer.state
-
-data class TokenPosition(val line: Int, val column: Int, val length: Int)

src/parser/Parser.kt

@@ -1,137 +1,11 @@
 package parser
 
-import lexer.Token
+interface Parser {
-import lexer.TokenType
-import parser.errors.ParsingError
-import parser.errors.ParsingErrorType
-import parser.state.ParserPosition
-import prolog.ast.logic.Clause
-import prolog.ast.logic.Fact
-import prolog.ast.logic.Rule
-import prolog.ast.terms.Atom
-import prolog.ast.terms.Structure
-import prolog.ast.terms.Term
-
-class Parser(private val tokens: List<Token>) {
-    private val position: ParserPosition = ParserPosition(0)
-
-    fun parse(): List<Term> {
-        val terms = mutableListOf<Term>()
-
-        while (hasNext()) {
-            position.save()
-
-            var term: Term? = null
-
-            while (term == null) {
-                // Try each parser rule in order
-
-            }
-
-            require(term != null) {
-                ParsingError(ParsingErrorType.UNEXPECTED_TOKEN, "Expected a term", position)
-            }
-
-            terms.add(term)
-        }
-
-        return terms
-    }
-
     /**
-     * Matches the current token with any of the expected types.
+     * Parses the input string and returns the parsed result.
-     * If it matches, it consumes the token and returns true.
      *
-     * @param types The list of expected token types.
+     * @param input The input string to parse.
-     * @return True if the current token matches any of the expected types, false otherwise.
+     * @return The parsed result, which is the AST of the input.
      */
-    private fun match(types: List<TokenType>): Boolean {
+    fun parse(input: String): Any
-        for (type in types) {
-            if (check(type)) {
-                next()
-                return true
-            }
-        }
-
-        return false
-    }
-
-    /**
-     * Checks if the current token matches the expected type.
-     */
-    private fun check(type: TokenType): Boolean {
-        return hasNext() && peek().type == type
-    }
-
-    private fun hasNext(): Boolean {
-        // Check if the position is within the tokens list
-        // TODO Check for EOF instead?
-        return position.offset < tokens.size
-    }
-
-    private fun peek(): Token {
-        require(hasNext()) { "Unexpected end of input" }
-
-        return tokens[position.offset]
-    }
-
-    private fun next(): Token {
-        val token = peek()
-        position.offset++
-        return token
-    }
-
-    private fun previous(): Token {
-        require(0 < position.offset) { "No previous token" }
-        return tokens[position.offset - 1]
-    }
-
-    /* * * * * *
-     * Parsers *
-     * * * * * */
-
-    private fun parseWithTry(parseRule: () -> Term): Term {
-        try {
-            return parseRule()
-        } catch (e: Exception) {
-            throw ParsingError(ParsingErrorType.UNEXPECTED_TOKEN, "Unexpected token", position)
-        }
-    }
-
-    private fun parseClause(): Clause {
-        return try {
-            Fact(parseStructure())
-        } catch (e: Exception) {
-            Fact(parseAtom())
-        }
-    }
-
-    private fun parseStructure(): Structure {
-        val name = parseAtom()
-        val args = mutableListOf<Term>()
-
-        require(match(listOf(TokenType.PARENTHESIS_LEFT))) {
-            ParsingError(ParsingErrorType.UNEXPECTED_TOKEN, "Expected '(' after structure name", position)
-        }
-
-        // TODO Handle arguments
-
-        require(match(listOf(TokenType.PARENTHESIS_RIGHT))) {
-            ParsingError(ParsingErrorType.UNEXPECTED_TOKEN, "Expected ')' after structure arguments", position)
-        }
-
-        return Structure(name, args)
-    }
-
-    private fun parseAtom(): Atom {
-        return Atom(parseLetterDigit())
-    }
-
-    private fun parseLetterDigit(): String {
-        require(match(listOf(TokenType.ALPHANUMERIC)) && previous().value[0].isLowerCase()) {
-            ParsingError(ParsingErrorType.UNEXPECTED_TOKEN, "Expected lowercase letter", position)
-        }
-
-        return previous().value
-    }
 }

src/parser/ReplParser.kt

@@ -0,0 +1,12 @@
+package parser
+
+import com.github.h0tk3y.betterParse.grammar.Grammar
+import com.github.h0tk3y.betterParse.grammar.parseToEnd
+import parser.grammars.QueryGrammar
+import prolog.builtins.Query
+
+class ReplParser : Parser {
+    private val grammar: Grammar<Query> = QueryGrammar() as Grammar<Query>
+
+    override fun parse(input: String): Query = grammar.parseToEnd(input)
+}

src/parser/ScriptParser.kt

@@ -0,0 +1,18 @@
+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> {
+        val raw = grammar.parseToEnd(input)
+        return preprocessor.preprocess(raw)
+    }
+}

src/parser/errors/ParsingError.kt

@@ -1,12 +0,0 @@
-package parser.errors
-
-import parser.state.ParserPosition
-
-class ParsingError(private val type: ParsingErrorType, override val message: String, private val position: ParserPosition) :
-    Throwable() {
-    override fun toString(): String {
-        return """
-            ($position) ${type}: $message
-        """.trimIndent()
-    }
-}

src/parser/errors/ParsingErrorType.kt

@@ -1,7 +0,0 @@
-package parser.errors
-
-enum class ParsingErrorType {
-    UNEXPECTED_TOKEN,
-
-    INTERNAL_ERROR,
-}

src/parser/grammars/LogicGrammar.kt

@@ -0,0 +1,21 @@
+package parser.grammars
+
+import com.github.h0tk3y.betterParse.combinators.*
+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 constraint or fact) * -dot)
+    protected val clauses: Parser<List<Clause>> by oneOrMore(clause)
+
+    override val rootParser: Parser<Any> by clauses
+}

src/parser/grammars/QueryGrammar.kt

@@ -0,0 +1,16 @@
+package parser.grammars
+
+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.LogicOperand
+import prolog.builtins.Query
+
+class QueryGrammar : TermsGrammar() {
+    protected val query: Parser<Query> by (body * -dot) use {
+        Query(this as LogicOperand)
+    }
+
+    override val rootParser: Parser<Any> by query
+}

src/parser/grammars/TermsGrammar.kt

@@ -0,0 +1,124 @@
+package parser.grammars
+
+import com.github.h0tk3y.betterParse.combinators.*
+import com.github.h0tk3y.betterParse.grammar.parser
+import com.github.h0tk3y.betterParse.parser.Parser
+import prolog.ast.arithmetic.Float
+import prolog.ast.arithmetic.Integer
+import prolog.ast.terms.*
+import prolog.builtins.Dynamic
+
+/**
+ * Precedence is based on the following table:
+ *
+ * | Precedence | Type | Operators                                                                                     |
+ * |------------|------|-----------------------------------------------------------------------------------------------|
+ * | 1200       | xfx  | --\>, :-, =\>, ==\>                                                                           |
+ * | 1200       | fx   | :-, ?-                                                                                        |
+ * | 1150       | fx   | dynamic                                                                                       |
+ * | 1105       | xfy  | |                                                                                             |
+ * | 1100       | xfy  | ;                                                                                             |
+ * | 1050       | xfy  | ->, *->                                                                                       |
+ * | 1000       | xfy  | ,                                                                                             |
+ * | 990        | xfx  | :=                                                                                            |
+ * | 900        | fy   | \+                                                                                            |
+ * | 700        | xfx  | <, =, =.., =:=, =<, ==, =\=, >, >=, \=, \==, as, is, >:<, :<                                  |
+ * | 600        | xfy  | :                                                                                             |
+ * | 500        | yfx  | +, -, /\, \/, xor                                                                             |
+ * | 500        | fx   | ?                                                                                             |
+ * | 400        | yfx  | *, /, //, div, rdiv, <<, >>, mod, rem                                                         |
+ * | 200        | xfx  | **                                                                                            |
+ * | 200        | xfy  | ^                                                                                             |
+ * | 200        | fy   | +, -, \                                                                                       |
+ * | 100        | yfx  | .                                                                                             |
+ * | 1          | fx   | $                                                                                             |
+ *
+ * It is very easy to extend this grammar to support more operators. Just add them at the appropriate rule or create a
+ * new rule and chain it to the existing ones.
+ *
+ * @see [SWI-Prolog Predicate op/3](https://www.swi-prolog.org/pldoc/man?predicate=op/3)
+ */
+open class TermsGrammar : Tokens() {
+    // Basic named terms
+    protected val variable: Parser<Variable> by (variableToken or anonymousVariableToken) use { Variable(text) }
+    protected val simpleAtom: Parser<Atom> by (nameToken or exclamation) use { Atom(text) }
+    protected val quotedAtom: Parser<Atom> by (dummy
+            or ticked
+            or doubleTicked
+            or backTicked
+            ) use { Atom(text.substring(1, text.length - 1)) }
+    protected val atom: Parser<Atom> by (quotedAtom or simpleAtom)
+    protected val compound: Parser<Structure> by (atom * -leftParenthesis * separated(
+        parser(::termNoConjunction),
+        comma,
+        acceptZero = true
+    ) * -rightParenthesis) use {
+        Structure(t1, t2.terms)
+    }
+
+    // Basic arithmetic
+    protected val int: Parser<Integer> by integerToken use { Integer(text.toInt()) }
+    protected val float: Parser<Float> by floatToken use { Float(text.toFloat()) }
+
+    protected val functor: Parser<String> by (nameToken * divide * int) use { "${t1.text}${t2.text}$t3" }
+
+    // Base terms (atoms, compounds, variables, numbers)
+    protected val baseTerm: Parser<Term> by (dummy
+            or (-leftParenthesis * parser(::term) * -rightParenthesis)
+            or compound
+            or atom
+            or variable
+            or float
+            or int
+            )
+
+    protected val op200: Parser<CompoundTerm> by ((plus or minus) * parser(::term200)) use {
+        CompoundTerm(Atom(t1.text), listOf(t2))
+    }
+    protected val term200: Parser<Term> by (op200 or baseTerm)
+
+    protected val op400: Parser<String> by (multiply or divide) use { text }
+    protected val term400: Parser<Term> by (term200 * zeroOrMore(op400 * term200)) use {
+        t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
+    }
+
+    protected val op500: Parser<String> by (plus or minus) use { text }
+    protected val term500: Parser<Term> by (term400 * zeroOrMore(op500 * term400)) use {
+        t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
+    }
+
+    protected val op700: Parser<String> by (equivalent or equals or notEquals or isOp) use { text }
+    protected val term700: Parser<Term> by (term500 * optional(op700 * term500)) use {
+        if (t2 == null) t1 else CompoundTerm(Atom(t2!!.t1), listOf(t1, t2!!.t2))
+    }
+
+    protected val op1000: Parser<String> by (comma) use { text }
+    protected val term1000: Parser<Term> by (term700 * zeroOrMore(op1000 * term700)) use {
+        t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
+    }
+
+    protected val op1100: Parser<String> by (semicolon) use { text }
+    protected val term1100: Parser<Term> by (term1000 * zeroOrMore(op1100 * term1000)) use {
+        t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
+    }
+
+    protected val dynamic: Parser<Term> by (dynamicOp * functor) use {
+        CompoundTerm( Atom(t1.text), listOf(Atom(t2)) )
+    }
+    protected val term1150: Parser<Term> by (dynamic or term1100) use { this }
+
+    protected val op1200: Parser<String> by (neck) use { text }
+    protected val term1200: Parser<Term> by (term1150 * zeroOrMore(op1200 * term1100)) use {
+        t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
+    }
+
+    // Term - highest level expression
+    protected val term: Parser<Term> by term1200
+    protected val termNoConjunction: Parser<Term> by term700
+
+    // Parts for clauses
+    protected val head: Parser<Head> by (compound or atom)
+    protected val body: Parser<Body> by term use { this as Body }
+
+    override val rootParser: Parser<Any> by term
+}

src/parser/grammars/Tokens.kt

@@ -0,0 +1,56 @@
+package parser.grammars
+
+import com.github.h0tk3y.betterParse.combinators.use
+import com.github.h0tk3y.betterParse.grammar.Grammar
+import com.github.h0tk3y.betterParse.lexer.Token
+import com.github.h0tk3y.betterParse.lexer.literalToken
+import com.github.h0tk3y.betterParse.lexer.regexToken
+import com.github.h0tk3y.betterParse.lexer.token
+
+abstract class Tokens : Grammar<Any>() {
+    protected val leftParenthesis: Token by literalToken("(")
+    protected val rightParenthesis: Token by literalToken(")")
+    protected val exclamation: Token by literalToken("!")
+    // 1200
+    protected val neck by literalToken(":-")
+    // 1150
+    protected val dynamicOp by literalToken("dynamic")
+    // 1100
+    protected val semicolon: Token by literalToken(";")
+    // 1000
+    protected val comma: Token by literalToken(",")
+    // 700
+    protected val equivalent: Token by literalToken("==")
+    protected val equals: Token by literalToken("=")
+    protected val isOp: Token by literalToken("is")
+    // 500
+    protected val plus: Token by literalToken("+")
+    protected val minus: Token by literalToken("-")
+    protected val notEquals: Token by literalToken("\\=")
+    // 400
+    protected val multiply: Token by literalToken("*")
+    protected val divide: Token by literalToken("/")
+    // 100
+    protected val dot by literalToken(".")
+
+    // Prolog tokens
+    protected val nameToken: Token by regexToken("[a-z][a-zA-Z0-9_]*")
+    protected val variableToken: Token by regexToken("[A-Z][a-zA-Z0-9_]*")
+    protected val anonymousVariableToken: Token by literalToken("_")
+
+    // Arithmetic tokens
+    protected val floatToken: Token by regexToken("-?[1-9][0-9]*\\.[0-9]+")
+    protected val integerToken: Token by regexToken("-?([1-9][0-9]*|0)")
+
+    // Ignored tokens
+    protected val whitespace: Token by regexToken("\\s+", ignore = true)
+    protected val singleLineComment: Token by regexToken("%[^\\n]*", ignore = true)
+    protected val multiLineComment: Token by regexToken("/\\*.*?\\*/", ignore = true)
+
+    protected val ticked: Token by regexToken("'[^']*'")
+    protected val doubleTicked: Token by regexToken("\"[^\"]*\"")
+    protected val backTicked: Token by regexToken("`[^`]*`")
+
+    // Helper
+    protected val dummy by token { _, _ -> -1 } use { throw IllegalStateException("This parser should not be used") }
+}

src/parser/state/ParserPosition.kt

@@ -1,25 +0,0 @@
-package parser.state
-
-import parser.errors.ParsingError
-import parser.errors.ParsingErrorType
-
-data class ParserPosition(var offset: Int) {
-    private val checkpoints: ArrayDeque<ParserPosition> = ArrayDeque()
-
-    fun save() {
-        checkpoints.addLast(this.copy())
-    }
-
-    fun reload() {
-        require(checkpoints.isNotEmpty()) {
-            ParsingError(ParsingErrorType.INTERNAL_ERROR, "No checkpoint to reload from", this)
-        }
-
-        val checkpoint = checkpoints.removeLast()
-        offset = checkpoint.offset
-    }
-
-    override fun toString(): String {
-        return "at $offset"
-    }
-}

src/prolog/Program.kt

@@ -1,80 +0,0 @@
-package prolog
-
-import Debug
-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 Program: Resolvent {
-    var predicates: Map<Functor, Predicate> = emptyMap()
-
-    init {
-        setup()
-    }
-
-    private fun setup() {
-        if (Debug.on) {
-            println("Setting up Prolog program...")
-        }
-        // Initialize the program with built-in predicates
-        load(listOf(
-        ))
-    }
-
-    /**
-     * Queries the program with a goal.
-     * @return true if the goal can be proven, false otherwise.
-     */
-    fun query(goal: Goal): Answers = solve(goal, emptyMap())
-
-    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)))
-            }
-        }
-    }
-
-    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() {
-        predicates = emptyMap()
-        setup()
-    }
-}

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,130 @@
+package prolog.ast
+
+import io.Logger
+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
+ */
+open class Database(val sourceFile: String) {
+    var predicates: Map<Functor, Predicate> = emptyMap()
+
+    /**
+     * Initializes the database by running the initialization clauses of that database.
+     */
+    fun initialize() {
+        databases.add(this)
+
+        if (sourceFile !== "") {
+            Logger.debug("Moving clauses from $sourceFile to main database")
+            predicates.filter { it.key != "/_" }
+                .forEach { (_, predicate) -> db.load(predicate, force = true) }
+        }
+
+        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()
+            }
+        }
+    }
+
+    /**
+     * Loads a list of clauses into the program.
+     *
+     * @param clauses The list of clauses to load.
+     * @param index The index at which to insert the clause. If null, the clause is added to the end of the list.
+     * @param force If true, the clause is added even if the predicate is static.
+     */
+    fun load(clauses: List<Clause>, index: Int? = null, force: Boolean = false) {
+        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, index, force)
+            } else {
+                // If the predicate does not exist, create a new one, usually during Program execution, so dynamic.
+                predicates += Pair(functor, Predicate(listOf(clause), dynamic = true))
+            }
+
+            Logger.debug("Loaded clause $clause into predicate $functor")
+        }
+    }
+
+    fun load(predicate: Predicate, force: Boolean = false) {
+        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() {
+        if (sourceFile == "") {
+            Logger.debug("Clearing main database")
+            predicates = emptyMap()
+            return
+        }
+
+        Logger.debug("Clearing database $sourceFile")
+        // Remove our clauses from the database
+        predicates.forEach { (_, predicate) ->
+            val dbPredicate = db.predicates[predicate.functor]
+            predicate.clauses.forEach { clause -> dbPredicate?.clauses?.remove(clause) }
+        }
+        databases.remove(this)
+    }
+
+    /**
+     * Object to handle execution
+     *
+     * This object is a singleton that manages a list of databases.
+     */
+    companion object Program : Resolvent {
+        var db = Database("")
+        var databases: MutableList<Database> = mutableListOf(db)
+        var storeNewLine: Boolean = false
+        var variableRenamingStart: Int = 0
+
+        /**
+         * Queries the program with a goal.
+         * @return true if the goal can be proven, false otherwise.
+         */
+        fun query(goal: Goal): Answers = solve(goal, emptyMap())
+
+        override fun solve(goal: Goal, subs: Substitutions): Answers {
+            val functor = goal.functor
+            // If the predicate does not exist, return false
+            val predicate = db.predicates[functor] ?: return emptySequence()
+            // If the predicate exists, evaluate the goal against it
+            return predicate.solve(goal, subs)
+        }
+
+        fun consult(database: Database) = database.initialize()
+        fun disregard(database: Database) = database.clear()
+
+        fun load(clauses: List<Clause>, index: Int? = null, force: Boolean = false) = db.load(clauses, index, force)
+
+        fun reset() {
+            databases.toList().map { it.clear() }
+            variableRenamingStart = 0
+            storeNewLine = false
+        }
+    }
+}

src/prolog/ast/arithmetic/Float.kt

@@ -1,6 +1,7 @@
 package prolog.ast.arithmetic
 
 import prolog.Substitutions
+import prolog.ast.terms.Term
 
 class Float(override val value: kotlin.Float): Number {
     // Floats are already evaluated
@@ -31,4 +32,18 @@ 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()
+    }
+
+    override fun clone(): Float = Float(value)
+    override fun applySubstitution(subs: Substitutions): Float = this
 }

src/prolog/ast/arithmetic/Integer.kt

@@ -1,11 +1,16 @@
 package prolog.ast.arithmetic
 
+import prolog.Answers
 import prolog.Substitutions
+import prolog.ast.logic.LogicOperand
+import prolog.ast.terms.Term
 
-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) {
@@ -37,4 +42,7 @@ data class Integer(override val value: Int) : Number {
         is Integer -> Integer(value * other.value)
         else -> throw IllegalArgumentException("Cannot multiply $this and $other")
     }
+
+    override fun clone(): Integer = Integer(value)
+    override fun applySubstitution(subs: Substitutions): Integer = this
 }

src/prolog/ast/logic/Clause.kt

@@ -1,13 +1,14 @@
 package prolog.ast.logic
 
 import prolog.Answers
+import prolog.ast.Database.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.occurs
 import prolog.logic.unifyLazy
 
 /**
@@ -15,29 +16,45 @@ import prolog.logic.unifyLazy
  *
  * A clause consists of a [Head] and body separated by the neck operator, or it is a [Fact].
  *
- * @see [prolog.ast.terms.Variable]
+ * @see [Variable]
  * @see [Predicate]
  */
-abstract class Clause(val head: Head, val body: Body) : Resolvent {
+abstract class Clause(var head: Head, var body: Body) : Term, 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 ->
+        val preHead = applySubstitution(head, subs)
+        val preGoal = applySubstitution(goal, subs)
+
+        val (headEnd, headRenaming) = numbervars(preHead, Program.variableRenamingStart, subs)
+        val headReverse = headRenaming.entries.associate { (a, b) -> b to a }
+        Program.variableRenamingStart = headEnd
+
+        val renamedHead = applySubstitution(head, headRenaming)
+        unifyLazy(preGoal, renamedHead, subs).forEach { headAnswer ->
+            headAnswer.map { headSubs ->
                 // If the body can be proven, yield the (combined) substitutions
-                body.satisfy(subs + newHeadSubs).forEach { bodyAnswer ->
+                val preBody = applySubstitution(body, headRenaming + headSubs) as Body
+                preBody.satisfy(subs).forEach { bodyAnswer ->
                     bodyAnswer.fold(
-                        onSuccess = { newBodySubs ->
+                        onSuccess = { bodySubs ->
-                            yield(Result.success(newHeadSubs + newBodySubs))
+                            var result = (headSubs + bodySubs)
+                                .mapKeys { applySubstitution(it.key, headReverse) }
+                                .mapValues { applySubstitution(it.value, headReverse) }
+                            result = result.map { it.key to applySubstitution(it.value, result) }
+                                .toMap()
+                                .filterNot { it.key in headRenaming.keys && !occurs(it.key as Variable, goal, emptyMap())}
+                            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 +69,19 @@ 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()
+    override fun equals(other: Any?): Boolean {
-            else -> "$head :- $body"
+        if (this === other) return true
-        }
+        if (other !is Clause) return false
+
+        if (head != other.head) return false
+        if (body != other.body) return false
+
+        return true
+    }
+
+    override fun hashCode(): Int {
+        return super.hashCode()
     }
 }

src/prolog/ast/logic/Fact.kt

@@ -1,6 +1,12 @@
 package prolog.ast.logic
 
+import prolog.Substitutions
 import prolog.ast.terms.Head
+import prolog.ast.terms.Term
 import prolog.builtins.True
+import prolog.logic.applySubstitution
 
-class Fact(head: Head) : Clause(head, True)
+class Fact(head: Head) : Clause(head, True) {
+    override fun clone(): Fact = Fact(head)
+    override fun applySubstitution(subs: Substitutions): Fact = Fact(applySubstitution(head as Term, subs) as Head)
+}

src/prolog/ast/logic/Predicate.kt

@@ -15,48 +15,54 @@ import prolog.flags.AppliedCut
 class Predicate : Resolvent {
     val functor: Functor
     val clauses: MutableList<Clause>
+    var dynamic = false
 
     /**
      * Creates a predicate with the given functor and an empty list of clauses.
      */
-    constructor(functor: Functor) {
+    constructor(functor: Functor, dynamic: Boolean = false) {
         this.functor = functor
         this.clauses = mutableListOf()
+        this.dynamic = dynamic
     }
 
     /**
      * Creates a predicate with the given clauses.
      */
-    constructor(clauses: List<Clause>) {
+    constructor(clauses: List<Clause>, dynamic: Boolean = false) {
         this.functor = clauses.first().functor
-
         require(clauses.all { it.functor == functor }) { "All clauses must have the same functor" }
         this.clauses = clauses.toMutableList()
+        this.dynamic = dynamic
     }
 
     /**
      * Adds a clause to the predicate.
+     *
+     * @param clause The clause to add.
+     * @param index The index at which to insert the clause. If null, the clause is added to the end of the list.
+     * @param force If true, the clause is added even if the predicate is static.
      */
-    fun add(clause: Clause) {
+    fun add(clause: Clause, index: Int? = null, force: Boolean = false) {
         require(clause.functor == functor) { "Clause functor does not match predicate functor" }
+        require(dynamic || force) { "No permission to modify static procedure '$functor'" }
 
-        if (Debug.on) {
+        if (index != null) clauses.add(index, clause) else clauses.add(clause)
-            println("Adding clause $clause to predicate $functor")
-        }
-
-        clauses.add(clause)
     }
 
     /**
      * Adds a list of clauses to the predicate.
      */
-    fun addAll(clauses: List<Clause>) {
+    fun addAll(clauses: List<Clause>, force: Boolean = false) {
         require(clauses.all { it.functor == functor }) { "All clauses must have the same functor" }
+        require(dynamic || force) { "No permission to modify static procedure '$functor'" }
+
         this.clauses.addAll(clauses)
     }
 
     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/logic/Rule.kt

@@ -1,6 +1,15 @@
 package prolog.ast.logic
 
+import prolog.Substitutions
 import prolog.ast.terms.Body
 import prolog.ast.terms.Head
+import prolog.ast.terms.Term
+import prolog.logic.applySubstitution
 
-class Rule(head: Head, body: Body) : Clause(head, body)
+class Rule(head: Head, body: Body) : Clause(head, body) {
+    override fun clone(): Rule = Rule(head, body)
+    override fun applySubstitution(subs: Substitutions): Rule = Rule(
+        head = applySubstitution(head as Term, subs) as Head,
+        body = applySubstitution(body, subs) as Body
+    )
+}

src/prolog/ast/terms/AnonymousVariable.kt

@@ -0,0 +1,21 @@
+package prolog.ast.terms
+
+import io.Logger
+import prolog.Substitutions
+
+class AnonymousVariable(private val id: Int) : Variable("_$id") {
+    companion object {
+        private var counter = 0
+        fun create(): AnonymousVariable {
+            val id = counter
+            counter++
+            Logger.debug("Creating anonymous variable: _${id}")
+            return AnonymousVariable(id)
+        }
+    }
+
+    override fun toString(): String = "_"
+
+    override fun clone(): AnonymousVariable = AnonymousVariable(id)
+    override fun applySubstitution(subs: Substitutions): AnonymousVariable = this
+}

src/prolog/ast/terms/Atom.kt

@@ -21,4 +21,7 @@ open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
     override fun hashCode(): Int {
         return javaClass.hashCode()
     }
+
+    override fun clone(): Atom = Atom(name)
+    override fun applySubstitution(subs: Substitutions): Atom = Atom(name)
 }

src/prolog/ast/terms/Body.kt

@@ -2,4 +2,4 @@ package prolog.ast.terms
 
 import prolog.ast.logic.Satisfiable
 
-interface Body : Satisfiable
+interface Body : Term, Satisfiable

src/prolog/ast/terms/Goal.kt

@@ -1,7 +1,7 @@
 package prolog.ast.terms
 
 import prolog.Answers
-import prolog.Program
+import prolog.ast.Database.Program
 import prolog.Substitutions
 import prolog.ast.logic.LogicOperand
 

src/prolog/ast/terms/Operator.kt

@@ -6,7 +6,7 @@ abstract class Operator(
     private val symbol: Atom,
     private val leftOperand: Operand? = null,
     private val rightOperand: Operand
-) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)) {
+) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)), Term {
     override fun toString(): String {
         return when (leftOperand) {
             null -> "${symbol.name} $rightOperand"

src/prolog/ast/terms/Structure.kt

@@ -3,6 +3,7 @@ package prolog.ast.terms
 import prolog.Answers
 import prolog.Substitutions
 import prolog.ast.logic.Resolvent
+import prolog.logic.applySubstitution
 import prolog.logic.unifyLazy
 
 typealias Argument = Term
@@ -22,4 +23,21 @@ open class Structure(val name: Atom, var arguments: List<Argument>) : Goal(), He
             else -> "${name.name}(${arguments.joinToString(", ")})"
         }
     }
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (other !is Structure) return false
+        if (functor != other.functor) return false
+        return arguments.zip(other.arguments).all { (a, b) -> a == b }
+    }
+
+    override fun hashCode(): Int {
+        return javaClass.hashCode()
+    }
+
+    override fun clone(): Structure = Structure(name, arguments)
+    override fun applySubstitution(subs: Substitutions): Structure = Structure(
+        name,
+        arguments.map { applySubstitution(it, subs) }
+    )
 }

src/prolog/ast/terms/Term.kt

@@ -1,14 +1,19 @@
 package prolog.ast.terms
 
+import prolog.Substitutions
 import prolog.logic.compare
+import prolog.ast.arithmetic.Integer
+import prolog.ast.arithmetic.Float
 
 /**
  * Value in Prolog.
  *
- * A [Term] is either a [Variable], [Atom], [Integer][prolog.ast.arithmetic.Integer],
+ * A [Term] is either a [Variable], [Atom], [Integer],
- * [Float][prolog.ast.arithmetic.Float] or [CompoundTerm].
+ * [Float] or [CompoundTerm].
  * In addition, SWI-Prolog also defines the type TODO string.
  */
-interface Term : Comparable<Term> {
+interface Term : Comparable<Term>, Cloneable {
     override fun compareTo(other: Term): Int = compare(this, other, emptyMap())
+    fun applySubstitution(subs: Substitutions): Term
+    public override fun clone(): Term
 }

src/prolog/ast/terms/Variable.kt

@@ -1,10 +1,12 @@
 package prolog.ast.terms
 
+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, Expression {
+open 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
@@ -16,5 +18,28 @@ 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 equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (other == null || other !is Variable) return false
+        return name == other.name
+    }
+
+    override fun hashCode(): Int {
+        return name.hashCode()
+    }
+
     override fun toString(): String = name
+
+    override fun clone(): Variable = Variable(name)
+    override fun applySubstitution(subs: Substitutions): Variable = this
 }

src/prolog/builtins/arithmeticOperators.kt

@@ -62,11 +62,11 @@ 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) :
+class Is(val number: Expression, val expr: Expression) :
-    Operator(Atom("is"), left, right), Satisfiable {
+    Operator(Atom("is"), number, expr), Satisfiable {
     override fun satisfy(subs: Substitutions): Answers {
-        val t1 = left.simplify(subs)
+        val t1 = number.simplify(subs)
-        val t2 = right.simplify(subs)
+        val t2 = expr.simplify(subs)
 
         if (!atomic(t2.to, subs)) {
             return sequenceOf(Result.failure(IllegalArgumentException("Right operand must be instantiated")))
@@ -119,7 +119,7 @@ open class Subtract(private val expr1: Expression, private val expr2: Expression
 /**
  * Result = Expr1 * Expr2
  */
-class Multiply(private val expr1: Expression, private val expr2: Expression) :
+class Multiply(val expr1: Expression, val expr2: Expression) :
     ArithmeticOperator(Atom("*"), expr1, expr2) {
     override fun simplify(subs: Substitutions): Simplification {
         val result = Variable("Result")
@@ -144,7 +144,7 @@ class Divide(private val expr1: Expression, private val expr2: Expression) :
 // TODO Expr rem Expr
 
 class Between(private val expr1: Expression, private val expr2: Expression, private val expr3: Expression) :
-    Operator(Atom("between"), expr1, expr2) {
+    CompoundTerm(Atom("between"), listOf(expr1, expr2, expr3)), Satisfiable {
     override fun satisfy(subs: Substitutions): Answers {
         val e1 = expr1.simplify(subs)
         val e2 = expr2.simplify(subs)
@@ -152,8 +152,8 @@ class Between(private val expr1: Expression, private val expr2: Expression, priv
 
         require(e1.to is Integer && e2.to is Integer) { "Arguments must be integers" }
 
-        val v1 = e1.to as Integer
+        val v1 = e1.to
-        val v2 = e2.to as Integer
+        val v2 = e2.to
 
         return if (variable(e3.to, subs)) {
             between(v1, v2, e3.to as Variable).map { answer ->
@@ -165,4 +165,6 @@ class Between(private val expr1: Expression, private val expr2: Expression, priv
             }
         }
     }
+
+    override fun toString(): String = "$expr1..$expr3..$expr2"
 }

src/prolog/builtins/controlOperators.kt

@@ -3,10 +3,11 @@ package prolog.builtins
 import prolog.Answers
 import prolog.Substitutions
 import prolog.ast.logic.LogicOperand
+import prolog.ast.logic.LogicOperator
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Body
 import prolog.ast.terms.Goal
-import prolog.ast.logic.LogicOperator
+import prolog.ast.terms.Structure
 import prolog.flags.AppliedCut
 
 /**
@@ -34,6 +35,8 @@ class Cut() : Atom("!") {
     override fun satisfy(subs: Substitutions): Answers {
         return sequenceOf(Result.failure(AppliedCut(emptyMap())))
     }
+
+    override fun applySubstitution(subs: Substitutions): Cut = Cut()
 }
 
 /**
@@ -94,6 +97,11 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
             )
         }
     }
+
+    override fun applySubstitution(subs: Substitutions): Conjunction = Conjunction(
+        left.applySubstitution(subs) as LogicOperand,
+        right.applySubstitution(subs) as LogicOperand
+    )
 }
 
 /**
@@ -105,6 +113,12 @@ open class Disjunction(private val left: LogicOperand, private val right: LogicO
         yieldAll(left.satisfy(subs))
         yieldAll(right.satisfy(subs))
     }
+
+    override fun clone(): Disjunction = Disjunction(left.clone() as LogicOperand, right.clone() as LogicOperand)
+    override fun applySubstitution(subs: Substitutions): Disjunction = Disjunction(
+        left.applySubstitution(subs) as LogicOperand,
+        right.applySubstitution(subs) as LogicOperand
+    )
 }
 
 @Deprecated("Use Disjunction instead")
@@ -120,7 +134,8 @@ class Bar(leftOperand: LogicOperand, rightOperand: LogicOperand) : Disjunction(l
 class Not(private val goal: Goal) : LogicOperator(Atom("\\+"), rightOperand = goal) {
     override fun satisfy(subs: Substitutions): Answers {
         // If the goal can be proven, return an empty sequence
-        if (goal.satisfy(subs).toList().isNotEmpty()) {
+        val goalResults = goal.satisfy(subs).iterator()
+        if (goalResults.hasNext()) {
             return emptySequence()
         }
         // If the goal cannot be proven, return a sequence with an empty map

src/prolog/builtins/databaseOperators.kt

@@ -0,0 +1,116 @@
+package prolog.builtins
+
+import prolog.Answers
+import prolog.Substitutions
+import prolog.ast.logic.Clause
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Structure
+import prolog.ast.logic.Predicate
+import prolog.ast.Database.Program
+import prolog.ast.terms.Functor
+import prolog.ast.terms.Term
+import prolog.ast.logic.Fact
+import prolog.ast.Database
+import prolog.ast.terms.Body
+import prolog.ast.terms.Goal
+import prolog.ast.terms.Operator
+import prolog.logic.applySubstitution
+import prolog.logic.unifyLazy
+
+/**
+ * (Make) the [Predicate] with the corresponding [Functor] dynamic.
+ */
+class Dynamic(private val dynamicFunctor: Functor): Goal(), Body {
+    override val functor: Functor = "dynamic/1"
+
+    override fun satisfy(subs: Substitutions): Answers {
+        val predicate = Program.db.predicates[dynamicFunctor]
+        if (predicate == null) {
+            return sequenceOf(Result.failure(Exception("Predicate $dynamicFunctor not found")))
+        }
+
+        predicate.dynamic = true
+        return sequenceOf(Result.success(emptyMap()))
+    }
+
+    override fun toString(): String = "dynamic $dynamicFunctor"
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (other !is Dynamic) return false
+        return dynamicFunctor == other.dynamicFunctor
+    }
+
+    override fun hashCode(): Int = super.hashCode()
+
+    override fun clone(): Dynamic = Dynamic(dynamicFunctor)
+    override fun applySubstitution(subs: Substitutions): Dynamic = Dynamic(dynamicFunctor)
+}
+
+class Assert(clause: Clause) : AssertZ(clause) {
+    override val functor: Functor = "assert/1"
+}
+
+/**
+ * Assert a [Clause] as a first clause of the [Predicate] into the [Program].
+ */
+class AssertA(val clause: Clause) : Operator(Atom("asserta"), null, clause) {
+    override fun satisfy(subs: Substitutions): Answers {
+        // Add clause to the program
+        val evaluatedClause = applySubstitution(clause, subs) as Clause
+        Program.load(listOf(evaluatedClause), 0)
+
+        return sequenceOf(Result.success(emptyMap()))
+    }
+}
+
+/**
+ * Assert a [Clause] as a last clause of the [Predicate] into the [Program].
+ */
+open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause) {
+    override fun satisfy(subs: Substitutions): Answers {
+        // Add clause to the program
+        val evaluatedClause = applySubstitution(clause, subs) as Clause
+        Program.load(listOf(evaluatedClause))
+
+        return sequenceOf(Result.success(emptyMap()))
+    }
+}
+
+/**
+ * When [Term] is an [Atom] or a term, it is unified with the first unifying [Clause] in the [Database].
+ * The [Fact] or Clause is removed from the Database. It respects the logical update view.
+ *
+ * @see [SWI-Prolog Predicate retract/1](https://www.swi-prolog.org/pldoc/doc_for?object=retract/1)
+ */
+class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
+    override fun satisfy(subs: Substitutions): Answers = sequence {
+        // Check that term is a structure or atom
+        if (term !is Structure && term !is Atom) {
+            yield(Result.failure(Exception("Cannot retract a non-structure or non-atom")))
+            return@sequence
+        }
+
+        val functorName = term.functor
+
+        val predicate = Program.db.predicates[functorName]
+        if (predicate == null) {
+            return@sequence
+        }
+
+        predicate.clauses.toList().forEach { clause ->
+            unifyLazy(term, clause.head, subs).forEach { unifyResult ->
+                unifyResult.fold(
+                    onSuccess = { substitutions ->
+                        // If unification is successful, remove the clause
+                        predicate.clauses.remove(clause)
+                        yield(Result.success(substitutions))
+                    },
+                    onFailure = {
+                        // If unification fails, do nothing
+                    }
+                )
+            }
+        }
+    }
+}

src/prolog/builtins/ioOperators.kt

@@ -0,0 +1,75 @@
+package prolog.builtins
+
+import io.Logger
+import io.Terminal
+import parser.ReplParser
+import prolog.Answers
+import prolog.ast.Database.Program
+import prolog.Substitutions
+import prolog.ast.logic.Satisfiable
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Operator
+import prolog.ast.terms.Term
+import prolog.logic.applySubstitution
+import prolog.logic.unifyLazy
+
+/**
+ * Write [Term] to the current output, using brackets and operators where appropriate.
+ */
+class Write(private val term: Term) : Operator(Atom("write"), null, term), Satisfiable {
+    override fun satisfy(subs: Substitutions): Answers {
+        val t = applySubstitution(term, subs)
+
+        Terminal().say(t.toString())
+
+        Program.storeNewLine = true
+
+        return sequenceOf(Result.success(emptyMap()))
+    }
+
+    override fun toString(): String = "write($term)"
+}
+
+/**
+ * Write a newline character to the current output stream.
+ */
+object Nl : Atom("nl"), Satisfiable {
+    override fun satisfy(subs: Substitutions): Answers {
+        Terminal().say("\n")
+        Program.storeNewLine = false
+        return sequenceOf(Result.success(emptyMap()))
+    }
+}
+
+/**
+ * Read the next Prolog term from the current input stream and unify it with [Term].
+ *
+ * On reaching end-of-file, [Term] is unified with the [Atom] `end_of_file`.
+ */
+class Read(private val term: Term) : Operator(Atom("read"), null, term), Satisfiable {
+    private val io = Terminal()
+    private val parser = ReplParser()
+
+    private fun readTerm(): Term {
+        val input = io.readLine()
+        Logger.debug("Read input: $input")
+
+        return when (input) {
+            "end_of_file" -> Atom("end_of_file")
+            else -> {
+                val out = parser.parse(input).query
+                Logger.debug("Parsed input: $out")
+                out as? Term ?: throw IllegalArgumentException("Expected a term, but got: $out")
+            }
+        }
+    }
+
+    override fun satisfy(subs: Substitutions): Answers = sequence {
+        val t1 = applySubstitution(term, subs)
+
+        val t2 = readTerm()
+        Logger.debug("Read term: $t2")
+
+        yieldAll(unifyLazy(t1, t2, subs))
+    }
+}

src/prolog/builtins/other.kt

@@ -6,6 +6,11 @@ import prolog.ast.logic.LogicOperand
 import prolog.ast.terms.Atom
 import prolog.ast.logic.LogicOperator
 
-class Query(private val query: LogicOperand) : LogicOperator(Atom("?-"), null, query) {
+class Initialization(val goal: LogicOperand) : LogicOperator(Atom(":-"), null, goal) {
+    override fun satisfy(subs: Substitutions): Answers = goal.satisfy(subs).take(1)
+    override fun toString(): String = goal.toString()
+}
+
+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/arithmetic.kt

@@ -58,7 +58,7 @@ fun succ(term1: Expression, term2: Expression, subs: Substitutions): Answers {
             it.fold(
                 onSuccess = { result ->
                     val t1 = applySubstitution(term1, result)
-                    if (t1 in result) {
+                    if (t1 in result || t1 in result.values) {
                         val e1 = t1.simplify(result)
                         if (e1.to is Integer && e1.to.value < 0) {
                             return@sequence

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).any { (it.key as Variable).name == suggestedName }) {
+                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 = applySubstitution(term, subs) 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

@@ -4,42 +4,52 @@ import prolog.Answer
 import prolog.Answers
 import prolog.Substitutions
 import prolog.ast.arithmetic.Expression
-import prolog.ast.logic.LogicOperator
-import prolog.ast.terms.*
-import kotlin.NoSuchElementException
-import prolog.ast.arithmetic.Number
-import prolog.ast.arithmetic.Integer
 import prolog.ast.arithmetic.Float
+import prolog.ast.arithmetic.Integer
+import prolog.ast.arithmetic.Number
+import prolog.ast.logic.Clause
+import prolog.ast.logic.Fact
+import prolog.ast.logic.LogicOperator
+import prolog.ast.logic.Rule
+import prolog.ast.terms.*
 
 // Apply substitutions to a term
 fun applySubstitution(term: Term, subs: Substitutions): Term = when {
-    variable(term, emptyMap()) -> subs[(term as Variable)] ?: term
+    term is Fact -> term.applySubstitution(subs)
-    atomic(term, subs)   -> term
+
-    compound(term, subs) -> {
+    variable(term, emptyMap()) -> {
-        val structure = term as Structure
+        val variable = term as Variable
-        Structure(structure.name, structure.arguments.map { applySubstitution(it, subs) })
+        subs[variable]?.let { applySubstitution(term = it, subs = subs) } ?: term
     }
+    atomic(term, subs) -> term
+    compound(term, subs) -> {
+        term.applySubstitution(subs)
+    }
+
     else -> term
 }
+
 //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
+    variable(expr, emptyMap()) -> applySubstitution(expr as Term, subs) as Expression
-    atomic(expr, subs)   -> expr
+    atomic(expr, subs) -> expr
     expr is LogicOperator -> {
         expr.arguments = expr.arguments.map { applySubstitution(it, subs) }
         expr
     }
+
     else -> expr
 }
 
 // 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) -> {
         val structure = term as Structure
         structure.arguments.any { occurs(variable, it, subs) }
     }
+
     else -> false
 }
 
@@ -49,19 +59,21 @@ 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)))
             }
         }
+
         compound(t1, subs) && compound(t2, subs) -> {
             val structure1 = t1 as Structure
             val structure2 = t2 as Structure
@@ -75,22 +87,25 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
                     }
                     // Combine the results of all unifications
                     val combinedResults = results.reduce { acc, result ->
-                        acc.flatMap { a -> result.map { b ->
+                        acc.flatMap { a ->
-                            if (a.isSuccess && b.isSuccess) a.getOrThrow() + b.getOrThrow() else emptyMap()
+                            result.map { b ->
-                        } }.map { Result.success(it) }
+                                if (a.isSuccess && b.isSuccess) a.getOrThrow() + b.getOrThrow() else emptyMap()
+                            }
+                        }.map { Result.success(it) }
                     }
                     yieldAll(combinedResults)
                 }
             }
         }
+
         else -> {}
     }
 }
 
 fun unify(term1: Term, term2: Term): Answer {
-    val substitutions = unifyLazy(term1, term2, emptyMap()).toList()
+    val substitutions = unifyLazy(term1, term2, emptyMap()).iterator()
-    return if (substitutions.isNotEmpty()) {
+    return if (substitutions.hasNext()) {
-        substitutions.first()
+        substitutions.next()
     } else {
         Result.failure(NoSuchElementException())
     }
@@ -122,37 +137,40 @@ fun compare(term1: Term, term2: Term, subs: Substitutions): Int {
     return when (t1) {
         is Variable -> {
             when (t2) {
-                is Variable  -> t1.name.compareTo(t2.name)
+                is Variable -> t1.name.compareTo(t2.name)
                 is Number -> -1
-                is Atom      -> -1
+                is Atom -> -1
                 is Structure -> -1
                 else -> throw IllegalArgumentException("Cannot compare $t1 with $t2")
             }
         }
+
         is Number -> {
             when (t2) {
-                is Variable  -> 1
+                is Variable -> 1
-                is Integer   -> (t1.value as Int).compareTo(t2.value)
+                is Integer -> (t1.value as Int).compareTo(t2.value)
-                is Float     -> (t1.value as kotlin.Float).compareTo(t2.value)
+                is Float -> (t1.value as kotlin.Float).compareTo(t2.value)
-                is Atom      -> -1
+                is Atom -> -1
                 is Structure -> -1
                 else -> throw IllegalArgumentException("Cannot compare $t1 with $t2")
             }
         }
+
         is Atom -> {
             when (t2) {
-                is Variable  -> 1
+                is Variable -> 1
                 is Number -> 1
-                is Atom      -> t1.name.compareTo(t2.name)
+                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 Number -> 1
-                is Atom     -> 1
+                is Atom -> 1
                 is Structure -> {
                     val arityComparison = t1.arguments.size.compareTo(t2.arguments.size)
                     if (arityComparison != 0) return arityComparison
@@ -164,9 +182,11 @@ fun compare(term1: Term, term2: Term, subs: Substitutions): Int {
                     }
                     return 0
                 }
+
                 else -> throw IllegalArgumentException("Cannot compare $t1 with $t2")
             }
         }
+
         else -> throw IllegalArgumentException("Cannot compare $t1 with $t2")
     }
 }

src/repl/Repl.kt

@@ -1,4 +1,99 @@
 package repl
 
+import interpreter.Preprocessor
+import io.Logger
+import io.Terminal
+import parser.ReplParser
+import prolog.Answer
+import prolog.Answers
+
 class Repl {
+    private val io = Terminal()
+    private val parser = ReplParser()
+    private val preprocessor = Preprocessor()
+
+    init {
+        welcome()
+        while (true) {
+            try {
+                printAnswers(query())
+            } catch (e: Exception) {
+                Logger.error("Error parsing REPL: ${e.message}")
+            }
+        }
+    }
+
+    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)
+        return query.satisfy(emptyMap())
+    }
+
+    private fun printAnswers(answers: Answers) {
+        val knownCommands = setOf(";", "a", ".", "h")
+
+        val iterator = answers.iterator()
+
+        if (!iterator.hasNext()) {
+            io.say("false.\n")
+        } else {
+            io.say(prettyPrint(iterator.next()))
+
+            while (iterator.hasNext()) {
+                var command = io.prompt("")
+
+                while (command !in knownCommands) {
+                    io.say("Unknown action: $command (h for help)\n")
+                    command = io.prompt("Action?")
+                }
+
+                when (command) {
+                    ";" -> {
+                        io.say(prettyPrint(iterator.next()))
+                    }
+                    "a" -> return
+                    "." -> return
+                    "h" -> {
+                        help()
+                        io.say("Action?")
+                    }
+                }
+            }
+        }
+
+        io.say("\n")
+    }
+
+    private fun help(): String {
+        io.say("Commands:\n")
+        io.say("  ;   find next solution\n")
+        io.say("  a   abort\n")
+        io.say("  .   end query\n")
+        io.say("  h   help\n")
+        return ""
+    }
+
+    private fun prettyPrint(result: Answer): String {
+        result.fold(
+            onSuccess = {
+                val subs = result.getOrNull()!!
+                if (subs.isEmpty()) {
+                    io.checkNewLine()
+                    return "true."
+                }
+                return subs.entries.joinToString(",\n") { "${it.key} = ${it.value}" }
+            },
+            onFailure = {
+                val text = "Failure: ${it.message}"
+                Logger.warn(text)
+                return text
+            }
+        )
+    }
 }

tests/better_parser/SimplePrologPrologParserTests.kt

@@ -1,156 +0,0 @@
-package better_parser
-
-import com.github.h0tk3y.betterParse.grammar.Grammar
-import com.github.h0tk3y.betterParse.grammar.parseToEnd
-import org.junit.jupiter.api.Assertions.assertEquals
-import org.junit.jupiter.api.Assertions.assertTrue
-import org.junit.jupiter.api.BeforeEach
-import org.junit.jupiter.api.Test
-import org.junit.jupiter.params.ParameterizedTest
-import org.junit.jupiter.params.provider.ValueSource
-import prolog.ast.arithmetic.Float
-import prolog.ast.arithmetic.Integer
-import prolog.ast.terms.Atom
-import prolog.ast.terms.Structure
-import prolog.ast.terms.Term
-import prolog.ast.terms.Variable
-import prolog.logic.equivalent
-
-class SimplePrologPrologParserTests {
-    private lateinit var parser: Grammar<Term>
-
-    @BeforeEach
-    fun setup() {
-        parser = SimplePrologParser() as Grammar<Term>
-    }
-
-    @ParameterizedTest
-    @ValueSource(strings = ["a", "foo", "foo1", "fooBar", "foo_bar"])
-    fun `parse atom`(name: String) {
-        val result = parser.parseToEnd(name)
-
-        assertEquals(Atom(name), result, "Expected atom '$name'")
-    }
-
-    @ParameterizedTest
-    @ValueSource(strings = ["X", "X1", "X_1"])
-    fun `parse variable`(name: String) {
-        val result = parser.parseToEnd(name)
-
-        assertEquals(Variable(name), result, "Expected atom '$name'")
-    }
-
-    @Test
-    fun `empty compound term`() {
-        val input = "f()"
-
-        val result = parser.parseToEnd(input)
-
-        assertTrue(
-            equivalent(Structure(Atom("f"), emptyList()), result, emptyMap()),
-            "Expected atom 'f'"
-        )
-    }
-
-    @Test
-    fun `parse compound term f(a)`() {
-        val input = "f(a)"
-
-        val result = parser.parseToEnd(input)
-
-        assertTrue(
-            equivalent(Structure(Atom("f"), listOf(Atom("a"))), result, emptyMap()),
-            "Expected atom 'f(a)'"
-        )
-    }
-
-    @Test
-    fun `parse compound term f(a, b)`() {
-        val input = "f(a, b)"
-
-        val result = parser.parseToEnd(input)
-
-        assertTrue(
-            equivalent(Structure(Atom("f"), listOf(Atom("a"), Atom("b"))), result, emptyMap()),
-            "Expected atom 'f(a, b)'"
-        )
-    }
-
-    @Test
-    fun `parse compound term with variable f(a, X)`() {
-        val input = "f(a, X)"
-
-        val result = parser.parseToEnd(input)
-
-        assertTrue(
-            equivalent(Structure(Atom("f"), listOf(Atom("a"), Variable("X"))), result, emptyMap()),
-            "Expected atom 'f(a, X)'"
-        )
-    }
-
-    @Test
-    fun `parse nested compound term f(a, g(b))`() {
-        val input = "f(a, g(b))"
-
-        val result = parser.parseToEnd(input)
-
-        assertTrue(
-            equivalent(
-                Structure(Atom("f"), listOf(Atom("a"), Structure(Atom("g"), listOf(Atom("b"))))),
-                result,
-                emptyMap()
-            ),
-            "Expected atom 'f(a, g(b))'"
-        )
-    }
-
-    @Test
-    fun `parse compound term with variable f(a, g(X))`() {
-        val input = "f(a, g(X))"
-
-        val result = parser.parseToEnd(input)
-
-        assertTrue(
-            equivalent(
-                Structure(Atom("f"), listOf(Atom("a"), Structure(Atom("g"), listOf(Variable("X"))))),
-                result,
-                emptyMap()
-            ),
-            "Expected atom 'f(a, g(X))'"
-        )
-    }
-
-    @ParameterizedTest
-    @ValueSource(ints = [-987654321, -543, -21, -1, 0, 1, 5, 12, 345, 123456789])
-    fun `parse integer`(number: Int) {
-        val input = number.toString()
-
-        val result = parser.parseToEnd(input)
-
-        assertEquals(Integer(number), result, "Expected integer '$number'")
-    }
-
-    @Test
-    fun `parse float`() {
-        val input = "42.0"
-
-        val result = parser.parseToEnd(input)
-
-        assertTrue(
-            equivalent(Float(42.0f), result, emptyMap()),
-            "Expected float '42.0'"
-        )
-    }
-
-    @Test
-    fun `parse negative float`() {
-        val input = "-42.0"
-
-        val result = parser.parseToEnd(input)
-
-        assertTrue(
-            equivalent(Float(-42.0f), result, emptyMap()),
-            "Expected float '-42.0'"
-        )
-    }
-}

tests/compare.sh

@@ -0,0 +1,75 @@
+#!/usr/bin/env bash
+
+# This script is expected to be run from the root of the project.
+
+WATCH_ALONG=0
+
+# Paths to the two implementations
+GPL="src/gpl"
+SPL="swipl"
+
+GPL_FLAGS=("--error")
+SPL_FLAGS=("--quiet" "-t" "'true'")
+
+# Directory containing test files
+TEST_DIR="examples"
+
+# Temporary files for storing outputs
+GPL_OUT=$(mktemp)
+GPL_ERR=$(mktemp)
+SPL_OUT=$(mktemp)
+SPL_ERR=$(mktemp)
+
+touch "$GPL_OUT" "$GPL_ERR" "$SPL_OUT" "$SPL_ERR"
+
+# 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"
+"examples/basics/unification.pl"
+"examples/basics/write.pl"
+)
+for TESTFILE in "${files[@]}"; do
+    # Run both programs with the test file
+    "${SPL}" "${SPL_FLAGS[@]}" "$TESTFILE" > "${SPL_OUT}" 2> "${SPL_ERR}"
+    "${GPL}" "${GPL_FLAGS[@]}" -s "$TESTFILE" > "${GPL_OUT}" 2> "${GPL_ERR}"
+
+    # Compare the outputs
+    was_different="$(
+        diff -q "$SPL_OUT" "$GPL_OUT" > /dev/null
+        echo $?
+    )"
+    if [[ "${was_different}" -ne 0 || "${WATCH_ALONG}" -eq 1 ]]; then
+        if [ "${was_different}" -ne 0 ]; then
+            message="TEST FAILED"
+        fi
+        printf "%s for %s\n" "${message:="Result"}" "${TESTFILE}"
+        printf "\nTest:\n%s\n" "$(cat "${TESTFILE}")"
+        printf "\nExpected:\n%s\n" "$(cat "${SPL_OUT}" && cat "${SPL_ERR}")"
+        printf "\nGot:\n%s\n" "$(cat "${GPL_OUT}" && cat "${GPL_ERR}")"
+        echo "-----------------------------------------"
+    fi
+
+    if [ "${was_different}" -ne 0 ]; then
+        FAILED=$((FAILED + 1))
+    else
+        PASSED=$((PASSED + 1))
+    fi
+done
+
+# Clean up temporary files
+rm "$SPL_OUT" "$GPL_OUT" "$SPL_ERR" "$GPL_ERR"
+
+# 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/Examples.kt

@@ -0,0 +1,63 @@
+package e2e
+
+import interpreter.FileLoader
+import org.junit.jupiter.api.Assertions.assertEquals
+import org.junit.jupiter.api.BeforeEach
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.TestInstance
+import org.junit.jupiter.params.ParameterizedTest
+import org.junit.jupiter.params.provider.Arguments
+import org.junit.jupiter.params.provider.MethodSource
+import prolog.ast.Database.Program
+import java.io.ByteArrayOutputStream
+import java.io.PrintStream
+
+@TestInstance(TestInstance.Lifecycle.PER_CLASS)
+class Examples {
+    private val loader = FileLoader()
+    private lateinit var outStream: ByteArrayOutputStream
+
+    @BeforeEach
+    fun setup() {
+        Program.reset()
+
+        outStream = ByteArrayOutputStream()
+        System.setOut(PrintStream(outStream))
+    }
+
+    @Test
+    fun debugHelper() {
+        loader.load("examples/basics/backtracking.pl")
+    }
+
+    @ParameterizedTest
+    @MethodSource("basics")
+    fun `Identical output for basics`(inputFile: String, expected: String) {
+        loader.load("examples/basics/$inputFile")
+        assertEquals(expected, outStream.toString())
+    }
+
+    @ParameterizedTest
+    @MethodSource("other")
+    fun `Identical output for other`(inputFile: String, expected: String) {
+        loader.load("examples/$inputFile")
+        assertEquals(expected, outStream.toString())
+    }
+
+    fun basics() = listOf(
+        Arguments.of("arithmetics.pl", "gimli is a level 4 fighter with 35 hitpoints.\nlegolas is a level 5 ranger with 30 hitpoints.\ngandalf is a level 10 wizard with 25 hitpoints.\nfrodo is a level 2 rogue with 20 hitpoints.\nlegolas threw gimli, and gimli took 5 damage.\ngimli is a level 4 fighter with 30 hitpoints.\ngandalf casts aid.\ngimli is a level 4 fighter with 35 hitpoints.\nlegolas leveled up.\nlegolas is a level 6 ranger with 30 hitpoints"),
+        Arguments.of("backtracking.pl", "0\ns(0)\ns(s(0))\ns(s(s(0)))\n"),
+        Arguments.of("cut.pl", "0\n"),
+        Arguments.of("disjunction.pl", "Alice likes Italian food.\nBob likes Italian food.\n"),
+        Arguments.of("equality.pl", "X == Y failed\nX = Y succeeded\nX == Y succeeded\nX = Y succeeded\nX == Y succeeded\n"),
+        Arguments.of("forall.pl", "Only alice likes pizza.\n"),
+        Arguments.of("fraternity.pl", "Citizen robespierre is eligible for the event.\nCitizen danton is eligible for the event.\nCitizen camus is eligible for the event.\n"),
+        Arguments.of("liberty.pl", "Give me Liberty, or give me Death!\nI disapprove of what you say, but I will defend to the death your right to say it.\nThe revolution devours its own children.\nSo this is how liberty dies, with thunderous applause.\n"),
+        Arguments.of("unification.pl", "While alice got an A, carol got an A, but bob did not get an A, dave did not get an A, unfortunately.\n"),
+        Arguments.of("write.pl", "gpl zegt: dag(wereld)\n"),
+    )
+
+    fun other() = listOf(
+        Arguments.of("program.pl", "10\nhello(world)")
+    )
+}

tests/interpreter/OpenPreprocessor.kt

@@ -0,0 +1,9 @@
+package interpreter
+
+import prolog.ast.terms.Term
+
+class OpenPreprocessor : Preprocessor() {
+    public override fun preprocess(term: Term, nested: Boolean): Term {
+        return super.preprocess(term, nested)
+    }
+}

tests/interpreter/ParserPreprocessorIntegrationTests.kt

@@ -0,0 +1,92 @@
+package interpreter
+
+import com.github.h0tk3y.betterParse.grammar.parseToEnd
+import org.junit.jupiter.api.Assertions.assertEquals
+import org.junit.jupiter.api.Nested
+import org.junit.jupiter.params.ParameterizedTest
+import org.junit.jupiter.params.provider.ValueSource
+import parser.grammars.TermsGrammar
+import prolog.ast.arithmetic.Float
+import prolog.ast.arithmetic.Integer
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Goal
+import prolog.ast.terms.Structure
+import prolog.ast.terms.Term
+import prolog.ast.terms.Variable
+import prolog.builtins.Is
+import prolog.builtins.Subtract
+
+class ParserPreprocessorIntegrationTests {
+    @Nested
+    class `Arithmetic`() {
+        val parser = TermsGrammar()
+        val preprocessor = OpenPreprocessor()
+
+        @ParameterizedTest
+        @ValueSource(strings = ["-1", "-1.0", "-1.5"])
+        fun `can parse negative numbers`(input: String) {
+            val number = if (input.contains('.')) {
+                Float(input.substring(1).toFloat())
+            } else {
+                Integer(input.substring(1).toInt())
+            }
+            val negativeNumber = if (input.contains('.')) {
+                Float(input.toFloat())
+            } else {
+                Integer(input.toInt())
+            }
+
+            // Check if parser returns the same result
+
+            val parsed = parser.parseToEnd("X is $input") as Term
+
+            assertEquals(
+                Structure(Atom("is"), listOf(
+                    Variable("X"),
+                    Structure(Atom("-"), listOf(number)),
+                )),
+                parsed
+            )
+
+            // Check if preprocessor returns the same result
+
+            val prepped = preprocessor.preprocess(parsed)
+
+            val expected = Is(
+                Variable("X"),
+                Subtract(Integer(0), number)
+            )
+
+            assertEquals(expected, prepped)
+            assertEquals(expected.toString(), prepped.toString())
+
+            // Check if evaluation is correct
+
+            val solutions = (prepped as Is).satisfy(emptyMap()).toList()
+
+            assertEquals(1, solutions.size)
+            assertEquals(negativeNumber, solutions[0].getOrNull()!![Variable("X")])
+        }
+
+        @ParameterizedTest
+        @ValueSource(strings = ["X is 1 - 2", "X is 1-2"])
+        fun `can add negative numbers`(input: String) {
+            val result = parser.parseToEnd(input) as Term
+
+            assertEquals(
+                Structure(Atom("is"), listOf(Variable("X"), Structure(Atom("-"), listOf(Integer(1), Integer(2))))),
+                result
+            )
+
+            val prepped = preprocessor.preprocess(result)
+
+            val expected = Is(
+                Variable("X"),
+                Subtract(Integer(1), Integer(2))
+            )
+
+            assertEquals(expected, prepped)
+            assertEquals(expected.toString(), prepped.toString())
+        }
+    }
+}

tests/interpreter/PreprocessorTests.kt

@@ -0,0 +1,622 @@
+package interpreter
+
+import com.github.h0tk3y.betterParse.grammar.parseToEnd
+import org.junit.jupiter.api.Assertions.*
+import org.junit.jupiter.api.Nested
+import org.junit.jupiter.api.Test
+import parser.grammars.TermsGrammar
+import prolog.ast.arithmetic.Integer
+import prolog.ast.logic.Fact
+import prolog.ast.logic.Rule
+import prolog.ast.terms.*
+import prolog.builtins.*
+
+class PreprocessorTests {
+    val preprocessor = OpenPreprocessor()
+
+    companion object {
+        val preprocessor = OpenPreprocessor()
+
+        fun test(tests: Map<Term, Term>) {
+            for ((input, expected) in tests) {
+                val result = preprocessor.preprocess(input)
+                assertEquals(expected, result, "Expected preprocessed")
+                assertEquals(expected::class, result::class, "Expected same class")
+            }
+        }
+    }
+
+    @Test
+    fun `can preprocess anonymous variable`() {
+        val input = Variable("_")
+
+        val result = preprocessor.preprocess(input)
+
+        assertInstanceOf(AnonymousVariable::class.java, result, "Expected anonymous variable")
+        assertTrue((result as Variable).name.matches("_\\d+".toRegex()), "Expected anonymous variable name")
+    }
+
+    @Test
+    fun `multiple anonymous variables should be unique`() {
+        val input = CompoundTerm(Atom("foo"), listOf(Variable("_"), Variable("_")))
+
+        val result = preprocessor.preprocess(input)
+
+        assertInstanceOf(CompoundTerm::class.java, result, "Expected compound term")
+        assertEquals(2, (result as CompoundTerm).arguments.size, "Expected two terms")
+        for (argument in result.arguments) {
+            assertTrue(
+                (argument as Variable).name.matches("_\\d+".toRegex()),
+                "Expected anonymous variable name, but got ${argument.name}"
+            )
+        }
+        val first = result.arguments[0] as Variable
+        val second = result.arguments[1] as Variable
+        assertNotEquals(first.name, second.name, "Expected different anonymous variable names")
+    }
+
+    @Test
+    fun `can preprocess nested anonymous variables`() {
+        val input = TermsGrammar().parseToEnd("name(character(Name, _, _, _))") as Term
+
+        val result = preprocessor.preprocess(input)
+
+        assertInstanceOf(CompoundTerm::class.java, result, "Expected compound term")
+        assertEquals(1, (result as CompoundTerm).arguments.size, "Expected one term")
+        assertInstanceOf(CompoundTerm::class.java, result.arguments[0], "Expected compound term")
+        val inner = result.arguments[0] as CompoundTerm
+        assertEquals(4, inner.arguments.size, "Expected four terms")
+        for (argument in inner.arguments) {
+            if ((argument as Variable).name != "Name") {
+                assertTrue(
+                    (argument as Variable).name.matches("_\\d+".toRegex()),
+                    "Expected anonymous variable name, but got ${argument.name}"
+                )
+            }
+        }
+
+    }
+
+    @Nested
+    class `Arithmetic operators` {
+        @Test
+        fun `evaluates to different`() {
+            test(
+                mapOf(
+                    Atom("=\\=") to Atom("=\\="),
+                    CompoundTerm(Atom("=\\="), emptyList()) to CompoundTerm(Atom("=\\="), emptyList()),
+                    Atom("EvaluatesToDifferent") to Atom("EvaluatesToDifferent"),
+                    CompoundTerm(Atom("EvaluatesToDifferent"), emptyList()) to CompoundTerm(
+                        Atom("EvaluatesToDifferent"),
+                        emptyList()
+                    ),
+                    CompoundTerm(Atom("=\\="), listOf(Atom("a"))) to CompoundTerm(
+                        Atom("=\\="),
+                        listOf(Atom("a"))
+                    ),
+                    CompoundTerm(Atom("=\\="), listOf(Integer(1))) to CompoundTerm(
+                        Atom("=\\="),
+                        listOf(Integer(1))
+                    ),
+                    CompoundTerm(Atom("=\\="), listOf(Atom("=\\="))) to CompoundTerm(
+                        Atom("=\\="),
+                        listOf(Atom("=\\="))
+                    ),
+                    CompoundTerm(Atom("=\\="), listOf(Integer(1), Integer(2))) to EvaluatesToDifferent(
+                        Integer(1), Integer(2)
+                    )
+                )
+            )
+        }
+
+        @Test
+        fun `evaluates to`() {
+            test(
+                mapOf(
+                    Atom("=:=") to Atom("=:="),
+                    CompoundTerm(Atom("=:="), emptyList()) to CompoundTerm(Atom("=:="), emptyList()),
+                    Atom("EvaluatesTo") to Atom("EvaluatesTo"),
+                    CompoundTerm(Atom("EvaluatesTo"), emptyList()) to CompoundTerm(
+                        Atom("EvaluatesTo"),
+                        emptyList()
+                    ),
+                    CompoundTerm(Atom("=:="), listOf(Atom("a"))) to CompoundTerm(
+                        Atom("=:="),
+                        listOf(Atom("a"))
+                    ),
+                    CompoundTerm(Atom("=:="), listOf(Atom("=:="))) to CompoundTerm(
+                        Atom("=:="),
+                        listOf(Atom("=:="))
+                    ),
+                    CompoundTerm(Atom("=:="), listOf(Integer(1), Integer(2))) to EvaluatesTo(
+                        Integer(1), Integer(2)
+                    )
+                )
+            )
+        }
+
+        @Test
+        fun `is`() {
+            test(
+                mapOf(
+                    Atom("is") to Atom("is"),
+                    CompoundTerm(Atom("is"), emptyList()) to CompoundTerm(Atom("is"), emptyList()),
+                    Atom("Is") to Atom("Is"),
+                    CompoundTerm(Atom("Is"), emptyList()) to CompoundTerm(Atom("Is"), emptyList()),
+                    CompoundTerm(Atom("is"), listOf(Atom("a"))) to CompoundTerm(
+                        Atom("is"),
+                        listOf(Atom("a"))
+                    ),
+                    CompoundTerm(Atom("is"), listOf(Integer(1))) to CompoundTerm(
+                        Atom("is"),
+                        listOf(Integer(1))
+                    ),
+                    CompoundTerm(Atom("is"), listOf(Atom("is"))) to CompoundTerm(
+                        Atom("is"),
+                        listOf(Atom("is"))
+                    ),
+                    CompoundTerm(Atom("is"), listOf(Integer(1), Integer(2))) to Is(
+                        Integer(1), Integer(2)
+                    )
+                )
+            )
+        }
+
+        @Test
+        fun `negate and subtract`() {
+            test(
+                mapOf(
+                    Atom("-") to Atom("-"),
+                    CompoundTerm(Atom("-"), emptyList()) to CompoundTerm(Atom("-"), emptyList()),
+                    Atom("Negate") to Atom("Negate"),
+                    CompoundTerm(Atom("Negate"), emptyList()) to CompoundTerm(
+                        Atom("Negate"),
+                        emptyList()
+                    ),
+                    CompoundTerm(Atom("-"), listOf(Atom("a"))) to CompoundTerm(
+                        Atom("-"),
+                        listOf(Atom("a"))
+                    ),
+                    CompoundTerm(Atom("-"), listOf(Integer(1))) to Negate(Integer(1)),
+                    CompoundTerm(Atom("-"), listOf(Atom("-"))) to CompoundTerm(
+                        Atom("-"),
+                        listOf(Atom("-"))
+                    ),
+                    CompoundTerm(Atom("-"), listOf(Integer(1), Integer(2))) to Subtract(
+                        Integer(1), Integer(2)
+                    ),
+                    CompoundTerm(Atom("-"), listOf(Atom("1"), Atom("2"))) to CompoundTerm(
+                        Atom("-"),
+                        listOf(Atom("1"), Atom("2"))
+                    ),
+                    CompoundTerm(Atom("-"), listOf(Integer(1), Integer(2), Integer(3))) to CompoundTerm(
+                        Atom("-"),
+                        listOf(Integer(1), Integer(2), Integer(3))
+                    )
+                )
+            )
+        }
+
+        @Test
+        fun `positive and add`() {
+            test(
+                mapOf(
+                    Atom("+") to Atom("+"),
+                    CompoundTerm(Atom("+"), emptyList()) to CompoundTerm(Atom("+"), emptyList()),
+                    Atom("Positive") to Atom("Positive"),
+                    CompoundTerm(Atom("Positive"), emptyList()) to CompoundTerm(
+                        Atom("Positive"),
+                        emptyList()
+                    ),
+                    CompoundTerm(Atom("+"), listOf(Atom("a"))) to CompoundTerm(
+                        Atom("+"),
+                        listOf(Atom("a"))
+                    ),
+                    CompoundTerm(Atom("+"), listOf(Integer(1))) to Positive(Integer(1)),
+                    CompoundTerm(Atom("+"), listOf(Atom("+"))) to CompoundTerm(
+                        Atom("+"),
+                        listOf(Atom("+"))
+                    ),
+                    CompoundTerm(Atom("+"), listOf(Integer(1), Integer(2))) to Add(
+                        Integer(1), Integer(2)
+                    ),
+                    CompoundTerm(Atom("+"), listOf(Atom("1"), Atom("2"))) to CompoundTerm(
+                        Atom("+"),
+                        listOf(Atom("1"), Atom("2"))
+                    ),
+                    CompoundTerm(Atom("+"), listOf(Integer(1), Integer(2), Integer(3))) to CompoundTerm(
+                        Atom("+"),
+                        listOf(Integer(1), Integer(2), Integer(3))
+                    )
+                )
+            )
+        }
+
+        @Test
+        fun multiply() {
+            test(
+                mapOf(
+                    Atom("*") to Atom("*"),
+                    CompoundTerm(Atom("*"), emptyList()) to CompoundTerm(Atom("*"), emptyList()),
+                    Atom("Multiply") to Atom("Multiply"),
+                    CompoundTerm(Atom("Multiply"), emptyList()) to CompoundTerm(
+                        Atom("Multiply"),
+                        emptyList()
+                    ),
+                    CompoundTerm(Atom("*"), listOf(Atom("a"))) to CompoundTerm(
+                        Atom("*"),
+                        listOf(Atom("a"))
+                    ),
+                    CompoundTerm(Atom("*"), listOf(Integer(1))) to CompoundTerm(Atom("*"), listOf(Integer(1))),
+                    CompoundTerm(Atom("*"), listOf(Atom("*"))) to CompoundTerm(
+                        Atom("*"),
+                        listOf(Atom("*"))
+                    ),
+                    CompoundTerm(Atom("*"), listOf(Integer(1), Integer(2))) to Multiply(
+                        Integer(1), Integer(2)
+                    ),
+                    CompoundTerm(Atom("*"), listOf(Atom("1"), Atom("2"))) to CompoundTerm(
+                        Atom("*"),
+                        listOf(Atom("1"), Atom("2"))
+                    ),
+                    CompoundTerm(Atom("*"), listOf(Integer(1), Integer(2), Integer(3))) to CompoundTerm(
+                        Atom("*"),
+                        listOf(Integer(1), Integer(2), Integer(3))
+                    )
+                )
+            )
+        }
+
+        @Test
+        fun divide() {
+            test(
+                mapOf(
+                    Atom("/") to Atom("/"),
+                    CompoundTerm(Atom("/"), emptyList()) to CompoundTerm(Atom("/"), emptyList()),
+                    Atom("Divide") to Atom("Divide"),
+                    CompoundTerm(Atom("Divide"), emptyList()) to CompoundTerm(
+                        Atom("Divide"),
+                        emptyList()
+                    ),
+                    CompoundTerm(Atom("/"), listOf(Atom("a"))) to CompoundTerm(
+                        Atom("/"),
+                        listOf(Atom("a"))
+                    ),
+                    CompoundTerm(Atom("/"), listOf(Integer(1))) to CompoundTerm(Atom("/"), listOf(Integer(1))),
+                    CompoundTerm(Atom("/"), listOf(Atom("/"))) to CompoundTerm(
+                        Atom("/"),
+                        listOf(Atom("/"))
+                    ),
+                    CompoundTerm(Atom("/"), listOf(Integer(1), Integer(2))) to Divide(
+                        Integer(1), Integer(2)
+                    ),
+                    CompoundTerm(Atom("/"), listOf(Atom("1"), Atom("2"))) to CompoundTerm(
+                        Atom("/"),
+                        listOf(Atom("1"), Atom("2"))
+                    ),
+                    CompoundTerm(Atom("/"), listOf(Integer(1), Integer(2), Integer(3))) to CompoundTerm(
+                        Atom("/"),
+                        listOf(Integer(1), Integer(2), Integer(3))
+                    )
+                )
+            )
+        }
+
+        @Test
+        fun between() {
+            test(
+                mapOf(
+                    Atom("between") to Atom("between"),
+                    CompoundTerm(Atom("between"), emptyList()) to CompoundTerm(
+                        Atom("between"),
+                        emptyList()
+                    ),
+                    Atom("Between") to Atom("Between"),
+                    CompoundTerm(Atom("Between"), emptyList()) to CompoundTerm(
+                        Atom("Between"),
+                        emptyList()
+                    ),
+                    CompoundTerm(Atom("between"), listOf(Atom("a"))) to CompoundTerm(
+                        Atom("between"),
+                        listOf(Atom("a"))
+                    ),
+                    CompoundTerm(Atom("between"), listOf(Integer(1))) to CompoundTerm(
+                        Atom("between"),
+                        listOf(Integer(1))
+                    ),
+                    CompoundTerm(Atom("between"), listOf(Atom("between"))) to CompoundTerm(
+                        Atom("between"),
+                        listOf(Atom("between"))
+                    ),
+                    CompoundTerm(Atom("between"), listOf(Integer(1), Integer(2))) to CompoundTerm(
+                        Atom("between"),
+                        listOf(Integer(1), Integer(2))
+                    ),
+                    CompoundTerm(Atom("between"), listOf(Integer(1), Integer(2), Integer(3))) to Between(
+                        Integer(1), Integer(2), Integer(3)
+                    ),
+                )
+            )
+        }
+
+        @Test
+        fun `fun combinations`() {
+            /*
+             * [X - 1] is [(1 + 2) * ((12 / 3) - 0)]
+             * should return
+             * X = 13
+             */
+            val sum_ = CompoundTerm(Atom("+"), listOf(Integer(1), Integer(2)))
+            val sum = Add(Integer(1), Integer(2))
+
+            val div_ = CompoundTerm(Atom("/"), listOf(Integer(12), Integer(3)))
+            val div = Divide(Integer(12), Integer(3))
+
+            val sub_ = CompoundTerm(Atom("-"), listOf(div_, Integer(0)))
+            val sub = Subtract(div, Integer(0))
+
+            val right_ = CompoundTerm(Atom("*"), listOf(sum_, sub_))
+            val right = Multiply(sum, sub)
+
+            val left_ = CompoundTerm(Atom("-"), listOf(Variable("X"), Integer(1)))
+            val left = Subtract(Variable("X"), Integer(1))
+
+            val expr_ = CompoundTerm(Atom("is"), listOf(left_, right_))
+            val expr = Is(left, right)
+
+            val result = OpenPreprocessor().preprocess(expr_)
+
+            assertEquals(expr, result)
+            assertEquals(Is::class, result::class)
+            val `is` = result as Is
+
+            assertEquals(left, `is`.number)
+            assertEquals(Subtract::class, `is`.number::class)
+
+            assertEquals(right, `is`.expr)
+            assertEquals(Multiply::class, `is`.expr::class)
+            val multiply = `is`.expr as Multiply
+
+            assertEquals(sum, multiply.expr1)
+            assertEquals(Add::class, multiply.expr1::class)
+        }
+    }
+
+    @Nested
+    class `Control operators` {
+        private var preprocessor = OpenPreprocessor()
+
+        @Test
+        fun fail() {
+            test(
+                mapOf(
+                    Atom("fail") to Fail,
+                    CompoundTerm(Atom("fail"), emptyList()) to Fail,
+                    Atom("Fail") to Atom("Fail"),
+                    CompoundTerm(Atom("Fail"), emptyList()) to CompoundTerm(Atom("Fail"), emptyList()),
+                    CompoundTerm(Atom("fail"), listOf(Atom("a"))) to CompoundTerm(Atom("fail"), listOf(Atom("a"))),
+                    CompoundTerm(Atom("fail"), listOf(Atom("fail"))) to CompoundTerm(Atom("fail"), listOf(Fail))
+                )
+            )
+        }
+
+        @Test
+        fun `true`() {
+            test(
+                mapOf(
+                    Atom("true") to True,
+                    CompoundTerm(Atom("true"), emptyList()) to True,
+                    Atom("True") to Atom("True"),
+                    CompoundTerm(Atom("True"), emptyList()) to CompoundTerm(Atom("True"), emptyList()),
+                    CompoundTerm(Atom("true"), listOf(Atom("a"))) to CompoundTerm(Atom("true"), listOf(Atom("a"))),
+                    CompoundTerm(Atom("true"), listOf(Atom("true"))) to CompoundTerm(Atom("true"), listOf(True))
+                )
+            )
+        }
+
+        @Test
+        fun cut() {
+            test(
+                mapOf(
+                    Atom("!") to Cut(),
+                    CompoundTerm(Atom("!"), emptyList()) to Cut(),
+                    CompoundTerm(Atom("!"), listOf(Atom("a"))) to CompoundTerm(Atom("!"), listOf(Atom("a"))),
+                    CompoundTerm(Atom("!"), listOf(Atom("!"))) to CompoundTerm(Atom("!"), listOf(Cut()))
+                )
+            )
+        }
+
+        @Test
+        fun conjunction() {
+            test(
+                mapOf(
+                    CompoundTerm(Atom(","), listOf(Atom("a"), Atom("b"))) to Conjunction(Atom("a"), Atom("b")),
+                    CompoundTerm(Atom(","), listOf(Atom("a"), Atom("b"), Atom("c"))) to CompoundTerm(
+                        Atom(","),
+                        listOf(Atom("a"), Atom("b"), Atom("c"))
+                    ),
+                    // Nested conjunctions
+                    CompoundTerm(
+                        Atom(","),
+                        listOf(Atom("a"), CompoundTerm(Atom(","), listOf(Atom("b"), Atom("c"))))
+                    ) to Conjunction(Atom("a"), Conjunction(Atom("b"), Atom("c"))),
+                )
+            )
+        }
+
+        @Test
+        fun disjunction() {
+            test(
+                mapOf(
+                    CompoundTerm(Atom(";"), listOf(Atom("a"), Atom("b"))) to Disjunction(Atom("a"), Atom("b")),
+                    CompoundTerm(Atom(";"), listOf(Atom("a"), Atom("b"), Atom("c"))) to CompoundTerm(
+                        Atom(";"),
+                        listOf(Atom("a"), Atom("b"), Atom("c"))
+                    ),
+                    // Nested disjunctions
+                    CompoundTerm(
+                        Atom(";"),
+                        listOf(Atom("a"), CompoundTerm(Atom(";"), listOf(Atom("b"), Atom("c"))))
+                    ) to Disjunction(Atom("a"), Disjunction(Atom("b"), Atom("c"))),
+                )
+            )
+        }
+
+        @Test
+        fun not() {
+            test(
+                mapOf(
+                    CompoundTerm(Atom("\\+"), listOf(Atom("a"))) to Not(Atom("a")),
+                    CompoundTerm(Atom("\\+"), listOf(Atom("a"), Atom("b"))) to CompoundTerm(
+                        Atom("\\+"),
+                        listOf(Atom("a"), Atom("b"))
+                    ),
+                    // Nested not
+                    CompoundTerm(
+                        Atom("foo"),
+                        listOf(
+                            Atom("bar"),
+                            CompoundTerm(Atom("\\+"), listOf(CompoundTerm(Atom("\\+"), listOf(Atom("baz")))))
+                        )
+                    ) to CompoundTerm(Atom("foo"), listOf(Atom("bar"), Not(Not(Atom("baz"))))),
+                )
+            )
+        }
+
+        @Test
+        fun `is`() {
+            test(
+                mapOf(
+                    CompoundTerm(Atom("is"), listOf(Variable("T"), Integer(1))) to Is(Variable("T"), Integer(1)),
+                    CompoundTerm(Atom("is"), listOf(Variable("T"), Add(Variable("HP"), Integer(5)))) to Is(
+                        Variable("T"),
+                        Add(Variable("HP"), Integer(5))
+                    ),
+                    CompoundTerm(Atom("is"), listOf(Variable("T"), Subtract(Variable("HP"), Integer(5)))) to Is(
+                        Variable("T"),
+                        Subtract(Variable("HP"), Integer(5))
+                    ),
+                )
+            )
+        }
+    }
+
+    @Nested
+    class `Database operators` {
+        private val preprocessor = OpenPreprocessor()
+
+        @Test
+        fun `assert(fact)`() {
+            val input = Structure(
+                Atom("assert"), listOf(
+                    Structure(
+                        Atom(":-"), listOf(
+                            Atom("a"),
+                            Atom("b")
+                        )
+                    )
+                )
+            )
+            val expected = Assert(
+                Rule(
+                    Atom("a"),
+                    Atom("b")
+                )
+            )
+
+            val result = preprocessor.preprocess(input)
+
+            assertEquals(expected, result)
+        }
+
+        @Test
+        fun `asserta(fact)`() {
+            val input = Structure(
+                Atom("asserta"), listOf(
+                    Structure(
+                        Atom(":-"), listOf(
+                            Atom("a"),
+                            Atom("b")
+                        )
+                    )
+                )
+            )
+            val expected = AssertA(
+                Rule(
+                    Atom("a"),
+                    Atom("b")
+                )
+            )
+
+            val result = preprocessor.preprocess(input)
+
+            assertEquals(expected, result)
+        }
+
+        @Test
+        fun `assertz(fact)`() {
+            val input = Structure(
+                Atom("assertz"), listOf(
+                    Structure(
+                        Atom(":-"), listOf(
+                            Atom("a"),
+                            Atom("b")
+                        )
+                    )
+                )
+            )
+            val expected = AssertZ(
+                Rule(
+                    Atom("a"),
+                    Atom("b")
+                )
+            )
+
+            val result = preprocessor.preprocess(input)
+
+            assertEquals(expected, result)
+        }
+
+        @Test
+        fun `retract(atom)`() {
+            val input = Structure(
+                Atom("retract"), listOf(
+                    Atom("a")
+                )
+            )
+            val expected = Retract(Atom("a"))
+
+            val result = preprocessor.preprocess(input)
+
+            assertEquals(expected, result)
+        }
+
+        @Test
+        fun `retract(compund with variable)`() {
+            val input = Structure(
+                Atom("retract"), listOf(
+                    CompoundTerm(Atom("a"), listOf(Variable("X")))
+                )
+            )
+            val expected = Retract(CompoundTerm(Atom("a"), listOf(Variable("X"))))
+
+            val result = preprocessor.preprocess(input)
+
+            assertEquals(expected, result)
+        }
+
+        @Test
+        fun `dynamic declaration`() {
+            val input = Structure(
+                Atom("dynamic"), listOf(
+                    Atom("declaration/1")
+                )
+            )
+            val expected = Dynamic("declaration/1")
+
+            val result = preprocessor.preprocess(input)
+
+            assertEquals(expected, result)
+        }
+    }
+}

tests/interpreter/SourceFileReaderTests.kt

@@ -2,31 +2,27 @@ package interpreter
 
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
-import prolog.Program
+import prolog.ast.Database.Program
 
 class SourceFileReaderTests {
     @BeforeEach
     fun setup() {
-        Program.clear()
+        Program.reset()
     }
 
     @Test
     fun a() {
-        val inputFile = "tests/better_parser/resources/a.pl"
+        val inputFile = "tests/parser/resources/a.pl"
-        val reader = SourceFileReader()
+        val reader = FileLoader()
 
         reader.readFile(inputFile)
-
-        println(Program.predicates)
     }
 
     @Test
     fun foo() {
-        val inputFile = "tests/better_parser/resources/foo.pl"
+        val inputFile = "tests/parser/resources/foo.pl"
-        val reader = SourceFileReader()
+        val reader = FileLoader()
 
         reader.readFile(inputFile)
-
-        println(Program.predicates)
     }
 }

tests/lexer/ScanPrologParserTests.kt

@@ -1,62 +0,0 @@
-package lexer
-
-import lexer.errors.LexingError
-import org.junit.jupiter.api.Test
-import org.junit.jupiter.api.assertThrows
-import kotlin.test.assertEquals
-
-/**
- * Tests for the Prolog lexer.
- *
- * These tests are based on the Prolog syntax.
- */
-class ScanPrologParserTests {
-    @Test
-    fun scan_simple_atom() {
-        val tokens = Lexer("atom.").scan()
-
-        assertEquals(3, tokens.size)
-
-        assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
-        assertEquals(TokenType.DOT, tokens[1].type, "Expected DOT token, got ${tokens[1].type}")
-        assertEquals(TokenType.EOF, tokens[2].type, "Expected EOF token, got ${tokens[2].type}")
-    }
-
-    @Test
-    fun scan_variable() {
-        val tokens = Lexer("X.").scan()
-
-        assertEquals(3, tokens.size)
-
-        assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
-        assertEquals(TokenType.DOT, tokens[1].type, "Expected DOT token, got ${tokens[1].type}")
-        assertEquals(TokenType.EOF, tokens[2].type, "Expected EOF token, got ${tokens[2].type}")
-    }
-
-    @Test
-    fun scan_variable_with_number() {
-        val tokens = Lexer("X1.").scan()
-
-        assertEquals(3, tokens.size)
-
-        assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
-        assertEquals(TokenType.DOT, tokens[1].type, "Expected DOT token, got ${tokens[1].type}")
-        assertEquals(TokenType.EOF, tokens[2].type, "Expected EOF token, got ${tokens[2].type}")
-    }
-
-    @Test
-    fun scan_variable_with_underscore() {
-        val tokens = Lexer("X_1.").scan()
-
-        assertEquals(3, tokens.size)
-
-        assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
-        assertEquals(TokenType.DOT, tokens[1].type, "Expected DOT token, got ${tokens[1].type}")
-        assertEquals(TokenType.EOF, tokens[2].type, "Expected EOF token, got ${tokens[2].type}")
-    }
-
-    @Test
-    fun scan_variable_that_starts_with_a_number() {
-        assertThrows<LexingError> { Lexer("1X.").scan() }
-    }
-}

tests/lexer/ScanTests.kt

@@ -1,191 +0,0 @@
-package lexer
-
-import lexer.errors.LexingError
-import org.junit.jupiter.api.Test
-import org.junit.jupiter.api.assertThrows
-import org.junit.jupiter.api.Assertions.*
-
-class ScanTests {
-    @Test
-    fun scan_emptyString_returns_EOF() {
-        val tokens = Lexer("").scan()
-        assertEquals(1, tokens.size, "Expected 1 token, got ${tokens.size}")
-        assertEquals(TokenType.EOF, tokens[0].type, "Expected EOF token, got ${tokens[0].type}")
-    }
-
-    @Test
-    fun scan_unknownSymbol_returns_Error() {
-        assertThrows<LexingError> { Lexer("€").scan() }
-    }
-
-    @Test
-    fun scan_dot_returns_Dot() {
-        val tokens = Lexer(".").scan()
-        assertEquals(2, tokens.size)
-        assertEquals(TokenType.DOT, tokens[0].type, "Expected DOT token, got ${tokens[0].type}")
-        assertEquals(TokenType.EOF, tokens[1].type, "Expected EOF token, got ${tokens[1].type}")
-    }
-
-    @Test
-    fun scan_two_dots_returns_two_dots() {
-        val tokens = Lexer("..").scan()
-        assertEquals(3, tokens.size)
-        assertEquals(TokenType.DOT, tokens[0].type, "Expected DOT token, got ${tokens[0].type}")
-        assertEquals(TokenType.DOT, tokens[1].type, "Expected DOT token, got ${tokens[1].type}")
-        assertEquals(TokenType.EOF, tokens[2].type, "Expected EOF token, got ${tokens[2].type}")
-    }
-
-    @Test
-    fun scan_letter_returns_letter() {
-        val tokens = Lexer("a").scan()
-
-        assertEquals(2, tokens.size)
-
-        assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
-        assertEquals(TokenType.EOF, tokens[1].type, "Expected EOF token, got ${tokens[1].type}")
-
-        assertEquals(0, tokens[0].position.line, "Expected line 0, got ${tokens[0].position.line}")
-        assertEquals(0, tokens[0].position.column, "Expected column 0, got ${tokens[0].position.column}")
-        assertEquals(1, tokens[0].position.length, "Expected length 1, got ${tokens[0].position.length}")
-    }
-
-    @Test
-    fun scan_word_returns_alphanumerics() {
-        val lexer = Lexer("word")
-        val tokens = lexer.scan()
-
-        assertEquals(2, tokens.size)
-
-        assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
-        assertEquals(TokenType.EOF, tokens[1].type, "Expected EOF token, got ${tokens[1].type}")
-
-        assertEquals(4, tokens[0].position.length, "Expected length 4, got ${tokens[0].position.length}")
-
-        assertEquals("word", tokens[0].value, "Expected 'word', got ${tokens[0].value}")
-    }
-
-    @Test
-    fun scan_space_returns_nothing() {
-        val lexer = Lexer(" ")
-        val tokens = lexer.scan()
-
-        assertEquals(1, tokens.size)
-
-        assertEquals(TokenType.EOF, tokens[0].type, "Expected EOF token, got ${tokens[0].type}")
-    }
-
-    @Test
-    fun scan_whitespace_various_returns_nothing() {
-        val lexer = Lexer(" \t\n\r")
-        val tokens = lexer.scan()
-
-        assertEquals(1, tokens.size)
-
-        assertEquals(TokenType.EOF, tokens[0].type, "Expected EOF token, got ${tokens[0].type}")
-    }
-
-
-    @Test
-    fun scan_separated_words() {
-        val tokens = Lexer("word1 word2").scan()
-
-        assertEquals(3, tokens.size, "Expected 3 tokens, got ${tokens.size}")
-
-        assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
-        assertEquals("word1", tokens[0].value, "Expected 'word1', got ${tokens[0].value}")
-        assertEquals(5, tokens[0].position.length, "Expected length 5, got ${tokens[0].position.length}")
-
-        assertEquals(TokenType.ALPHANUMERIC, tokens[1].type, "Expected ALPHANUMERIC token, got ${tokens[1].type}")
-        assertEquals("word2", tokens[1].value, "Expected 'word2', got ${tokens[1].value}")
-        assertEquals(5, tokens[1].position.length, "Expected length 5, got ${tokens[1].position.length}")
-    }
-
-    @Test
-    fun scan_multiline() {
-        val tokens = Lexer(
-            """
-            word1
-            word2
-        """.trimIndent()
-        ).scan()
-
-        assertEquals(3, tokens.size, "Expected 3 tokens, got ${tokens.size}")
-
-        assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
-        assertEquals("word1", tokens[0].value, "Expected 'word1', got ${tokens[0].value}")
-        assertEquals(5, tokens[0].position.length, "Expected length 5, got ${tokens[0].position.length}")
-
-        assertEquals(TokenType.ALPHANUMERIC, tokens[1].type, "Expected ALPHANUMERIC token, got ${tokens[1].type}")
-        assertEquals("word2", tokens[1].value, "Expected 'word2', got ${tokens[1].value}")
-        assertEquals(5, tokens[1].position.length, "Expected length 5, got ${tokens[1].position.length}")
-    }
-
-    @Test
-    fun scan_parenthesis_returns_parenthesis() {
-        val lexer = Lexer("()")
-        val tokens = lexer.scan()
-
-        assertEquals(3, tokens.size)
-
-        assertEquals(
-            TokenType.PARENTHESIS_LEFT,
-            tokens[0].type,
-            "Expected LEFT_PARENTHESES token, got ${tokens[0].type}"
-        )
-        assertEquals(
-            TokenType.PARENTHESIS_RIGHT,
-            tokens[1].type,
-            "Expected RIGHT_PARENTHESES token, got ${tokens[1].type}"
-        )
-        assertEquals(TokenType.EOF, tokens[2].type, "Expected EOF token, got ${tokens[2].type}")
-    }
-
-    @Test
-    fun scan_simple_quoted_string_returns_string() {
-        val lexer = Lexer("\"string\"")
-        val tokens = lexer.scan()
-
-        assertEquals(2, tokens.size)
-
-        assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
-        assertEquals(TokenType.EOF, tokens[1].type, "Expected EOF token, got ${tokens[1].type}")
-
-        assertEquals("string", tokens[0].value, "Expected 'string', got ${tokens[0].value}")
-    }
-
-    @Test
-    fun scan_quoted_string_with_space_returns_string() {
-        val lexer = Lexer("\"string with space\"")
-        val tokens = lexer.scan()
-
-        assertEquals(2, tokens.size)
-
-        assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
-        assertEquals(TokenType.EOF, tokens[1].type, "Expected EOF token, got ${tokens[1].type}")
-
-        assertEquals("string with space", tokens[0].value, "Expected 'string with space', got ${tokens[0].value}")
-    }
-
-    @Test
-    fun scan_comments_returns_nothing() {
-        val lexer = Lexer("% comment")
-        val tokens = lexer.scan()
-
-        assertEquals(1, tokens.size)
-
-        assertEquals(TokenType.EOF, tokens[0].type, "Expected EOF token, got ${tokens[0].type}")
-    }
-
-    @Test
-    fun scan_comment_and_sentence_returns_sentence() {
-        val tokens = Lexer("""
-            % comment
-            sentence
-        """.trimIndent()).scan()
-
-        assertEquals(2, tokens.size)
-
-        assertEquals(TokenType.ALPHANUMERIC, tokens[0].type, "Expected ALPHANUMERIC token, got ${tokens[0].type}")
-        assertEquals("sentence", tokens[0].value, "Expected 'sentence', got ${tokens[0].value}")
-    }
-}

tests/parser/OperatorParserTests.kt

@@ -0,0 +1,43 @@
+package parser
+
+import com.github.h0tk3y.betterParse.combinators.use
+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.assertEquals
+import org.junit.jupiter.api.Test
+import parser.grammars.TermsGrammar
+import prolog.ast.terms.Atom
+import prolog.ast.terms.CompoundTerm
+import prolog.ast.terms.Operator
+import prolog.ast.terms.Structure
+
+class OperatorParserTests {
+    class OperatorParser: TermsGrammar() {
+        override val rootParser: Parser<CompoundTerm> by body use { this as CompoundTerm }
+    }
+
+    private var parser = OperatorParser() as Grammar<CompoundTerm>
+
+    @Test
+    fun `parse conjunction`() {
+        val input = "a, b"
+
+        val result = parser.parseToEnd(input)
+
+        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/ParseFromTextTests.kt

@@ -1,4 +0,0 @@
-package parser
-
-class ParseFromTextTests {
-}

tests/parser/ParseTests.kt

@@ -1,91 +0,0 @@
-package parser
-
-import lexer.Token
-import lexer.state.TokenPosition
-import lexer.TokenType
-import org.junit.jupiter.api.Assertions.assertEquals
-import org.junit.jupiter.api.Assertions.assertTrue
-import org.junit.jupiter.api.Test
-import prolog.ast.terms.Atom
-import prolog.ast.terms.CompoundTerm
-
-class ParseTests {
-    @Test
-    fun `parse atom a`() {
-        val input = Token(TokenType.ALPHANUMERIC, "a", TokenPosition(0, 0, 1))
-
-        val result = Parser(listOf(input)).parse()
-
-        assertEquals(1, result.size, "Expected 1 term")
-        assertEquals(Atom("a"), result[0], "Expected atom 'a'")
-    }
-
-    @Test
-    fun `parse atom foo`() {
-        val input = Token(TokenType.ALPHANUMERIC, "foo", TokenPosition(0, 0, 3))
-
-        val result = Parser(listOf(input)).parse()
-
-        assertEquals(1, result.size, "Expected 1 term")
-        assertEquals(Atom("foo"), result[0], "Expected atom 'foo'")
-    }
-
-    @Test
-    fun `parse atom foo1`() {
-        val input = Token(TokenType.ALPHANUMERIC, "foo1", TokenPosition(0, 0, 4))
-
-        val result = Parser(listOf(input)).parse()
-
-        assertEquals(1, result.size, "Expected 1 term")
-        assertEquals(Atom("foo1"), result[0], "Expected atom 'foo1'")
-    }
-
-    @Test
-    fun `parse atom fooBar`() {
-        val name = "fooBar"
-        val input = Token(TokenType.ALPHANUMERIC, name, TokenPosition(0, 0, 6))
-
-        val result = Parser(listOf(input)).parse()
-
-        assertEquals(1, result.size, "Expected 1 term")
-        assertEquals(Atom(name), result[0], "Expected atom 'fooBar'")
-    }
-
-    @Test
-    fun `parse atom foo_bar`() {
-        val name = "foo_bar"
-        val input = Token(TokenType.ALPHANUMERIC, name, TokenPosition(0, 0, 7))
-
-        val result = Parser(listOf(input)).parse()
-
-        assertEquals(1, result.size, "Expected 1 term")
-        assertEquals(Atom(name), result[0], "Expected atom 'foo_bar'")
-    }
-
-    @Test
-    fun `parse atom my_FooBar1`() {
-        val name = "my_FooBar1"
-        val input = Token(TokenType.ALPHANUMERIC, name, TokenPosition(0, 0, 11))
-
-        val result = Parser(listOf(input)).parse()
-
-        assertEquals(1, result.size, "Expected 1 term")
-        assertEquals(Atom(name), result[0], "Expected atom 'my_FooBar1'")
-    }
-
-    @Test
-    fun `parse compound term f()`() {
-        val input = listOf(
-            Token(TokenType.ALPHANUMERIC, "f", TokenPosition(0, 0, 1)),
-            Token(TokenType.PARENTHESIS_LEFT, "(", TokenPosition(0, 1, 2)),
-            Token(TokenType.PARENTHESIS_RIGHT, ")", TokenPosition(0, 3, 4))
-        )
-
-        val result = Parser(input).parse()
-
-        assertEquals(1, result.size, "Expected 1 term")
-        assertTrue(result[0] is CompoundTerm)
-        assertEquals("f", (result[0] as CompoundTerm).name)
-        assertEquals(0, (result[0] as CompoundTerm).arguments.size)
-    }
-}

tests/parser/builtins/DatabaseOperatorsParserTests.kt

@@ -0,0 +1,75 @@
+package parser.builtins
+
+import com.github.h0tk3y.betterParse.grammar.Grammar
+import com.github.h0tk3y.betterParse.grammar.parseToEnd
+import org.junit.jupiter.api.Assertions.assertEquals
+import org.junit.jupiter.api.BeforeEach
+import org.junit.jupiter.api.Test
+import parser.grammars.TermsGrammar
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Structure
+import prolog.ast.terms.Term
+
+class DatabaseOperatorsParserTests {
+    private lateinit var parser: Grammar<Term>
+
+    @BeforeEach
+    fun setup() {
+        parser = TermsGrammar() as Grammar<Term>
+    }
+
+    @Test
+    fun `parse assert(rule)`() {
+        val input = "assert((a :- b))"
+        val expected = Structure(Atom("assert"), listOf(
+            Structure(Atom(":-"), listOf(
+                Atom("a"),
+                Atom("b")
+            ))
+        ))
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(expected, result)
+    }
+
+    @Test
+    fun `parse assertA(rule)`() {
+        val input = "assertA((a :- b))"
+        val expected = Structure(Atom("assertA"), listOf(
+            Structure(Atom(":-"), listOf(
+                Atom("a"),
+                Atom("b")
+            ))
+        ))
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(expected, result)
+    }
+
+    @Test
+    fun `parse assertZ(rule)`() {
+        val input = "assertZ((a :- b))"
+        val expected = Structure(Atom("assertZ"), listOf(
+            Structure(Atom(":-"), listOf(
+                Atom("a"),
+                Atom("b")
+            ))
+        ))
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(expected, result)
+    }
+
+    @Test
+    fun `parse dynamic declaration`() {
+        val input = "dynamic declaration/1"
+        val expected = Structure(Atom("dynamic"), listOf(Atom("declaration/1")))
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(expected, result)
+    }
+}

tests/parser/grammars/LogicGrammarTests.kt

@@ -1,7 +1,8 @@
-package better_parser
+package parser.grammars
 
 import com.github.h0tk3y.betterParse.grammar.Grammar
 import com.github.h0tk3y.betterParse.grammar.parseToEnd
+import org.junit.jupiter.api.Assertions
 import org.junit.jupiter.api.Assertions.*
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
@@ -14,14 +15,13 @@ import prolog.ast.terms.CompoundTerm
 import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable
 import prolog.builtins.Conjunction
-import prolog.builtins.Disjunction
 
-class SimpleSourcePrologParserTests {
+class LogicGrammarTests {
     private lateinit var parser: Grammar<List<Clause>>
 
     @BeforeEach
     fun setup() {
-        parser = SimpleSourceParser() as Grammar<List<Clause>>
+        parser = LogicGrammar() as Grammar<List<Clause>>
     }
 
     @ParameterizedTest
@@ -40,7 +40,7 @@ class SimpleSourcePrologParserTests {
 
         assertEquals(1, result.size, "Expected 1 fact")
         assertTrue(result[0] is Fact, "Expected a fact")
-        assertEquals(input, "${result[0].toString()}.", "Expected fact to be '$input'")
+        assertEquals(input, "${result[0]}.", "Expected fact to be '$input'")
     }
 
     @ParameterizedTest
@@ -114,7 +114,7 @@ class SimpleSourcePrologParserTests {
         assertEquals(1, result.size, "Expected 1 rule")
         assertInstanceOf(Rule::class.java, result[0], "Expected a rule")
         val rule = result[0] as Rule
-        assertInstanceOf(Conjunction::class.java, rule.body, "Expected body to be a conjunction")
+        assertInstanceOf(CompoundTerm::class.java, rule.body, "Expected body to be a compound term")
     }
 
     @Test
@@ -125,8 +125,38 @@ class SimpleSourcePrologParserTests {
 
         assertEquals(1, result.size, "Expected 1 rule")
         val rule = result[0] as Rule
-        assertTrue(rule.body is Conjunction, "Expected body to be a conjunction")
+        assertEquals("guest/2", rule.head.functor, "Expected functor 'guest/2'")
-        val conjunction = rule.body as Conjunction
+        assertEquals(",/2", (rule.body as CompoundTerm).functor, "Expected functor ',/2'")
-        assertEquals("invited/2", (conjunction.left as CompoundTerm).functor, "Expected functor 'invited/2'")
+        val l1 = (rule.body as CompoundTerm).arguments[0] as CompoundTerm
+        assertEquals(",/2", l1.functor, "Expected functor ',/2'")
+        val l2 = l1.arguments[0] as CompoundTerm
+        assertEquals("invited/2", l2.functor, "Expected functor 'invited/2'")
+    }
+
+    @Test
+    fun `parse check_identical(X, Y)`() {
+        var input = "check_identical(X, Y) :- X == Y."
+
+        assertDoesNotThrow {
+            val result = parser.parseToEnd(input)
+        }
+
+        input = "check_identical(X, Y) :- X = Y, !, write('X == Y succeeded'), nl."
+
+        assertDoesNotThrow {
+            val result = parser.parseToEnd(input)
+        }
+    }
+
+    @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

@@ -0,0 +1,355 @@
+package parser.grammars
+
+import com.github.h0tk3y.betterParse.grammar.Grammar
+import com.github.h0tk3y.betterParse.grammar.parseToEnd
+import org.junit.jupiter.api.Assertions
+import org.junit.jupiter.api.Assertions.assertTrue
+import org.junit.jupiter.api.Assertions.assertEquals
+import org.junit.jupiter.api.BeforeEach
+import org.junit.jupiter.api.Nested
+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
+import prolog.ast.arithmetic.Integer
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Structure
+import prolog.ast.terms.Term
+import prolog.ast.terms.Variable
+import prolog.builtins.Is
+import prolog.logic.equivalent
+
+class TermsGrammarTests {
+    private lateinit var parser: Grammar<Term>
+
+    @BeforeEach
+    fun setup() {
+        parser = TermsGrammar() as Grammar<Term>
+    }
+
+    @ParameterizedTest
+    @ValueSource(strings = ["a", "foo", "foo1", "fooBar", "foo_bar"])
+    fun `parse atom`(name: String) {
+        val result = parser.parseToEnd(name)
+
+        assertEquals(Atom(name), result, "Expected atom '$name'")
+    }
+
+    @ParameterizedTest
+    @ValueSource(
+        strings = [
+            "'tick'",
+            "\"doubleTick\"",
+            "`backTick`",
+            "'i have spaces'",
+            "`i have a 'quote' inside`",
+            "'I have Cases'",
+            "'I, h@v3 many (!!!) special characters?! {}'"
+        ]
+    )
+    fun `Parse a quoted atom`(input: String) {
+        val result = parser.parseToEnd(input)
+
+        val expected = input.substring(1, input.length - 1)
+
+        assertEquals(Atom(expected), result, "Expected atom")
+    }
+
+    @ParameterizedTest
+    @ValueSource(strings = ["X", "X1", "X_1"])
+    fun `parse variable`(name: String) {
+        val result = parser.parseToEnd(name)
+
+        assertEquals(Variable(name), result)
+    }
+
+    @Test
+    fun `parse anonymous variable`() {
+        val input = "_"
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(Variable("_"), result, "Expected anonymous variable")
+    }
+
+    @Test
+    fun `empty compound term`() {
+        val input = "f()"
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(Structure(Atom("f"), emptyList()), result, "Expected atom 'f'")
+    }
+
+    @Test
+    fun `parse compound term f(a)`() {
+        val input = "f(a)"
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(Structure(Atom("f"), listOf(Atom("a"))), result, "Expected atom 'f(a)'")
+    }
+
+    @Test
+    fun `parse compound term f(a, b)`() {
+        val input = "f(a, b)"
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(
+            Structure(Atom("f"), listOf(Atom("a"), Atom("b"))),
+            result,
+            "Expected atom 'f(a, b)'"
+        )
+    }
+
+    @Test
+    fun `parse compound term with variable f(a, X)`() {
+        val input = "f(a, X)"
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(
+            Structure(Atom("f"), listOf(Atom("a"), Variable("X"))),
+            result,
+            "Expected atom 'f(a, X)'"
+        )
+    }
+
+    @Test
+    fun `parse compound term with var and int`() {
+        val input = "check_identical(A, 13)"
+        val result = parser.parseToEnd(input)
+        assertEquals(
+            Structure(Atom("check_identical"), listOf(Variable("A"), Integer(13))),
+            result,
+            "Expected atom 'check_identical(A, 13)'"
+        )
+    }
+
+    @Test
+    fun `parse nested compound term f(a, g(b))`() {
+        val input = "f(a, g(b))"
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(
+            Structure(Atom("f"), listOf(Atom("a"), Structure(Atom("g"), listOf(Atom("b"))))),
+            result,
+            "Expected atom 'f(a, g(b))'"
+        )
+    }
+
+    @Test
+    fun `parse compound term with variable f(a, g(X))`() {
+        val input = "f(a, g(X))"
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(
+            Structure(Atom("f"), listOf(Atom("a"), Structure(Atom("g"), listOf(Variable("X"))))),
+            result,
+            "Expected atom 'f(a, g(X))'"
+        )
+    }
+
+    @Test
+    fun `parse nested compound term with variables`() {
+        val input = "hit(character(Name, Class, Level, HP), character(Name, Class, Level, T))"
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(
+            Structure(
+                Atom("hit"),
+                listOf(
+                    Structure(Atom("character"), listOf(Variable("Name"), Variable("Class"), Variable("Level"), Variable("HP"))),
+                    Structure(Atom("character"), listOf(Variable("Name"), Variable("Class"), Variable("Level"), Variable("T")))
+                )
+            ),
+            result,
+            "Expected atom 'hit(character(Name, Class, Level, HP), character(Name, Class, Level, T))'"
+        )
+    }
+
+    @Test
+    fun `parse compound term with anonymous variables`() {
+        val input = "f(a, _, g(X))"
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(
+            Structure(Atom("f"), listOf(Atom("a"), Variable("_"), Structure(Atom("g"), listOf(Variable("X"))))),
+            result,
+            "Expected atom 'f(a, _, g(X))'"
+        )
+    }
+
+    @ParameterizedTest
+    @ValueSource(ints = [0, 1, 5, 12, 345, 123456789])
+    fun `parse positive integer`(number: Int) {
+        val input = number.toString()
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(Integer(number), result, "Expected integer '$number'")
+    }
+
+    @ParameterizedTest
+    @ValueSource(ints = [-987654321, -543, -21, -1])
+    fun `parse negative integer`(number: Int) {
+        val input = number.toString()
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(Structure(Atom("-"), listOf(Integer(0 - number))), result, "Expected integer '$number'")
+    }
+
+    @Test
+    fun `parse float`() {
+        val input = "42.0"
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(Float(42.0f), result, "Expected float '42.0'")
+    }
+
+    @Test
+    fun `parse negative float`() {
+        val input = "-42.0"
+
+        val result = parser.parseToEnd(input)
+
+        assertEquals(Structure(Atom("-"), listOf(Float(42.0f))), result, "Expected float '-42.0'")
+    }
+
+    @ParameterizedTest
+    @ValueSource(strings = ["got_an_a(Student)", "grade(Student, Grade)"])
+    fun `parse unification`(input: String) {
+        assertDoesNotThrow { parser.parseToEnd(input) }
+    }
+
+    @Nested
+    class `Operators and precedence` {
+        private lateinit var parser: Grammar<Term>
+
+        @BeforeEach
+        fun setup() {
+            parser = TermsGrammar() as Grammar<Term>
+        }
+
+        @Test
+        fun `can parse equivalent`() {
+            val input = "X == Y"
+
+            val result = parser.parseToEnd(input)
+
+            assertEquals(
+                Structure(Atom("=="), listOf(Variable("X"), Variable("Y"))),
+                result,
+                "Expected equivalent operator"
+            )
+        }
+
+        @Test
+        fun `can parse cut`() {
+            val input = "!"
+            val result = parser.parseToEnd(input)
+            assertEquals(Atom("!"), result, "Expected cut operator")
+        }
+
+        @Test
+        fun `can parse 'is'`() {
+            val input = "T is 1"
+            val result = parser.parseToEnd(input)
+            assertEquals(
+                Structure(Atom("is"), listOf(Variable("T"), Integer(1))),
+                result
+            )
+        }
+
+        @Test
+        fun `can parse 'is' with addition`() {
+            val input = "T is 1 + 2"
+            val result = parser.parseToEnd(input)
+            assertEquals(
+                Structure(Atom("is"), listOf(Variable("T"), Structure(Atom("+"), listOf(Integer(1), Integer(2))))),
+                result
+            )
+        }
+
+        @ParameterizedTest
+        @ValueSource(strings = ["+", "-", "*", "/"])
+        fun `can parse with spaces`(operator: String) {
+            val input = "1 $operator 2"
+
+            val result = parser.parseToEnd(input)
+
+            assertEquals(
+                Structure(Atom(operator), listOf(Integer(1), Integer(2))),
+                result,
+                "Expected operator '$operator'"
+            )
+        }
+
+        @ParameterizedTest
+        @ValueSource(strings = ["+", "-", "*", "/"])
+        fun `can parse without spaces`(operator: String) {
+            val input = "1${operator}2"
+
+            val result = parser.parseToEnd(input)
+
+            assertEquals(
+                Structure(Atom(operator), listOf(Integer(1), Integer(2))),
+                result,
+                "Expected operator '$operator' without spaces"
+            )
+        }
+
+        @Test
+        fun `parse addition and multiplication`() {
+            val input = "1 + 2 * 3"
+
+            val result = parser.parseToEnd(input)
+
+            assertEquals(
+                Structure(Atom("+"), listOf(Integer(1), Structure(Atom("*"), listOf(Integer(2), Integer(3))))),
+                result,
+                "Expected addition and multiplication"
+            )
+        }
+
+        @Test
+        fun `parse multiplication and addition`() {
+            val input = "1 * 2 + 3"
+
+            val result = parser.parseToEnd(input)
+
+            assertEquals(
+                Structure(Atom("+"), listOf(Structure(Atom("*"), listOf(Integer(1), Integer(2))), Integer(3))),
+                result,
+                "Expected multiplication and addition"
+            )
+        }
+
+        @Test
+        fun `complex expression`() {
+            val input = "1 + 2 * 3 - 4 / 5"
+
+            val result = parser.parseToEnd(input)
+
+            assertEquals(
+                Structure(
+                    Atom("-"),
+                    listOf(
+                        Structure(Atom("+"), listOf(Integer(1), Structure(Atom("*"), listOf(Integer(2), Integer(3))))),
+                        Structure(Atom("/"), listOf(Integer(4), Integer(5)))
+                    )
+                ),
+                result,
+                "Expected complex expression"
+            )
+        }
+    }
+}

tests/parser/resources/parent.pl

@@ -5,5 +5,3 @@ parent(john, jimmy).
 parent(mary, jimmy).
 father(X, Y) :- parent(X, Y), male(X).
 mother(X, Y) :- parent(X, Y), female(X).
-
-kan_goed_koken(miriam).

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
@@ -12,11 +13,12 @@ import prolog.logic.equivalent
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable
+import prolog.ast.Database.Program
 
 class EvaluationTests {
     @BeforeEach
     fun setUp() {
-        Program.clear()
+        Program.reset()
     }
 
     @Test
@@ -106,20 +108,24 @@ class EvaluationTests {
         val variable2 = Variable("Y")
 
         val parent = Rule(
-            Structure(Atom("parent"), listOf(variable1, variable2)),
+            Structure(Atom("parent"), listOf(variable1, variable2)), /* :- */
-            /* :- */ Disjunction(
+            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))
             )
         )
 
         Program.load(listOf(father, mother, parent))
 
-        val result1 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy"))))
+        val result1 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy")))).toList()
-        assertTrue(result1.toList().isNotEmpty())
+        assertEquals(1, result1.size, "Expected 1 result")
-        val result2 = Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy"))))
+        assertTrue(result1[0].isSuccess, "Expected success")
-        assertTrue(result2.toList().isNotEmpty())
+        assertTrue(result1[0].getOrNull()!!.isEmpty(), "Expected no substitutions")
+        val result2 = Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy")))).toList()
+        assertEquals(1, result2.size, "Expected 1 result")
+        assertTrue(result2[0].isSuccess, "Expected success")
+        assertTrue(result2[0].getOrNull()!!.isEmpty(), "Expected no substitutions")
 
         val result3 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jane"))))
         assertFalse(result3.any())
@@ -212,7 +218,204 @@ 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.reset()
+            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")
+        }
+
+        @Test
+        fun `likes_italian_food(Person)`() {
+            val result = Program.query(Structure(Atom("likes_italian_food"), listOf(Variable("Person")))).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")
+            assertEquals(Atom("alice"), subs3[Variable("Person")], "Expected alice")
+
+            assertTrue(result[1].isSuccess, "Expected success")
+            val subs4 = result[1].getOrNull()!!
+            assertEquals(1, subs4.size, "Expected 1 substitution")
+            assertEquals(Atom("alice"), subs4[Variable("Person")], "Expected alice")
+
+            assertTrue(result[2].isSuccess, "Expected success")
+            val subs5 = result[2].getOrNull()!!
+            assertEquals(1, subs5.size, "Expected 1 substitution")
+            assertEquals(Atom("bob"), subs5[Variable("Person")], "Expected bob")
         }
     }
 }

tests/prolog/builtins/ControlOperatorsTests.kt

@@ -3,7 +3,7 @@ package prolog.builtins
 import org.junit.jupiter.api.Assertions.*
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
-import prolog.Program
+import prolog.ast.Database.Program
 import prolog.ast.logic.Fact
 import prolog.ast.logic.Rule
 import prolog.ast.terms.Atom
@@ -14,7 +14,25 @@ import prolog.ast.terms.Variable
 class ControlOperatorsTests {
     @BeforeEach
     fun setUp() {
-        Program.clear()
+        Program.reset()
+    }
+
+    @Test
+    fun `rule with cut as body`() {
+        Program.load(
+            listOf(
+                Rule(Atom("foo"), Cut()),
+                Fact(Atom("foo"))
+            )
+        )
+
+        val goal = Atom("foo")
+
+        val result = Program.query(goal).toList()
+
+        assertEquals(1, result.size, "Expected 1 result")
+        assertTrue(result[0].isSuccess, "Expected success")
+        assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitutions")
     }
 
     // See also: https://stackoverflow.com/a/23292126
@@ -37,7 +55,7 @@ class ControlOperatorsTests {
 
         // Now with cut
 
-        Program.clear()
+        Program.reset()
 
         Program.load(
             listOf(
@@ -86,7 +104,7 @@ class ControlOperatorsTests {
 
         // Now with cut in the middle
 
-        Program.clear()
+        Program.reset()
 
         Program.load(
             listOf(
@@ -120,7 +138,7 @@ class ControlOperatorsTests {
 
         // Now with cut at the end
 
-        Program.clear()
+        Program.reset()
 
         Program.load(
             listOf(

tests/prolog/builtins/DatabaseOperatorsTests.kt

@@ -0,0 +1,295 @@
+package prolog.builtins
+
+import org.junit.jupiter.api.Assertions.assertEquals
+import org.junit.jupiter.api.Assertions.assertFalse
+import org.junit.jupiter.api.Assertions.assertTrue
+import org.junit.jupiter.api.BeforeEach
+import org.junit.jupiter.api.Nested
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.params.ParameterizedTest
+import org.junit.jupiter.params.provider.ValueSource
+import prolog.ast.Database
+import prolog.ast.Database.Program
+import prolog.ast.logic.Clause
+import prolog.ast.logic.Fact
+import prolog.ast.logic.Predicate
+import prolog.ast.logic.Rule
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Structure
+import prolog.ast.terms.Variable
+
+class DatabaseOperatorsTests {
+    @BeforeEach
+    fun setup() {
+        Program.reset()
+    }
+
+    abstract class AssertTestsBase<T : Structure> {
+        protected abstract fun createAssert(clause: Clause): Structure
+
+        @BeforeEach
+        fun setup() {
+            Program.reset()
+        }
+
+        @ParameterizedTest
+        @ValueSource(classes = [AssertA::class, AssertZ::class, Assert::class])
+        fun `assert(fact atom)`(assertKind: Class<*>) {
+            val fact = Fact(Atom("a"))
+            createAssert(fact).satisfy(emptyMap())
+
+            assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
+            assertEquals(fact, Program.db.predicates["a/_"]!!.clauses[0])
+        }
+
+        @Test
+        fun `assert(fact structure)`() {
+            val fact = Fact(Structure(Atom("a"), listOf(Atom("b"))))
+            createAssert(fact).satisfy(emptyMap())
+
+            assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
+            assertEquals(fact, Program.db.predicates["a/1"]!!.clauses[0])
+        }
+
+        @Test
+        fun `assert(rule)`() {
+            val rule = Rule(
+                Structure(Atom("a"), listOf(Atom("b"))),
+                Atom("c")
+            )
+            createAssert(rule).satisfy(emptyMap())
+
+            assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
+            assertEquals(rule, Program.db.predicates["a/1"]!!.clauses[0])
+        }
+    }
+
+    @Nested
+    class AssertTests : AssertTestsBase<Assert>() {
+        override fun createAssert(clause: Clause): Structure {
+            return Assert(clause)
+        }
+    }
+
+    @Nested
+    class AssertATests : AssertTestsBase<AssertA>() {
+        override fun createAssert(clause: Clause): Structure {
+            return AssertA(clause)
+        }
+
+        @Test
+        fun `asserta adds to the beginning`() {
+            val rule1 = Rule(
+                Structure(Atom("a"), listOf(Atom("b"))),
+                Atom("c")
+            )
+            val rule2 = Rule(
+                Structure(Atom("a"), listOf(Atom("d"))),
+                Atom("e")
+            )
+            AssertA(rule1).satisfy(emptyMap())
+            AssertA(rule2).satisfy(emptyMap())
+
+            assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
+            assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[0])
+            assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[1])
+        }
+    }
+
+    @Nested
+    class AssertZTests : AssertTestsBase<AssertZ>() {
+        override fun createAssert(clause: Clause): Structure {
+            return AssertZ(clause)
+        }
+
+        @Test
+        fun `assertz adds to the end`() {
+            val rule1 = Rule(
+                Structure(Atom("a"), listOf(Atom("b"))),
+                Atom("c")
+            )
+            val rule2 = Rule(
+                Structure(Atom("a"), listOf(Atom("d"))),
+                Atom("e")
+            )
+            AssertZ(rule1).satisfy(emptyMap())
+            AssertZ(rule2).satisfy(emptyMap())
+
+            assertEquals(1, Program.db.predicates.size, "Expected 1 predicate")
+            assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[0])
+            assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[1])
+        }
+    }
+
+    @Test
+    fun `retract fails silently for unknown predicates`() {
+        val retract = Retract(Atom("unknown"))
+        val result = retract.satisfy(emptyMap())
+
+        assertTrue(result.none(), "Expected no results")
+    }
+
+    @Test
+    fun `simple retract`() {
+        val predicate = Predicate(listOf(Fact(Atom("a"))))
+        Program.db.load(predicate)
+
+        assertEquals(1, Program.query(Atom("a")).count())
+
+        val retract = Retract(Atom("a"))
+
+        assertEquals(1, retract.satisfy(emptyMap()).toList().size, "Expected 1 result")
+        assertEquals(0, predicate.clauses.size, "Expected 0 clauses")
+
+        assertTrue(retract.satisfy(emptyMap()).none())
+    }
+
+    @Test
+    fun `retract atom`() {
+        val predicate = Predicate(listOf(
+            Fact(Atom("a")),
+            Fact(Atom("a")),
+            Fact(Atom("a"))
+        ))
+        Program.db.load(predicate)
+
+        val control = Program.query(Atom("a")).toList()
+
+        assertEquals(3, control.size, "Expected 3 results")
+
+        val retract = Retract(Atom("a"))
+
+        val result = retract.satisfy(emptyMap()).iterator()
+
+        assertEquals(3, predicate.clauses.size, "Expected 3 clauses")
+
+        assertTrue(result.hasNext(), "Expected more results")
+
+        val answer = result.next()
+
+        assertTrue(answer.isSuccess, "Expected success")
+        assertTrue(answer.getOrNull()!!.isEmpty(), "Expected no substitutions")
+
+        assertTrue(result.hasNext(), "Expected more results")
+        assertEquals(2, predicate.clauses.size, "Expected 2 clauses")
+
+        assertTrue(result.next().isSuccess)
+        assertTrue(result.hasNext(), "Expected more results")
+        assertTrue(result.next().isSuccess)
+
+        assertFalse(result.hasNext(), "Expected more results")
+        assertEquals(0, predicate.clauses.size, "Expected no remaining clauses")
+    }
+
+    @Test
+    fun `retract compound with variable`() {
+        val predicate = Predicate(listOf(
+            Fact(Structure(Atom("a"), listOf(Atom("b")))),
+            Fact(Structure(Atom("a"), listOf(Atom("c")))),
+            Fact(Structure(Atom("a"), listOf(Atom("d"))))
+        ))
+        Program.db.load(predicate)
+
+        val control = Program.query(Structure(Atom("a"), listOf(Variable("X")))).toList()
+
+        assertEquals(3, control.size, "Expected 3 results")
+
+        val retract = Retract(Structure(Atom("a"), listOf(Variable("X"))))
+
+        val result = retract.satisfy(emptyMap()).iterator()
+
+        assertEquals(3, predicate.clauses.size, "Expected 3 clauses")
+
+        assertTrue(result.hasNext(), "Expected more results")
+        var answer = result.next()
+
+        assertTrue(answer.isSuccess, "Expected success")
+        var subs = answer.getOrNull()!!
+        assertTrue(subs.isNotEmpty(), "Expected substitutions")
+        assertTrue(Variable("X") in subs, "Expected variable X")
+        assertEquals(Atom("b"), subs[Variable("X")], "Expected b")
+        assertTrue(result.hasNext(), "Expected more results")
+        assertEquals(2, predicate.clauses.size, "Expected 2 clauses")
+
+        answer = result.next()
+
+        assertTrue(answer.isSuccess, "Expected success")
+        subs = answer.getOrNull()!!
+        assertTrue(subs.isNotEmpty(), "Expected substitutions")
+        assertTrue(Variable("X") in subs, "Expected variable X")
+        assertEquals(Atom("c"), subs[Variable("X")], "Expected c")
+        assertTrue(result.hasNext(), "Expected more results")
+        assertEquals(1, predicate.clauses.size, "Expected 1 clause")
+
+        answer = result.next()
+
+        assertTrue(answer.isSuccess, "Expected success")
+        subs = answer.getOrNull()!!
+        assertTrue(subs.isNotEmpty(), "Expected substitutions")
+        assertTrue(Variable("X") in subs, "Expected variable X")
+        assertEquals(Atom("d"), subs[Variable("X")], "Expected d")
+        assertFalse(result.hasNext(), "Expected no more results")
+        assertEquals(0, predicate.clauses.size, "Expected no clauses")
+    }
+
+    @Test
+    fun `custom assert example`() {
+        var query = Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza")))
+
+        var result = Program.query(query).toList()
+        assertEquals(0, result.size, "Expected 0 results")
+
+        var assert: Structure = Assert(Fact(query))
+        assert.satisfy(emptyMap())
+
+        result = Program.query(query).toList()
+        assertEquals(1, result.size, "Expected 1 result")
+        assertTrue(result[0].getOrNull()!!.isEmpty())
+
+        assert = AssertZ(Fact(Structure(Atom("likes"), listOf(Atom("bob"), Atom("sushi")))))
+        assert.satisfy(emptyMap())
+
+        query = Structure(Atom("likes"), listOf(Atom("bob"), Variable("X")))
+
+        result = Program.query(query).toList()
+        assertEquals(1, result.size, "Expected 1 result")
+        assertTrue(result[0].isSuccess, "Expected success")
+        assertEquals(Atom("sushi"), result[0].getOrNull()!![Variable("X")], "Expected sushi")
+
+        query = Structure(Atom("likes"), listOf(Variable("X"), Variable("Y")))
+
+        result = Program.query(query).toList()
+        assertEquals(2, result.size, "Expected 2 results")
+        assertTrue(result[0].isSuccess, "Expected success")
+        var result0 = result[0].getOrNull()!!
+        assertEquals(Atom("alice"), result0[Variable("X")], "Expected alice")
+        assertEquals(Atom("pizza"), result0[Variable("Y")], "Expected pizza")
+        assertTrue(result[1].isSuccess, "Expected success")
+        var result1 = result[1].getOrNull()!!
+        assertEquals(Atom("bob"), result1[Variable("X")], "Expected bob")
+        assertEquals(Atom("sushi"), result1[Variable("Y")], "Expected sushi")
+
+        assert = AssertA(
+            Rule(
+                Structure(Atom("likes"), listOf(Variable("X"), Atom("italian"))),
+                Structure(Atom("likes"), listOf(Variable("X"), Atom("pizza")))
+            )
+        )
+        assert.satisfy(emptyMap())
+
+        result = Program.query(query).toList()
+        assertEquals(3, result.size, "Expected 3 results")
+        assertTrue(result[0].isSuccess, "Expected success")
+        result0 = result[0].getOrNull()!!
+        assertEquals(Atom("alice"), result0[Variable("X")], "Expected alice")
+        assertEquals(Atom("italian"), result0[Variable("Y")], "Expected italian")
+        assertTrue(result[1].isSuccess, "Expected success")
+        result1 = result[1].getOrNull()!!
+        assertEquals(Atom("alice"), result1[Variable("X")], "Expected alice")
+        assertEquals(Atom("pizza"), result1[Variable("Y")], "Expected pizza")
+        assertTrue(result[2].isSuccess, "Expected success")
+        val result2 = result[2].getOrNull()!!
+        assertEquals(Atom("bob"), result2[Variable("X")], "Expected bob")
+        assertEquals(Atom("sushi"), result2[Variable("Y")], "Expected sushi")
+    }
+}

tests/prolog/builtins/IoOperatorsTests.kt

@@ -0,0 +1,164 @@
+package prolog.builtins
+
+import org.junit.jupiter.api.Assertions.*
+import org.junit.jupiter.api.BeforeEach
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.params.ParameterizedTest
+import org.junit.jupiter.params.provider.ValueSource
+import prolog.ast.arithmetic.Float
+import prolog.ast.arithmetic.Integer
+import prolog.ast.terms.Atom
+import prolog.ast.terms.CompoundTerm
+import prolog.ast.terms.Variable
+import java.io.ByteArrayInputStream
+import java.io.ByteArrayOutputStream
+import java.io.PrintStream
+
+class IoOperatorsTests {
+    private var outStream = ByteArrayOutputStream()
+
+    @BeforeEach
+    fun setup() {
+        outStream = ByteArrayOutputStream()
+        System.setOut(PrintStream(outStream))
+    }
+
+    @Test
+    fun dummyTest() {
+        val message = "Hello, World!"
+        print(message)
+        assertEquals(message, outStream.toString(), "Output should match the message")
+    }
+
+    @ParameterizedTest
+    @ValueSource(strings = [
+        "a",
+        "hello",
+        "a very special christmas",
+        "1 2 3 piano"
+    ])
+    fun `write atoms`(name: String) {
+        val write = Write(Atom(name))
+
+        val result = write.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Should return one result")
+        assertTrue(result[0].isSuccess, "Result should be successful")
+        assertEquals(name, outStream.toString(), "Output should match the atom")
+    }
+
+    @Test
+    fun `write structure`() {
+        val write = Write(CompoundTerm(Atom("person"), listOf(Atom("john"), Atom("doe"))))
+
+        val result = write.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Should return one result")
+        assertTrue(result[0].isSuccess, "Result should be successful")
+        assertEquals("person(john, doe)", outStream.toString().trim(), "Output should match the structure")
+    }
+
+    @Test
+    fun `write arithmetic`() {
+        val a = Integer(1)
+        val b = Variable("B")
+        val c = Float(2.0f)
+        val d = Variable("D")
+
+        val mul = Multiply(c, d)
+        val sub = Subtract(b, mul)
+        val expr = EvaluatesTo(a, sub)
+
+        val expected1 = "(1 =:= (B - (2.0 * D)))"
+        val expected2 = "=:=(1, -(B, *(2.0, D)))"
+
+        val write = Write(expr)
+
+        val result = write.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Should return one result")
+        assertTrue(result[0].isSuccess, "Result should be successful")
+
+        val output = outStream.toString()
+        assertTrue(output == expected1 || output == expected2, "Output should match the arithmetic expression")
+    }
+
+    @Test
+    fun `write nl`() {
+        val nl = Nl
+
+        val result = nl.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Should return one result")
+        assertTrue(result[0].isSuccess, "Result should be successful")
+        assertTrue(outStream.toString().contains("\n"), "Output should contain a newline")
+    }
+
+    @Test
+    fun `read term`() {
+        val inputStream = ByteArrayInputStream("hello.".toByteArray())
+        System.setIn(inputStream)
+
+        val read = Read(Variable("X"))
+
+        val result = read.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Should return one result")
+        assertTrue(result[0].isSuccess, "Result should be successful")
+        val answer = result[0].getOrNull()!!
+        assertTrue(answer.containsKey(Variable("X")), "Result should be successful")
+        assertInstanceOf(Atom::class.java, answer[Variable("X")], "Output should be an atom")
+        assertEquals(Atom("hello"), answer[Variable("X")], "Output should match the read term")
+    }
+
+    @Test
+    fun `read between(1, 2, 3)`() {
+        val inputStream = ByteArrayInputStream("between(1, 2, 3).".toByteArray())
+        System.setIn(inputStream)
+
+        val read = Read(Variable("X"))
+
+        val result = read.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Should return one result")
+        assertTrue(result[0].isSuccess, "Result should be successful")
+        val answer = result[0].getOrNull()!!
+        assertTrue(answer.containsKey(Variable("X")), "Result should be successful")
+        assertInstanceOf(CompoundTerm::class.java, answer[Variable("X")], "Output should be a compound term")
+        assertEquals(
+            CompoundTerm(Atom("between"), listOf(Integer(1), Integer(2), Integer(3))),
+            answer[Variable("X")],
+            "Output should match the read term"
+        )
+    }
+
+    @Test
+    fun `read foo(a, X, b, Y, c, Z)`() {
+        val inputStream = ByteArrayInputStream("foo(A, x, B, y, C, z).".toByteArray())
+        System.setIn(inputStream)
+
+        val read = Read(CompoundTerm(Atom("foo"), listOf(
+            Atom("a"),
+            Variable("X"),
+            Atom("b"),
+            Variable("Y"),
+            Atom("c"),
+            Variable("Z")
+        )))
+
+        val result = read.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Should return one result")
+        assertTrue(result[0].isSuccess, "Result should be successful")
+
+        val answer = result[0].getOrNull()!!
+
+        assertTrue(answer.containsKey(Variable("X")), "Result should be successful")
+        assertTrue(answer.containsKey(Variable("Y")), "Result should be successful")
+        assertTrue(answer.containsKey(Variable("Z")), "Result should be successful")
+
+        assertEquals(Atom("x"), answer[Variable("X")], "Output should match the read term")
+        assertEquals(Atom("y"), answer[Variable("Y")], "Output should match the read term")
+        assertEquals(Atom("z"), answer[Variable("Z")], "Output should match the read term")
+    }
+}

tests/prolog/logic/ArithmeticTests.kt

@@ -583,10 +583,23 @@ class ArithmeticTests {
         assertTrue(equivalent(result[0].getOrThrow()[t3]!!, Float(6.0f), result[0].getOrNull()!!), "X should be equal to 6.0")
     }
 
+    @Test
+    fun `addition with negative`() {
+        val t1 = Integer(1)
+        val t2 = Integer(-1)
+        val t3 = Integer(0)
+
+        val result = plus(t1, t2, t3, emptyMap()).toList()
+
+        assertEquals(1, result.size, "There should be one solution")
+        assertTrue(result[0].isSuccess, "Expected success")
+        assertTrue(result[0].getOrNull()!!.isEmpty(), "1 + -1 should already be equal to 0")
+    }
+
     @RepeatedTest(100)
     fun `random test for mul`() {
-        val t1 = Integer((0..1000).random())
+        val t1 = Integer((-1000..1000).random())
-        val t2 = Integer((0..1000).random())
+        val t2 = Integer((-1000..1000).random())
         val t3 = Variable("X")
 
         val result = mul(t1, t2, t3, emptyMap()).toList()

tests/prolog/logic/TermsTests.kt

@@ -0,0 +1,110 @@
+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 variable1 = subs1[variable] as Variable
+
+        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(variable1), "Expected subs to contain the variable")
+        assertEquals(Variable("X@$start@$end1"), subs2[variable1], "Expected subs to contain the new term")
+    }
+}

tests/prolog/logic/UnificationTests.kt

@@ -0,0 +1,370 @@
+package prolog.logic
+
+import org.junit.jupiter.api.Assertions.*
+import org.junit.jupiter.api.Test
+import prolog.Substitutions
+import prolog.ast.arithmetic.Integer
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Structure
+import prolog.ast.terms.Variable
+import prolog.builtins.Add
+import org.junit.jupiter.api.Disabled
+import org.junit.jupiter.api.Nested
+
+/*
+ * Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms
+ */
+class UnificationTests {
+    @Nested
+    class `unify` {
+        @Test
+        fun identical_atoms_unify() {
+            val atom1 = Atom("a")
+            val atom2 = Atom("a")
+
+            val result = unify(atom1, atom2)
+
+            assertTrue(result.isSuccess, "Identical atoms should unify")
+            assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made")
+        }
+
+        @Test
+        fun different_atoms_do_not_unify() {
+            val atom1 = Atom("a")
+            val atom2 = Atom("b")
+
+            val result = unify(atom1, atom2)
+
+            assertFalse(result.isSuccess, "Different atoms should not unify")
+        }
+
+        /**
+         * ?- X = X.
+         * true.
+         */
+        @Test
+        fun identical_variables_unify() {
+            val variable1 = Variable("X")
+            val variable2 = Variable("X")
+
+            val result = unify(variable1, variable2)
+
+            assertTrue(result.isSuccess, "Identical variables should unify")
+            assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made")
+        }
+
+        @Test
+        fun variable_unifies_with_atom() {
+            val variable = Variable("X")
+            val atom = Atom("a")
+
+            val result = unify(atom, variable)
+
+            assertTrue(result.isSuccess, "Variable should unify with atom")
+            assertEquals(1, result.getOrNull()!!.size, "There should be one substitution")
+            assertEquals(atom, result.getOrNull()!![variable], "Variable should be substituted with atom")
+        }
+
+        @Test
+        fun variables_alias_when_unified() {
+            val variable1 = Variable("X")
+            val variable2 = Variable("Y")
+
+            val result = unify(variable1, variable2)
+
+            assertTrue(result.isSuccess)
+            assertEquals(1, result.getOrNull()!!.size)
+            assertEquals(variable2, result.getOrNull()!![variable1], "Variable 1 should alias to variable 2")
+        }
+
+        @Test
+        fun identical_compound_terms_unify() {
+            val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
+            val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
+
+            val result = unify(structure1, structure2)
+
+            assertTrue(result.isSuccess, "Identical compound terms should unify")
+            assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made")
+        }
+
+        @Test
+        fun compound_terms_with_different_arguments_do_not_unify() {
+            val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
+            val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("c")))
+
+            val result = unify(structure1, structure2)
+
+            assertFalse(result.isSuccess, "Different compound terms should not unify")
+        }
+
+        @Test
+        fun compound_terms_with_different_functors_do_not_unify() {
+            val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
+            val structure2 = Structure(Atom("g"), listOf(Atom("a"), Atom("b")))
+
+            val result = unify(structure1, structure2)
+
+            assertFalse(result.isSuccess, "Compound terms with different functors should not unify")
+        }
+
+        /**
+         * ?- X = f(a, b).
+         * X = f(a, b).
+         */
+        @Test
+        fun variable_unifies_with_compound_term() {
+            val variable = Variable("X")
+            val structure = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
+
+            val result = unify(variable, structure)
+
+            assertTrue(result.isSuccess, "Variable should unify with compound term")
+
+            val subs = result.getOrNull()!!
+
+            assertEquals(1, subs.size, "There should be one substitution")
+            assertTrue(subs.containsKey(variable), "Variable should be in the substitution map")
+            assertTrue(
+                equivalent(Structure(Atom("f"), listOf(Atom("a"), Atom("b"))), subs[variable]!!, subs),
+                "Variable should be substituted with compound term"
+            )
+        }
+
+        @Test
+        fun compound_term_with_variable_unifies_with_part() {
+            val variable = Variable("X")
+            val structure1 = Structure(Atom("f"), listOf(Atom("a"), variable))
+            val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
+
+            val result = unify(structure1, structure2)
+
+            assertTrue(result.isSuccess, "Compound term with variable should unify with part")
+
+            val subs = result.getOrNull()!!
+
+            assertEquals(1, subs.size, "There should be one substitution")
+            assertTrue(subs.containsKey(variable), "Variable should be in the substitution map")
+            val equivalence = equivalent(Atom("b"), subs[variable]!!, subs)
+            assertTrue(equivalence, "Variable should be substituted with atom")
+        }
+
+        @Test
+        fun compound_terms_with_variable_arguments_lists_alias_variables() {
+            val variable1 = Variable("X")
+            val variable2 = Variable("Y")
+
+            val structure1 = Structure(Atom("f"), listOf(variable1))
+            val structure2 = Structure(Atom("f"), listOf(variable2))
+
+            val result = unify(structure1, structure2)
+
+            assertTrue(result.isSuccess, "Compound terms with variable arguments should unify")
+
+            val subs = result.getOrNull()!!
+
+            assertEquals(1, subs.size, "There should be one substitution")
+            assertTrue(subs.containsKey(variable1), "Variable 1 should be in the substitution map")
+            assertEquals(variable2, subs[variable1], "Variable 1 should alias to variable 2")
+        }
+
+        /**
+         * f(X) = f(Y, Z)
+         */
+        @Test
+        fun compound_terms_with_different_arity_do_not_unify() {
+            val structure1 = Structure(Atom("f"), listOf(Variable("X")))
+            val structure2 = Structure(Atom("f"), listOf(Variable("Y"), Variable("Z")))
+
+            val result = unify(structure1, structure2)
+
+            assertFalse(result.isSuccess, "Compound terms with different arity should not unify")
+        }
+
+        /**
+         * ?- f(g(X)) = f(Y).
+         * Y = g(X).
+         */
+        @Test
+        fun nested_compound_terms_with_variables_unify() {
+            val variable2 = Variable("Y")
+
+            val structure1 = Structure(Atom("f"), listOf(Structure(Atom("g"), listOf(Variable("X")))))
+            val structure2 = Structure(Atom("f"), listOf(variable2))
+
+            val result = unify(structure1, structure2)
+
+            assertTrue(result.isSuccess, "Nested compound terms with variables should unify")
+
+            val subs = result.getOrNull()!!
+
+            assertEquals(1, subs.size, "There should be one substitution")
+            assertTrue(subs.containsKey(variable2), "Variable 2 should be in the substitution map")
+            assertTrue(
+                equivalent(Structure(Atom("g"), listOf(Variable("X"))), subs[variable2]!!, subs),
+                "Variable should be substituted with compound term"
+            )
+        }
+
+        /**
+         * ?- f(g(X), X) = f(Y, a).
+         * X = a,
+         * Y = g(a).
+         */
+        @Test
+        fun compound_terms_with_more_variables() {
+            val variable1 = Variable("X")
+            val variable2 = Variable("Y")
+
+            val structure1 = Structure(Atom("f"), listOf(Structure(Atom("g"), listOf(variable1)), variable1))
+            val structure2 = Structure(Atom("f"), listOf(variable2, Atom("a")))
+
+            val result = unify(structure1, structure2)
+
+            assertTrue(result.isSuccess, "Compound terms with more variables should unify")
+
+            val subs = result.getOrNull()!!
+
+            assertEquals(2, subs.size, "There should be two substitutions")
+            assertTrue(subs.containsKey(variable1), "Variable 1 should be in the substitution map")
+            assertTrue(
+                equivalent(Atom("a"), subs[variable1]!!, subs),
+                "Variable 1 should be substituted with atom"
+            )
+            assertTrue(subs.containsKey(variable2), "Variable 2 should be in the substitution map")
+            assertTrue(
+                equivalent(Structure(Atom("g"), listOf(Atom("a"))), subs[variable2]!!, subs),
+                "Variable 2 should be substituted with compound term"
+
+            )
+        }
+
+        /**
+         * ?- X = f(X).
+         * X = f(f(X)).
+         */
+        @Test
+        @Disabled("If the occurs check is applied, this should fail")
+        fun recursive_unification() {
+            val variable1 = Variable("X")
+            val structure2 = Structure(Atom("f"), listOf(Variable("X")))
+
+            val result = unifyLazy(variable1, structure2, emptyMap()).toList()
+
+            assertEquals(1, result.size, "There should be one result")
+            assertTrue(result[0].isSuccess, "Recursive unification should succeed")
+
+            val subs = result[0].getOrNull()!!
+
+            assertEquals(1, subs.size, "There should be one substitution")
+            assertTrue(subs.containsKey(variable1), "Variable should be in the substitution map")
+            assertEquals(structure2, subs[variable1], "Variable should be substituted with compound term")
+        }
+
+        /**
+         * ?- X = bar, Y = bar, X = Y.
+         * X = Y, Y = bar.
+         */
+        @Test
+        fun multiple_unification() {
+            val variable1 = Variable("X")
+            val variable2 = Variable("Y")
+            val atom = Atom("bar")
+
+            val map: Substitutions = mapOf(
+                variable1 to atom,
+                variable2 to atom
+            )
+            val result = unifyLazy(variable1, variable2, map).toList()
+
+            assertEquals(1, result.size, "There should be one substitution")
+            assertTrue(result[0].isSuccess, "Multiple unification should succeed")
+            assertEquals(0, result[0].getOrNull()!!.size, "No (additional) substitutions should be made")
+        }
+
+        /**
+         * ?- a = a().
+         * false.
+         */
+        @Test
+        fun atom_with_different_arity() {
+            val atom1 = Atom("a")
+            val structure2 = Structure(Atom("a"), emptyList())
+
+            val result = unify(atom1, structure2)
+
+            assertFalse(result.isSuccess, "Atom with different arity should not unify")
+        }
+
+        @Test
+        fun identical_integers_unify() {
+            val int1 = Integer(1)
+            val int2 = Integer(1)
+
+            val result = unify(int1, int2)
+
+            assertTrue(result.isSuccess, "Identical integers should unify")
+            assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made")
+        }
+
+        @Test
+        fun different_integers_do_not_unify() {
+            val int1 = Integer(1)
+            val int2 = Integer(2)
+
+            val result = unify(int1, int2)
+
+            assertFalse(result.isSuccess, "Different integers should not unify")
+        }
+
+
+        @Test
+        fun `1 + 2 does not unify with 3`() {
+            val expr1 = Add(Integer(1), Integer(2))
+            val expr2 = Integer(3)
+
+            val result = unify(expr1, expr2)
+
+            assertFalse(result.isSuccess, "1 + 2 should not unify with 3")
+        }
+    }
+
+    @Nested
+    class `applySubstitution` {
+        @Test
+        fun `apply substitution without sub`() {
+            val term = Variable("X")
+            val subs: Substitutions = emptyMap()
+
+            val result = applySubstitution(term, subs)
+
+            assertEquals(term, result)
+        }
+
+        @Test
+        fun `apply single substitution`() {
+            val sub = Variable("X") to Integer(5)
+            val subs: Substitutions = mapOf(sub)
+
+            val term = Variable("X")
+
+            val result = applySubstitution(term, subs)
+
+            assertEquals(Integer(5), result)
+        }
+
+        @Test
+        fun `apply chained substitution`() {
+            val sub1 = Variable("HP") to Variable("HP(19)")
+            val sub2 = Variable("HP(19)") to Integer(35)
+
+            val subs: Substitutions = mapOf(sub1, sub2)
+
+            val term = Variable("HP")
+
+            val result = applySubstitution(term, subs)
+
+            assertEquals(Integer(35), result)
+        }
+    }
+}

tests/prolog/logic/UnifyTests.kt

@@ -1,327 +0,0 @@
-package prolog.logic
-
-import org.junit.jupiter.api.Assertions.*
-import org.junit.jupiter.api.Disabled
-import org.junit.jupiter.api.Test
-import prolog.Substitutions
-import prolog.ast.arithmetic.Integer
-import prolog.ast.terms.Atom
-import prolog.ast.terms.Structure
-import prolog.ast.terms.Variable
-import prolog.builtins.Add
-
-/*
- * Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms
- */
-class UnifyTests {
-    @Test
-    fun identical_atoms_unify() {
-        val atom1 = Atom("a")
-        val atom2 = Atom("a")
-
-        val result = unify(atom1, atom2)
-
-        assertTrue(result.isSuccess, "Identical atoms should unify")
-        assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made")
-    }
-
-    @Test
-    fun different_atoms_do_not_unify() {
-        val atom1 = Atom("a")
-        val atom2 = Atom("b")
-
-        val result = unify(atom1, atom2)
-
-        assertFalse(result.isSuccess, "Different atoms should not unify")
-    }
-
-    /**
-     * ?- X = X.
-     * true.
-     */
-    @Test
-    fun identical_variables_unify() {
-        val variable1 = Variable("X")
-        val variable2 = Variable("X")
-
-        val result = unify(variable1, variable2)
-
-        assertTrue(result.isSuccess, "Identical variables should unify")
-        assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made")
-    }
-
-    @Test
-    fun variable_unifies_with_atom() {
-        val variable = Variable("X")
-        val atom = Atom("a")
-
-        val result = unify(atom, variable)
-
-        assertTrue(result.isSuccess, "Variable should unify with atom")
-        assertEquals(1, result.getOrNull()!!.size, "There should be one substitution")
-        assertEquals(atom, result.getOrNull()!![variable], "Variable should be substituted with atom")
-    }
-
-    @Test
-    fun variables_alias_when_unified() {
-        val variable1 = Variable("X")
-        val variable2 = Variable("Y")
-
-        val result = unify(variable1, variable2)
-
-        assertTrue(result.isSuccess)
-        assertEquals(1, result.getOrNull()!!.size)
-        assertEquals(variable2, result.getOrNull()!![variable1], "Variable 1 should alias to variable 2")
-    }
-
-    @Test
-    fun identical_compound_terms_unify() {
-        val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
-        val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
-
-        val result = unify(structure1, structure2)
-
-        assertTrue(result.isSuccess, "Identical compound terms should unify")
-        assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made")
-    }
-
-    @Test
-    fun compound_terms_with_different_arguments_do_not_unify() {
-        val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
-        val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("c")))
-
-        val result = unify(structure1, structure2)
-
-        assertFalse(result.isSuccess, "Different compound terms should not unify")
-    }
-
-    @Test
-    fun compound_terms_with_different_functors_do_not_unify() {
-        val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
-        val structure2 = Structure(Atom("g"), listOf(Atom("a"), Atom("b")))
-
-        val result = unify(structure1, structure2)
-
-        assertFalse(result.isSuccess, "Compound terms with different functors should not unify")
-    }
-
-    /**
-     * ?- X = f(a, b).
-     * X = f(a, b).
-     */
-    @Test
-    fun variable_unifies_with_compound_term() {
-        val variable = Variable("X")
-        val structure = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
-
-        val result = unify(variable, structure)
-
-        assertTrue(result.isSuccess, "Variable should unify with compound term")
-
-        val subs = result.getOrNull()!!
-
-        assertEquals(1, subs.size, "There should be one substitution")
-        assertTrue(subs.containsKey(variable), "Variable should be in the substitution map")
-        assertTrue(
-            equivalent(Structure(Atom("f"), listOf(Atom("a"), Atom("b"))), subs[variable]!!, subs),
-            "Variable should be substituted with compound term"
-        )
-    }
-
-    @Test
-    fun compound_term_with_variable_unifies_with_part() {
-        val variable = Variable("X")
-        val structure1 = Structure(Atom("f"), listOf(Atom("a"), variable))
-        val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
-
-        val result = unify(structure1, structure2)
-
-        assertTrue(result.isSuccess, "Compound term with variable should unify with part")
-
-        val subs = result.getOrNull()!!
-
-        assertEquals(1, subs.size, "There should be one substitution")
-        assertTrue(subs.containsKey(variable), "Variable should be in the substitution map")
-        val equivalence = equivalent(Atom("b"), subs[variable]!!, subs)
-        assertTrue(equivalence, "Variable should be substituted with atom")
-    }
-
-    @Test
-    fun compound_terms_with_variable_arguments_lists_alias_variables() {
-        val variable1 = Variable("X")
-        val variable2 = Variable("Y")
-
-        val structure1 = Structure(Atom("f"), listOf(variable1))
-        val structure2 = Structure(Atom("f"), listOf(variable2))
-
-        val result = unify(structure1, structure2)
-
-        assertTrue(result.isSuccess, "Compound terms with variable arguments should unify")
-
-        val subs = result.getOrNull()!!
-
-        assertEquals(1, subs.size, "There should be one substitution")
-        assertTrue(subs.containsKey(variable1), "Variable 1 should be in the substitution map")
-        assertEquals(variable2, subs[variable1], "Variable 1 should alias to variable 2")
-    }
-
-    /**
-     * f(X) = f(Y, Z)
-     */
-    @Test
-    fun compound_terms_with_different_arity_do_not_unify() {
-        val structure1 = Structure(Atom("f"), listOf(Variable("X")))
-        val structure2 = Structure(Atom("f"), listOf(Variable("Y"), Variable("Z")))
-
-        val result = unify(structure1, structure2)
-
-        assertFalse(result.isSuccess, "Compound terms with different arity should not unify")
-    }
-
-    /**
-     * ?- f(g(X)) = f(Y).
-     * Y = g(X).
-     */
-    @Test
-    fun nested_compound_terms_with_variables_unify() {
-        val variable2 = Variable("Y")
-
-        val structure1 = Structure(Atom("f"), listOf(Structure(Atom("g"), listOf(Variable("X")))))
-        val structure2 = Structure(Atom("f"), listOf(variable2))
-
-        val result = unify(structure1, structure2)
-
-        assertTrue(result.isSuccess, "Nested compound terms with variables should unify")
-
-        val subs = result.getOrNull()!!
-
-        assertEquals(1, subs.size, "There should be one substitution")
-        assertTrue(subs.containsKey(variable2), "Variable 2 should be in the substitution map")
-        assertTrue(
-            equivalent(Structure(Atom("g"), listOf(Variable("X"))), subs[variable2]!!, subs),
-            "Variable should be substituted with compound term"
-        )
-    }
-
-    /**
-     * ?- f(g(X), X) = f(Y, a).
-     * X = a,
-     * Y = g(a).
-     */
-    @Test
-    fun compound_terms_with_more_variables() {
-        val variable1 = Variable("X")
-        val variable2 = Variable("Y")
-
-        val structure1 = Structure(Atom("f"), listOf(Structure(Atom("g"), listOf(variable1)), variable1))
-        val structure2 = Structure(Atom("f"), listOf(variable2, Atom("a")))
-
-        val result = unify(structure1, structure2)
-
-        assertTrue(result.isSuccess, "Compound terms with more variables should unify")
-
-        val subs = result.getOrNull()!!
-
-        assertEquals(2, subs.size, "There should be two substitutions")
-        assertTrue(subs.containsKey(variable1), "Variable 1 should be in the substitution map")
-        assertTrue(
-            equivalent(Atom("a"), subs[variable1]!!, subs),
-            "Variable 1 should be substituted with atom"
-        )
-        assertTrue(subs.containsKey(variable2), "Variable 2 should be in the substitution map")
-        assertTrue(
-            equivalent(Structure(Atom("g"), listOf(Atom("a"))), subs[variable2]!!, subs),
-            "Variable 2 should be substituted with compound term"
-
-        )
-    }
-
-    /**
-     * ?- X = f(X).
-     * X = f(f(X)).
-     */
-    @Test
-    fun recursive_unification() {
-        val variable1 = Variable("X")
-        val structure2 = Structure(Atom("f"), listOf(Variable("X")))
-
-        val result = unifyLazy(variable1, structure2, emptyMap()).toList()
-
-        assertEquals(1, result.size, "There should be one result")
-        assertTrue(result[0].isSuccess, "Recursive unification should succeed")
-
-        val subs = result[0].getOrNull()!!
-
-        assertEquals(1, subs.size, "There should be one substitution")
-        assertTrue(subs.containsKey(variable1), "Variable should be in the substitution map")
-        assertEquals(structure2, subs[variable1], "Variable should be substituted with compound term")
-    }
-
-    /**
-     * ?- X = bar, Y = bar, X = Y.
-     * X = Y, Y = bar.
-     */
-    @Disabled
-    @Test
-    fun multiple_unification() {
-        val variable1 = Variable("X")
-        val variable2 = Variable("Y")
-        val atom = Atom("bar")
-
-        val map: Substitutions = mapOf(
-            variable1 to atom,
-            variable2 to atom
-        )
-        val result = unifyLazy(variable1, variable2, map).toList()
-
-        assertEquals(1, result.size, "There should be one substitution")
-        assertTrue(result[0].isSuccess, "Multiple unification should succeed")
-        assertEquals(0, result[0].getOrNull()!!.size, "No (additional) substitutions should be made")
-    }
-
-    /**
-     * ?- a = a().
-     * false.
-     */
-    @Test
-    fun atom_with_different_arity() {
-        val atom1 = Atom("a")
-        val structure2 = Structure(Atom("a"), emptyList())
-
-        val result = unify(atom1, structure2)
-
-        assertFalse(result.isSuccess, "Atom with different arity should not unify")
-    }
-
-    @Test
-    fun identical_integers_unify() {
-        val int1 = Integer(1)
-        val int2 = Integer(1)
-
-        val result = unify(int1, int2)
-
-        assertTrue(result.isSuccess, "Identical integers should unify")
-        assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made")
-    }
-
-    @Test
-    fun different_integers_do_not_unify() {
-        val int1 = Integer(1)
-        val int2 = Integer(2)
-
-        val result = unify(int1, int2)
-
-        assertFalse(result.isSuccess, "Different integers should not unify")
-    }
-
-
-    @Test
-    fun `1 + 2 does not unify with 3`() {
-        val expr1 = Add(Integer(1), Integer(2))
-        val expr2 = Integer(3)
-
-        val result = unify(expr1, expr2)
-
-        assertFalse(result.isSuccess, "1 + 2 should not unify with 3")
-    }
-}