diff --git a/examples/meta/continuations.pl b/examples/meta/continuations.pl new file mode 100644 index 0000000..cb31677 --- /dev/null +++ b/examples/meta/continuations.pl @@ -0,0 +1,19 @@ +test(Cont, Term) :- + writeln("Inside test"), + reset(test_, Term, Cont), + writeln("After reset"). + +test_ :- + writeln("Entering reset"), + shift(Y), + X is 1 + (2 * Y), + write("In test X = "), write(X), writeln("; done"). + +main :- + test(Cont, Term), + \+ \+ ( writeln("Calling Cont(2)"), + Term = 2, call(Cont)), + \+ \+ ( writeln("Calling Cont(4)"), + Term = 4, call(Cont)). + +:- initialization(main). diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt index 5088012..7076dc8 100644 --- a/src/interpreter/Preprocessor.kt +++ b/src/interpreter/Preprocessor.kt @@ -145,6 +145,10 @@ open class Preprocessor { } } + // Delimited Continuations + Functor.of("reset/3") -> Reset(args[0] as Goal, args[1], args[2]) + Functor.of("shift/1") -> Shift(args[0]) + // IO Functor.of("write/1") -> Write(args[0]) Functor.of("nl/0") -> Nl @@ -155,7 +159,7 @@ open class Preprocessor { Functor.of("member/2") -> Member(args[0], args[1] as PList) // Meta - Functor.of("call/1") -> Call(args[0] as Goal) + Functor.of("call/1") -> Call(args[0]) Functor.of("ignore/1") -> Ignore(args[0] as Goal) // Other diff --git a/src/parser/grammars/TermsGrammar.kt b/src/parser/grammars/TermsGrammar.kt index 8db42e9..9051484 100644 --- a/src/parser/grammars/TermsGrammar.kt +++ b/src/parser/grammars/TermsGrammar.kt @@ -3,9 +3,10 @@ package parser.grammars import com.github.h0tk3y.betterParse.combinators.* import com.github.h0tk3y.betterParse.grammar.parser import com.github.h0tk3y.betterParse.parser.Parser +import com.github.h0tk3y.betterParse.utils.Tuple2 import prolog.ast.arithmetic.Float import prolog.ast.arithmetic.Integer -import prolog.ast.lists.List +import prolog.ast.lists.List as PList import prolog.ast.terms.* import prolog.builtins.Dynamic import prolog.ast.lists.List.Empty @@ -96,14 +97,19 @@ open class TermsGrammar : Tokens() { if (t2 == null) t1 else CompoundTerm(Atom(t2!!.t1), listOf(t1, t2!!.t2)) } + protected val not: Parser by (notOp * parser(::term900)) use { + CompoundTerm(Atom(t1.text), listOf(t2)) + } + protected val term900: Parser by (not or term700) + protected val op1000: Parser by (comma) use { text } - protected val term1000: Parser by (term700 * zeroOrMore(op1000 * term700)) use { - t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) } + protected val term1000: Parser by (term900 * zeroOrMore(op1000 * term900)) use { + constructRightAssociative(t1, t2) } protected val op1100: Parser by (semicolon) use { text } protected val term1100: Parser by (term1000 * zeroOrMore(op1100 * term1000)) use { - t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) } + constructRightAssociative(t1, t2) } protected val dynamic: Parser by (dynamicOp * functor) use { @@ -117,12 +123,12 @@ open class TermsGrammar : Tokens() { } // Lists - protected val list: Parser by (-leftBracket * separated( + protected val list: Parser by (-leftBracket * separated( parser(::termNoConjunction), comma, acceptZero = true ) * -rightBracket) use { - var list: List = Empty + var list: PList = Empty // Construct the list in reverse order for (term in this.terms.reversed()) { list = Cons(term, list) @@ -139,4 +145,12 @@ open class TermsGrammar : Tokens() { protected val body: Parser by term use { this as Body } override val rootParser: Parser by term + + fun constructRightAssociative(left: Term, pairs: List>): Term { + if (pairs.isEmpty()) return left + + val (name, next) = pairs.first() + val remainingPairs = pairs.drop(1) + return CompoundTerm(Atom(name), listOf(left, constructRightAssociative(next, remainingPairs))) + } } diff --git a/src/parser/grammars/Tokens.kt b/src/parser/grammars/Tokens.kt index b998fee..ccdbae9 100644 --- a/src/parser/grammars/Tokens.kt +++ b/src/parser/grammars/Tokens.kt @@ -21,6 +21,8 @@ abstract class Tokens : Grammar() { protected val semicolon: Token by literalToken(";") // 1000 protected val comma: Token by literalToken(",") + // 900 + protected val notOp: Token by literalToken("\\+") // 700 protected val univOp: Token by literalToken("=..") protected val notEquivalent: Token by literalToken("\\==") diff --git a/src/prolog/builtins/controlOperators.kt b/src/prolog/builtins/controlOperators.kt index eb3d48c..c948701 100644 --- a/src/prolog/builtins/controlOperators.kt +++ b/src/prolog/builtins/controlOperators.kt @@ -9,6 +9,7 @@ import prolog.ast.terms.Atom import prolog.ast.terms.Body import prolog.ast.terms.Goal import prolog.flags.AppliedCut +import prolog.flags.AppliedShift import prolog.logic.applySubstitution import prolog.logic.numbervars @@ -46,7 +47,7 @@ class Cut() : Atom("!") { /** * Conjunction (and). True if both Goal1 and Goal2 are true. */ -class Conjunction(val left: LogicOperand, private val right: LogicOperand) : +open class Conjunction(val left: LogicOperand, private val right: LogicOperand) : LogicOperator(Atom(","), left, right) { override fun satisfy(subs: Substitutions): Answers = sequence { // Satisfy the left part first, which either succeeds or fails @@ -93,6 +94,36 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) : 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 + } + + // If it's not a cut, yield the failure + yield(Result.failure(exception)) + } + ) + } + } } else { // 2. Any other failure should be returned as is yield(Result.failure(exception)) diff --git a/src/prolog/builtins/delimitedContinuationsOperators.kt b/src/prolog/builtins/delimitedContinuationsOperators.kt new file mode 100644 index 0000000..8487ca8 --- /dev/null +++ b/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))) +} diff --git a/src/prolog/builtins/ioOperators.kt b/src/prolog/builtins/ioOperators.kt index 5708bab..514690c 100644 --- a/src/prolog/builtins/ioOperators.kt +++ b/src/prolog/builtins/ioOperators.kt @@ -50,6 +50,7 @@ object Nl : Atom("nl"), Satisfiable { class WriteLn(private val term: Term) : Conjunction(Write(term), Nl) { constructor(message: String) : this(Atom(message)) override fun applySubstitution(subs: Substitutions): WriteLn = WriteLn(applySubstitution(term, subs)) + override fun toString(): String = "writeln($term)" } /** diff --git a/src/prolog/builtins/listOperators.kt b/src/prolog/builtins/listOperators.kt index 5dedc11..5ef7ea2 100644 --- a/src/prolog/builtins/listOperators.kt +++ b/src/prolog/builtins/listOperators.kt @@ -7,7 +7,9 @@ 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 class Member(private val element: Term, private val list: List) : Operator(Atom("member"), element, list) { private var solution: Operator = when (list) { @@ -20,5 +22,10 @@ class Member(private val element: Term, private val list: List) : Operator(Atom( override fun satisfy(subs: Substitutions): Answers = solution.satisfy(subs) + override fun applySubstitution(subs: Substitutions): Member = Member( + applySubstitution(element, subs), + applySubstitution(list, subs) as List + ) + override fun toString(): String = "$element ∈ $list" } diff --git a/src/prolog/builtins/metaOperators.kt b/src/prolog/builtins/metaOperators.kt index 379fb9b..047fa5f 100644 --- a/src/prolog/builtins/metaOperators.kt +++ b/src/prolog/builtins/metaOperators.kt @@ -5,10 +5,15 @@ import prolog.Substitutions import prolog.ast.terms.Atom import prolog.ast.terms.Goal import prolog.ast.terms.Operator +import prolog.ast.terms.Term import prolog.flags.AppliedCut +import prolog.logic.applySubstitution -class Call(private val goal: Goal) : Operator(Atom("call"), null, goal) { - override fun satisfy(subs: Substitutions): Answers = goal.satisfy(subs) +class Call(private val goal: Term) : Operator(Atom("call"), null, goal) { + override fun satisfy(subs: Substitutions): Answers { + val appliedGoal = applySubstitution(goal, subs) as Goal + return appliedGoal.satisfy(subs) + } } /** diff --git a/src/prolog/flags/AppliedShift.kt b/src/prolog/flags/AppliedShift.kt new file mode 100644 index 0000000..a96b55d --- /dev/null +++ b/src/prolog/flags/AppliedShift.kt @@ -0,0 +1,14 @@ +package prolog.flags + +import prolog.Substitutions +import prolog.ast.terms.Goal +import prolog.ast.terms.Term + +/** + * An exception that indicates that a shift has been applied in the Prolog engine. + */ +data class AppliedShift( + val subs: Substitutions, + val ball: Term, + val cont: Term? = null, +) : Throwable() \ No newline at end of file diff --git a/tests/e2e/Examples.kt b/tests/e2e/Examples.kt index 4c86e0d..250f804 100644 --- a/tests/e2e/Examples.kt +++ b/tests/e2e/Examples.kt @@ -27,7 +27,7 @@ class Examples { @Test fun debugHelper() { - loader.load("examples/basics/arithmetics.pl") + loader.load("examples/meta/continuations.pl") } @ParameterizedTest @@ -65,6 +65,7 @@ class Examples { ) fun meta() = listOf( + Arguments.of("continuations.pl", "Inside test\nEntering reset\nAfter reset\nCalling Cont(2)\nIn test X = 5; done\nCalling Cont(4)\nIn test X = 9; done\n"), Arguments.of("mib_voorbeelden.pl", "b\nf(b)\nf(g(a,a),h(c,d),i(e,f))\nf(g(a,a),h(c,c),i(e,f))\nf(g(a,a),h(c,c),i(e,e))\n") ) diff --git a/tests/parser/grammars/LogicGrammarTests.kt b/tests/parser/grammars/LogicGrammarTests.kt index f5cde74..5ca662a 100644 --- a/tests/parser/grammars/LogicGrammarTests.kt +++ b/tests/parser/grammars/LogicGrammarTests.kt @@ -126,10 +126,11 @@ class LogicGrammarTests { val rule = result[0] as Rule assertEquals(Functor.of("guest/2"), rule.head.functor, "Expected functor 'guest/2'") assertEquals(Functor.of(",/2"), (rule.body as CompoundTerm).functor, "Expected functor ',/2'") - val l1 = (rule.body as CompoundTerm).arguments[0] as CompoundTerm - assertEquals(Functor.of(",/2"), l1.functor, "Expected functor ',/2'") - val l2 = l1.arguments[0] as CompoundTerm - assertEquals(Functor.of("invited/2"), l2.functor, "Expected functor 'invited/2'") + val l0 = (rule.body as CompoundTerm) + val l1 = l0.arguments[0] as CompoundTerm + assertEquals(Functor.of("invited/2"), l1.functor, "Expected functor 'invited/2'") + val l2 = l0.arguments[1] as CompoundTerm + assertEquals(Functor.of(",/2"), l2.functor, "Expected functor ',/2'") } @Test diff --git a/tests/prolog/builtins/DelimitedContinuationsOperatorsTests.kt b/tests/prolog/builtins/DelimitedContinuationsOperatorsTests.kt new file mode 100644 index 0000000..994a992 --- /dev/null +++ b/tests/prolog/builtins/DelimitedContinuationsOperatorsTests.kt @@ -0,0 +1,75 @@ +package prolog.builtins + +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.Test +import prolog.ast.Database.Program +import prolog.ast.arithmetic.Integer +import prolog.ast.lists.List.Cons +import prolog.ast.lists.List.Empty +import prolog.ast.logic.Rule +import prolog.ast.terms.Atom +import prolog.ast.terms.Structure +import prolog.ast.terms.Variable +import java.io.ByteArrayOutputStream +import java.io.PrintStream + +class DelimitedContinuationsOperatorsTests { + @BeforeEach + fun setup() { + Program.reset() + } + + @Test + fun `example member`() { + val member = Member(Variable("X"), Cons(Integer(1), Cons(Integer(2), Cons(Integer(3), Empty)))) + val reset = Reset(member, Variable("Ball"), Variable("Cont")) + + val result = reset.satisfy(emptyMap()).toList() + + assertEquals(3, result.size, "Expected 3 results") + + assertTrue(result[0].isSuccess, "Expected success for first result") + val subs0 = result[0].getOrNull()!! + assertEquals(2, subs0.size, "Expected 2 substitutions for first result") + assertEquals(Integer(1), subs0[Variable("X")]) + assertEquals(Integer(0), subs0[Variable("Cont")]) + + assertTrue(result[1].isSuccess, "Expected success for second result") + val subs1 = result[1].getOrNull()!! + assertEquals(2, subs1.size, "Expected 2 substitutions for second result") + assertEquals(Integer(2), subs1[Variable("X")]) + assertEquals(Integer(0), subs1[Variable("Cont")]) + + assertTrue(result[2].isSuccess, "Expected success for third result") + val subs2 = result[2].getOrNull()!! + assertEquals(2, subs2.size, "Expected 2 substitutions for third result") + assertEquals(Integer(3), subs2[Variable("X")]) + assertEquals(Integer(0), subs2[Variable("Cont")]) + } + + @Test + fun `example with output`() { + val reset = Reset(Atom("test_"), Variable("Term"), Variable("Cont")) + val isOp = Is(Variable("X"), Add(Integer(1), Multiply(Integer(2), Variable("Y")))) + Program.load( + listOf( + Rule( + Structure(Atom("test"), listOf(Variable("Cont"), Variable("Term"))), + Conjunction(WriteLn("Inside test"), Conjunction(reset, WriteLn("After reset"))) + ), + Rule( + Atom("test_"), + Conjunction(WriteLn("Entering reset"), Conjunction(Shift(Variable("Y")), Conjunction(isOp, Conjunction(Write("In test X = "), Conjunction(Write(Variable("X")), WriteLn("; done")))))) + ) + ) + ) + + val notNot2 = Not(Not(Conjunction(WriteLn("calling Cont(2)"), Conjunction(Unify(Variable("Term"), Integer(2)), Call(Variable("Cont")))))) + val notNot4 = Not(Not(Conjunction(WriteLn("calling Cont(4)"), Conjunction(Unify(Variable("Term"), Integer(4)), Call(Variable("Cont")))))) + val query = Conjunction(Structure(Atom("test"), listOf(Variable("Cont"), Variable("Term"))), Conjunction(notNot2, notNot4)) + + val result = query.satisfy(emptyMap()).toList() + } +}