diff --git a/examples/scratchpad.pl b/examples/scratchpad.pl index 901da32..2959dee 100644 --- a/examples/scratchpad.pl +++ b/examples/scratchpad.pl @@ -1,3 +1,2 @@ -a. -f(a). -f(X, _) :- X. +not_equal(X, Y) :- X = Y, !, fail. +not_equal(_, _). \ No newline at end of file diff --git a/src/prolog/ast/logic/Clause.kt b/src/prolog/ast/logic/Clause.kt index b899dd8..98a5a6b 100644 --- a/src/prolog/ast/logic/Clause.kt +++ b/src/prolog/ast/logic/Clause.kt @@ -7,6 +7,7 @@ import prolog.ast.terms.Functor import prolog.ast.terms.Goal import prolog.ast.terms.Head import prolog.builtins.True +import prolog.exceptions.AppliedCut import prolog.logic.unifyLazy /** @@ -28,9 +29,20 @@ abstract class Clause(private val head: Head, private val body: Body) : Resolven headAnswer.map { newHeadSubs -> // If the body can be proven, yield the (combined) substitutions body.satisfy(subs + newHeadSubs).forEach { bodyAnswer -> - bodyAnswer.map { newBodySubs -> - yield(Result.success(newHeadSubs + newBodySubs)) - } + bodyAnswer.fold( + onSuccess = { newBodySubs -> + yield(Result.success(newHeadSubs + newBodySubs)) + }, + onFailure = { error -> + if (error is AppliedCut) { + // Find single solution and return immediately + yield(Result.failure(AppliedCut(newHeadSubs + error.subs))) + return@sequence + } else { + yield(Result.failure(error)) + } + } + ) } } } diff --git a/src/prolog/ast/logic/Predicate.kt b/src/prolog/ast/logic/Predicate.kt index 3a1e3aa..9b8fb64 100644 --- a/src/prolog/ast/logic/Predicate.kt +++ b/src/prolog/ast/logic/Predicate.kt @@ -4,6 +4,7 @@ import prolog.Answers import prolog.Substitutions import prolog.ast.terms.Functor import prolog.ast.terms.Goal +import prolog.exceptions.AppliedCut /** * Collection of [Clause]s with the same [Functor]. @@ -53,6 +54,23 @@ class Predicate : Resolvent { require(goal.functor == functor) { "Goal functor does not match predicate functor" } // Try to unify the goal with the clause // If the unification is successful, yield the substitutions - clauses.forEach { yieldAll(it.solve(goal, subs)) } + clauses.forEach { clause -> + clause.solve(goal, subs).forEach { clauseResult -> + clauseResult.fold( + onSuccess = { + yield(Result.success(it)) + }, + onFailure = { + if (it is AppliedCut) { + // If it's a cut, yield the result with the left substitutions + yield(Result.failure(AppliedCut(it.subs))) + return@sequence + } else { + yield(Result.failure(it)) + } + } + ) + } + } } } diff --git a/src/prolog/builtins/controlOperators.kt b/src/prolog/builtins/controlOperators.kt index 8f193b9..36873b2 100644 --- a/src/prolog/builtins/controlOperators.kt +++ b/src/prolog/builtins/controlOperators.kt @@ -7,6 +7,7 @@ import prolog.ast.terms.Atom import prolog.ast.terms.Body import prolog.ast.terms.Goal import prolog.ast.logic.LogicOperator +import prolog.exceptions.AppliedCut /** * Always fail. @@ -29,21 +30,64 @@ object True : Atom("true"), Body { // TODO Repeat/0 -// TODO !/0 (Cut) +class Cut() : Atom("!") { + override fun satisfy(subs: Substitutions): Answers { + return sequenceOf(Result.failure(AppliedCut(emptyMap()))) + } +} /** * Conjunction (and). True if both Goal1 and Goal2 are true. */ -class Conjunction(private val left: LogicOperand, private val right: LogicOperand) : LogicOperator(Atom(","), left, right) { +class Conjunction(private val left: LogicOperand, private val right: LogicOperand) : + LogicOperator(Atom(","), left, right) { override fun satisfy(subs: Substitutions): Answers = sequence { - left.satisfy(subs).forEach { leftResult -> - leftResult.mapCatching { left -> - right.satisfy(subs + left).forEach { rightResult -> - rightResult.map { right -> - yield(Result.success(left + right)) + // Satisfy the left part first, which either succeeds or fails + left.satisfy(subs).forEach { left -> + left.fold( + // If it succeeds, satisfy the right part with the updated substitutions and return all results + onSuccess = { leftSubs -> + right.satisfy(subs + leftSubs).forEach { + it.fold( + // If the right part succeeds, yield the result with the left substitutions + onSuccess = { rightSubs -> + yield(Result.success(leftSubs + rightSubs)) + }, + // If the right part fails, check if it's a cut + onFailure = { exception -> + if (exception is AppliedCut) { + // If it's a cut, yield the result with the left substitutions + yield(Result.failure(AppliedCut(leftSubs + exception.subs))) + return@sequence + } else { + // If it's not a cut, yield the failure + yield(Result.failure(exception)) + } + } + ) + } + }, + // If it fails, check these conditions: + onFailure = { exception -> + // 1. If the left part is a cut, satisfy the right part ONCE, and stop searching for more solutions + if (exception is AppliedCut) { + right.satisfy(subs + exception.subs).first().fold( + onSuccess = { + // If the right part succeeds, yield the result with the left substitutions + yield(Result.success(exception.subs + it)) + return@sequence + }, + onFailure = { + // If the right part fails, yield the failure + yield(Result.failure(it)) + } + ) + } else { + // 2. Any other failure should be returned as is + yield(Result.failure(exception)) } } - } + ) } } } diff --git a/src/prolog/exceptions/AppliedCut.kt b/src/prolog/exceptions/AppliedCut.kt new file mode 100644 index 0000000..d1d492a --- /dev/null +++ b/src/prolog/exceptions/AppliedCut.kt @@ -0,0 +1,5 @@ +package prolog.exceptions + +import prolog.Substitutions + +class AppliedCut(val subs: Substitutions): Exception() diff --git a/tests/prolog/builtins/ControlOperatorsTests.kt b/tests/prolog/builtins/ControlOperatorsTests.kt new file mode 100644 index 0000000..9aaab2f --- /dev/null +++ b/tests/prolog/builtins/ControlOperatorsTests.kt @@ -0,0 +1,201 @@ +package prolog.builtins + +import org.junit.jupiter.api.Assertions.* +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.Test +import prolog.Program +import prolog.ast.logic.Fact +import prolog.ast.logic.Rule +import prolog.ast.terms.Atom +import prolog.ast.terms.CompoundTerm +import prolog.ast.terms.Integer +import prolog.ast.terms.Variable + +class ControlOperatorsTests { + @BeforeEach + fun setUp() { + Program.clear() + } + + @Test + fun `simple cut program`() { + // First an example without cut + Program.load( + listOf( + Fact(CompoundTerm(Atom("foo"), listOf(Atom("a")))), + Fact(CompoundTerm(Atom("foo"), listOf(Atom("b")))), + ) + ) + + val goal = CompoundTerm(Atom("foo"), listOf(Variable("X"))) + + var result = Program.query(goal).toList() + + assertEquals(2, result.size, "Expected 2 results") + + // Now with cut + + Program.clear() + + Program.load( + listOf( + Rule(CompoundTerm(Atom("foo"), listOf(Atom("a"))), Cut()), + Fact(CompoundTerm(Atom("foo"), listOf(Atom("b")))), + ) + ) + + result = Program.query(goal).toList() + + assertEquals(1, result.size, "Expected 1 result") + } + + @Test + fun `cut with pruning`() { + // First an example without cut + Program.load( + listOf( + Fact(CompoundTerm(Atom("a"), listOf(Integer(1)))), + Fact(CompoundTerm(Atom("a"), listOf(Integer(2)))), + Fact(CompoundTerm(Atom("b"), listOf(Integer(1)))), + Fact(CompoundTerm(Atom("b"), listOf(Integer(2)))), + + Rule( + CompoundTerm(Atom("foo"), listOf(Variable("X"), Variable("Y"))), + Conjunction( + CompoundTerm(Atom("a"), listOf(Variable("X"))), + CompoundTerm(Atom("b"), listOf(Variable("Y"))) + ) + ) + ) + ) + + val goal = CompoundTerm(Atom("foo"), listOf(Variable("X"), Variable("Y"))) + + /* ?- foo(X, Y). + * X = Y, Y = 1 ; + * X = 1, + * Y = 2 ; + * X = 2, + * Y = 1 ; + * X = Y, Y = 2. */ + var result = Program.query(goal).toList() + + assertEquals(4, result.size, "Expected 4 results") + + // Now with cut in the middle + + Program.clear() + + Program.load( + listOf( + Fact(CompoundTerm(Atom("a"), listOf(Integer(1)))), + Fact(CompoundTerm(Atom("a"), listOf(Integer(2)))), + Fact(CompoundTerm(Atom("b"), listOf(Integer(1)))), + Fact(CompoundTerm(Atom("b"), listOf(Integer(2)))), + + Rule( + CompoundTerm(Atom("foo"), listOf(Variable("X"), Variable("Y"))), + Conjunction( + CompoundTerm(Atom("a"), listOf(Variable("X"))), + Conjunction( + Cut(), + CompoundTerm(Atom("b"), listOf(Variable("Y"))) + ) + ) + ) + ) + ) + + /* + ?- foo(X, Y). + X = Y, Y = 1 ; + X = 1, + Y = 2. + */ + result = Program.query(goal).toList() + + assertEquals(2, result.size, "Expected 2 results") + + // Now with cut at the end + + Program.clear() + + Program.load( + listOf( + Fact(CompoundTerm(Atom("a"), listOf(Integer(1)))), + Fact(CompoundTerm(Atom("a"), listOf(Integer(2)))), + Fact(CompoundTerm(Atom("b"), listOf(Integer(1)))), + Fact(CompoundTerm(Atom("b"), listOf(Integer(2)))), + + Rule( + CompoundTerm(Atom("foo"), listOf(Variable("X"), Variable("Y"))), + Conjunction( + CompoundTerm(Atom("a"), listOf(Variable("X"))), + Conjunction( + CompoundTerm(Atom("b"), listOf(Variable("Y"))), + Cut() + ) + ) + ) + ) + ) + + /* + ?- foo(X, Y). + X = Y, Y = 1 ; + */ + result = Program.query(goal).toList() + + assertEquals(1, result.size, "Expected 1 result") + } + + @Test + fun not_atom() { + val success = Fact(Atom("a")) + + Program.load(listOf(success)) + + val goal = Atom("a") + val notGoal = Not(goal) + + val result1 = Program.query(goal) + val result2 = Program.query(notGoal) + + assertTrue(result1.any(), "Expected query to succeed") + assertFalse(result2.any(), "Expected query to fail") + } + + @Test + fun not_compound() { + val success = Fact(Atom("f")) + val failure = Fact(Atom("g")) + + Program.load(listOf(success, failure)) + + val goal = Atom("f") + val notGoal = Not(Atom("g")) + + val result1 = Program.query(goal) + val result2 = Program.query(notGoal) + + assertTrue(result1.any(), "Expected query to succeed") + assertFalse(result2.any(), "Expected query to fail") + } + + @Test + fun fail_should_cause_fails() { + val success = Fact(Atom("a")) + val failure = Fact(Atom("b")) + + Program.load(listOf(success, failure)) + + val goal = Atom("a") + val failGoal = Fail + + val result1 = Program.query(goal) + val result2 = Program.query(failGoal) + + assertTrue(result1.any(), "Expected query to succeed") + assertFalse(result2.any(), "Expected query to fail") + } +} \ No newline at end of file diff --git a/tests/prolog/builtins/ControlTest.kt b/tests/prolog/builtins/ControlTest.kt deleted file mode 100644 index 11e835e..0000000 --- a/tests/prolog/builtins/ControlTest.kt +++ /dev/null @@ -1,66 +0,0 @@ -package prolog.builtins - -import org.junit.jupiter.api.Assertions.assertFalse -import org.junit.jupiter.api.Assertions.assertTrue -import org.junit.jupiter.api.BeforeEach -import org.junit.jupiter.api.Test -import prolog.Program -import prolog.ast.logic.Fact -import prolog.ast.terms.Atom - -class ControlTest { - @BeforeEach - fun setUp() { - Program.clear() - } - - @Test - fun not_atom() { - val success = Fact(Atom("a")) - - Program.load(listOf(success)) - - val goal = Atom("a") - val notGoal = Not(goal) - - val result1 = Program.query(goal) - val result2 = Program.query(notGoal) - - assertTrue(result1.any(), "Expected query to succeed") - assertFalse(result2.any(), "Expected query to fail") - } - - @Test - fun not_compound() { - val success = Fact(Atom("f")) - val failure = Fact(Atom("g")) - - Program.load(listOf(success, failure)) - - val goal = Atom("f") - val notGoal = Not(Atom("g")) - - val result1 = Program.query(goal) - val result2 = Program.query(notGoal) - - assertTrue(result1.any(), "Expected query to succeed") - assertFalse(result2.any(), "Expected query to fail") - } - - @Test - fun fail_should_cause_fails() { - val success = Fact(Atom("a")) - val failure = Fact(Atom("b")) - - Program.load(listOf(success, failure)) - - val goal = Atom("a") - val failGoal = Fail - - val result1 = Program.query(goal) - val result2 = Program.query(failGoal) - - assertTrue(result1.any(), "Expected query to succeed") - assertFalse(result2.any(), "Expected query to fail") - } -} \ No newline at end of file