From 83f65bd683636c3ee1db0e7821274b8e0fdc1cdd Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Sun, 18 May 2025 14:56:16 +0200 Subject: [PATCH] fix: Fixes --- examples/basics/summer.pl | 8 +-- examples/meta/calculator.pl | 15 ++++++ src/prolog/ast/arithmetic/Integer.kt | 3 +- src/prolog/ast/logic/Clause.kt | 52 ++++++++++++------- src/prolog/ast/terms/Body.kt | 5 +- src/prolog/builtins/controlOperators.kt | 6 +-- .../delimitedContinuationsOperators.kt | 2 +- tests/e2e/Examples.kt | 3 +- 8 files changed, 65 insertions(+), 29 deletions(-) create mode 100644 examples/meta/calculator.pl diff --git a/examples/basics/summer.pl b/examples/basics/summer.pl index 35a2eac..ba759d9 100644 --- a/examples/basics/summer.pl +++ b/examples/basics/summer.pl @@ -3,9 +3,7 @@ summer(Start, End, Sum) :- Start \== End, Next is Start + 1, summer(Next, End, Rest), - writeln(rest(Rest)), - Sum is Start + Rest, - writeln(sum(Sum)). + Sum is Start + Rest. my_sum :- write('Enter start: '), @@ -17,6 +15,8 @@ my_sum :- write(Sum), nl. main :- - summer(1, 5, Sum). + Start = 1, End = 9, + summer(Start, End, Sum), + write('The sum of '), write(Start), write(' to '), write(End), write(' is: '), write(Sum), nl. :- initialization(main). diff --git a/examples/meta/calculator.pl b/examples/meta/calculator.pl new file mode 100644 index 0000000..3ac4216 --- /dev/null +++ b/examples/meta/calculator.pl @@ -0,0 +1,15 @@ +accumulator :- + Sum = 0, + shift(Number), + NewSum is Sum + Number, + write("Result is: "), writeln(NewSum). + +main :- + reset(accumulator, Number, Cont), + between(1, 5, Number), + forall() + call(Cont), + writeln("End of calculation"). + +:- initialization(main). + diff --git a/src/prolog/ast/arithmetic/Integer.kt b/src/prolog/ast/arithmetic/Integer.kt index c12cfcd..96fd098 100644 --- a/src/prolog/ast/arithmetic/Integer.kt +++ b/src/prolog/ast/arithmetic/Integer.kt @@ -3,8 +3,9 @@ package prolog.ast.arithmetic import prolog.Answers import prolog.Substitutions import prolog.ast.logic.LogicOperand +import prolog.ast.terms.Body -data class Integer(override val value: Int) : Number, LogicOperand() { +data class Integer(override val value: Int) : Number, Body, LogicOperand() { // Integers are already evaluated override fun simplify(subs: Substitutions): Simplification = Simplification(this, this) diff --git a/src/prolog/ast/logic/Clause.kt b/src/prolog/ast/logic/Clause.kt index dc1c0c4..b73298d 100644 --- a/src/prolog/ast/logic/Clause.kt +++ b/src/prolog/ast/logic/Clause.kt @@ -6,6 +6,7 @@ import prolog.ast.Database.Program import prolog.ast.terms.* import prolog.builtins.True import prolog.flags.AppliedCut +import prolog.flags.AppliedShift import prolog.logic.applySubstitution import prolog.logic.numbervars import prolog.logic.occurs @@ -27,18 +28,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. + val simplifiedGoal = applySubstitution(goal, subs) + // 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 (headEnd, headRenaming) = numbervars(head, Program.variableRenamingStart, emptyMap()) - Program.variableRenamingStart = headEnd + val (goalEnd, goalRenaming) = numbervars(simplifiedGoal, headEnd, emptyMap()) + Program.variableRenamingStart = goalEnd + + val reverseGoalRenaming = goalRenaming.entries.associate { (key, value) -> value to key } val renamedHead = applySubstitution(head, headRenaming) - val simplifiedGoal = applySubstitution(goal, subs) - unifyLazy(simplifiedGoal, renamedHead, emptyMap()).forEach { headAnswer -> + val renamedGoal = applySubstitution(simplifiedGoal, goalRenaming) + unifyLazy(renamedGoal, renamedHead, emptyMap()).forEach { headAnswer -> headAnswer.map { headAndGoalSubs -> // Filter the substitutions to only include those that map from head to goal val headToGoalSubs = headAndGoalSubs.filterKeys { it in headRenaming.values } - val goalToHeadSubs = headAndGoalSubs.filterKeys { occurs(it as Variable, simplifiedGoal) } + val goalToHeadSubs = headAndGoalSubs.filterKeys { occurs(it as Variable, renamedGoal) } val headResult = headToGoalSubs.filterKeys { key -> goalToHeadSubs.any { occurs(key as Variable, it.value) } } @@ -47,24 +53,34 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent { bodyAnswer.fold( onSuccess = { bodySubs -> // If the body can be proven, yield the (combined) substitutions - val goalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) } - val bodyResult = bodySubs.filterKeys { occurs(it as Variable, simplifiedGoal) } + val renamedGoalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) } + val goalResult = + renamedGoalResult.mapKeys { applySubstitution(it.key, reverseGoalRenaming) } + val renamedBodyResult = bodySubs.filterKeys { occurs(it as Variable, renamedGoal) } + val bodyResult = renamedBodyResult.mapKeys { applySubstitution(it.key, reverseGoalRenaming) } yield(Result.success(goalResult + headResult + bodyResult)) }, onFailure = { error -> - if (error is AppliedCut) { - // Find single solution and return immediately - if (error.subs != null) { - val bodySubs = error.subs - val goalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) } - val bodyResult = bodySubs.filterKeys { occurs(it as Variable, simplifiedGoal) } - yield(Result.failure(AppliedCut(goalResult + headResult + bodyResult))) - } else { - yield(Result.failure(AppliedCut())) + when (error) { + is AppliedCut -> { + // Find single solution and return immediately + if (error.subs != null) { + val bodySubs = error.subs + val goalResult = + goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) } + val bodyResult = bodySubs.filterKeys { occurs(it as Variable, renamedGoal) } + yield(Result.failure(AppliedCut(goalResult + headResult + bodyResult))) + } else { + yield(Result.failure(AppliedCut())) + } + return@sequence } - return@sequence - } else { - yield(Result.failure(error)) + + is AppliedShift -> { + yield(Result.failure(error)) + } + + else -> yield(Result.failure(error)) } } ) diff --git a/src/prolog/ast/terms/Body.kt b/src/prolog/ast/terms/Body.kt index 989c4d9..af78788 100644 --- a/src/prolog/ast/terms/Body.kt +++ b/src/prolog/ast/terms/Body.kt @@ -1,5 +1,8 @@ package prolog.ast.terms +import prolog.Substitutions import prolog.ast.logic.Satisfiable -interface Body : Term, Satisfiable +interface Body : Term, Satisfiable { + override fun applySubstitution(subs: Substitutions): Body +} diff --git a/src/prolog/builtins/controlOperators.kt b/src/prolog/builtins/controlOperators.kt index 3d81786..5fdcf80 100644 --- a/src/prolog/builtins/controlOperators.kt +++ b/src/prolog/builtins/controlOperators.kt @@ -55,7 +55,7 @@ open class Conjunction(val left: LogicOperand, private val right: LogicOperand) right.fold( // If the right part succeeds, yield the result with the left substitutions onSuccess = { rightSubs -> - yield(Result.success(leftSubs + rightSubs)) + yield(Result.success(rightSubs + leftSubs)) }, onFailure = { exception -> // If the right part fails, check if it's a cut @@ -74,8 +74,8 @@ open class Conjunction(val left: LogicOperand, private val right: LogicOperand) } fun findNextCutSolution(appliedCut: AppliedCut): Answers = sequence { - val leftSubs = appliedCut.subs - right.satisfy(subs + (appliedCut.subs!!)).firstOrNull()?.map { rightSubs -> + val leftSubs = appliedCut.subs ?: emptyMap() + right.satisfy(subs + leftSubs).firstOrNull()?.map { rightSubs -> // If the right part succeeds, yield the result with the left substitutions yield(Result.success(leftSubs + rightSubs)) return@sequence diff --git a/src/prolog/builtins/delimitedContinuationsOperators.kt b/src/prolog/builtins/delimitedContinuationsOperators.kt index 43f6e22..0d26a9b 100644 --- a/src/prolog/builtins/delimitedContinuationsOperators.kt +++ b/src/prolog/builtins/delimitedContinuationsOperators.kt @@ -39,7 +39,7 @@ class Reset(private val goal: Goal, private val ball: Term, private val cont: Te if (failure is AppliedShift) { require(failure.cont != null) { "Shift must have a continuation" } // Reset/3 succeeds immediately, binding Term1 to Term2 and Cont to the remainder of Goal. - val shiftSubs = failure.subs + val shiftSubs = failure.subs + subs val appliedBall = applySubstitution(failure.ball, shiftSubs) val appliedCont = applySubstitution(failure.cont, shiftSubs) Conjunction(Unify(ball, appliedBall), Unify(appliedCont, cont)) diff --git a/tests/e2e/Examples.kt b/tests/e2e/Examples.kt index 6df1df2..69de8ca 100644 --- a/tests/e2e/Examples.kt +++ b/tests/e2e/Examples.kt @@ -27,7 +27,7 @@ class Examples { @Test fun debugHelper() { - loader.load("examples/meta/continuations.pl") + loader.load("examples/meta/mib_voorbeelden.pl") } @ParameterizedTest @@ -60,6 +60,7 @@ class Examples { Arguments.of("forall.pl", "Only alice likes pizza.\n"), Arguments.of("fraternity.pl", "Citizen robespierre is eligible for the event.\nCitizen danton is eligible for the event.\nCitizen camus is eligible for the event.\n"), Arguments.of("liberty.pl", "Give me Liberty, or give me Death!\nI disapprove of what you say, but I will defend to the death your right to say it.\nThe revolution devours its own children.\nSo this is how liberty dies, with thunderous applause.\n"), + Arguments.of("summer.pl", "The sum of 1 to 9 is: 36\n"), Arguments.of("unification.pl", "While alice got an A, carol got an A, but bob did not get an A, dave did not get an A, unfortunately.\n"), Arguments.of("write.pl", "gpl zegt: dag(wereld)\n"), )