From fc8b83fca3fcb2be6acf55f365bda1b03b5d4142 Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Mon, 5 May 2025 18:04:37 +0200 Subject: [PATCH] Sync --- src/prolog/ast/logic/Clause.kt | 18 ++++------ src/prolog/ast/terms/Term.kt | 1 - src/prolog/builtins/arithmeticOperators.kt | 40 +++++++++++++++++++++ src/prolog/builtins/controlOperators.kt | 14 +++++--- src/prolog/builtins/databaseOperators.kt | 6 ++++ src/prolog/builtins/ioOperators.kt | 6 ++++ src/prolog/builtins/unificationOperators.kt | 16 ++++++++- tests/prolog/EvaluationTests.kt | 35 ++++++++++++++++++ 8 files changed, 117 insertions(+), 19 deletions(-) diff --git a/src/prolog/ast/logic/Clause.kt b/src/prolog/ast/logic/Clause.kt index ed8690f..d511641 100644 --- a/src/prolog/ast/logic/Clause.kt +++ b/src/prolog/ast/logic/Clause.kt @@ -27,27 +27,21 @@ 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. - val preHead = applySubstitution(head, subs) - val preGoal = applySubstitution(goal, subs) - - val (headEnd, headRenaming) = numbervars(preHead, Program.variableRenamingStart, subs) - val headReverse = headRenaming.entries.associate { (a, b) -> b to a } + val (headEnd, headRenaming) = numbervars(head, Program.variableRenamingStart, subs) Program.variableRenamingStart = headEnd val renamedHead = applySubstitution(head, headRenaming) - unifyLazy(preGoal, renamedHead, subs).forEach { headAnswer -> + unifyLazy(goal, renamedHead, subs).forEach { headAnswer -> headAnswer.map { headSubs -> // If the body can be proven, yield the (combined) substitutions val preBody = applySubstitution(body, headRenaming + headSubs) as Body preBody.satisfy(subs).forEach { bodyAnswer -> bodyAnswer.fold( onSuccess = { bodySubs -> - var result = (headSubs + bodySubs) - .mapKeys { applySubstitution(it.key, headReverse) } - .mapValues { applySubstitution(it.value, headReverse) } - result = result.map { it.key to applySubstitution(it.value, result) } - .toMap() - .filterNot { it.key in headRenaming.keys && !occurs(it.key as Variable, goal, emptyMap())} + val newSubs = headSubs + bodySubs + val result = newSubs + .mapValues { applySubstitution(it.value, newSubs) } + .filter { it.key !is AnonymousVariable && occurs(it.key as Variable, goal, emptyMap()) } yield(Result.success(result)) }, onFailure = { error -> diff --git a/src/prolog/ast/terms/Term.kt b/src/prolog/ast/terms/Term.kt index 8174310..7720457 100644 --- a/src/prolog/ast/terms/Term.kt +++ b/src/prolog/ast/terms/Term.kt @@ -15,5 +15,4 @@ import prolog.ast.arithmetic.Float interface Term : Comparable, Cloneable { override fun compareTo(other: Term): Int = compare(this, other, emptyMap()) fun applySubstitution(subs: Substitutions): Term - public override fun clone(): Term } 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 b9eeef4..41c8b6d 100644 --- a/src/prolog/builtins/controlOperators.kt +++ b/src/prolog/builtins/controlOperators.kt @@ -9,12 +9,14 @@ 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 } /** @@ -27,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 @@ -99,8 +102,8 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) : } override fun applySubstitution(subs: Substitutions): Conjunction = Conjunction( - left.applySubstitution(subs) as LogicOperand, - right.applySubstitution(subs) as LogicOperand + applySubstitution(left, subs) as LogicOperand, + applySubstitution(right, subs) as LogicOperand ) } @@ -114,10 +117,9 @@ open class Disjunction(private val left: LogicOperand, private val right: LogicO yieldAll(right.satisfy(subs)) } - override fun clone(): Disjunction = Disjunction(left.clone() as LogicOperand, right.clone() as LogicOperand) override fun applySubstitution(subs: Substitutions): Disjunction = Disjunction( - left.applySubstitution(subs) as LogicOperand, - right.applySubstitution(subs) as LogicOperand + applySubstitution(left, subs) as LogicOperand, + applySubstitution(right, subs) as LogicOperand ) } @@ -141,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 54ebeb3..c8f3b29 100644 --- a/src/prolog/builtins/databaseOperators.kt +++ b/src/prolog/builtins/databaseOperators.kt @@ -62,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) } /** @@ -75,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) } /** @@ -113,4 +117,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/tests/prolog/EvaluationTests.kt b/tests/prolog/EvaluationTests.kt index a1cbbfc..d8310dd 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 @@ -418,4 +420,37 @@ 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)") + } }