Retract

src/prolog/Program.kt

@@ -13,7 +13,7 @@ import prolog.ast.terms.Goal
  */
 object Program : Resolvent {
     val internalDb = Database("")
-    private val databases: MutableList<Database> = mutableListOf(internalDb)
+    val databases: MutableList<Database> = mutableListOf(internalDb)
 
     var storeNewLine: Boolean = false
     var variableRenamingStart: Int = 0

src/prolog/Substitution.kt

@@ -8,4 +8,4 @@ abstract class Substitution(val from: Term, val to: Term) {
 }
 typealias Substitutions = Map<Term, Term>
 typealias Answer = Result<Substitutions>
-typealias Answers = Sequence<Answer>
+typealias Answers = Sequence<Answer>

src/prolog/builtins/databaseOperators.kt

@@ -8,6 +8,11 @@ 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"
@@ -16,7 +21,7 @@ class Assert(clause: Clause) : AssertZ(clause) {
 /**
  * Assert a [Clause] as a first clause of the [Predicate] into the [Program].
  */
-class AssertA(val clause: Clause) : Structure(Atom("asserta"), listOf(clause)) {
+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)
@@ -28,7 +33,7 @@ class AssertA(val clause: Clause) : Structure(Atom("asserta"), listOf(clause)) {
 /**
  * Assert a [Clause] as a last clause of the [Predicate] into the [Program].
  */
-open class AssertZ(val clause: Clause) : Structure(Atom("assertz"), listOf(clause)) {
+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))
@@ -36,3 +41,43 @@ open class AssertZ(val clause: Clause) : Structure(Atom("assertz"), listOf(claus
         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
+                            }
+                        )
+                    }
+                }
+            }
+    }
+}