From a937b1bc4479b3c793bacf1b924dcad58b280ef1 Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Mon, 5 May 2025 00:18:38 +0200 Subject: [PATCH 1/2] Sync --- src/prolog/ast/arithmetic/Float.kt | 4 ++++ src/prolog/ast/arithmetic/Integer.kt | 4 ++++ src/prolog/ast/logic/Clause.kt | 24 +++++++++++------------ src/prolog/ast/logic/Fact.kt | 8 +++++++- src/prolog/ast/logic/Rule.kt | 11 ++++++++++- src/prolog/ast/terms/AnonymousVariable.kt | 6 +++++- src/prolog/ast/terms/Atom.kt | 3 +++ src/prolog/ast/terms/Body.kt | 2 +- src/prolog/ast/terms/Structure.kt | 7 +++++++ src/prolog/ast/terms/Term.kt | 11 ++++++++--- src/prolog/ast/terms/Variable.kt | 3 +++ src/prolog/builtins/controlOperators.kt | 14 +++++++++++++ src/prolog/builtins/databaseOperators.kt | 3 +++ src/prolog/logic/unification.kt | 7 ++----- tests/prolog/EvaluationTests.kt | 16 +++++++++------ 15 files changed, 93 insertions(+), 30 deletions(-) diff --git a/src/prolog/ast/arithmetic/Float.kt b/src/prolog/ast/arithmetic/Float.kt index da49530..80d0bde 100644 --- a/src/prolog/ast/arithmetic/Float.kt +++ b/src/prolog/ast/arithmetic/Float.kt @@ -1,6 +1,7 @@ package prolog.ast.arithmetic import prolog.Substitutions +import prolog.ast.terms.Term class Float(override val value: kotlin.Float): Number { // Floats are already evaluated @@ -42,4 +43,7 @@ class Float(override val value: kotlin.Float): Number { override fun hashCode(): Int { return super.hashCode() } + + override fun clone(): Float = Float(value) + override fun applySubstitution(subs: Substitutions): Float = this } \ No newline at end of file diff --git a/src/prolog/ast/arithmetic/Integer.kt b/src/prolog/ast/arithmetic/Integer.kt index dbf9c39..d0a48cb 100644 --- a/src/prolog/ast/arithmetic/Integer.kt +++ b/src/prolog/ast/arithmetic/Integer.kt @@ -3,6 +3,7 @@ package prolog.ast.arithmetic import prolog.Answers import prolog.Substitutions import prolog.ast.logic.LogicOperand +import prolog.ast.terms.Term data class Integer(override val value: Int) : Number, LogicOperand() { // Integers are already evaluated @@ -41,4 +42,7 @@ 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 clone(): Integer = Integer(value) + 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..ed8690f 100644 --- a/src/prolog/ast/logic/Clause.kt +++ b/src/prolog/ast/logic/Clause.kt @@ -27,27 +27,27 @@ 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 preHead = applySubstitution(head, subs) + val preGoal = applySubstitution(goal, subs) - val reverse = renamed.entries.associate { (a, b) -> b to a } - Program.variableRenamingStart = end + val (headEnd, headRenaming) = numbervars(preHead, Program.variableRenamingStart, subs) + val headReverse = headRenaming.entries.associate { (a, b) -> b to a } + Program.variableRenamingStart = headEnd - var newSubs: Substitutions = subs + renamed - unifyLazy(applySubstitution(goal, subs), head, newSubs).forEach { headAnswer -> + val renamedHead = applySubstitution(head, headRenaming) + unifyLazy(preGoal, 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 preBody = applySubstitution(body, headRenaming + headSubs) as Body + preBody.satisfy(subs).forEach { bodyAnswer -> bodyAnswer.fold( onSuccess = { bodySubs -> var result = (headSubs + bodySubs) - .mapKeys { applySubstitution(it.key, reverse)} - .mapValues { applySubstitution(it.value, reverse) } + .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 renamed.keys && !occurs(it.key as Variable, goal, emptyMap())} + .filterNot { it.key in headRenaming.keys && !occurs(it.key as Variable, goal, emptyMap())} yield(Result.success(result)) }, onFailure = { error -> diff --git a/src/prolog/ast/logic/Fact.kt b/src/prolog/ast/logic/Fact.kt index a52990e..f0cae19 100644 --- a/src/prolog/ast/logic/Fact.kt +++ b/src/prolog/ast/logic/Fact.kt @@ -1,6 +1,12 @@ package prolog.ast.logic +import prolog.Substitutions import prolog.ast.terms.Head +import prolog.ast.terms.Term 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 clone(): Fact = Fact(head) + override fun applySubstitution(subs: Substitutions): Fact = Fact(applySubstitution(head as Term, subs) as Head) +} \ No newline at end of file diff --git a/src/prolog/ast/logic/Rule.kt b/src/prolog/ast/logic/Rule.kt index 9eba36e..add106d 100644 --- a/src/prolog/ast/logic/Rule.kt +++ b/src/prolog/ast/logic/Rule.kt @@ -1,6 +1,15 @@ package prolog.ast.logic +import prolog.Substitutions import prolog.ast.terms.Body import prolog.ast.terms.Head +import prolog.ast.terms.Term +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 clone(): Rule = Rule(head, body) + override fun applySubstitution(subs: Substitutions): Rule = Rule( + head = applySubstitution(head as Term, 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..8211292 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 { @@ -14,4 +15,7 @@ class AnonymousVariable(id: Int) : Variable("_$id") { } override fun toString(): String = "_" + + override fun clone(): AnonymousVariable = AnonymousVariable(id) + override fun applySubstitution(subs: Substitutions): AnonymousVariable = this } \ No newline at end of file diff --git a/src/prolog/ast/terms/Atom.kt b/src/prolog/ast/terms/Atom.kt index 3a6afad..dcd0a7d 100644 --- a/src/prolog/ast/terms/Atom.kt +++ b/src/prolog/ast/terms/Atom.kt @@ -21,4 +21,7 @@ open class Atom(val name: String) : Goal(), Head, Body, Resolvent { override fun hashCode(): Int { return javaClass.hashCode() } + + override fun clone(): Atom = Atom(name) + override fun applySubstitution(subs: Substitutions): Atom = Atom(name) } \ No newline at end of file diff --git a/src/prolog/ast/terms/Body.kt b/src/prolog/ast/terms/Body.kt index dc61c7d..4918d1e 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 \ No newline at end of file diff --git a/src/prolog/ast/terms/Structure.kt b/src/prolog/ast/terms/Structure.kt index 385da2c..bcd5e71 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 @@ -33,4 +34,10 @@ open class Structure(val name: Atom, var arguments: List) : Goal(), He override fun hashCode(): Int { return javaClass.hashCode() } + + override fun clone(): Structure = Structure(name, arguments) + override fun applySubstitution(subs: Substitutions): Structure = Structure( + name, + arguments.map { applySubstitution(it, subs) } + ) } diff --git a/src/prolog/ast/terms/Term.kt b/src/prolog/ast/terms/Term.kt index 0fdad49..8174310 100644 --- a/src/prolog/ast/terms/Term.kt +++ b/src/prolog/ast/terms/Term.kt @@ -1,14 +1,19 @@ package prolog.ast.terms +import prolog.Substitutions import prolog.logic.compare +import prolog.ast.arithmetic.Integer +import prolog.ast.arithmetic.Float /** * 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 { +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/ast/terms/Variable.kt b/src/prolog/ast/terms/Variable.kt index 2d23170..8068864 100644 --- a/src/prolog/ast/terms/Variable.kt +++ b/src/prolog/ast/terms/Variable.kt @@ -39,4 +39,7 @@ open class Variable(val name: String) : Term, Body, Expression, LogicOperand() { } override fun toString(): String = name + + override fun clone(): Variable = Variable(name) + override fun applySubstitution(subs: Substitutions): Variable = this } \ No newline at end of file diff --git a/src/prolog/builtins/controlOperators.kt b/src/prolog/builtins/controlOperators.kt index 613c915..b9eeef4 100644 --- a/src/prolog/builtins/controlOperators.kt +++ b/src/prolog/builtins/controlOperators.kt @@ -7,6 +7,7 @@ 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 /** @@ -34,6 +35,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 +97,11 @@ 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 + ) } /** @@ -105,6 +113,12 @@ open class Disjunction(private val left: LogicOperand, private val right: LogicO yieldAll(left.satisfy(subs)) 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 + ) } @Deprecated("Use Disjunction instead") diff --git a/src/prolog/builtins/databaseOperators.kt b/src/prolog/builtins/databaseOperators.kt index eaf67b8..54ebeb3 100644 --- a/src/prolog/builtins/databaseOperators.kt +++ b/src/prolog/builtins/databaseOperators.kt @@ -42,6 +42,9 @@ class Dynamic(private val dynamicFunctor: Functor): Goal(), Body { } override fun hashCode(): Int = super.hashCode() + + override fun clone(): Dynamic = Dynamic(dynamicFunctor) + override fun applySubstitution(subs: Substitutions): Dynamic = Dynamic(dynamicFunctor) } class Assert(clause: Clause) : AssertZ(clause) { diff --git a/src/prolog/logic/unification.kt b/src/prolog/logic/unification.kt index 1e7b57f..5b5d21e 100644 --- a/src/prolog/logic/unification.kt +++ b/src/prolog/logic/unification.kt @@ -15,9 +15,7 @@ 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 @@ -25,8 +23,7 @@ fun applySubstitution(term: Term, subs: Substitutions): Term = when { } atomic(term, subs) -> term compound(term, subs) -> { - val structure = term as Structure - Structure(structure.name, structure.arguments.map { applySubstitution(it, subs) }) + term.applySubstitution(subs) } else -> term diff --git a/tests/prolog/EvaluationTests.kt b/tests/prolog/EvaluationTests.kt index ac3df3f..a1cbbfc 100644 --- a/tests/prolog/EvaluationTests.kt +++ b/tests/prolog/EvaluationTests.kt @@ -108,8 +108,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 +118,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()) From fc8b83fca3fcb2be6acf55f365bda1b03b5d4142 Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Mon, 5 May 2025 18:04:37 +0200 Subject: [PATCH 2/2] 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)") + } }