Continuations

src/prolog/builtins/delimitedContinuationsOperators.kt

@@ -0,0 +1,66 @@
+package prolog.builtins
+
+import prolog.Answers
+import prolog.Substitutions
+import prolog.ast.arithmetic.Integer
+import prolog.ast.terms.Atom
+import prolog.ast.terms.CompoundTerm
+import prolog.ast.terms.Goal
+import prolog.ast.terms.Structure
+import prolog.ast.terms.Term
+import prolog.flags.AppliedShift
+import prolog.logic.unifyLazy
+
+class Reset(private val goal: Goal, private val term1: Term, private val cont: Term) :
+    Structure(Atom("reset"), listOf(goal, term1, cont)) {
+    override fun satisfy(subs: Substitutions): Answers = sequence {
+        goal.satisfy(subs).forEach { goalResult ->
+            goalResult.fold(
+                // If Goal succeeds, then reset/3 also succeeds and binds Cont and Term1 to 0.
+                onSuccess = { goalSubs ->
+                    // Unify Cont with 0
+                    unifyLazy(cont, Integer(0), goalSubs).forEach { contResult ->
+                        contResult.map { contSubs ->
+                            yield(Result.success(goalSubs + contSubs))
+//                            // Unify Term1 with 0
+//                            unifyLazy(term1, Integer(0), goalSubs + contSubs).forEach { termResult ->
+//                                termResult.map { termSubs ->
+//                                    yield(Result.success(goalSubs + termSubs + contSubs))
+//                                }
+//                            }
+                        }
+                    }
+
+                    // TODO
+//                    val conjunction = Conjunction(Unify(term1, Integer(0)), Unify(cont, Integer(0)))
+//                    yieldAll(conjunction.satisfy(goalSubs))
+                },
+                onFailure = { failure ->
+                    // If at some point Goal calls shift(Term2), then its further execution is suspended.
+                    // Reset/3 succeeds immediately, binding Term1 to Term2 and Cont to the remainder of Goal.
+                    // If Goal fails, then reset also fails.
+//                    yield(Result.failure(failure))
+
+                    // Unify Term1 with the ball
+                    if (failure is AppliedShift) {
+                        require(failure.cont != null) { "Shift must have a continuation" }
+                        val newSubs: Substitutions = mapOf(
+                            term1 to failure.ball,
+                            cont to failure.cont
+                        )
+                        yield(Result.success(failure.subs + newSubs))
+                    } else {
+                        yield(Result.failure(failure))
+                    }
+                }
+            )
+        }
+    }
+}
+
+/**
+ * Variables that have been bound during the procedure called by reset/3 stay bound after a shift/1:
+ */
+class Shift(private val ball: Term) : Structure(Atom("shift"), listOf(ball)) {
+    override fun satisfy(subs: Substitutions): Answers = sequenceOf(Result.failure(AppliedShift(subs, ball)))
+}