.idea/2025LogProg-PrologInterpreter.iml

@@ -1,8 +0,0 @@
-<?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

@@ -1,8 +0,0 @@
-<?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>

src/Main.kt

@@ -1,4 +1,5 @@
 import com.xenomachina.argparser.ArgParser
+import com.xenomachina.argparser.mainBody
 import interpreter.FileLoader
 import io.GhentPrologArgParser
 import io.Logger

src/interpreter/Preprocessor.kt

@@ -66,53 +66,71 @@ open class Preprocessor {
 
                 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" -> {
-                    term.functor == "\\=/2" -> NotUnify(args[0], args[1])
+                        Unify(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" -> {
-                    term.functor == "=:=/2" && args.all { it is Expression } -> EvaluatesTo(args[0] as Expression, args[1] as Expression)
+                        NotUnify(args[0], args[1])
-                    term.functor == "is/2" && args.all { it is Expression } -> Is(args[0] as Expression, args[1] as Expression)
+                    }
+
+                    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 == "-/1" && args.all { it is Expression } -> {
-                    term.functor == "-/2" && args.all { it is Expression } -> Subtract(args[0] as Expression, args[1] as Expression)
+                        Negate(args[0] 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 == "-/2" && args.all { it is Expression } -> {
-                    term.functor == "retract/1" -> Retract(args[0])
+                        Subtract(args[0] as Expression, args[1] as Expression)
-                    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) {
+                    term.functor == "+/1" && args.all { it is Expression } -> {
-                            AssertA(args[0] as Rule)
+                        Positive(args[0] as Expression)
-                        } else {
-                            AssertA(Fact(args[0] as Head))
-                        }
                     }
-                    term.functor == "assertz/1" -> {
+
-                        if (args[0] is Rule) {
+                    term.functor == "+/2" && args.all { it is Expression } -> {
-                            AssertZ(args[0] as Rule)
+                        Add(args[0] as Expression, args[1] as Expression)
-                        } else {
+                    }
-                            AssertZ(Fact(args[0] as Head))
+
-                        }
+                    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)
                     }
 
                     // Other

src/parser/grammars/TermsGrammar.kt

@@ -31,12 +31,10 @@ import prolog.ast.terms.*
  * | 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) }
@@ -68,43 +66,42 @@ open class TermsGrammar : Tokens() {
             or int
             )
 
+    // Level 200 - prefix operators (+, -, \)
     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)
 
+    // Level 400 - multiplication, division
     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)) }
     }
 
+    // Level 500 - addition, subtraction
     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)) }
     }
 
+    // Level 700 - comparison operators
     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 }
+    // Level 1000 - conjunction (,)
-    protected val term1000: Parser<Term> by (term700 * zeroOrMore(op1000 * term700)) use {
+    protected val term1000: Parser<Term> by (term700 * zeroOrMore(comma * term700)) use {
-        t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
+        t2.fold(t1) { acc, (_, term) -> CompoundTerm(Atom(","), listOf(acc, term)) }
     }
 
-    protected val op1100: Parser<String> by (semicolon) use { text }
+    // Level 1100 - disjunction (;)
-    protected val term1100: Parser<Term> by (term1000 * zeroOrMore(op1100 * term1000)) use {
+    protected val term1100: Parser<Term> by (term1000 * zeroOrMore(semicolon * term1000)) use {
-        t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
+        t2.fold(t1) { acc, (_, term) -> CompoundTerm(Atom(";"), listOf(acc, term)) }
-    }
-
-    protected val op1200: Parser<String> by (neck) use { text }
-    protected val term1200: Parser<Term> by (term1100 * 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 term: Parser<Term> by term1100
     protected val termNoConjunction: Parser<Term> by term700
 
     // Parts for clauses

src/prolog/Program.kt

@@ -12,8 +12,8 @@ import prolog.ast.terms.Goal
  * This object is a singleton that manages a list of databases.
  */
 object Program : Resolvent {
-    val internalDb = Database("")
+    private val internalDb = Database("")
-    val databases: MutableList<Database> = mutableListOf(internalDb)
+    private val databases: MutableList<Database> = mutableListOf(internalDb)
 
     var storeNewLine: Boolean = false
     var variableRenamingStart: Int = 0
@@ -35,7 +35,7 @@ object Program : Resolvent {
         }
     }
 
-    fun load(clauses: List<Clause>, index: Int? = null) = internalDb.load(clauses, index)
+    fun load(clauses: List<Clause>) = internalDb.load(clauses)
 
     fun clear() {
         databases.forEach { it.clear() }

src/prolog/ast/Database.kt

@@ -14,7 +14,7 @@ import prolog.ast.terms.Goal
  * Prolog Program or Database
  */
 class Database(val sourceFile: String): Resolvent {
-    var predicates: Map<Functor, Predicate> = emptyMap()
+    private var predicates: Map<Functor, Predicate> = emptyMap()
 
     fun initialize() {
         Logger.info("Initializing database from $sourceFile")
@@ -39,14 +39,14 @@ class Database(val sourceFile: String): Resolvent {
     /**
      * Loads a list of clauses into the program.
      */
-    fun load(clauses: List<Clause>, index: Int? = null) {
+    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, index)
+                predicate.add(clause)
             } else {
                 // If the predicate does not exist, create a new one
                 predicates += Pair(functor, Predicate(listOf(clause)))

src/prolog/ast/logic/Clause.kt

@@ -19,7 +19,7 @@ import prolog.logic.unifyLazy
  * @see [prolog.ast.terms.Variable]
  * @see [Predicate]
  */
-abstract class Clause(val head: Head, val body: Body) : Term, Resolvent {
+abstract class Clause(val head: Head, val body: Body) : Resolvent {
     val functor: Functor = head.functor
 
     override fun solve(goal: Goal, subs: Substitutions): Answers = sequence {
@@ -70,18 +70,4 @@ abstract class Clause(val head: Head, val body: Body) : Term, Resolvent {
     }
 
     override fun toString(): String = if (body is True) head.toString() else "$head :- $body"
-
-    override fun equals(other: Any?): Boolean {
-        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/Predicate.kt

@@ -36,9 +36,9 @@ class Predicate : Resolvent {
     /**
      * Adds a clause to the predicate.
      */
-    fun add(clause: Clause, index: Int? = null) {
+    fun add(clause: Clause) {
         require(clause.functor == functor) { "Clause functor does not match predicate functor" }
-        if (index != null) clauses.add(index, clause) else clauses.add(clause)
+        clauses.add(clause)
     }
 
     /**

src/prolog/builtins/databaseOperators.kt

@@ -1,83 +0,0 @@
-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.Program
-import prolog.ast.terms.Functor
-import prolog.ast.terms.Term
-import prolog.ast.logic.Fact
-import prolog.ast.Database
-import prolog.ast.terms.Operator
-import prolog.logic.unifyLazy
-
-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
-        Program.load(listOf(clause), 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
-        Program.load(listOf(clause))
-
-        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
-
-        Program.databases
-            .filter { it.predicates.containsKey(functorName) }
-            .mapNotNull { it.predicates[functorName] }
-            .map { predicate ->
-                val clausesIterator = predicate.clauses.iterator()
-                while (clausesIterator.hasNext()) {
-                    val clause = clausesIterator.next()
-                    unifyLazy(term, clause.head, subs).forEach { unifyResult ->
-                        unifyResult.fold(
-                            onSuccess = { substitutions ->
-                                // If unification is successful, remove the clause
-                                yield(Result.success(substitutions))
-                                clausesIterator.remove()
-                            },
-                            onFailure = {
-                                // If unification fails, do nothing
-                            }
-                        )
-                    }
-                }
-            }
-    }
-}

src/repl/Repl.kt

@@ -42,9 +42,10 @@ class Repl {
         val iterator = answers.iterator()
 
         if (!iterator.hasNext()) {
-            io.say("false.\n")
+            io.say("false.")
         } else {
-            io.say(prettyPrint(iterator.next()))
+            var previous = iterator.next()
+            io.say(prettyPrint(previous))
 
             while (iterator.hasNext()) {
                 var command = io.prompt("")
@@ -56,7 +57,8 @@ class Repl {
 
                 when (command) {
                     ";" -> {
-                        io.say(prettyPrint(iterator.next()))
+                        previous = iterator.next()
+                        io.say(prettyPrint(previous))
                     }
                     "a" -> return
                     "." -> return
@@ -86,7 +88,7 @@ class Repl {
                 val subs = result.getOrNull()!!
                 if (subs.isEmpty()) {
                     io.checkNewLine()
-                    return "true."
+                    return "true.\n"
                 }
                 return subs.entries.joinToString(",\n") { "${it.key} = ${it.value}" }
             },

tests/interpreter/PreprocessorTests.kt

@@ -6,8 +6,6 @@ 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.*
 
@@ -500,109 +498,4 @@ class PreprocessorTests {
             )
         }
     }
-
-    @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)
-        }
-    }
 }

tests/parser/builtins/DatabaseOperatorsParserTests.kt

@@ -1,65 +0,0 @@
-package parser.builtins
-
-import com.github.h0tk3y.betterParse.grammar.Grammar
-import com.github.h0tk3y.betterParse.grammar.parseToEnd
-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
-import kotlin.test.assertEquals
-
-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)
-    }
-}

tests/prolog/builtins/DatabaseOperatorsTests.kt

@@ -1,286 +0,0 @@
-package prolog.builtins
-
-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.params.ParameterizedTest
-import org.junit.jupiter.params.provider.ValueSource
-import prolog.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
-import kotlin.test.assertTrue
-
-class DatabaseOperatorsTests {
-    @BeforeEach
-    fun setup() {
-        Program.clear()
-    }
-
-    abstract class AssertTestsBase<T : Structure> {
-        protected abstract fun createAssert(clause: Clause): Structure
-
-        @BeforeEach
-        fun setup() {
-            Program.clear()
-        }
-
-        @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.internalDb.predicates.size, "Expected 1 predicate")
-            assertEquals(fact, Program.internalDb.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.internalDb.predicates.size, "Expected 1 predicate")
-            assertEquals(fact, Program.internalDb.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.internalDb.predicates.size, "Expected 1 predicate")
-            assertEquals(rule, Program.internalDb.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.internalDb.predicates.size, "Expected 1 predicate")
-            assertEquals(rule2, Program.internalDb.predicates["a/1"]!!.clauses[0])
-            assertEquals(rule1, Program.internalDb.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.internalDb.predicates.size, "Expected 1 predicate")
-            assertEquals(rule1, Program.internalDb.predicates["a/1"]!!.clauses[0])
-            assertEquals(rule2, Program.internalDb.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.internalDb.load(predicate)
-
-        assertEquals(1, Program.query(Atom("a")).count())
-
-        val retract = Retract(Atom("a"))
-
-        assertTrue(retract.satisfy(emptyMap()).any(), "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.internalDb.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())
-
-        assertEquals(3, predicate.clauses.size, "Expected 3 clauses")
-
-        var answer = result.first()
-
-        assertTrue(answer.isSuccess, "Expected success")
-        var subs = answer.getOrNull()!!
-        assertTrue(subs.isEmpty(), "Expected no substitutions")
-        assertEquals(2, predicate.clauses.size, "Expected 2 clauses")
-
-        assertTrue(result.first().isSuccess)
-        assertTrue(result.first().isSuccess)
-
-        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.internalDb.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())
-
-        assertEquals(3, predicate.clauses.size, "Expected 3 clauses")
-
-        var answer = result.first()
-
-        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")
-        assertEquals(2, predicate.clauses.size, "Expected 2 clauses")
-
-        answer = result.first()
-
-        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")
-        assertEquals(1, predicate.clauses.size, "Expected 1 clause")
-
-        answer = result.first()
-
-        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")
-        assertEquals(0, predicate.clauses.size, "Expected no clauses")
-
-        assertEquals(0, result.count(), "Expected no remaining results")
-    }
-
-    @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")
-    }
-}