Retract

.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>

src/Main.kt

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

src/interpreter/Preprocessor.kt

@@ -66,71 +66,53 @@ 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" -> 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" -> {
-                        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)
-                    }
+                    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 } -> 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)
 
-                    term.functor == "-/2" && args.all { it is Expression } -> {
-                        Subtract(args[0] as Expression, args[1] as Expression)
+                    // Database
+                    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 == "+/1" && args.all { it is Expression } -> {
-                        Positive(args[0] as Expression)
+                    term.functor == "asserta/1" -> {
+                        if (args[0] is Rule) {
+                            AssertA(args[0] as Rule)
+                        } else {
+                            AssertA(Fact(args[0] as Head))
+                        }
                     }
-
-                    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)
+                    term.functor == "assertz/1" -> {
+                        if (args[0] is Rule) {
+                            AssertZ(args[0] as Rule)
+                        } else {
+                            AssertZ(Fact(args[0] as Head))
+                        }
                     }
 
                     // Other

src/parser/grammars/TermsGrammar.kt

@@ -31,10 +31,12 @@ 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) }
@@ -66,42 +68,43 @@ 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))
     }
 
-    // Level 1000 - conjunction (,)
-    protected val term1000: Parser<Term> by (term700 * zeroOrMore(comma * term700)) use {
-        t2.fold(t1) { acc, (_, term) -> CompoundTerm(Atom(","), listOf(acc, term)) }
+    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)) }
     }
 
-    // Level 1100 - disjunction (;)
-    protected val term1100: Parser<Term> by (term1000 * zeroOrMore(semicolon * term1000)) use {
-        t2.fold(t1) { acc, (_, term) -> CompoundTerm(Atom(";"), 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 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 term1100
+    protected val term: Parser<Term> by term1200
     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 {
-    private val internalDb = Database("")
-    private val databases: MutableList<Database> = mutableListOf(internalDb)
+    val internalDb = Database("")
+    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>) = internalDb.load(clauses)
+    fun load(clauses: List<Clause>, index: Int? = null) = internalDb.load(clauses, index)
 
     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 {
-    private var predicates: Map<Functor, Predicate> = emptyMap()
+    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>) {
+    fun load(clauses: List<Clause>, index: Int? = null) {
         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)
+                predicate.add(clause, index)
             } 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) : Resolvent {
+abstract class Clause(val head: Head, val body: Body) : Term, Resolvent {
     val functor: Functor = head.functor
 
     override fun solve(goal: Goal, subs: Substitutions): Answers = sequence {
@@ -70,4 +70,18 @@ abstract class Clause(val head: Head, val body: Body) : 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) {
+    fun add(clause: Clause, index: Int? = null) {
         require(clause.functor == functor) { "Clause functor does not match predicate functor" }
-        clauses.add(clause)
+        if (index != null) clauses.add(index, clause) else clauses.add(clause)
     }
 
     /**

src/prolog/builtins/databaseOperators.kt

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

tests/interpreter/PreprocessorTests.kt

@@ -6,6 +6,8 @@ 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.*
 
@@ -498,4 +500,109 @@ 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

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

@@ -0,0 +1,286 @@
+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")
+    }
+}