diff --git a/src/prolog/builtins/controlOperators.kt b/src/prolog/builtins/controlOperators.kt index c948701..c1376f9 100644 --- a/src/prolog/builtins/controlOperators.kt +++ b/src/prolog/builtins/controlOperators.kt @@ -18,7 +18,7 @@ import prolog.logic.numbervars */ object Fail : Atom("fail"), Body { override fun satisfy(subs: Substitutions): Answers = emptySequence() - override fun applySubstitution(subs: Substitutions): Fail = Fail + override fun applySubstitution(subs: Substitutions): Fail = this } /** @@ -31,7 +31,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 + override fun applySubstitution(subs: Substitutions): True = this } // TODO Repeat/0 @@ -41,7 +41,7 @@ class Cut() : Atom("!") { return sequenceOf(Result.failure(AppliedCut(emptyMap()))) } - override fun applySubstitution(subs: Substitutions): Cut = Cut() + override fun applySubstitution(subs: Substitutions): Cut = this } /** @@ -50,83 +50,63 @@ class Cut() : Atom("!") { open class Conjunction(val left: LogicOperand, private val right: LogicOperand) : LogicOperator(Atom(","), left, right) { override fun satisfy(subs: Substitutions): Answers = sequence { + fun satisfyRight(leftSubs: Substitutions): Answers = sequence { + right.satisfy(subs + leftSubs).forEach { right -> + right.fold( + // If the right part succeeds, yield the result with the left substitutions + onSuccess = { rightSubs -> + yield(Result.success(leftSubs + rightSubs)) + }, + onFailure = { exception -> + // If the right part fails, check if it's a cut + if (exception is AppliedCut) { + // If it's a cut, yield the result with the left substitutions + val newSubs = if (exception.subs != null) leftSubs + exception.subs else null + yield(Result.failure(AppliedCut(newSubs))) + return@sequence + } + + // If it's not a cut, yield the failure + yield(Result.failure(exception)) + } + ) + } + } + + fun findNextCutSolution(appliedCut: AppliedCut): Answers = sequence { + val leftSubs = appliedCut.subs + right.satisfy(subs + (appliedCut.subs!!)).firstOrNull()?.map { rightSubs -> + // If the right part succeeds, yield the result with the left substitutions + yield(Result.success(leftSubs + rightSubs)) + return@sequence + } ?: yield(Result.failure(AppliedCut())) + } + // 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 { right -> - right.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 (exception.subs != null) { - // If it's a cut, yield the result with the left substitutions - yield(Result.failure(AppliedCut(leftSubs + exception.subs))) - } else { - yield(Result.failure(AppliedCut())) - } - return@sequence - } - - // If it's not a cut, yield the failure - yield(Result.failure(exception)) - } - ) - } - }, + onSuccess = { leftSubs -> yieldAll(satisfyRight(leftSubs)) }, // 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!!)).firstOrNull()?.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)) - } - ) ?: yield(Result.failure(AppliedCut())) - } else if (exception is AppliedShift) { - if (exception.cont == null) { - // Goal should be our right operand - yield(Result.failure(AppliedShift(exception.subs, exception.ball, right as Goal))) - } else { - val leftSubs = exception.subs - right.satisfy(subs + leftSubs).forEach { right -> - right.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 (exception.subs != null) { - // If it's a cut, yield the result with the left substitutions - yield(Result.failure(AppliedCut(leftSubs + exception.subs))) - } else { - yield(Result.failure(AppliedCut())) - } - return@sequence - } + when (exception) { + // 1. If the left part is a cut, satisfy the right part ONCE, and stop searching for more solutions + is AppliedCut -> yieldAll(findNextCutSolution(exception)) - // If it's not a cut, yield the failure - yield(Result.failure(exception)) - } - ) + // 2. If the left part is a shift, we need to check if the right part can be satisfied + is AppliedShift -> { + if (exception.cont == null) { + // Pass the right of our disjunction as the continuation + val newShift = AppliedShift(exception.subs, exception.ball, right as Goal) + yield(Result.failure(newShift)) + } else { + // Satisfy the right part with the updated substitutions + yieldAll(satisfyRight(exception.subs)) } } - } else { - // 2. Any other failure should be returned as is - yield(Result.failure(exception)) + + // 3. Any other failure should be returned as is + else -> yield(Result.failure(exception)) } } ) diff --git a/src/prolog/builtins/delimitedContinuationsOperators.kt b/src/prolog/builtins/delimitedContinuationsOperators.kt index 8487ca8..5a01eb4 100644 --- a/src/prolog/builtins/delimitedContinuationsOperators.kt +++ b/src/prolog/builtins/delimitedContinuationsOperators.kt @@ -4,52 +4,54 @@ 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.applySubstitution 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)) { +/** + * These classes provide support for delimited continuations in Prolog. + * More specifically, they implement the reset/3 and shift/1 operators. + * + * See also [SWI-Prolog 4.9 Delimited Continuations](https://www.swi-prolog.org/pldoc/man?section=delcont) + */ + +/** + * Call [Goal]. If Goal calls [Shift], and the arguments of Shift can be unified with Ball, Shift causes Reset to + * return, unifying Cont with a Goal that represents the continuation after shift. + */ +class Reset(private val goal: Goal, private val ball: Term, private val cont: Term) : + Structure(Atom("reset"), listOf(goal, ball, 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)) + // Reset/3 succeeds immediately, binding Term1 to Term2 and Cont to the remainder of Goal. + val shiftSubs = failure.subs + val appliedBall = applySubstitution(failure.ball, shiftSubs) + val appliedCont = applySubstitution(failure.cont, shiftSubs) + Conjunction(Unify(ball, appliedBall), Unify(appliedCont, cont)) + .satisfy(shiftSubs) + .forEach { conResult -> + conResult.map { conSubs -> + yield(Result.success(shiftSubs + conSubs)) + } + } } else { + // If Goal fails, then reset also fails. yield(Result.failure(failure)) } } @@ -62,5 +64,12 @@ class Reset(private val goal: Goal, private val term1: Term, private val cont: T * 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))) + override fun satisfy(subs: Substitutions): Answers = sequence { + val shift = AppliedShift( + subs = subs, + ball = ball, + cont = null + ) + yield(Result.failure(shift)) + } } diff --git a/src/prolog/builtins/listOperators.kt b/src/prolog/builtins/listOperators.kt index 5ef7ea2..d1a1944 100644 --- a/src/prolog/builtins/listOperators.kt +++ b/src/prolog/builtins/listOperators.kt @@ -7,7 +7,6 @@ import prolog.ast.lists.List.Cons import prolog.ast.lists.List.Empty import prolog.ast.terms.Atom import prolog.ast.terms.Operator -import prolog.ast.terms.Structure import prolog.ast.terms.Term import prolog.logic.applySubstitution diff --git a/src/tool/mapEach.kt b/src/tool/mapEach.kt new file mode 100644 index 0000000..1786867 --- /dev/null +++ b/src/tool/mapEach.kt @@ -0,0 +1,3 @@ +package tool + +fun Sequence.mapEach(transform: (T) -> R): Sequence = map(transform)