feat: Cut

examples/scratchpad.pl

@@ -1,3 +1,2 @@
-a.
+not_equal(X, Y) :- X = Y, !, fail.
-f(a).
+not_equal(_, _).
-f(X, _) :- X.

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 ->
+                    bodyAnswer.fold(
-                        yield(Result.success(newHeadSubs + newBodySubs))
+                        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))
+                            }
+                        }
+                    )
                 }
             }
         }

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))
+                        }
+                    }
+                )
+            }
+        }
     }
 }

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 ->
+        // Satisfy the left part first, which either succeeds or fails
-            leftResult.mapCatching { left ->
+        left.satisfy(subs).forEach { left ->
-                right.satisfy(subs + left).forEach { rightResult ->
+            left.fold(
-                    rightResult.map { right ->
+                // If it succeeds, satisfy the right part with the updated substitutions and return all results
-                        yield(Result.success(left + right))
+                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))
                     }
                 }
-            }
+            )
         }
     }
 }

src/prolog/exceptions/AppliedCut.kt

@@ -0,0 +1,5 @@
+package prolog.exceptions
+
+import prolog.Substitutions
+
+class AppliedCut(val subs: Substitutions): Exception()

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")
+    }
+}

tests/prolog/builtins/ControlTest.kt

@@ -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")
-    }
-}