Compare commits
5 commits
9b454a9669
...
717e5e0954
Author | SHA1 | Date | |
---|---|---|---|
717e5e0954 | |||
2089e20da5 | |||
026218ddbd | |||
88c90220fe | |||
5bfeb96176 |
17 changed files with 415 additions and 83 deletions
22
examples/meta/continuations.pl
Normal file
22
examples/meta/continuations.pl
Normal file
|
@ -0,0 +1,22 @@
|
||||||
|
% Based on
|
||||||
|
% https://occasionallycogent.com/continuations_in_prolog/
|
||||||
|
|
||||||
|
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).
|
|
@ -3,6 +3,7 @@ package interpreter
|
||||||
import io.Logger
|
import io.Logger
|
||||||
import prolog.ast.arithmetic.Expression
|
import prolog.ast.arithmetic.Expression
|
||||||
import prolog.ast.arithmetic.Integer
|
import prolog.ast.arithmetic.Integer
|
||||||
|
import prolog.ast.lists.List as PList
|
||||||
import prolog.ast.logic.Clause
|
import prolog.ast.logic.Clause
|
||||||
import prolog.ast.logic.Fact
|
import prolog.ast.logic.Fact
|
||||||
import prolog.ast.logic.LogicOperand
|
import prolog.ast.logic.LogicOperand
|
||||||
|
@ -50,9 +51,9 @@ open class Preprocessor {
|
||||||
protected open fun preprocess(term: Term, nested: Boolean = false): Term {
|
protected open fun preprocess(term: Term, nested: Boolean = false): Term {
|
||||||
// TODO Remove hardcoding by storing the functors as constants in operators?
|
// TODO Remove hardcoding by storing the functors as constants in operators?
|
||||||
|
|
||||||
val prepped = when {
|
val prepped = when (term) {
|
||||||
term == Variable("_") -> AnonymousVariable.create()
|
Variable("_") -> AnonymousVariable.create()
|
||||||
term is Atom || term is Structure -> {
|
is Atom, is Structure -> {
|
||||||
// Preprocess the arguments first to recognize builtins
|
// Preprocess the arguments first to recognize builtins
|
||||||
val args = if (term is Structure) {
|
val args = if (term is Structure) {
|
||||||
term.arguments.map { preprocess(it, nested = true) }
|
term.arguments.map { preprocess(it, nested = true) }
|
||||||
|
@ -144,11 +145,23 @@ 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
|
// IO
|
||||||
Functor.of("write/1") -> Write(args[0])
|
Functor.of("write/1") -> Write(args[0])
|
||||||
Functor.of("nl/0") -> Nl
|
Functor.of("nl/0") -> Nl
|
||||||
|
Functor.of("writeln/1") -> WriteLn(args[0])
|
||||||
Functor.of("read/1") -> Read(args[0])
|
Functor.of("read/1") -> Read(args[0])
|
||||||
|
|
||||||
|
// Lists
|
||||||
|
Functor.of("member/2") -> Member(args[0], args[1] as PList)
|
||||||
|
|
||||||
|
// Meta
|
||||||
|
Functor.of("call/1") -> Call(args[0])
|
||||||
|
Functor.of("ignore/1") -> Ignore(args[0] as Goal)
|
||||||
|
|
||||||
// Other
|
// Other
|
||||||
Functor.of("initialization/1") -> Initialization(args[0] as Goal)
|
Functor.of("initialization/1") -> Initialization(args[0] as Goal)
|
||||||
Functor.of("forall/2") -> ForAll(args[0] as LogicOperand, args[1] as Goal)
|
Functor.of("forall/2") -> ForAll(args[0] as LogicOperand, args[1] as Goal)
|
||||||
|
|
|
@ -3,9 +3,10 @@ package parser.grammars
|
||||||
import com.github.h0tk3y.betterParse.combinators.*
|
import com.github.h0tk3y.betterParse.combinators.*
|
||||||
import com.github.h0tk3y.betterParse.grammar.parser
|
import com.github.h0tk3y.betterParse.grammar.parser
|
||||||
import com.github.h0tk3y.betterParse.parser.Parser
|
import com.github.h0tk3y.betterParse.parser.Parser
|
||||||
|
import com.github.h0tk3y.betterParse.utils.Tuple2
|
||||||
import prolog.ast.arithmetic.Float
|
import prolog.ast.arithmetic.Float
|
||||||
import prolog.ast.arithmetic.Integer
|
import prolog.ast.arithmetic.Integer
|
||||||
import prolog.ast.lists.List
|
import prolog.ast.lists.List as PList
|
||||||
import prolog.ast.terms.*
|
import prolog.ast.terms.*
|
||||||
import prolog.builtins.Dynamic
|
import prolog.builtins.Dynamic
|
||||||
import prolog.ast.lists.List.Empty
|
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))
|
if (t2 == null) t1 else CompoundTerm(Atom(t2!!.t1), listOf(t1, t2!!.t2))
|
||||||
}
|
}
|
||||||
|
|
||||||
|
protected val not: Parser<Term> by (notOp * parser(::term900)) use {
|
||||||
|
CompoundTerm(Atom(t1.text), listOf(t2))
|
||||||
|
}
|
||||||
|
protected val term900: Parser<Term> by (not or term700)
|
||||||
|
|
||||||
protected val op1000: Parser<String> by (comma) use { text }
|
protected val op1000: Parser<String> by (comma) use { text }
|
||||||
protected val term1000: Parser<Term> by (term700 * zeroOrMore(op1000 * term700)) use {
|
protected val term1000: Parser<Term> by (term900 * zeroOrMore(op1000 * term900)) use {
|
||||||
t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
|
constructRightAssociative(t1, t2)
|
||||||
}
|
}
|
||||||
|
|
||||||
protected val op1100: Parser<String> by (semicolon) use { text }
|
protected val op1100: Parser<String> by (semicolon) use { text }
|
||||||
protected val term1100: Parser<Term> by (term1000 * zeroOrMore(op1100 * term1000)) use {
|
protected val term1100: Parser<Term> 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<Term> by (dynamicOp * functor) use {
|
protected val dynamic: Parser<Term> by (dynamicOp * functor) use {
|
||||||
|
@ -117,12 +123,12 @@ open class TermsGrammar : Tokens() {
|
||||||
}
|
}
|
||||||
|
|
||||||
// Lists
|
// Lists
|
||||||
protected val list: Parser<List> by (-leftBracket * separated(
|
protected val list: Parser<PList> by (-leftBracket * separated(
|
||||||
parser(::termNoConjunction),
|
parser(::termNoConjunction),
|
||||||
comma,
|
comma,
|
||||||
acceptZero = true
|
acceptZero = true
|
||||||
) * -rightBracket) use {
|
) * -rightBracket) use {
|
||||||
var list: List = Empty
|
var list: PList = Empty
|
||||||
// Construct the list in reverse order
|
// Construct the list in reverse order
|
||||||
for (term in this.terms.reversed()) {
|
for (term in this.terms.reversed()) {
|
||||||
list = Cons(term, list)
|
list = Cons(term, list)
|
||||||
|
@ -139,4 +145,12 @@ open class TermsGrammar : Tokens() {
|
||||||
protected val body: Parser<Body> by term use { this as Body }
|
protected val body: Parser<Body> by term use { this as Body }
|
||||||
|
|
||||||
override val rootParser: Parser<Any> by term
|
override val rootParser: Parser<Any> by term
|
||||||
|
|
||||||
|
fun constructRightAssociative(left: Term, pairs: List<Tuple2<String, Term>>): 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)))
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -21,6 +21,8 @@ abstract class Tokens : Grammar<Any>() {
|
||||||
protected val semicolon: Token by literalToken(";")
|
protected val semicolon: Token by literalToken(";")
|
||||||
// 1000
|
// 1000
|
||||||
protected val comma: Token by literalToken(",")
|
protected val comma: Token by literalToken(",")
|
||||||
|
// 900
|
||||||
|
protected val notOp: Token by literalToken("\\+")
|
||||||
// 700
|
// 700
|
||||||
protected val univOp: Token by literalToken("=..")
|
protected val univOp: Token by literalToken("=..")
|
||||||
protected val notEquivalent: Token by literalToken("\\==")
|
protected val notEquivalent: Token by literalToken("\\==")
|
||||||
|
|
|
@ -9,6 +9,7 @@ import prolog.ast.terms.Atom
|
||||||
import prolog.ast.terms.Body
|
import prolog.ast.terms.Body
|
||||||
import prolog.ast.terms.Goal
|
import prolog.ast.terms.Goal
|
||||||
import prolog.flags.AppliedCut
|
import prolog.flags.AppliedCut
|
||||||
|
import prolog.flags.AppliedShift
|
||||||
import prolog.logic.applySubstitution
|
import prolog.logic.applySubstitution
|
||||||
import prolog.logic.numbervars
|
import prolog.logic.numbervars
|
||||||
|
|
||||||
|
@ -17,7 +18,7 @@ import prolog.logic.numbervars
|
||||||
*/
|
*/
|
||||||
object Fail : Atom("fail"), Body {
|
object Fail : Atom("fail"), Body {
|
||||||
override fun satisfy(subs: Substitutions): Answers = emptySequence()
|
override fun satisfy(subs: Substitutions): Answers = emptySequence()
|
||||||
override fun applySubstitution(subs: Substitutions): Fail = Fail
|
override fun applySubstitution(subs: Substitutions): Fail = this
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
@ -30,7 +31,7 @@ typealias False = Fail
|
||||||
*/
|
*/
|
||||||
object True : Atom("true"), Body {
|
object True : Atom("true"), Body {
|
||||||
override fun satisfy(subs: Substitutions): Answers = sequenceOf(Result.success(emptyMap()))
|
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
|
// TODO Repeat/0
|
||||||
|
@ -40,35 +41,28 @@ class Cut() : Atom("!") {
|
||||||
return sequenceOf(Result.failure(AppliedCut(emptyMap())))
|
return sequenceOf(Result.failure(AppliedCut(emptyMap())))
|
||||||
}
|
}
|
||||||
|
|
||||||
override fun applySubstitution(subs: Substitutions): Cut = Cut()
|
override fun applySubstitution(subs: Substitutions): Cut = this
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Conjunction (and). True if both Goal1 and Goal2 are true.
|
* 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) {
|
LogicOperator(Atom(","), left, right) {
|
||||||
override fun satisfy(subs: Substitutions): Answers = sequence {
|
override fun satisfy(subs: Substitutions): Answers = sequence {
|
||||||
// Satisfy the left part first, which either succeeds or fails
|
fun satisfyRight(leftSubs: Substitutions): Answers = sequence {
|
||||||
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.satisfy(subs + leftSubs).forEach { right ->
|
||||||
right.fold(
|
right.fold(
|
||||||
// If the right part succeeds, yield the result with the left substitutions
|
// If the right part succeeds, yield the result with the left substitutions
|
||||||
onSuccess = { rightSubs ->
|
onSuccess = { rightSubs ->
|
||||||
yield(Result.success(leftSubs + rightSubs))
|
yield(Result.success(leftSubs + rightSubs))
|
||||||
},
|
},
|
||||||
// If the right part fails, check if it's a cut
|
|
||||||
onFailure = { exception ->
|
onFailure = { exception ->
|
||||||
|
// If the right part fails, check if it's a cut
|
||||||
if (exception is AppliedCut) {
|
if (exception is AppliedCut) {
|
||||||
if (exception.subs != null) {
|
|
||||||
// If it's a cut, yield the result with the left substitutions
|
// If it's a cut, yield the result with the left substitutions
|
||||||
yield(Result.failure(AppliedCut(leftSubs + exception.subs)))
|
val newSubs = if (exception.subs != null) leftSubs + exception.subs else null
|
||||||
} else {
|
yield(Result.failure(AppliedCut(newSubs)))
|
||||||
yield(Result.failure(AppliedCut()))
|
|
||||||
}
|
|
||||||
return@sequence
|
return@sequence
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -77,25 +71,42 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
|
||||||
}
|
}
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
},
|
}
|
||||||
|
|
||||||
|
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 -> yieldAll(satisfyRight(leftSubs)) },
|
||||||
// If it fails, check these conditions:
|
// If it fails, check these conditions:
|
||||||
onFailure = { exception ->
|
onFailure = { exception ->
|
||||||
|
when (exception) {
|
||||||
// 1. If the left part is a cut, satisfy the right part ONCE, and stop searching for more solutions
|
// 1. If the left part is a cut, satisfy the right part ONCE, and stop searching for more solutions
|
||||||
if (exception is AppliedCut) {
|
is AppliedCut -> yieldAll(findNextCutSolution(exception))
|
||||||
right.satisfy(subs + (exception.subs!!)).firstOrNull()?.fold(
|
|
||||||
onSuccess = {
|
// 2. If the left part is a shift, we need to check if the right part can be satisfied
|
||||||
// If the right part succeeds, yield the result with the left substitutions
|
is AppliedShift -> {
|
||||||
yield(Result.success(exception.subs + it))
|
if (exception.cont == null) {
|
||||||
return@sequence
|
// Pass the right of our disjunction as the continuation
|
||||||
},
|
val newShift = AppliedShift(exception.subs, exception.ball, right as Goal)
|
||||||
onFailure = {
|
yield(Result.failure(newShift))
|
||||||
// If the right part fails, yield the failure
|
|
||||||
yield(Result.failure(it))
|
|
||||||
}
|
|
||||||
) ?: yield(Result.failure(AppliedCut()))
|
|
||||||
} else {
|
} else {
|
||||||
// 2. Any other failure should be returned as is
|
// Satisfy the right part with the updated substitutions
|
||||||
yield(Result.failure(exception))
|
yieldAll(satisfyRight(exception.subs))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// 3. Any other failure should be returned as is
|
||||||
|
else -> yield(Result.failure(exception))
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
)
|
)
|
||||||
|
@ -114,7 +125,20 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
|
||||||
open class Disjunction(private val left: LogicOperand, private val right: LogicOperand) :
|
open class Disjunction(private val left: LogicOperand, private val right: LogicOperand) :
|
||||||
LogicOperator(Atom(";"), left, right) {
|
LogicOperator(Atom(";"), left, right) {
|
||||||
override fun satisfy(subs: Substitutions): Answers = sequence {
|
override fun satisfy(subs: Substitutions): Answers = sequence {
|
||||||
yieldAll(left.satisfy(subs))
|
left.satisfy(subs).forEach { left ->
|
||||||
|
left.fold(
|
||||||
|
onSuccess = { leftSubs ->
|
||||||
|
yield(Result.success(leftSubs))
|
||||||
|
},
|
||||||
|
onFailure = { failure ->
|
||||||
|
if (failure is AppliedCut) {
|
||||||
|
val leftSubs = failure.subs
|
||||||
|
yield(Result.failure(AppliedCut(leftSubs)))
|
||||||
|
return@sequence
|
||||||
|
}
|
||||||
|
}
|
||||||
|
)
|
||||||
|
}
|
||||||
yieldAll(right.satisfy(subs))
|
yieldAll(right.satisfy(subs))
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
75
src/prolog/builtins/delimitedContinuationsOperators.kt
Normal file
75
src/prolog/builtins/delimitedContinuationsOperators.kt
Normal file
|
@ -0,0 +1,75 @@
|
||||||
|
package prolog.builtins
|
||||||
|
|
||||||
|
import prolog.Answers
|
||||||
|
import prolog.Substitutions
|
||||||
|
import prolog.ast.arithmetic.Integer
|
||||||
|
import prolog.ast.terms.Atom
|
||||||
|
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
|
||||||
|
|
||||||
|
/**
|
||||||
|
* 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 ->
|
||||||
|
unifyLazy(cont, Integer(0), goalSubs).forEach { contResult ->
|
||||||
|
contResult.map { contSubs ->
|
||||||
|
yield(Result.success(goalSubs + contSubs))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
},
|
||||||
|
onFailure = { failure ->
|
||||||
|
// If at some point Goal calls shift(Term2), then its further execution is suspended.
|
||||||
|
if (failure is AppliedShift) {
|
||||||
|
require(failure.cont != null) { "Shift must have a continuation" }
|
||||||
|
// 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))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* 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 = sequence {
|
||||||
|
val shift = AppliedShift(
|
||||||
|
subs = subs,
|
||||||
|
ball = ball,
|
||||||
|
cont = null
|
||||||
|
)
|
||||||
|
yield(Result.failure(shift))
|
||||||
|
}
|
||||||
|
}
|
|
@ -17,6 +17,8 @@ import prolog.logic.unifyLazy
|
||||||
* Write [Term] to the current output, using brackets and operators where appropriate.
|
* Write [Term] to the current output, using brackets and operators where appropriate.
|
||||||
*/
|
*/
|
||||||
class Write(private val term: Term) : Operator(Atom("write"), null, term), Satisfiable {
|
class Write(private val term: Term) : Operator(Atom("write"), null, term), Satisfiable {
|
||||||
|
constructor(message: String) : this(Atom(message))
|
||||||
|
|
||||||
override fun satisfy(subs: Substitutions): Answers {
|
override fun satisfy(subs: Substitutions): Answers {
|
||||||
val t = applySubstitution(term, subs)
|
val t = applySubstitution(term, subs)
|
||||||
|
|
||||||
|
@ -45,6 +47,12 @@ object Nl : Atom("nl"), Satisfiable {
|
||||||
override fun applySubstitution(subs: Substitutions): Nl = this
|
override fun applySubstitution(subs: Substitutions): Nl = this
|
||||||
}
|
}
|
||||||
|
|
||||||
|
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)"
|
||||||
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Read the next Prolog term from the current input stream and unify it with [Term].
|
* Read the next Prolog term from the current input stream and unify it with [Term].
|
||||||
*
|
*
|
||||||
|
|
|
@ -8,20 +8,23 @@ import prolog.ast.lists.List.Empty
|
||||||
import prolog.ast.terms.Atom
|
import prolog.ast.terms.Atom
|
||||||
import prolog.ast.terms.Operator
|
import prolog.ast.terms.Operator
|
||||||
import prolog.ast.terms.Term
|
import prolog.ast.terms.Term
|
||||||
|
import prolog.logic.applySubstitution
|
||||||
|
|
||||||
class Member(private val element: Term, private val list: List) : Operator(Atom("member"), element, list) {
|
class Member(private val element: Term, private val list: List) : Operator(Atom("member"), element, list) {
|
||||||
private var solution: Operator = if (list is Empty) {
|
private var solution: Operator = when (list) {
|
||||||
Unify(element, list)
|
is Empty -> Disjunction(Fail, Fail)
|
||||||
} else if (list is Cons) {
|
is Cons -> Disjunction(
|
||||||
Disjunction(
|
|
||||||
Unify(element, list.head),
|
Unify(element, list.head),
|
||||||
Member(element, list.tail)
|
Member(element, list.tail)
|
||||||
)
|
)
|
||||||
} else {
|
|
||||||
throw IllegalArgumentException("Invalid list type: ${list::class.simpleName}")
|
|
||||||
}
|
}
|
||||||
|
|
||||||
override fun satisfy(subs: Substitutions): Answers = solution.satisfy(subs)
|
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"
|
override fun toString(): String = "$element ∈ $list"
|
||||||
}
|
}
|
||||||
|
|
44
src/prolog/builtins/metaOperators.kt
Normal file
44
src/prolog/builtins/metaOperators.kt
Normal file
|
@ -0,0 +1,44 @@
|
||||||
|
package prolog.builtins
|
||||||
|
|
||||||
|
import prolog.Answers
|
||||||
|
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: Term) : Operator(Atom("call"), null, goal) {
|
||||||
|
override fun satisfy(subs: Substitutions): Answers {
|
||||||
|
val appliedGoal = applySubstitution(goal, subs) as Goal
|
||||||
|
return appliedGoal.satisfy(subs)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Calls [Goal] once, but succeeds, regardless of whether Goal succeeded or not.
|
||||||
|
*/
|
||||||
|
class Ignore(goal: Goal) : Operator(Atom("ignore"), null, goal) {
|
||||||
|
private val disjunction = Disjunction(
|
||||||
|
Conjunction(Call(goal), Cut()),
|
||||||
|
True
|
||||||
|
)
|
||||||
|
|
||||||
|
override fun satisfy(subs: Substitutions): Answers = sequence {
|
||||||
|
disjunction.satisfy(subs).forEach { result ->
|
||||||
|
result.fold(
|
||||||
|
onSuccess = { newSubs ->
|
||||||
|
yield(Result.success(newSubs))
|
||||||
|
},
|
||||||
|
onFailure = { failure ->
|
||||||
|
if (failure is AppliedCut && failure.subs != null) {
|
||||||
|
yield(Result.success(failure.subs))
|
||||||
|
} else {
|
||||||
|
yield(Result.failure(failure))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
14
src/prolog/flags/AppliedShift.kt
Normal file
14
src/prolog/flags/AppliedShift.kt
Normal file
|
@ -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()
|
|
@ -7,12 +7,11 @@ import prolog.ast.arithmetic.Expression
|
||||||
import prolog.ast.arithmetic.Float
|
import prolog.ast.arithmetic.Float
|
||||||
import prolog.ast.arithmetic.Integer
|
import prolog.ast.arithmetic.Integer
|
||||||
import prolog.ast.arithmetic.Number
|
import prolog.ast.arithmetic.Number
|
||||||
import prolog.ast.lists.List
|
|
||||||
import prolog.ast.lists.List.Cons
|
import prolog.ast.lists.List.Cons
|
||||||
import prolog.ast.lists.List.Empty
|
import prolog.ast.lists.List.Empty
|
||||||
import prolog.ast.logic.Fact
|
import prolog.ast.logic.Fact
|
||||||
import prolog.ast.logic.LogicOperator
|
|
||||||
import prolog.ast.terms.*
|
import prolog.ast.terms.*
|
||||||
|
import prolog.ast.lists.List as PList
|
||||||
|
|
||||||
// Apply substitutions to a term
|
// Apply substitutions to a term
|
||||||
fun applySubstitution(term: Term, subs: Substitutions): Term = when {
|
fun applySubstitution(term: Term, subs: Substitutions): Term = when {
|
||||||
|
@ -29,16 +28,8 @@ fun applySubstitution(term: Term, subs: Substitutions): Term = when {
|
||||||
else -> term
|
else -> term
|
||||||
}
|
}
|
||||||
|
|
||||||
//TODO Combine with the other applySubstitution function
|
fun applySubstitution(expr: Expression, subs: Substitutions): Expression {
|
||||||
fun applySubstitution(expr: Expression, subs: Substitutions): Expression = when {
|
return applySubstitution(expr as Term, subs) as Expression
|
||||||
variable(expr, emptyMap()) -> applySubstitution(expr as Term, subs) as Expression
|
|
||||||
atomic(expr, subs) -> expr
|
|
||||||
expr is LogicOperator -> {
|
|
||||||
expr.arguments = expr.arguments.map { applySubstitution(it, subs) }
|
|
||||||
expr
|
|
||||||
}
|
|
||||||
|
|
||||||
else -> expr
|
|
||||||
}
|
}
|
||||||
|
|
||||||
// Check if a variable occurs in a term
|
// Check if a variable occurs in a term
|
||||||
|
@ -90,7 +81,7 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
t1 is List && t2 is List -> {
|
t1 is PList && t2 is PList -> {
|
||||||
if (equivalent(t1, t2, subs)) {
|
if (equivalent(t1, t2, subs)) {
|
||||||
yield(Result.success(emptyMap()))
|
yield(Result.success(emptyMap()))
|
||||||
} else if (t1.size == t2.size) {
|
} else if (t1.size == t2.size) {
|
||||||
|
@ -120,8 +111,8 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
|
||||||
}
|
}
|
||||||
|
|
||||||
private fun unifyArgs(
|
private fun unifyArgs(
|
||||||
args1: kotlin.collections.List<Argument>,
|
args1: List<Argument>,
|
||||||
args2: kotlin.collections.List<Argument>,
|
args2: List<Argument>,
|
||||||
subs: Substitutions
|
subs: Substitutions
|
||||||
): Answers = sequence {
|
): Answers = sequence {
|
||||||
// Using the current subs, unify the first argument of each list
|
// Using the current subs, unify the first argument of each list
|
||||||
|
@ -171,7 +162,7 @@ fun equivalent(term1: Term, term2: Term, subs: Substitutions): Boolean {
|
||||||
term1 is Variable && term2 is Variable -> term1 == term2
|
term1 is Variable && term2 is Variable -> term1 == term2
|
||||||
term1 is Variable -> term1 in subs && equivalent(subs[term1]!!, term2, subs)
|
term1 is Variable -> term1 in subs && equivalent(subs[term1]!!, term2, subs)
|
||||||
term2 is Variable -> term2 in subs && equivalent(subs[term2]!!, term1, subs)
|
term2 is Variable -> term2 in subs && equivalent(subs[term2]!!, term1, subs)
|
||||||
term1 is List && term2 is List -> {
|
term1 is PList && term2 is PList -> {
|
||||||
if (term1.isEmpty() && term2.isEmpty()) {
|
if (term1.isEmpty() && term2.isEmpty()) {
|
||||||
true
|
true
|
||||||
} else if (term1.isEmpty() || term2.isEmpty()) {
|
} else if (term1.isEmpty() || term2.isEmpty()) {
|
||||||
|
|
|
@ -6,6 +6,7 @@ import io.Terminal
|
||||||
import parser.ReplParser
|
import parser.ReplParser
|
||||||
import prolog.Answer
|
import prolog.Answer
|
||||||
import prolog.Answers
|
import prolog.Answers
|
||||||
|
import prolog.flags.AppliedCut
|
||||||
|
|
||||||
class Repl {
|
class Repl {
|
||||||
private val io = Terminal()
|
private val io = Terminal()
|
||||||
|
@ -101,8 +102,15 @@ class Repl {
|
||||||
}
|
}
|
||||||
return subs.entries.joinToString(",\n") { "${it.key} = ${it.value}" }
|
return subs.entries.joinToString(",\n") { "${it.key} = ${it.value}" }
|
||||||
},
|
},
|
||||||
onFailure = {
|
onFailure = { failure ->
|
||||||
return "ERROR: ${it.message}"
|
if (failure is AppliedCut) {
|
||||||
|
if (failure.subs != null) {
|
||||||
|
return prettyPrint(Result.success(failure.subs))
|
||||||
|
}
|
||||||
|
return "false."
|
||||||
|
}
|
||||||
|
|
||||||
|
return "ERROR: ${failure.message}"
|
||||||
}
|
}
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
3
src/tool/mapEach.kt
Normal file
3
src/tool/mapEach.kt
Normal file
|
@ -0,0 +1,3 @@
|
||||||
|
package tool
|
||||||
|
|
||||||
|
fun <T, R> Sequence<T>.mapEach(transform: (T) -> R): Sequence<R> = map(transform)
|
|
@ -27,7 +27,7 @@ class Examples {
|
||||||
|
|
||||||
@Test
|
@Test
|
||||||
fun debugHelper() {
|
fun debugHelper() {
|
||||||
loader.load("examples/basics/arithmetics.pl")
|
loader.load("examples/meta/continuations.pl")
|
||||||
}
|
}
|
||||||
|
|
||||||
@ParameterizedTest
|
@ParameterizedTest
|
||||||
|
@ -65,6 +65,7 @@ class Examples {
|
||||||
)
|
)
|
||||||
|
|
||||||
fun meta() = listOf(
|
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")
|
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")
|
||||||
)
|
)
|
||||||
|
|
||||||
|
|
|
@ -126,10 +126,11 @@ class LogicGrammarTests {
|
||||||
val rule = result[0] as Rule
|
val rule = result[0] as Rule
|
||||||
assertEquals(Functor.of("guest/2"), rule.head.functor, "Expected functor 'guest/2'")
|
assertEquals(Functor.of("guest/2"), rule.head.functor, "Expected functor 'guest/2'")
|
||||||
assertEquals(Functor.of(",/2"), (rule.body as CompoundTerm).functor, "Expected functor ',/2'")
|
assertEquals(Functor.of(",/2"), (rule.body as CompoundTerm).functor, "Expected functor ',/2'")
|
||||||
val l1 = (rule.body as CompoundTerm).arguments[0] as CompoundTerm
|
val l0 = (rule.body as CompoundTerm)
|
||||||
assertEquals(Functor.of(",/2"), l1.functor, "Expected functor ',/2'")
|
val l1 = l0.arguments[0] as CompoundTerm
|
||||||
val l2 = l1.arguments[0] as CompoundTerm
|
assertEquals(Functor.of("invited/2"), l1.functor, "Expected functor 'invited/2'")
|
||||||
assertEquals(Functor.of("invited/2"), l2.functor, "Expected functor 'invited/2'")
|
val l2 = l0.arguments[1] as CompoundTerm
|
||||||
|
assertEquals(Functor.of(",/2"), l2.functor, "Expected functor ',/2'")
|
||||||
}
|
}
|
||||||
|
|
||||||
@Test
|
@Test
|
||||||
|
|
|
@ -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()
|
||||||
|
}
|
||||||
|
}
|
34
tests/prolog/builtins/MetaOperatorsTests.kt
Normal file
34
tests/prolog/builtins/MetaOperatorsTests.kt
Normal file
|
@ -0,0 +1,34 @@
|
||||||
|
package prolog.builtins
|
||||||
|
|
||||||
|
import org.junit.jupiter.api.Assertions.assertEquals
|
||||||
|
import org.junit.jupiter.api.Assertions.assertTrue
|
||||||
|
import org.junit.jupiter.api.Test
|
||||||
|
import prolog.ast.arithmetic.Integer
|
||||||
|
import prolog.ast.lists.List.Cons
|
||||||
|
import prolog.ast.lists.List.Empty
|
||||||
|
import prolog.ast.terms.Variable
|
||||||
|
|
||||||
|
class MetaOperatorsTests {
|
||||||
|
@Test
|
||||||
|
fun `ignore of failing goal succeeds`() {
|
||||||
|
val goal = Member(Integer(4), Cons(Integer(1), Cons(Integer(2), Cons(Integer(3), Empty))))
|
||||||
|
|
||||||
|
val result = Ignore(goal).satisfy(emptyMap()).toList()
|
||||||
|
|
||||||
|
assertEquals(1, result.size, "Should return one result")
|
||||||
|
assertTrue(result[0].isSuccess, "Result should be successful")
|
||||||
|
assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitutions")
|
||||||
|
}
|
||||||
|
|
||||||
|
@Test
|
||||||
|
fun `ignore of succeeding goal returns first solution`() {
|
||||||
|
val goal = Member(Variable("X"), Cons(Integer(1), Cons(Integer(2), Cons(Integer(3), Empty))))
|
||||||
|
|
||||||
|
val result = Ignore(goal).satisfy(emptyMap()).toList()
|
||||||
|
|
||||||
|
assertEquals(1, result.size, "Should return one result")
|
||||||
|
assertTrue(result[0].isSuccess, "Result should be successful")
|
||||||
|
val subs = result[0].getOrNull()!!
|
||||||
|
assertEquals(Integer(1), subs[Variable("X")], "Expected first solution to be 1")
|
||||||
|
}
|
||||||
|
}
|
Reference in a new issue