Succ operator

src/interpreter/Preprocessor.kt

@@ -75,6 +75,7 @@ open class Preprocessor {
                     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" -> NotEquivalent(args[0], args[1])
                     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)
@@ -90,10 +91,12 @@ open class Preprocessor {
                     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 == "succ/2" && args.all { it is Expression } -> Successor(args[0] as Expression, args[1] as Expression)
 
                     // Database
                     term.functor == "dynamic/1" -> Dynamic((args[0] as Atom).name)
                     term.functor == "retract/1" -> Retract(args[0])
+                    term.functor == "retractall/1" -> RetractAll(args[0])
                     term.functor == "assert/1" -> {
                         if (args[0] is Rule) {
                             Assert(args[0] as Rule)

src/io/IoHandler.kt

@@ -3,7 +3,8 @@ package io
 interface IoHandler {
     fun prompt(
         message: String,
-        hint: () -> String = { "Please enter a valid input." }
+        hint: () -> String = { "Please enter a valid input." },
+        check: (String) -> Boolean = { true }
     ): String
 
     fun say(message: String)

src/io/Terminal.kt

@@ -20,15 +20,16 @@ class Terminal(
 
     override fun prompt(
         message: String,
-        hint: () -> String
+        hint: () -> String,
+        check: (String) -> Boolean,
     ): String {
         say("$message ")
-        var input: String = readLine()
+        var input: String = readLine().trim()
-        while (input.isBlank()) {
+        while (!check(input)) {
             say(hint(), error)
-            input = readLine()
+            input += readLine().trim()
         }
-        return input
+        return input.trim()
     }
 
     override fun say(message: String) {

src/parser/grammars/TermsGrammar.kt

@@ -87,7 +87,7 @@ open class TermsGrammar : Tokens() {
         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 op700: Parser<String> by (equivalent or notEquivalent 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))
     }

src/parser/grammars/Tokens.kt

@@ -20,6 +20,7 @@ abstract class Tokens : Grammar<Any>() {
     // 1000
     protected val comma: Token by literalToken(",")
     // 700
+    protected val notEquivalent: Token by literalToken("\\==")
     protected val equivalent: Token by literalToken("==")
     protected val equals: Token by literalToken("=")
     protected val isOp: Token by literalToken("is")

src/prolog/ast/arithmetic/Float.kt

@@ -32,6 +32,8 @@ class Float(override val value: kotlin.Float): Number {
         else -> throw IllegalArgumentException("Cannot multiply $this and $other")
     }
 
+    override fun applySubstitution(subs: Substitutions): Float = this
+
     override fun equals(other: Any?): Boolean {
         if (this === other) return true
         if (other !is Float) return false

src/prolog/ast/arithmetic/Integer.kt

@@ -33,6 +33,7 @@ data class Integer(override val value: Int) : Number, LogicOperand() {
                 Float(value / other.value.toFloat())
             }
         }
+
         else -> throw IllegalArgumentException("Cannot divide $this and $other")
     }
 
@@ -41,4 +42,6 @@ data class Integer(override val value: Int) : Number, LogicOperand() {
         is Integer -> Integer(value * other.value)
         else -> throw IllegalArgumentException("Cannot multiply $this and $other")
     }
+
+    override fun applySubstitution(subs: Substitutions): Integer = this
 }

src/prolog/ast/logic/Clause.kt

@@ -27,27 +27,23 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
         // Only if the body can be proven, the substitutions should be returned.
         // Do this in a lazy way.
 
-        // Since we are only interested in substitutions in the goal (as opposed to the head of this clause),
+        val (headEnd, headRenaming) = numbervars(head, Program.variableRenamingStart, subs)
-        //  we can use variable renaming and filter out the substitutions that are not in the goal.
+        Program.variableRenamingStart = headEnd
-        val (end, renamed: Substitutions) = numbervars(head, Program.variableRenamingStart, subs)
 
-        val reverse = renamed.entries.associate { (a, b) -> b to a }
+        val renamedHead = applySubstitution(head, subs + headRenaming)
-        Program.variableRenamingStart = end
+        val renamedBody = applySubstitution(body, subs + headRenaming) as Body
 
-        var newSubs: Substitutions = subs + renamed
+        unifyLazy(goal, renamedHead, subs).forEach { headAnswer ->
-        unifyLazy(applySubstitution(goal, subs), head, newSubs).forEach { headAnswer ->
             headAnswer.map { headSubs ->
-                // If the body can be proven, yield the (combined) substitutions
+                val subsNotInGoal = headSubs.filterNot { occurs(it.key as Variable, goal, emptyMap()) }
-                newSubs = subs + renamed + headSubs
+                renamedBody.satisfy(subsNotInGoal).forEach { bodyAnswer ->
-                body.satisfy(newSubs).forEach { bodyAnswer ->
                     bodyAnswer.fold(
+                        // If the body can be proven, yield the (combined) substitutions
                         onSuccess = { bodySubs ->
-                            var result = (headSubs + bodySubs)
+                            var result = headSubs + bodySubs
-                                .mapKeys { applySubstitution(it.key, reverse)}
+                            result = result
-                                .mapValues { applySubstitution(it.value, reverse) }
+                                .mapValues { applySubstitution(it.value, result) }
-                            result = result.map { it.key to applySubstitution(it.value, result) }
+                                .filterKeys { it !is AnonymousVariable && occurs(it as Variable, goal, emptyMap()) }
-                                .toMap()
-                                .filterNot { it.key in renamed.keys && !occurs(it.key as Variable, goal, emptyMap())}
                             yield(Result.success(result))
                         },
                         onFailure = { error ->
@@ -81,7 +77,5 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
         return true
     }
 
-    override fun hashCode(): Int {
+    override fun hashCode(): Int = super.hashCode()
-        return super.hashCode()
-    }
 }

src/prolog/ast/logic/Fact.kt

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

src/prolog/ast/logic/Rule.kt

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

src/prolog/ast/terms/AnonymousVariable.kt

@@ -1,8 +1,9 @@
 package prolog.ast.terms
 
 import io.Logger
+import prolog.Substitutions
 
-class AnonymousVariable(id: Int) : Variable("_$id") {
+class AnonymousVariable(private val id: Int) : Variable("_$id") {
     companion object {
         private var counter = 0
         fun create(): AnonymousVariable {
@@ -13,5 +14,7 @@ class AnonymousVariable(id: Int) : Variable("_$id") {
         }
     }
 
+    override fun applySubstitution(subs: Substitutions): AnonymousVariable = this
+
     override fun toString(): String = "_"
 }

src/prolog/ast/terms/Atom.kt

@@ -10,6 +10,8 @@ open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
 
     override fun solve(goal: Goal, subs: Substitutions): Answers = unifyLazy(goal, this, subs)
 
+    override fun applySubstitution(subs: Substitutions): Atom = Atom(name)
+
     override fun toString(): String {
         return 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/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
@@ -23,6 +24,11 @@ open class Structure(val name: Atom, var arguments: List<Argument>) : Goal(), He
         }
     }
 
+    override fun applySubstitution(subs: Substitutions): Structure = Structure(
+        name,
+        arguments.map { applySubstitution(it, subs) }
+    )
+
     override fun equals(other: Any?): Boolean {
         if (this === other) return true
         if (other !is Structure) return false

src/prolog/ast/terms/Term.kt

@@ -1,14 +1,18 @@
 package prolog.ast.terms
 
+import prolog.Substitutions
+import prolog.ast.arithmetic.Float
+import prolog.ast.arithmetic.Integer
 import prolog.logic.compare
 
 /**
  * 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> {
     override fun compareTo(other: Term): Int = compare(this, other, emptyMap())
+    fun applySubstitution(subs: Substitutions): Term
 }

src/prolog/ast/terms/Variable.kt

@@ -34,6 +34,8 @@ open class Variable(val name: String) : Term, Body, Expression, LogicOperand() {
         return name == other.name
     }
 
+    override fun applySubstitution(subs: Substitutions): Variable = this
+
     override fun hashCode(): Int {
         return name.hashCode()
     }

src/prolog/builtins/arithmeticOperators.kt

@@ -39,6 +39,10 @@ class EvaluatesToDifferent(private val left: Expression, private val right: Expr
         }
     }
 
+    override fun applySubstitution(subs: Substitutions): EvaluatesToDifferent = EvaluatesToDifferent(
+        left.applySubstitution(subs) as Expression,
+        right.applySubstitution(subs) as Expression
+    )
 }
 
 /**
@@ -57,6 +61,11 @@ class EvaluatesTo(private val left: Expression, private val right: Expression) :
 
         return if (equivalent(t1.to, t2.to, subs)) sequenceOf(Result.success(emptyMap())) else emptySequence()
     }
+
+    override fun applySubstitution(subs: Substitutions): EvaluatesTo = EvaluatesTo(
+        left.applySubstitution(subs) as Expression,
+        right.applySubstitution(subs) as Expression
+    )
 }
 
 /**
@@ -78,6 +87,11 @@ class Is(val number: Expression, val expr: Expression) :
 
         return unifyLazy(t1.to, t2.to, subs)
     }
+
+    override fun applySubstitution(subs: Substitutions): Is = Is(
+        number.applySubstitution(subs) as Expression,
+        expr.applySubstitution(subs) as Expression
+    )
 }
 
 /**
@@ -101,6 +115,11 @@ open class Add(private val expr1: Expression, private val expr2: Expression) :
         val simplification = result.simplify(map.first().getOrThrow())
         return Simplification(this, simplification.to)
     }
+
+    override fun applySubstitution(subs: Substitutions): Add = Add(
+        expr1.applySubstitution(subs) as Expression,
+        expr2.applySubstitution(subs) as Expression
+    )
 }
 
 /**
@@ -114,6 +133,11 @@ open class Subtract(private val expr1: Expression, private val expr2: Expression
         val simplification = result.simplify(map.first().getOrThrow())
         return Simplification(this, simplification.to)
     }
+
+    override fun applySubstitution(subs: Substitutions): Subtract = Subtract(
+        expr1.applySubstitution(subs) as Expression,
+        expr2.applySubstitution(subs) as Expression
+    )
 }
 
 /**
@@ -127,6 +151,11 @@ class Multiply(val expr1: Expression, val expr2: Expression) :
         val simplification = result.simplify(map.first().getOrThrow())
         return Simplification(this, simplification.to)
     }
+
+    override fun applySubstitution(subs: Substitutions): Multiply = Multiply(
+        expr1.applySubstitution(subs) as Expression,
+        expr2.applySubstitution(subs) as Expression
+    )
 }
 
 class Divide(private val expr1: Expression, private val expr2: Expression) :
@@ -137,6 +166,11 @@ class Divide(private val expr1: Expression, private val expr2: Expression) :
         val simplification = result.simplify(map.first().getOrThrow())
         return Simplification(this, simplification.to)
     }
+
+    override fun applySubstitution(subs: Substitutions): Divide = Divide(
+        expr1.applySubstitution(subs) as Expression,
+        expr2.applySubstitution(subs) as Expression
+    )
 }
 
 // TODO Expr mod Expr
@@ -166,5 +200,16 @@ class Between(private val expr1: Expression, private val expr2: Expression, priv
         }
     }
 
+    override fun applySubstitution(subs: Substitutions): Between = Between(
+        expr1.applySubstitution(subs) as Expression,
+        expr2.applySubstitution(subs) as Expression,
+        expr3.applySubstitution(subs) as Expression
+    )
+
     override fun toString(): String = "$expr1..$expr3..$expr2"
 }
+
+class Successor(private val expr1: Expression, private val expr2: Expression) :
+    CompoundTerm(Atom("succ"), listOf(expr1, expr2)), Satisfiable {
+    override fun satisfy(subs: Substitutions): Answers = succ(expr1, expr2, subs)
+}

src/prolog/builtins/controlOperators.kt

@@ -7,13 +7,16 @@ import prolog.ast.logic.LogicOperator
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Body
 import prolog.ast.terms.Goal
+import prolog.ast.terms.Structure
 import prolog.flags.AppliedCut
+import prolog.logic.applySubstitution
 
 /**
  * Always fail.
  */
 object Fail : Atom("fail"), Body {
     override fun satisfy(subs: Substitutions): Answers = emptySequence()
+    override fun applySubstitution(subs: Substitutions): Fail = Fail
 }
 
 /**
@@ -26,6 +29,7 @@ typealias False = Fail
  */
 object True : Atom("true"), Body {
     override fun satisfy(subs: Substitutions): Answers = sequenceOf(Result.success(emptyMap()))
+    override fun applySubstitution(subs: Substitutions): True = True
 }
 
 // TODO Repeat/0
@@ -34,6 +38,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 +100,11 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
             )
         }
     }
+
+    override fun applySubstitution(subs: Substitutions): Conjunction = Conjunction(
+        applySubstitution(left, subs) as LogicOperand,
+        applySubstitution(right, subs) as LogicOperand
+    )
 }
 
 /**
@@ -105,6 +116,11 @@ open class Disjunction(private val left: LogicOperand, private val right: LogicO
         yieldAll(left.satisfy(subs))
         yieldAll(right.satisfy(subs))
     }
+
+    override fun applySubstitution(subs: Substitutions): Disjunction = Disjunction(
+        applySubstitution(left, subs) as LogicOperand,
+        applySubstitution(right, subs) as LogicOperand
+    )
 }
 
 @Deprecated("Use Disjunction instead")
@@ -127,4 +143,6 @@ class Not(private val goal: Goal) : LogicOperator(Atom("\\+"), rightOperand = go
         // If the goal cannot be proven, return a sequence with an empty map
         return sequenceOf(Result.success(emptyMap()))
     }
+
+    override fun applySubstitution(subs: Substitutions): Not = Not(applySubstitution(goal, subs) as Goal)
 }

src/prolog/builtins/databaseOperators.kt

@@ -1,5 +1,6 @@
 package prolog.builtins
 
+import io.Logger
 import prolog.Answers
 import prolog.Substitutions
 import prolog.ast.logic.Clause
@@ -42,6 +43,8 @@ class Dynamic(private val dynamicFunctor: Functor): Goal(), Body {
     }
 
     override fun hashCode(): Int = super.hashCode()
+
+    override fun applySubstitution(subs: Substitutions): Dynamic = Dynamic(dynamicFunctor)
 }
 
 class Assert(clause: Clause) : AssertZ(clause) {
@@ -59,6 +62,8 @@ class AssertA(val clause: Clause) : Operator(Atom("asserta"), null, clause) {
 
         return sequenceOf(Result.success(emptyMap()))
     }
+
+    override fun applySubstitution(subs: Substitutions): AssertA = AssertA(applySubstitution(clause, subs) as Clause)
 }
 
 /**
@@ -72,6 +77,8 @@ open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause)
 
         return sequenceOf(Result.success(emptyMap()))
     }
+
+    override fun applySubstitution(subs: Substitutions): AssertZ = AssertZ(applySubstitution(clause, subs) as Clause)
 }
 
 /**
@@ -80,7 +87,7 @@ open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause)
  *
  * @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) {
+open 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) {
@@ -95,6 +102,12 @@ class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
             return@sequence
         }
 
+        // Check if the predicate is dynamic
+        if (!predicate.dynamic) {
+            yield(Result.failure(Exception("No permission to modify static procedure '$functorName'")))
+            return@sequence
+        }
+
         predicate.clauses.toList().forEach { clause ->
             unifyLazy(term, clause.head, subs).forEach { unifyResult ->
                 unifyResult.fold(
@@ -110,4 +123,32 @@ class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
             }
         }
     }
+
+    override fun applySubstitution(subs: Substitutions): Retract = Retract(applySubstitution(term, subs))
+}
+
+class RetractAll(term: Term) : Retract(term) {
+    override fun satisfy(subs: Substitutions): Answers {
+        // Check that term is a structure or atom
+        if (term !is Structure && term !is Atom) {
+            return sequenceOf(Result.failure(Exception("Cannot retract a non-structure or non-atom")))
+        }
+
+        // If the predicate does not exist, implicitly create it
+        val functor = term.functor
+        val predicate = Program.db.predicates[functor]
+        if (predicate == null) {
+            Logger.debug("Predicate $functor not found, creating it")
+            Program.db.predicates += functor to Predicate(functor, dynamic = true)
+        }
+
+        // Propagate errors from the super class
+        super.satisfy(subs).forEach {
+            if (it.isFailure) {
+                return sequenceOf(it)
+            }
+        }
+
+        return sequenceOf(Result.success(emptyMap()))
+    }
 }

src/prolog/builtins/ioOperators.kt

@@ -27,6 +27,8 @@ class Write(private val term: Term) : Operator(Atom("write"), null, term), Satis
         return sequenceOf(Result.success(emptyMap()))
     }
 
+    override fun applySubstitution(subs: Substitutions): Write = Write(applySubstitution(term, subs))
+
     override fun toString(): String = "write($term)"
 }
 
@@ -39,6 +41,8 @@ object Nl : Atom("nl"), Satisfiable {
         Program.storeNewLine = false
         return sequenceOf(Result.success(emptyMap()))
     }
+
+    override fun applySubstitution(subs: Substitutions): Nl = this
 }
 
 /**
@@ -72,4 +76,6 @@ class Read(private val term: Term) : Operator(Atom("read"), null, term), Satisfi
 
         yieldAll(unifyLazy(t1, t2, subs))
     }
+
+    override fun applySubstitution(subs: Substitutions): Read = Read(applySubstitution(term, subs))
 }

src/prolog/builtins/unificationOperators.kt

@@ -24,11 +24,20 @@ class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="
 
         yieldAll(unifyLazy(t1, t2, subs))
     }
+
+    override fun applySubstitution(subs: Substitutions): Unify = Unify(
+        applySubstitution(term1, subs),
+        applySubstitution(term2, subs)
+    )
 }
 
-class NotUnify(term1: Term, term2: Term) : Operator(Atom("\\="), term1, term2) {
+class NotUnify(private val term1: Term, private val term2: Term) : Operator(Atom("\\="), term1, term2) {
     private val not = Not(Unify(term1, term2))
     override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs)
+    override fun applySubstitution(subs: Substitutions): NotUnify = NotUnify(
+        applySubstitution(term1, subs),
+        applySubstitution(term2, subs)
+    )
 }
 
 class Equivalent(private val term1: Term, private val term2: Term) : Operator(Atom("=="), term1, term2) {
@@ -40,4 +49,18 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator(At
             yield(Result.success(emptyMap()))
         }
     }
+
+    override fun applySubstitution(subs: Substitutions): Equivalent = Equivalent(
+        applySubstitution(term1, subs),
+        applySubstitution(term2, subs)
+    )
+}
+
+class NotEquivalent(private val term1: Term, private val term2: Term) : Operator(Atom("\\=="), term1, term2) {
+    private val not = Not(Equivalent(term1, term2))
+    override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs)
+    override fun applySubstitution(subs: Substitutions): NotEquivalent = NotEquivalent(
+        applySubstitution(term1, subs),
+        applySubstitution(term2, subs)
+    )
 }

src/prolog/logic/unification.kt

@@ -15,19 +15,15 @@ import prolog.ast.terms.*
 
 // Apply substitutions to a term
 fun applySubstitution(term: Term, subs: Substitutions): Term = when {
-    term is Fact -> {
+    term is Fact -> term.applySubstitution(subs)
-        Fact(applySubstitution(term.head, subs) as Head)
-    }
 
     variable(term, emptyMap()) -> {
         val variable = term as Variable
         subs[variable]?.let { applySubstitution(term = it, subs = subs) } ?: term
     }
+
     atomic(term, subs) -> term
-    compound(term, subs) -> {
+    compound(term, subs) -> term.applySubstitution(subs)
-        val structure = term as Structure
-        Structure(structure.name, structure.arguments.map { applySubstitution(it, subs) })
-    }
 
     else -> term
 }

src/repl/Repl.kt

@@ -29,40 +29,45 @@ class Repl {
     }
 
     private fun query(): Answers {
-        val queryString = io.prompt("?-", { "|  " })
+        val queryString = io.prompt("?-", { "|  " }, { it.endsWith(".") })
         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 {
+            return
-            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()))
+
+        while (true) {
+            when (io.prompt("")) {
                 ";" -> {
+                    try {
                         io.say(prettyPrint(iterator.next()))
+                    } catch (_: NoSuchElementException) {
+                        break
                     }
+                }
+
                 "a" -> return
-                    "." -> return
+                "." -> {
+                    io.checkNewLine()
+                    return
+                }
                 "h" -> {
                     help()
                     io.say("Action?")
                 }
+
+                else -> {
+                    io.say("Unknown action: (h for help)\n")
+                    io.say("Action?")
                 }
             }
         }
@@ -90,9 +95,7 @@ class Repl {
                 return subs.entries.joinToString(",\n") { "${it.key} = ${it.value}" }
             },
             onFailure = {
-                val text = "Failure: ${it.message}"
+                return "ERROR: ${it.message}"
-                Logger.warn(text)
-                return text
             }
         )
     }

tests/prolog/EvaluationTests.kt

@@ -14,6 +14,8 @@ import prolog.ast.terms.Atom
 import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable
 import prolog.ast.Database.Program
+import prolog.ast.arithmetic.Integer
+import prolog.ast.terms.AnonymousVariable
 
 class EvaluationTests {
     @BeforeEach
@@ -108,8 +110,8 @@ 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("mother"), listOf(variable1, variable2))
@@ -118,10 +120,14 @@ class EvaluationTests {
 
         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())
@@ -414,4 +420,63 @@ class EvaluationTests {
             assertEquals(Atom("bob"), subs5[Variable("Person")], "Expected bob")
         }
     }
+
+    @Test
+    fun `leq Peano`() {
+        val fact = Fact(Structure(Atom("leq"), listOf(Integer(0), AnonymousVariable.create())))
+        val rule = Rule(
+            Structure(
+                Atom("leq"),
+                listOf(Structure(Atom("s"), listOf(Variable("X"))), Structure(Atom("s"), listOf(Variable("Y"))))
+            ),
+            Structure(Atom("leq"), listOf(Variable("X"), Variable("Y"))),
+        )
+
+        Program.db.load(listOf(fact, rule))
+
+        val result1 = Program.query(Structure(Atom("leq"), listOf(Variable("X"), Integer(0)))).toList()
+
+        assertEquals(1, result1.size, "Expected 1 result")
+        assertTrue(result1[0].isSuccess, "Expected success")
+        val subs = result1[0].getOrNull()!!
+        assertEquals(1, subs.size, "Expected 1 substitution")
+        assertEquals(Integer(0), subs[Variable("X")], "Expected X to be 0")
+
+        val result2 =
+            Program.query(Structure(Atom("leq"), listOf(Variable("X"), Structure(Atom("s"), listOf(Integer(0))))))
+                .toList()
+
+        assertEquals(2, result2.size, "Expected 2 results")
+
+        assertTrue(result2[0].isSuccess, "Expected success")
+        val subs2a = result2[0].getOrNull()!!
+        assertEquals(1, subs2a.size, "Expected 1 substitution")
+        assertEquals(Integer(0), subs2a[Variable("X")], "Expected X to be 0")
+
+        assertTrue(result2[1].isSuccess, "Expected success")
+        val subs2b = result2[1].getOrNull()!!
+        assertEquals(1, subs2b.size, "Expected 1 substitution")
+        assertEquals(Structure(Atom("s"), listOf(Integer(0))), subs2b[Variable("X")], "Expected X to be s(0)")
+
+        val result3 = Program.query(
+            Structure(
+                Atom("leq"),
+                listOf(Variable("X"), Structure(Atom("s"), listOf(Structure(Atom("s"), listOf(Integer(0))))))
+            )
+        ).toList()
+
+        assertEquals(3, result3.size, "Expected 3 results")
+        assertTrue(result3[0].isSuccess, "Expected success")
+        val subs3a = result3[0].getOrNull()!!
+        assertEquals(1, subs3a.size, "Expected 1 substitution")
+        assertEquals(Integer(0), subs3a[Variable("X")], "Expected X to be 0")
+        assertTrue(result3[1].isSuccess, "Expected success")
+        val subs3b = result3[1].getOrNull()!!
+        assertEquals(1, subs3b.size, "Expected 1 substitution")
+        assertEquals(Structure(Atom("s"), listOf(Integer(0))), subs3b[Variable("X")], "Expected X to be s(0)")
+        assertTrue(result3[2].isSuccess, "Expected success")
+        val subs3c = result3[2].getOrNull()!!
+        assertEquals(1, subs3c.size, "Expected 1 substitution")
+        assertEquals(Structure(Atom("s"), listOf(Structure(Atom("s"), listOf(Integer(0))))), subs3c[Variable("X")], "Expected X to be s(s(0))")
+    }
 }

tests/prolog/builtins/DatabaseOperatorsTests.kt

@@ -15,6 +15,7 @@ import prolog.ast.logic.Fact
 import prolog.ast.logic.Predicate
 import prolog.ast.logic.Rule
 import prolog.ast.terms.Atom
+import prolog.ast.terms.Functor
 import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable
 
@@ -131,7 +132,7 @@ class DatabaseOperatorsTests {
 
     @Test
     fun `simple retract`() {
-        val predicate = Predicate(listOf(Fact(Atom("a"))))
+        val predicate = Predicate(listOf(Fact(Atom("a"))), dynamic = true)
         Program.db.load(predicate)
 
         assertEquals(1, Program.query(Atom("a")).count())
@@ -146,11 +147,13 @@ class DatabaseOperatorsTests {
 
     @Test
     fun `retract atom`() {
-        val predicate = Predicate(listOf(
+        val predicate = Predicate(
+            listOf(
                 Fact(Atom("a")),
                 Fact(Atom("a")),
                 Fact(Atom("a"))
-        ))
+            ), dynamic = true
+        )
         Program.db.load(predicate)
 
         val control = Program.query(Atom("a")).toList()
@@ -170,11 +173,9 @@ class DatabaseOperatorsTests {
         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")
@@ -183,11 +184,13 @@ class DatabaseOperatorsTests {
 
     @Test
     fun `retract compound with variable`() {
-        val predicate = Predicate(listOf(
+        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"))))
-        ))
+            ), dynamic = true
+        )
         Program.db.load(predicate)
 
         val control = Program.query(Structure(Atom("a"), listOf(Variable("X")))).toList()
@@ -208,7 +211,6 @@ class DatabaseOperatorsTests {
         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()
@@ -218,7 +220,6 @@ class DatabaseOperatorsTests {
         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()
@@ -228,8 +229,9 @@ class DatabaseOperatorsTests {
         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")
+
+        assertFalse(result.hasNext(), "Expected no more results")
     }
 
     @Test
@@ -292,4 +294,45 @@ class DatabaseOperatorsTests {
         assertEquals(Atom("bob"), result2[Variable("X")], "Expected bob")
         assertEquals(Atom("sushi"), result2[Variable("Y")], "Expected sushi")
     }
+
+    @Test
+    fun `retract all`() {
+        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"))))
+            ), dynamic = true
+        )
+
+        Program.db.load(predicate)
+
+        val control = Program.query(Structure(Atom("a"), listOf(Variable("X")))).toList()
+        assertEquals(3, control.size, "Expected 3 results")
+        assertEquals(3, Program.db.predicates["a/1"]!!.clauses.size, "Expected 3 clauses")
+
+        val retract = RetractAll(Structure(Atom("a"), listOf(Variable("X"))))
+        val result = retract.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected 1 result")
+        assertTrue(result[0].isSuccess, "Expected success")
+        assertEquals(0, Program.db.predicates["a/1"]!!.clauses.size, "Expected 0 clauses")
+    }
+
+    @Test
+    fun `If Head refers to a predicate that is not defined, it is implicitly created as a dynamic predicate`() {
+        val predicateName = "idonotyetexist"
+        val predicateFunctor = "$predicateName/1"
+
+        assertFalse(predicateFunctor in Program.db.predicates, "Expected predicate to not exist before")
+
+        val retractAll = RetractAll(Structure(Atom(predicateName), listOf(Variable("X"))))
+        val result = retractAll.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size, "Expected 1 result")
+        assertTrue(result[0].isSuccess, "Expected success")
+
+        assertTrue(predicateFunctor in Program.db.predicates, "Expected predicate to exist after")
+        assertTrue(Program.db.predicates[predicateFunctor]!!.dynamic, "Expected predicate to be dynamic")
+    }
 }