From fd16c4cedca12d234f8f8ecbbe682ae3167fff42 Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Mon, 5 May 2025 20:11:44 +0200 Subject: [PATCH 1/5] Backtracking fixed --- src/prolog/ast/arithmetic/Float.kt | 2 + src/prolog/ast/arithmetic/Integer.kt | 3 + src/prolog/ast/logic/Clause.kt | 32 ++++----- src/prolog/ast/logic/Fact.kt | 6 +- src/prolog/ast/logic/Rule.kt | 9 ++- src/prolog/ast/terms/AnonymousVariable.kt | 5 +- src/prolog/ast/terms/Atom.kt | 2 + src/prolog/ast/terms/Body.kt | 2 +- src/prolog/ast/terms/Structure.kt | 6 ++ src/prolog/ast/terms/Term.kt | 8 ++- src/prolog/ast/terms/Variable.kt | 2 + src/prolog/builtins/arithmeticOperators.kt | 40 +++++++++++ src/prolog/builtins/controlOperators.kt | 18 +++++ src/prolog/builtins/databaseOperators.kt | 8 +++ src/prolog/builtins/ioOperators.kt | 6 ++ src/prolog/builtins/unificationOperators.kt | 16 ++++- src/prolog/logic/unification.kt | 10 +-- tests/prolog/EvaluationTests.kt | 77 +++++++++++++++++++-- 18 files changed, 213 insertions(+), 39 deletions(-) diff --git a/src/prolog/ast/arithmetic/Float.kt b/src/prolog/ast/arithmetic/Float.kt index da49530..a787cb2 100644 --- a/src/prolog/ast/arithmetic/Float.kt +++ b/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 diff --git a/src/prolog/ast/arithmetic/Integer.kt b/src/prolog/ast/arithmetic/Integer.kt index dbf9c39..c12cfcd 100644 --- a/src/prolog/ast/arithmetic/Integer.kt +++ b/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 } diff --git a/src/prolog/ast/logic/Clause.kt b/src/prolog/ast/logic/Clause.kt index 2abfa77..4e97a14 100644 --- a/src/prolog/ast/logic/Clause.kt +++ b/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), - // we can use variable renaming and filter out the substitutions that are not in the goal. - val (end, renamed: Substitutions) = numbervars(head, Program.variableRenamingStart, subs) + val (headEnd, headRenaming) = numbervars(head, Program.variableRenamingStart, subs) + Program.variableRenamingStart = headEnd - val reverse = renamed.entries.associate { (a, b) -> b to a } - Program.variableRenamingStart = end + val renamedHead = applySubstitution(head, subs + headRenaming) + val renamedBody = applySubstitution(body, subs + headRenaming) as Body - var newSubs: Substitutions = subs + renamed - unifyLazy(applySubstitution(goal, subs), head, newSubs).forEach { headAnswer -> + unifyLazy(goal, renamedHead, subs).forEach { headAnswer -> headAnswer.map { headSubs -> - // If the body can be proven, yield the (combined) substitutions - newSubs = subs + renamed + headSubs - body.satisfy(newSubs).forEach { bodyAnswer -> + val subsNotInGoal = headSubs.filterNot { occurs(it.key as Variable, goal, emptyMap()) } + renamedBody.satisfy(subsNotInGoal).forEach { bodyAnswer -> bodyAnswer.fold( + // If the body can be proven, yield the (combined) substitutions onSuccess = { bodySubs -> - var result = (headSubs + bodySubs) - .mapKeys { applySubstitution(it.key, reverse)} - .mapValues { applySubstitution(it.value, reverse) } - result = result.map { it.key to applySubstitution(it.value, result) } - .toMap() - .filterNot { it.key in renamed.keys && !occurs(it.key as Variable, goal, emptyMap())} + var result = headSubs + bodySubs + result = result + .mapValues { applySubstitution(it.value, result) } + .filterKeys { it !is AnonymousVariable && occurs(it 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 { - return super.hashCode() - } + override fun hashCode(): Int = super.hashCode() } diff --git a/src/prolog/ast/logic/Fact.kt b/src/prolog/ast/logic/Fact.kt index a52990e..b6cc83d 100644 --- a/src/prolog/ast/logic/Fact.kt +++ b/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) \ No newline at end of file +class Fact(head: Head) : Clause(head, True) { + override fun applySubstitution(subs: Substitutions): Fact = Fact(applySubstitution(head, subs) as Head) +} diff --git a/src/prolog/ast/logic/Rule.kt b/src/prolog/ast/logic/Rule.kt index 9eba36e..26148a3 100644 --- a/src/prolog/ast/logic/Rule.kt +++ b/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) \ No newline at end of file +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 + ) +} diff --git a/src/prolog/ast/terms/AnonymousVariable.kt b/src/prolog/ast/terms/AnonymousVariable.kt index 1bc0633..abb751c 100644 --- a/src/prolog/ast/terms/AnonymousVariable.kt +++ b/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 = "_" } \ No newline at end of file diff --git a/src/prolog/ast/terms/Atom.kt b/src/prolog/ast/terms/Atom.kt index 3a6afad..5bc2004 100644 --- a/src/prolog/ast/terms/Atom.kt +++ b/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 } diff --git a/src/prolog/ast/terms/Body.kt b/src/prolog/ast/terms/Body.kt index dc61c7d..989c4d9 100644 --- a/src/prolog/ast/terms/Body.kt +++ b/src/prolog/ast/terms/Body.kt @@ -2,4 +2,4 @@ package prolog.ast.terms import prolog.ast.logic.Satisfiable -interface Body : Satisfiable \ No newline at end of file +interface Body : Term, Satisfiable diff --git a/src/prolog/ast/terms/Structure.kt b/src/prolog/ast/terms/Structure.kt index 385da2c..afed37c 100644 --- a/src/prolog/ast/terms/Structure.kt +++ b/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) : 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 diff --git a/src/prolog/ast/terms/Term.kt b/src/prolog/ast/terms/Term.kt index 0fdad49..8e46626 100644 --- a/src/prolog/ast/terms/Term.kt +++ b/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], - * [Float][prolog.ast.arithmetic.Float] or [CompoundTerm]. + * A [Term] is either a [Variable], [Atom], [Integer], + * [Float] or [CompoundTerm]. * In addition, SWI-Prolog also defines the type TODO string. */ interface Term : Comparable { override fun compareTo(other: Term): Int = compare(this, other, emptyMap()) + fun applySubstitution(subs: Substitutions): Term } diff --git a/src/prolog/ast/terms/Variable.kt b/src/prolog/ast/terms/Variable.kt index 2d23170..bcfee5c 100644 --- a/src/prolog/ast/terms/Variable.kt +++ b/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() } diff --git a/src/prolog/builtins/arithmeticOperators.kt b/src/prolog/builtins/arithmeticOperators.kt index 306337e..5ce34b3 100644 --- a/src/prolog/builtins/arithmeticOperators.kt +++ b/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,11 @@ 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" } diff --git a/src/prolog/builtins/controlOperators.kt b/src/prolog/builtins/controlOperators.kt index 613c915..41c8b6d 100644 --- a/src/prolog/builtins/controlOperators.kt +++ b/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) } diff --git a/src/prolog/builtins/databaseOperators.kt b/src/prolog/builtins/databaseOperators.kt index eaf67b8..81e31aa 100644 --- a/src/prolog/builtins/databaseOperators.kt +++ b/src/prolog/builtins/databaseOperators.kt @@ -42,6 +42,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 +61,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 +76,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) } /** @@ -110,4 +116,6 @@ class Retract(val term: Term) : Operator(Atom("retract"), null, term) { } } } + + override fun applySubstitution(subs: Substitutions): Retract = Retract(applySubstitution(term, subs)) } diff --git a/src/prolog/builtins/ioOperators.kt b/src/prolog/builtins/ioOperators.kt index 1271296..4c80d61 100644 --- a/src/prolog/builtins/ioOperators.kt +++ b/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)) } diff --git a/src/prolog/builtins/unificationOperators.kt b/src/prolog/builtins/unificationOperators.kt index 892c616..6019b18 100644 --- a/src/prolog/builtins/unificationOperators.kt +++ b/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,9 @@ 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) + ) } diff --git a/src/prolog/logic/unification.kt b/src/prolog/logic/unification.kt index 1e7b57f..6dd033f 100644 --- a/src/prolog/logic/unification.kt +++ b/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 -> { - Fact(applySubstitution(term.head, subs) as Head) - } + term is Fact -> term.applySubstitution(subs) variable(term, emptyMap()) -> { val variable = term as Variable subs[variable]?.let { applySubstitution(term = it, subs = subs) } ?: term } + atomic(term, subs) -> term - compound(term, subs) -> { - val structure = term as Structure - Structure(structure.name, structure.arguments.map { applySubstitution(it, subs) }) - } + compound(term, subs) -> term.applySubstitution(subs) else -> term } diff --git a/tests/prolog/EvaluationTests.kt b/tests/prolog/EvaluationTests.kt index ac3df3f..1a62390 100644 --- a/tests/prolog/EvaluationTests.kt +++ b/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)), - /* :- */ Disjunction( + Structure(Atom("parent"), listOf(variable1, variable2)), /* :- */ + 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")))) - assertTrue(result1.toList().isNotEmpty()) - val result2 = Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy")))) - assertTrue(result2.toList().isNotEmpty()) + val result1 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy")))).toList() + assertEquals(1, result1.size, "Expected 1 result") + assertTrue(result1[0].isSuccess, "Expected success") + 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))") + } } From 4d334c160032f2ce897a9b4d8edea2bd0206b5f9 Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Mon, 5 May 2025 21:12:08 +0200 Subject: [PATCH 2/5] Repl trouble --- src/io/IoHandler.kt | 3 +- src/io/Terminal.kt | 11 ++--- src/repl/Repl.kt | 45 ++++++++++--------- .../prolog/builtins/DatabaseOperatorsTests.kt | 7 +-- 4 files changed, 35 insertions(+), 31 deletions(-) diff --git a/src/io/IoHandler.kt b/src/io/IoHandler.kt index c5706a1..f12deb7 100644 --- a/src/io/IoHandler.kt +++ b/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) diff --git a/src/io/Terminal.kt b/src/io/Terminal.kt index 1b9df94..d20c8e8 100644 --- a/src/io/Terminal.kt +++ b/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() - while (input.isBlank()) { + var input: String = readLine().trim() + while (!check(input)) { say(hint(), error) - input = readLine() + input += readLine().trim() } - return input + return input.trim() } override fun say(message: String) { diff --git a/src/repl/Repl.kt b/src/repl/Repl.kt index 5e8b0d4..073d76e 100644 --- a/src/repl/Repl.kt +++ b/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 { - io.say(prettyPrint(iterator.next())) + return + } - while (iterator.hasNext()) { - var command = io.prompt("") + io.say(prettyPrint(iterator.next())) - while (command !in knownCommands) { - io.say("Unknown action: $command (h for help)\n") - command = io.prompt("Action?") + while (true) { + when (io.prompt("")) { + ";" -> { + try { + io.say(prettyPrint(iterator.next())) + } catch (_: NoSuchElementException) { + break + } } - when (command) { - ";" -> { - io.say(prettyPrint(iterator.next())) - } - "a" -> return - "." -> return - "h" -> { - help() - io.say("Action?") - } + "a" -> return + "." -> { + io.checkNewLine() + return + } + "h" -> { + help() + io.say("Action?") + } + + else -> { + io.say("Unknown action: (h for help)\n") + io.say("Action?") } } } diff --git a/tests/prolog/builtins/DatabaseOperatorsTests.kt b/tests/prolog/builtins/DatabaseOperatorsTests.kt index 8e96085..aa5b7b1 100644 --- a/tests/prolog/builtins/DatabaseOperatorsTests.kt +++ b/tests/prolog/builtins/DatabaseOperatorsTests.kt @@ -170,11 +170,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") @@ -208,7 +206,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 +215,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 +224,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 From 1179e6a29b1b0f97302af50a24d960f667e07513 Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Mon, 5 May 2025 22:06:26 +0200 Subject: [PATCH 3/5] RetractAll --- src/interpreter/Preprocessor.kt | 3 +- src/prolog/builtins/databaseOperators.kt | 35 +++++++++- src/repl/Repl.kt | 4 +- .../prolog/builtins/DatabaseOperatorsTests.kt | 68 ++++++++++++++++--- 4 files changed, 94 insertions(+), 16 deletions(-) diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt index 6c17705..242a6ac 100644 --- a/src/interpreter/Preprocessor.kt +++ b/src/interpreter/Preprocessor.kt @@ -94,6 +94,7 @@ open class Preprocessor { // 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) @@ -138,4 +139,4 @@ open class Preprocessor { return prepped } -} \ No newline at end of file +} diff --git a/src/prolog/builtins/databaseOperators.kt b/src/prolog/builtins/databaseOperators.kt index 81e31aa..ea36376 100644 --- a/src/prolog/builtins/databaseOperators.kt +++ b/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 @@ -86,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) { @@ -101,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( @@ -119,3 +126,29 @@ 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())) + } +} diff --git a/src/repl/Repl.kt b/src/repl/Repl.kt index 073d76e..4db4fbc 100644 --- a/src/repl/Repl.kt +++ b/src/repl/Repl.kt @@ -95,9 +95,7 @@ class Repl { return subs.entries.joinToString(",\n") { "${it.key} = ${it.value}" } }, onFailure = { - val text = "Failure: ${it.message}" - Logger.warn(text) - return text + return "ERROR: ${it.message}" } ) } diff --git a/tests/prolog/builtins/DatabaseOperatorsTests.kt b/tests/prolog/builtins/DatabaseOperatorsTests.kt index aa5b7b1..73cfef0 100644 --- a/tests/prolog/builtins/DatabaseOperatorsTests.kt +++ b/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( - Fact(Atom("a")), - Fact(Atom("a")), - Fact(Atom("a")) - )) + 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() @@ -181,11 +184,13 @@ class DatabaseOperatorsTests { @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")))) - )) + 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() @@ -289,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") + } } \ No newline at end of file From cdf2513e968f8fd4df071e63a3286537da7c1765 Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Mon, 5 May 2025 22:14:10 +0200 Subject: [PATCH 4/5] NotEquivalent --- src/interpreter/Preprocessor.kt | 1 + src/parser/grammars/TermsGrammar.kt | 2 +- src/parser/grammars/Tokens.kt | 1 + src/prolog/builtins/unificationOperators.kt | 9 +++++++++ 4 files changed, 12 insertions(+), 1 deletion(-) diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt index 242a6ac..523598a 100644 --- a/src/interpreter/Preprocessor.kt +++ b/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) diff --git a/src/parser/grammars/TermsGrammar.kt b/src/parser/grammars/TermsGrammar.kt index 3fb9e48..0473200 100644 --- a/src/parser/grammars/TermsGrammar.kt +++ b/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 by (equivalent or equals or notEquals or isOp) use { text } + protected val op700: Parser by (equivalent or notEquivalent or equals or notEquals or isOp) use { text } protected val term700: Parser by (term500 * optional(op700 * term500)) use { if (t2 == null) t1 else CompoundTerm(Atom(t2!!.t1), listOf(t1, t2!!.t2)) } diff --git a/src/parser/grammars/Tokens.kt b/src/parser/grammars/Tokens.kt index ac8c36f..018417f 100644 --- a/src/parser/grammars/Tokens.kt +++ b/src/parser/grammars/Tokens.kt @@ -20,6 +20,7 @@ abstract class Tokens : Grammar() { // 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") diff --git a/src/prolog/builtins/unificationOperators.kt b/src/prolog/builtins/unificationOperators.kt index 6019b18..ad55acf 100644 --- a/src/prolog/builtins/unificationOperators.kt +++ b/src/prolog/builtins/unificationOperators.kt @@ -55,3 +55,12 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator(At 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) + ) +} From 6b46965435a8b4aeb3ee7cce795dfe73216ad7e9 Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Mon, 5 May 2025 22:20:55 +0200 Subject: [PATCH 5/5] Succ operator --- src/interpreter/Preprocessor.kt | 1 + src/prolog/builtins/arithmeticOperators.kt | 5 +++++ 2 files changed, 6 insertions(+) diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt index 523598a..3bd5fa9 100644 --- a/src/interpreter/Preprocessor.kt +++ b/src/interpreter/Preprocessor.kt @@ -91,6 +91,7 @@ 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) diff --git a/src/prolog/builtins/arithmeticOperators.kt b/src/prolog/builtins/arithmeticOperators.kt index 5ce34b3..963a2ca 100644 --- a/src/prolog/builtins/arithmeticOperators.kt +++ b/src/prolog/builtins/arithmeticOperators.kt @@ -208,3 +208,8 @@ class Between(private val expr1: Expression, private val expr2: Expression, priv 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) +}