Compare commits

..

No commits in common. "6b46965435a8b4aeb3ee7cce795dfe73216ad7e9" and "a85169dced2e2b57af5faf5c94395c9aabe7b32a" have entirely different histories.

25 changed files with 87 additions and 360 deletions

View file

@ -75,7 +75,6 @@ open class Preprocessor {
term.functor == ",/2" -> Conjunction(args[0] as LogicOperand, args[1] as LogicOperand)
term.functor == ";/2" -> Disjunction(args[0] as LogicOperand, args[1] as LogicOperand)
term.functor == "\\+/1" -> Not(args[0] as Goal)
term.functor == "\\==/2" -> NotEquivalent(args[0], args[1])
term.functor == "==/2" -> Equivalent(args[0], args[1])
term.functor == "=\\=/2" && args.all { it is Expression } -> EvaluatesToDifferent(args[0] as Expression, args[1] as Expression)
@ -91,12 +90,10 @@ open class Preprocessor {
term.functor == "*/2" && args.all { it is Expression } -> Multiply(args[0] as Expression, args[1] as Expression)
term.functor == "//2" && args.all { it is Expression } -> Divide(args[0] as Expression, args[1] as Expression)
term.functor == "between/3" && args.all { it is Expression } -> Between(args[0] as Expression, args[1] as Expression, args[2] as Expression)
term.functor == "succ/2" && args.all { it is Expression } -> Successor(args[0] as Expression, args[1] as Expression)
// Database
term.functor == "dynamic/1" -> Dynamic((args[0] as Atom).name)
term.functor == "retract/1" -> Retract(args[0])
term.functor == "retractall/1" -> RetractAll(args[0])
term.functor == "assert/1" -> {
if (args[0] is Rule) {
Assert(args[0] as Rule)
@ -141,4 +138,4 @@ open class Preprocessor {
return prepped
}
}
}

View file

@ -3,8 +3,7 @@ package io
interface IoHandler {
fun prompt(
message: String,
hint: () -> String = { "Please enter a valid input." },
check: (String) -> Boolean = { true }
hint: () -> String = { "Please enter a valid input." }
): String
fun say(message: String)

View file

@ -20,16 +20,15 @@ class Terminal(
override fun prompt(
message: String,
hint: () -> String,
check: (String) -> Boolean,
hint: () -> String
): String {
say("$message ")
var input: String = readLine().trim()
while (!check(input)) {
var input: String = readLine()
while (input.isBlank()) {
say(hint(), error)
input += readLine().trim()
input = readLine()
}
return input.trim()
return input
}
override fun say(message: String) {

View file

@ -87,7 +87,7 @@ open class TermsGrammar : Tokens() {
t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
}
protected val op700: Parser<String> by (equivalent or notEquivalent or equals or notEquals or isOp) use { text }
protected val op700: Parser<String> by (equivalent or equals or notEquals or isOp) use { text }
protected val term700: Parser<Term> by (term500 * optional(op700 * term500)) use {
if (t2 == null) t1 else CompoundTerm(Atom(t2!!.t1), listOf(t1, t2!!.t2))
}

View file

@ -20,7 +20,6 @@ abstract class Tokens : Grammar<Any>() {
// 1000
protected val comma: Token by literalToken(",")
// 700
protected val notEquivalent: Token by literalToken("\\==")
protected val equivalent: Token by literalToken("==")
protected val equals: Token by literalToken("=")
protected val isOp: Token by literalToken("is")

View file

@ -32,8 +32,6 @@ class Float(override val value: kotlin.Float): Number {
else -> throw IllegalArgumentException("Cannot multiply $this and $other")
}
override fun applySubstitution(subs: Substitutions): Float = this
override fun equals(other: Any?): Boolean {
if (this === other) return true
if (other !is Float) return false

View file

@ -33,7 +33,6 @@ data class Integer(override val value: Int) : Number, LogicOperand() {
Float(value / other.value.toFloat())
}
}
else -> throw IllegalArgumentException("Cannot divide $this and $other")
}
@ -42,6 +41,4 @@ data class Integer(override val value: Int) : Number, LogicOperand() {
is Integer -> Integer(value * other.value)
else -> throw IllegalArgumentException("Cannot multiply $this and $other")
}
override fun applySubstitution(subs: Substitutions): Integer = this
}

View file

@ -27,23 +27,27 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
// Only if the body can be proven, the substitutions should be returned.
// Do this in a lazy way.
val (headEnd, headRenaming) = numbervars(head, Program.variableRenamingStart, subs)
Program.variableRenamingStart = headEnd
// Since we are only interested in substitutions in the goal (as opposed to the head of this clause),
// we can use variable renaming and filter out the substitutions that are not in the goal.
val (end, renamed: Substitutions) = numbervars(head, Program.variableRenamingStart, subs)
val renamedHead = applySubstitution(head, subs + headRenaming)
val renamedBody = applySubstitution(body, subs + headRenaming) as Body
val reverse = renamed.entries.associate { (a, b) -> b to a }
Program.variableRenamingStart = end
unifyLazy(goal, renamedHead, subs).forEach { headAnswer ->
var newSubs: Substitutions = subs + renamed
unifyLazy(applySubstitution(goal, subs), head, newSubs).forEach { headAnswer ->
headAnswer.map { headSubs ->
val subsNotInGoal = headSubs.filterNot { occurs(it.key as Variable, goal, emptyMap()) }
renamedBody.satisfy(subsNotInGoal).forEach { bodyAnswer ->
// If the body can be proven, yield the (combined) substitutions
newSubs = subs + renamed + headSubs
body.satisfy(newSubs).forEach { bodyAnswer ->
bodyAnswer.fold(
// If the body can be proven, yield the (combined) substitutions
onSuccess = { bodySubs ->
var result = headSubs + bodySubs
result = result
.mapValues { applySubstitution(it.value, result) }
.filterKeys { it !is AnonymousVariable && occurs(it as Variable, goal, emptyMap()) }
var result = (headSubs + bodySubs)
.mapKeys { applySubstitution(it.key, reverse)}
.mapValues { applySubstitution(it.value, reverse) }
result = result.map { it.key to applySubstitution(it.value, result) }
.toMap()
.filterNot { it.key in renamed.keys && !occurs(it.key as Variable, goal, emptyMap())}
yield(Result.success(result))
},
onFailure = { error ->
@ -77,5 +81,7 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
return true
}
override fun hashCode(): Int = super.hashCode()
override fun hashCode(): Int {
return super.hashCode()
}
}

View file

@ -1,10 +1,6 @@
package prolog.ast.logic
import prolog.Substitutions
import prolog.ast.terms.Head
import prolog.builtins.True
import prolog.logic.applySubstitution
class Fact(head: Head) : Clause(head, True) {
override fun applySubstitution(subs: Substitutions): Fact = Fact(applySubstitution(head, subs) as Head)
}
class Fact(head: Head) : Clause(head, True)

View file

@ -1,13 +1,6 @@
package prolog.ast.logic
import prolog.Substitutions
import prolog.ast.terms.Body
import prolog.ast.terms.Head
import prolog.logic.applySubstitution
class Rule(head: Head, body: Body) : Clause(head, body) {
override fun applySubstitution(subs: Substitutions): Rule = Rule(
head = applySubstitution(head, subs) as Head,
body = applySubstitution(body, subs) as Body
)
}
class Rule(head: Head, body: Body) : Clause(head, body)

View file

@ -1,9 +1,8 @@
package prolog.ast.terms
import io.Logger
import prolog.Substitutions
class AnonymousVariable(private val id: Int) : Variable("_$id") {
class AnonymousVariable(id: Int) : Variable("_$id") {
companion object {
private var counter = 0
fun create(): AnonymousVariable {
@ -14,7 +13,5 @@ class AnonymousVariable(private val id: Int) : Variable("_$id") {
}
}
override fun applySubstitution(subs: Substitutions): AnonymousVariable = this
override fun toString(): String = "_"
}

View file

@ -10,8 +10,6 @@ open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
override fun solve(goal: Goal, subs: Substitutions): Answers = unifyLazy(goal, this, subs)
override fun applySubstitution(subs: Substitutions): Atom = Atom(name)
override fun toString(): String {
return name
}

View file

@ -2,4 +2,4 @@ package prolog.ast.terms
import prolog.ast.logic.Satisfiable
interface Body : Term, Satisfiable
interface Body : Satisfiable

View file

@ -3,7 +3,6 @@ package prolog.ast.terms
import prolog.Answers
import prolog.Substitutions
import prolog.ast.logic.Resolvent
import prolog.logic.applySubstitution
import prolog.logic.unifyLazy
typealias Argument = Term
@ -24,11 +23,6 @@ open class Structure(val name: Atom, var arguments: List<Argument>) : Goal(), He
}
}
override fun applySubstitution(subs: Substitutions): Structure = Structure(
name,
arguments.map { applySubstitution(it, subs) }
)
override fun equals(other: Any?): Boolean {
if (this === other) return true
if (other !is Structure) return false

View file

@ -1,18 +1,14 @@
package prolog.ast.terms
import prolog.Substitutions
import prolog.ast.arithmetic.Float
import prolog.ast.arithmetic.Integer
import prolog.logic.compare
/**
* Value in Prolog.
*
* A [Term] is either a [Variable], [Atom], [Integer],
* [Float] or [CompoundTerm].
* A [Term] is either a [Variable], [Atom], [Integer][prolog.ast.arithmetic.Integer],
* [Float][prolog.ast.arithmetic.Float] or [CompoundTerm].
* In addition, SWI-Prolog also defines the type TODO string.
*/
interface Term : Comparable<Term> {
override fun compareTo(other: Term): Int = compare(this, other, emptyMap())
fun applySubstitution(subs: Substitutions): Term
}

View file

@ -34,8 +34,6 @@ open class Variable(val name: String) : Term, Body, Expression, LogicOperand() {
return name == other.name
}
override fun applySubstitution(subs: Substitutions): Variable = this
override fun hashCode(): Int {
return name.hashCode()
}

View file

@ -39,10 +39,6 @@ class EvaluatesToDifferent(private val left: Expression, private val right: Expr
}
}
override fun applySubstitution(subs: Substitutions): EvaluatesToDifferent = EvaluatesToDifferent(
left.applySubstitution(subs) as Expression,
right.applySubstitution(subs) as Expression
)
}
/**
@ -61,11 +57,6 @@ class EvaluatesTo(private val left: Expression, private val right: Expression) :
return if (equivalent(t1.to, t2.to, subs)) sequenceOf(Result.success(emptyMap())) else emptySequence()
}
override fun applySubstitution(subs: Substitutions): EvaluatesTo = EvaluatesTo(
left.applySubstitution(subs) as Expression,
right.applySubstitution(subs) as Expression
)
}
/**
@ -87,11 +78,6 @@ class Is(val number: Expression, val expr: Expression) :
return unifyLazy(t1.to, t2.to, subs)
}
override fun applySubstitution(subs: Substitutions): Is = Is(
number.applySubstitution(subs) as Expression,
expr.applySubstitution(subs) as Expression
)
}
/**
@ -115,11 +101,6 @@ open class Add(private val expr1: Expression, private val expr2: Expression) :
val simplification = result.simplify(map.first().getOrThrow())
return Simplification(this, simplification.to)
}
override fun applySubstitution(subs: Substitutions): Add = Add(
expr1.applySubstitution(subs) as Expression,
expr2.applySubstitution(subs) as Expression
)
}
/**
@ -133,11 +114,6 @@ open class Subtract(private val expr1: Expression, private val expr2: Expression
val simplification = result.simplify(map.first().getOrThrow())
return Simplification(this, simplification.to)
}
override fun applySubstitution(subs: Substitutions): Subtract = Subtract(
expr1.applySubstitution(subs) as Expression,
expr2.applySubstitution(subs) as Expression
)
}
/**
@ -151,11 +127,6 @@ class Multiply(val expr1: Expression, val expr2: Expression) :
val simplification = result.simplify(map.first().getOrThrow())
return Simplification(this, simplification.to)
}
override fun applySubstitution(subs: Substitutions): Multiply = Multiply(
expr1.applySubstitution(subs) as Expression,
expr2.applySubstitution(subs) as Expression
)
}
class Divide(private val expr1: Expression, private val expr2: Expression) :
@ -166,11 +137,6 @@ class Divide(private val expr1: Expression, private val expr2: Expression) :
val simplification = result.simplify(map.first().getOrThrow())
return Simplification(this, simplification.to)
}
override fun applySubstitution(subs: Substitutions): Divide = Divide(
expr1.applySubstitution(subs) as Expression,
expr2.applySubstitution(subs) as Expression
)
}
// TODO Expr mod Expr
@ -200,16 +166,5 @@ class Between(private val expr1: Expression, private val expr2: Expression, priv
}
}
override fun applySubstitution(subs: Substitutions): Between = Between(
expr1.applySubstitution(subs) as Expression,
expr2.applySubstitution(subs) as Expression,
expr3.applySubstitution(subs) as Expression
)
override fun toString(): String = "$expr1..$expr3..$expr2"
}
class Successor(private val expr1: Expression, private val expr2: Expression) :
CompoundTerm(Atom("succ"), listOf(expr1, expr2)), Satisfiable {
override fun satisfy(subs: Substitutions): Answers = succ(expr1, expr2, subs)
}

View file

@ -7,16 +7,13 @@ import prolog.ast.logic.LogicOperator
import prolog.ast.terms.Atom
import prolog.ast.terms.Body
import prolog.ast.terms.Goal
import prolog.ast.terms.Structure
import prolog.flags.AppliedCut
import prolog.logic.applySubstitution
/**
* Always fail.
*/
object Fail : Atom("fail"), Body {
override fun satisfy(subs: Substitutions): Answers = emptySequence()
override fun applySubstitution(subs: Substitutions): Fail = Fail
}
/**
@ -29,7 +26,6 @@ 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
}
// TODO Repeat/0
@ -38,8 +34,6 @@ class Cut() : Atom("!") {
override fun satisfy(subs: Substitutions): Answers {
return sequenceOf(Result.failure(AppliedCut(emptyMap())))
}
override fun applySubstitution(subs: Substitutions): Cut = Cut()
}
/**
@ -100,11 +94,6 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
)
}
}
override fun applySubstitution(subs: Substitutions): Conjunction = Conjunction(
applySubstitution(left, subs) as LogicOperand,
applySubstitution(right, subs) as LogicOperand
)
}
/**
@ -116,11 +105,6 @@ open class Disjunction(private val left: LogicOperand, private val right: LogicO
yieldAll(left.satisfy(subs))
yieldAll(right.satisfy(subs))
}
override fun applySubstitution(subs: Substitutions): Disjunction = Disjunction(
applySubstitution(left, subs) as LogicOperand,
applySubstitution(right, subs) as LogicOperand
)
}
@Deprecated("Use Disjunction instead")
@ -143,6 +127,4 @@ class Not(private val goal: Goal) : LogicOperator(Atom("\\+"), rightOperand = go
// If the goal cannot be proven, return a sequence with an empty map
return sequenceOf(Result.success(emptyMap()))
}
override fun applySubstitution(subs: Substitutions): Not = Not(applySubstitution(goal, subs) as Goal)
}

View file

@ -1,6 +1,5 @@
package prolog.builtins
import io.Logger
import prolog.Answers
import prolog.Substitutions
import prolog.ast.logic.Clause
@ -43,8 +42,6 @@ class Dynamic(private val dynamicFunctor: Functor): Goal(), Body {
}
override fun hashCode(): Int = super.hashCode()
override fun applySubstitution(subs: Substitutions): Dynamic = Dynamic(dynamicFunctor)
}
class Assert(clause: Clause) : AssertZ(clause) {
@ -62,8 +59,6 @@ class AssertA(val clause: Clause) : Operator(Atom("asserta"), null, clause) {
return sequenceOf(Result.success(emptyMap()))
}
override fun applySubstitution(subs: Substitutions): AssertA = AssertA(applySubstitution(clause, subs) as Clause)
}
/**
@ -77,8 +72,6 @@ open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause)
return sequenceOf(Result.success(emptyMap()))
}
override fun applySubstitution(subs: Substitutions): AssertZ = AssertZ(applySubstitution(clause, subs) as Clause)
}
/**
@ -87,7 +80,7 @@ open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause)
*
* @see [SWI-Prolog Predicate retract/1](https://www.swi-prolog.org/pldoc/doc_for?object=retract/1)
*/
open class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
override fun satisfy(subs: Substitutions): Answers = sequence {
// Check that term is a structure or atom
if (term !is Structure && term !is Atom) {
@ -102,12 +95,6 @@ open class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
return@sequence
}
// Check if the predicate is dynamic
if (!predicate.dynamic) {
yield(Result.failure(Exception("No permission to modify static procedure '$functorName'")))
return@sequence
}
predicate.clauses.toList().forEach { clause ->
unifyLazy(term, clause.head, subs).forEach { unifyResult ->
unifyResult.fold(
@ -123,32 +110,4 @@ open class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
}
}
}
override fun applySubstitution(subs: Substitutions): Retract = Retract(applySubstitution(term, subs))
}
class RetractAll(term: Term) : Retract(term) {
override fun satisfy(subs: Substitutions): Answers {
// Check that term is a structure or atom
if (term !is Structure && term !is Atom) {
return sequenceOf(Result.failure(Exception("Cannot retract a non-structure or non-atom")))
}
// If the predicate does not exist, implicitly create it
val functor = term.functor
val predicate = Program.db.predicates[functor]
if (predicate == null) {
Logger.debug("Predicate $functor not found, creating it")
Program.db.predicates += functor to Predicate(functor, dynamic = true)
}
// Propagate errors from the super class
super.satisfy(subs).forEach {
if (it.isFailure) {
return sequenceOf(it)
}
}
return sequenceOf(Result.success(emptyMap()))
}
}

View file

@ -27,8 +27,6 @@ class Write(private val term: Term) : Operator(Atom("write"), null, term), Satis
return sequenceOf(Result.success(emptyMap()))
}
override fun applySubstitution(subs: Substitutions): Write = Write(applySubstitution(term, subs))
override fun toString(): String = "write($term)"
}
@ -41,8 +39,6 @@ object Nl : Atom("nl"), Satisfiable {
Program.storeNewLine = false
return sequenceOf(Result.success(emptyMap()))
}
override fun applySubstitution(subs: Substitutions): Nl = this
}
/**
@ -76,6 +72,4 @@ class Read(private val term: Term) : Operator(Atom("read"), null, term), Satisfi
yieldAll(unifyLazy(t1, t2, subs))
}
override fun applySubstitution(subs: Substitutions): Read = Read(applySubstitution(term, subs))
}

View file

@ -24,20 +24,11 @@ class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="
yieldAll(unifyLazy(t1, t2, subs))
}
override fun applySubstitution(subs: Substitutions): Unify = Unify(
applySubstitution(term1, subs),
applySubstitution(term2, subs)
)
}
class NotUnify(private val term1: Term, private val term2: Term) : Operator(Atom("\\="), term1, term2) {
class NotUnify(term1: Term, term2: Term) : Operator(Atom("\\="), term1, term2) {
private val not = Not(Unify(term1, term2))
override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs)
override fun applySubstitution(subs: Substitutions): NotUnify = NotUnify(
applySubstitution(term1, subs),
applySubstitution(term2, subs)
)
}
class Equivalent(private val term1: Term, private val term2: Term) : Operator(Atom("=="), term1, term2) {
@ -49,18 +40,4 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator(At
yield(Result.success(emptyMap()))
}
}
override fun applySubstitution(subs: Substitutions): Equivalent = Equivalent(
applySubstitution(term1, subs),
applySubstitution(term2, subs)
)
}
class NotEquivalent(private val term1: Term, private val term2: Term) : Operator(Atom("\\=="), term1, term2) {
private val not = Not(Equivalent(term1, term2))
override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs)
override fun applySubstitution(subs: Substitutions): NotEquivalent = NotEquivalent(
applySubstitution(term1, subs),
applySubstitution(term2, subs)
)
}

View file

@ -15,15 +15,19 @@ import prolog.ast.terms.*
// Apply substitutions to a term
fun applySubstitution(term: Term, subs: Substitutions): Term = when {
term is Fact -> term.applySubstitution(subs)
term is Fact -> {
Fact(applySubstitution(term.head, subs) as Head)
}
variable(term, emptyMap()) -> {
val variable = term as Variable
subs[variable]?.let { applySubstitution(term = it, subs = subs) } ?: term
}
atomic(term, subs) -> term
compound(term, subs) -> term.applySubstitution(subs)
compound(term, subs) -> {
val structure = term as Structure
Structure(structure.name, structure.arguments.map { applySubstitution(it, subs) })
}
else -> term
}

View file

@ -29,45 +29,40 @@ class Repl {
}
private fun query(): Answers {
val queryString = io.prompt("?-", { "| " }, { it.endsWith(".") })
val queryString = io.prompt("?-", { "| " })
val simpleQuery = parser.parse(queryString)
val query = preprocessor.preprocess(simpleQuery)
return query.satisfy(emptyMap())
}
private fun printAnswers(answers: Answers) {
val knownCommands = setOf(";", "a", ".", "h")
val iterator = answers.iterator()
if (!iterator.hasNext()) {
io.say("false.\n")
return
}
} else {
io.say(prettyPrint(iterator.next()))
io.say(prettyPrint(iterator.next()))
while (iterator.hasNext()) {
var command = io.prompt("")
while (true) {
when (io.prompt("")) {
";" -> {
try {
while (command !in knownCommands) {
io.say("Unknown action: $command (h for help)\n")
command = io.prompt("Action?")
}
when (command) {
";" -> {
io.say(prettyPrint(iterator.next()))
} catch (_: NoSuchElementException) {
break
}
}
"a" -> return
"." -> {
io.checkNewLine()
return
}
"h" -> {
help()
io.say("Action?")
}
else -> {
io.say("Unknown action: (h for help)\n")
io.say("Action?")
"a" -> return
"." -> return
"h" -> {
help()
io.say("Action?")
}
}
}
}
@ -95,7 +90,9 @@ class Repl {
return subs.entries.joinToString(",\n") { "${it.key} = ${it.value}" }
},
onFailure = {
return "ERROR: ${it.message}"
val text = "Failure: ${it.message}"
Logger.warn(text)
return text
}
)
}

View file

@ -14,8 +14,6 @@ import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Variable
import prolog.ast.Database.Program
import prolog.ast.arithmetic.Integer
import prolog.ast.terms.AnonymousVariable
class EvaluationTests {
@BeforeEach
@ -110,8 +108,8 @@ class EvaluationTests {
val variable2 = Variable("Y")
val parent = Rule(
Structure(Atom("parent"), listOf(variable1, variable2)), /* :- */
Disjunction(
Structure(Atom("parent"), listOf(variable1, variable2)),
/* :- */ Disjunction(
Structure(Atom("father"), listOf(variable1, variable2)),
/* ; */
Structure(Atom("mother"), listOf(variable1, variable2))
@ -120,14 +118,10 @@ class EvaluationTests {
Program.load(listOf(father, mother, parent))
val result1 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy")))).toList()
assertEquals(1, result1.size, "Expected 1 result")
assertTrue(result1[0].isSuccess, "Expected success")
assertTrue(result1[0].getOrNull()!!.isEmpty(), "Expected no substitutions")
val result2 = Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy")))).toList()
assertEquals(1, result2.size, "Expected 1 result")
assertTrue(result2[0].isSuccess, "Expected success")
assertTrue(result2[0].getOrNull()!!.isEmpty(), "Expected no substitutions")
val result1 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy"))))
assertTrue(result1.toList().isNotEmpty())
val result2 = Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy"))))
assertTrue(result2.toList().isNotEmpty())
val result3 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jane"))))
assertFalse(result3.any())
@ -420,63 +414,4 @@ class EvaluationTests {
assertEquals(Atom("bob"), subs5[Variable("Person")], "Expected bob")
}
}
@Test
fun `leq Peano`() {
val fact = Fact(Structure(Atom("leq"), listOf(Integer(0), AnonymousVariable.create())))
val rule = Rule(
Structure(
Atom("leq"),
listOf(Structure(Atom("s"), listOf(Variable("X"))), Structure(Atom("s"), listOf(Variable("Y"))))
),
Structure(Atom("leq"), listOf(Variable("X"), Variable("Y"))),
)
Program.db.load(listOf(fact, rule))
val result1 = Program.query(Structure(Atom("leq"), listOf(Variable("X"), Integer(0)))).toList()
assertEquals(1, result1.size, "Expected 1 result")
assertTrue(result1[0].isSuccess, "Expected success")
val subs = result1[0].getOrNull()!!
assertEquals(1, subs.size, "Expected 1 substitution")
assertEquals(Integer(0), subs[Variable("X")], "Expected X to be 0")
val result2 =
Program.query(Structure(Atom("leq"), listOf(Variable("X"), Structure(Atom("s"), listOf(Integer(0))))))
.toList()
assertEquals(2, result2.size, "Expected 2 results")
assertTrue(result2[0].isSuccess, "Expected success")
val subs2a = result2[0].getOrNull()!!
assertEquals(1, subs2a.size, "Expected 1 substitution")
assertEquals(Integer(0), subs2a[Variable("X")], "Expected X to be 0")
assertTrue(result2[1].isSuccess, "Expected success")
val subs2b = result2[1].getOrNull()!!
assertEquals(1, subs2b.size, "Expected 1 substitution")
assertEquals(Structure(Atom("s"), listOf(Integer(0))), subs2b[Variable("X")], "Expected X to be s(0)")
val result3 = Program.query(
Structure(
Atom("leq"),
listOf(Variable("X"), Structure(Atom("s"), listOf(Structure(Atom("s"), listOf(Integer(0))))))
)
).toList()
assertEquals(3, result3.size, "Expected 3 results")
assertTrue(result3[0].isSuccess, "Expected success")
val subs3a = result3[0].getOrNull()!!
assertEquals(1, subs3a.size, "Expected 1 substitution")
assertEquals(Integer(0), subs3a[Variable("X")], "Expected X to be 0")
assertTrue(result3[1].isSuccess, "Expected success")
val subs3b = result3[1].getOrNull()!!
assertEquals(1, subs3b.size, "Expected 1 substitution")
assertEquals(Structure(Atom("s"), listOf(Integer(0))), subs3b[Variable("X")], "Expected X to be s(0)")
assertTrue(result3[2].isSuccess, "Expected success")
val subs3c = result3[2].getOrNull()!!
assertEquals(1, subs3c.size, "Expected 1 substitution")
assertEquals(Structure(Atom("s"), listOf(Structure(Atom("s"), listOf(Integer(0))))), subs3c[Variable("X")], "Expected X to be s(s(0))")
}
}

View file

@ -15,7 +15,6 @@ import prolog.ast.logic.Fact
import prolog.ast.logic.Predicate
import prolog.ast.logic.Rule
import prolog.ast.terms.Atom
import prolog.ast.terms.Functor
import prolog.ast.terms.Structure
import prolog.ast.terms.Variable
@ -132,7 +131,7 @@ class DatabaseOperatorsTests {
@Test
fun `simple retract`() {
val predicate = Predicate(listOf(Fact(Atom("a"))), dynamic = true)
val predicate = Predicate(listOf(Fact(Atom("a"))))
Program.db.load(predicate)
assertEquals(1, Program.query(Atom("a")).count())
@ -147,13 +146,11 @@ class DatabaseOperatorsTests {
@Test
fun `retract atom`() {
val predicate = Predicate(
listOf(
Fact(Atom("a")),
Fact(Atom("a")),
Fact(Atom("a"))
), dynamic = true
)
val predicate = Predicate(listOf(
Fact(Atom("a")),
Fact(Atom("a")),
Fact(Atom("a"))
))
Program.db.load(predicate)
val control = Program.query(Atom("a")).toList()
@ -173,9 +170,11 @@ class DatabaseOperatorsTests {
assertTrue(answer.isSuccess, "Expected success")
assertTrue(answer.getOrNull()!!.isEmpty(), "Expected no substitutions")
assertTrue(result.hasNext(), "Expected more results")
assertEquals(2, predicate.clauses.size, "Expected 2 clauses")
assertTrue(result.next().isSuccess)
assertTrue(result.hasNext(), "Expected more results")
assertTrue(result.next().isSuccess)
assertFalse(result.hasNext(), "Expected more results")
@ -184,13 +183,11 @@ class DatabaseOperatorsTests {
@Test
fun `retract compound with variable`() {
val predicate = Predicate(
listOf(
Fact(Structure(Atom("a"), listOf(Atom("b")))),
Fact(Structure(Atom("a"), listOf(Atom("c")))),
Fact(Structure(Atom("a"), listOf(Atom("d"))))
), dynamic = true
)
val predicate = Predicate(listOf(
Fact(Structure(Atom("a"), listOf(Atom("b")))),
Fact(Structure(Atom("a"), listOf(Atom("c")))),
Fact(Structure(Atom("a"), listOf(Atom("d"))))
))
Program.db.load(predicate)
val control = Program.query(Structure(Atom("a"), listOf(Variable("X")))).toList()
@ -211,6 +208,7 @@ class DatabaseOperatorsTests {
assertTrue(subs.isNotEmpty(), "Expected substitutions")
assertTrue(Variable("X") in subs, "Expected variable X")
assertEquals(Atom("b"), subs[Variable("X")], "Expected b")
assertTrue(result.hasNext(), "Expected more results")
assertEquals(2, predicate.clauses.size, "Expected 2 clauses")
answer = result.next()
@ -220,6 +218,7 @@ class DatabaseOperatorsTests {
assertTrue(subs.isNotEmpty(), "Expected substitutions")
assertTrue(Variable("X") in subs, "Expected variable X")
assertEquals(Atom("c"), subs[Variable("X")], "Expected c")
assertTrue(result.hasNext(), "Expected more results")
assertEquals(1, predicate.clauses.size, "Expected 1 clause")
answer = result.next()
@ -229,9 +228,8 @@ class DatabaseOperatorsTests {
assertTrue(subs.isNotEmpty(), "Expected substitutions")
assertTrue(Variable("X") in subs, "Expected variable X")
assertEquals(Atom("d"), subs[Variable("X")], "Expected d")
assertEquals(0, predicate.clauses.size, "Expected no clauses")
assertFalse(result.hasNext(), "Expected no more results")
assertEquals(0, predicate.clauses.size, "Expected no clauses")
}
@Test
@ -294,45 +292,4 @@ class DatabaseOperatorsTests {
assertEquals(Atom("bob"), result2[Variable("X")], "Expected bob")
assertEquals(Atom("sushi"), result2[Variable("Y")], "Expected sushi")
}
@Test
fun `retract all`() {
val predicate = Predicate(
listOf(
Fact(Structure(Atom("a"), listOf(Atom("b")))),
Fact(Structure(Atom("a"), listOf(Atom("c")))),
Fact(Structure(Atom("a"), listOf(Atom("d"))))
), dynamic = true
)
Program.db.load(predicate)
val control = Program.query(Structure(Atom("a"), listOf(Variable("X")))).toList()
assertEquals(3, control.size, "Expected 3 results")
assertEquals(3, Program.db.predicates["a/1"]!!.clauses.size, "Expected 3 clauses")
val retract = RetractAll(Structure(Atom("a"), listOf(Variable("X"))))
val result = retract.satisfy(emptyMap()).toList()
assertEquals(1, result.size, "Expected 1 result")
assertTrue(result[0].isSuccess, "Expected success")
assertEquals(0, Program.db.predicates["a/1"]!!.clauses.size, "Expected 0 clauses")
}
@Test
fun `If Head refers to a predicate that is not defined, it is implicitly created as a dynamic predicate`() {
val predicateName = "idonotyetexist"
val predicateFunctor = "$predicateName/1"
assertFalse(predicateFunctor in Program.db.predicates, "Expected predicate to not exist before")
val retractAll = RetractAll(Structure(Atom(predicateName), listOf(Variable("X"))))
val result = retractAll.satisfy(emptyMap()).toList()
assertEquals(1, result.size, "Expected 1 result")
assertTrue(result[0].isSuccess, "Expected success")
assertTrue(predicateFunctor in Program.db.predicates, "Expected predicate to exist after")
assertTrue(Program.db.predicates[predicateFunctor]!!.dynamic, "Expected predicate to be dynamic")
}
}