diff --git a/.idea/2025LogProg-PrologInterpreter.iml b/.idea/2025LogProg-PrologInterpreter.iml new file mode 100644 index 0000000..42d53f5 --- /dev/null +++ b/.idea/2025LogProg-PrologInterpreter.iml @@ -0,0 +1,8 @@ + + + + + + + + \ No newline at end of file diff --git a/.idea/modules.xml b/.idea/modules.xml new file mode 100644 index 0000000..5b434ac --- /dev/null +++ b/.idea/modules.xml @@ -0,0 +1,8 @@ + + + + + + + + \ No newline at end of file diff --git a/src/Main.kt b/src/Main.kt index 55a12bf..2416fdb 100644 --- a/src/Main.kt +++ b/src/Main.kt @@ -1,5 +1,4 @@ import com.xenomachina.argparser.ArgParser -import com.xenomachina.argparser.mainBody import interpreter.FileLoader import io.GhentPrologArgParser import io.Logger diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt index 559a7b2..7477702 100644 --- a/src/interpreter/Preprocessor.kt +++ b/src/interpreter/Preprocessor.kt @@ -66,71 +66,53 @@ open class Preprocessor { when { // TODO Remove hardcoding by storing the functors as constants in operators? + + term.functor == ":-/2" -> Rule( args[0] as Head, args[1] as Body ) + // Logic - term.functor == "=/2" -> { - Unify(args[0], args[1]) - } + term.functor == "=/2" -> Unify(args[0], args[1]) + term.functor == "\\=/2" -> NotUnify(args[0], args[1]) + 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" -> Equivalent(args[0], args[1]) - term.functor == "\\=/2" -> { - NotUnify(args[0], args[1]) - } - - 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" -> { - Equivalent(args[0], args[1]) - } - - term.functor == "=\\=/2" && args.all { it is Expression } -> { - EvaluatesToDifferent(args[0] as Expression, args[1] as Expression) - } - - term.functor == "=:=/2" && args.all { it is Expression } -> { - EvaluatesTo(args[0] as Expression, args[1] as Expression) - } - - term.functor == "is/2" && args.all { it is Expression } -> { - Is(args[0] as Expression, args[1] as Expression) - } + term.functor == "=\\=/2" && args.all { it is Expression } -> EvaluatesToDifferent(args[0] as Expression, args[1] as Expression) + term.functor == "=:=/2" && args.all { it is Expression } -> EvaluatesTo(args[0] as Expression, args[1] as Expression) + term.functor == "is/2" && args.all { it is Expression } -> Is(args[0] as Expression, args[1] as Expression) // Arithmetic - term.functor == "-/1" && args.all { it is Expression } -> { - Negate(args[0] as Expression) - } + term.functor == "-/1" && args.all { it is Expression } -> Negate(args[0] as Expression) + term.functor == "-/2" && args.all { it is Expression } -> Subtract(args[0] as Expression, args[1] as Expression) + term.functor == "+/1" && args.all { it is Expression } -> Positive(args[0] as Expression) + term.functor == "+/2" && args.all { it is Expression } -> Add(args[0] as Expression, args[1] as Expression) + 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 == "-/2" && args.all { it is Expression } -> { - Subtract(args[0] as Expression, args[1] as Expression) + // Database + term.functor == "retract/1" -> Retract(args[0]) + term.functor == "assert/1" -> { + if (args[0] is Rule) { + Assert(args[0] as Rule) + } else { + Assert(Fact(args[0] as Head)) + } } - - term.functor == "+/1" && args.all { it is Expression } -> { - Positive(args[0] as Expression) + term.functor == "asserta/1" -> { + if (args[0] is Rule) { + AssertA(args[0] as Rule) + } else { + AssertA(Fact(args[0] as Head)) + } } - - term.functor == "+/2" && args.all { it is Expression } -> { - Add(args[0] as Expression, args[1] as Expression) - } - - 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 == "assertz/1" -> { + if (args[0] is Rule) { + AssertZ(args[0] as Rule) + } else { + AssertZ(Fact(args[0] as Head)) + } } // Other diff --git a/src/parser/grammars/TermsGrammar.kt b/src/parser/grammars/TermsGrammar.kt index 487f9f7..f62e54d 100644 --- a/src/parser/grammars/TermsGrammar.kt +++ b/src/parser/grammars/TermsGrammar.kt @@ -31,10 +31,12 @@ import prolog.ast.terms.* * | 100 | yfx | . | * | 1 | fx | $ | * + * It is very easy to extend this grammar to support more operators. Just add them at the appropriate rule or create a + * new rule and chain it to the existing ones. + * * @see [SWI-Prolog Predicate op/3](https://www.swi-prolog.org/pldoc/man?predicate=op/3) */ open class TermsGrammar : Tokens() { - // Basic named terms protected val variable: Parser by (variableToken or anonymousVariableToken) use { Variable(text) } protected val simpleAtom: Parser by (nameToken or exclamation) use { Atom(text) } @@ -66,42 +68,43 @@ open class TermsGrammar : Tokens() { or int ) - // Level 200 - prefix operators (+, -, \) protected val op200: Parser by ((plus or minus) * parser(::term200)) use { CompoundTerm(Atom(t1.text), listOf(t2)) } protected val term200: Parser by (op200 or baseTerm) - // Level 400 - multiplication, division protected val op400: Parser by (multiply or divide) use { text } protected val term400: Parser by (term200 * zeroOrMore(op400 * term200)) use { t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) } } - // Level 500 - addition, subtraction protected val op500: Parser by (plus or minus) use { text } protected val term500: Parser by (term400 * zeroOrMore(op500 * term400)) use { t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) } } - // Level 700 - comparison operators protected val op700: Parser by (equivalent or equals or notEquals or isOp) use { text } protected val term700: Parser by (term500 * optional(op700 * term500)) use { if (t2 == null) t1 else CompoundTerm(Atom(t2!!.t1), listOf(t1, t2!!.t2)) } - // Level 1000 - conjunction (,) - protected val term1000: Parser by (term700 * zeroOrMore(comma * term700)) use { - t2.fold(t1) { acc, (_, term) -> CompoundTerm(Atom(","), listOf(acc, term)) } + 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)) } } - // Level 1100 - disjunction (;) - protected val term1100: Parser by (term1000 * zeroOrMore(semicolon * term1000)) use { - t2.fold(t1) { acc, (_, term) -> CompoundTerm(Atom(";"), listOf(acc, term)) } + 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)) } + } + + protected val op1200: Parser by (neck) use { text } + protected val term1200: Parser by (term1100 * zeroOrMore(op1200 * term1100)) use { + t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) } } // Term - highest level expression - protected val term: Parser by term1100 + protected val term: Parser by term1200 protected val termNoConjunction: Parser by term700 // Parts for clauses diff --git a/src/prolog/Program.kt b/src/prolog/Program.kt index d129f0d..e82b0bf 100644 --- a/src/prolog/Program.kt +++ b/src/prolog/Program.kt @@ -12,8 +12,8 @@ import prolog.ast.terms.Goal * This object is a singleton that manages a list of databases. */ object Program : Resolvent { - private val internalDb = Database("") - private val databases: MutableList = mutableListOf(internalDb) + val internalDb = Database("") + val databases: MutableList = mutableListOf(internalDb) var storeNewLine: Boolean = false var variableRenamingStart: Int = 0 @@ -35,7 +35,7 @@ object Program : Resolvent { } } - fun load(clauses: List) = internalDb.load(clauses) + fun load(clauses: List, index: Int? = null) = internalDb.load(clauses, index) fun clear() { databases.forEach { it.clear() } diff --git a/src/prolog/Substitution.kt b/src/prolog/Substitution.kt index 062d63e..9058f8c 100644 --- a/src/prolog/Substitution.kt +++ b/src/prolog/Substitution.kt @@ -8,4 +8,4 @@ abstract class Substitution(val from: Term, val to: Term) { } typealias Substitutions = Map typealias Answer = Result -typealias Answers = Sequence \ No newline at end of file +typealias Answers = Sequence diff --git a/src/prolog/ast/Database.kt b/src/prolog/ast/Database.kt index e295e39..d10695d 100644 --- a/src/prolog/ast/Database.kt +++ b/src/prolog/ast/Database.kt @@ -14,7 +14,7 @@ import prolog.ast.terms.Goal * Prolog Program or Database */ class Database(val sourceFile: String): Resolvent { - private var predicates: Map = emptyMap() + var predicates: Map = emptyMap() fun initialize() { Logger.info("Initializing database from $sourceFile") @@ -39,14 +39,14 @@ class Database(val sourceFile: String): Resolvent { /** * Loads a list of clauses into the program. */ - fun load(clauses: List) { + fun load(clauses: List, index: Int? = null) { for (clause in clauses) { val functor = clause.functor val predicate = predicates[functor] if (predicate != null) { // If the predicate already exists, add the clause to it - predicate.add(clause) + predicate.add(clause, index) } else { // If the predicate does not exist, create a new one predicates += Pair(functor, Predicate(listOf(clause))) diff --git a/src/prolog/ast/logic/Clause.kt b/src/prolog/ast/logic/Clause.kt index f402951..a48fb1f 100644 --- a/src/prolog/ast/logic/Clause.kt +++ b/src/prolog/ast/logic/Clause.kt @@ -19,7 +19,7 @@ import prolog.logic.unifyLazy * @see [prolog.ast.terms.Variable] * @see [Predicate] */ -abstract class Clause(val head: Head, val body: Body) : Resolvent { +abstract class Clause(val head: Head, val body: Body) : Term, Resolvent { val functor: Functor = head.functor override fun solve(goal: Goal, subs: Substitutions): Answers = sequence { @@ -70,4 +70,18 @@ abstract class Clause(val head: Head, val body: Body) : Resolvent { } override fun toString(): String = if (body is True) head.toString() else "$head :- $body" + + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (other !is Clause) return false + + if (head != other.head) return false + if (body != other.body) return false + + return true + } + + override fun hashCode(): Int { + return super.hashCode() + } } diff --git a/src/prolog/ast/logic/Predicate.kt b/src/prolog/ast/logic/Predicate.kt index 236f286..5640f57 100644 --- a/src/prolog/ast/logic/Predicate.kt +++ b/src/prolog/ast/logic/Predicate.kt @@ -36,9 +36,9 @@ class Predicate : Resolvent { /** * Adds a clause to the predicate. */ - fun add(clause: Clause) { + fun add(clause: Clause, index: Int? = null) { require(clause.functor == functor) { "Clause functor does not match predicate functor" } - clauses.add(clause) + if (index != null) clauses.add(index, clause) else clauses.add(clause) } /** diff --git a/src/prolog/builtins/databaseOperators.kt b/src/prolog/builtins/databaseOperators.kt new file mode 100644 index 0000000..a002bfa --- /dev/null +++ b/src/prolog/builtins/databaseOperators.kt @@ -0,0 +1,83 @@ +package prolog.builtins + +import prolog.Answers +import prolog.Substitutions +import prolog.ast.logic.Clause +import prolog.ast.terms.Atom +import prolog.ast.terms.Structure +import prolog.ast.logic.Predicate +import prolog.Program +import prolog.ast.terms.Functor +import prolog.ast.terms.Term +import prolog.ast.logic.Fact +import prolog.ast.Database +import prolog.ast.terms.Operator +import prolog.logic.unifyLazy + +class Assert(clause: Clause) : AssertZ(clause) { + override val functor: Functor = "assert/1" +} + +/** + * Assert a [Clause] as a first clause of the [Predicate] into the [Program]. + */ +class AssertA(val clause: Clause) : Operator(Atom("asserta"), null, clause) { + override fun satisfy(subs: Substitutions): Answers { + // Add clause to the program + Program.load(listOf(clause), 0) + + return sequenceOf(Result.success(emptyMap())) + } +} + +/** + * Assert a [Clause] as a last clause of the [Predicate] into the [Program]. + */ +open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause) { + override fun satisfy(subs: Substitutions): Answers { + // Add clause to the program + Program.load(listOf(clause)) + + return sequenceOf(Result.success(emptyMap())) + } +} + +/** + * When [Term] is an [Atom] or a term, it is unified with the first unifying [Clause] in the [Database]. + * The [Fact] or Clause is removed from the Database. It respects the logical update view. + * + * @see [SWI-Prolog Predicate retract/1](https://www.swi-prolog.org/pldoc/doc_for?object=retract/1) + */ +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) { + yield(Result.failure(Exception("Cannot retract a non-structure or non-atom"))) + return@sequence + } + + val functorName = term.functor + + Program.databases + .filter { it.predicates.containsKey(functorName) } + .mapNotNull { it.predicates[functorName] } + .map { predicate -> + val clausesIterator = predicate.clauses.iterator() + while (clausesIterator.hasNext()) { + val clause = clausesIterator.next() + unifyLazy(term, clause.head, subs).forEach { unifyResult -> + unifyResult.fold( + onSuccess = { substitutions -> + // If unification is successful, remove the clause + yield(Result.success(substitutions)) + clausesIterator.remove() + }, + onFailure = { + // If unification fails, do nothing + } + ) + } + } + } + } +} diff --git a/src/prolog/builtins/io.kt b/src/prolog/builtins/ioOperators.kt similarity index 100% rename from src/prolog/builtins/io.kt rename to src/prolog/builtins/ioOperators.kt diff --git a/src/repl/Repl.kt b/src/repl/Repl.kt index a7c684a..aae1390 100644 --- a/src/repl/Repl.kt +++ b/src/repl/Repl.kt @@ -42,10 +42,9 @@ class Repl { val iterator = answers.iterator() if (!iterator.hasNext()) { - io.say("false.") + io.say("false.\n") } else { - var previous = iterator.next() - io.say(prettyPrint(previous)) + io.say(prettyPrint(iterator.next())) while (iterator.hasNext()) { var command = io.prompt("") @@ -57,8 +56,7 @@ class Repl { when (command) { ";" -> { - previous = iterator.next() - io.say(prettyPrint(previous)) + io.say(prettyPrint(iterator.next())) } "a" -> return "." -> return @@ -88,7 +86,7 @@ class Repl { val subs = result.getOrNull()!! if (subs.isEmpty()) { io.checkNewLine() - return "true.\n" + return "true." } return subs.entries.joinToString(",\n") { "${it.key} = ${it.value}" } }, diff --git a/tests/interpreter/PreprocessorTests.kt b/tests/interpreter/PreprocessorTests.kt index d7d6c19..0b98ff4 100644 --- a/tests/interpreter/PreprocessorTests.kt +++ b/tests/interpreter/PreprocessorTests.kt @@ -6,6 +6,8 @@ import org.junit.jupiter.api.Nested import org.junit.jupiter.api.Test import parser.grammars.TermsGrammar import prolog.ast.arithmetic.Integer +import prolog.ast.logic.Fact +import prolog.ast.logic.Rule import prolog.ast.terms.* import prolog.builtins.* @@ -498,4 +500,109 @@ class PreprocessorTests { ) } } + + @Nested + class `Database operators` { + private val preprocessor = OpenPreprocessor() + + @Test + fun `assert(fact)`() { + val input = Structure( + Atom("assert"), listOf( + Structure( + Atom(":-"), listOf( + Atom("a"), + Atom("b") + ) + ) + ) + ) + val expected = Assert( + Rule( + Atom("a"), + Atom("b") + ) + ) + + val result = preprocessor.preprocess(input) + + assertEquals(expected, result) + } + + @Test + fun `asserta(fact)`() { + val input = Structure( + Atom("asserta"), listOf( + Structure( + Atom(":-"), listOf( + Atom("a"), + Atom("b") + ) + ) + ) + ) + val expected = AssertA( + Rule( + Atom("a"), + Atom("b") + ) + ) + + val result = preprocessor.preprocess(input) + + assertEquals(expected, result) + } + + @Test + fun `assertz(fact)`() { + val input = Structure( + Atom("assertz"), listOf( + Structure( + Atom(":-"), listOf( + Atom("a"), + Atom("b") + ) + ) + ) + ) + val expected = AssertZ( + Rule( + Atom("a"), + Atom("b") + ) + ) + + val result = preprocessor.preprocess(input) + + assertEquals(expected, result) + } + + @Test + fun `retract(atom)`() { + val input = Structure( + Atom("retract"), listOf( + Atom("a") + ) + ) + val expected = Retract(Atom("a")) + + val result = preprocessor.preprocess(input) + + assertEquals(expected, result) + } + + @Test + fun `retract(compund with variable)`() { + val input = Structure( + Atom("retract"), listOf( + CompoundTerm(Atom("a"), listOf(Variable("X"))) + ) + ) + val expected = Retract(CompoundTerm(Atom("a"), listOf(Variable("X")))) + + val result = preprocessor.preprocess(input) + + assertEquals(expected, result) + } + } } diff --git a/tests/parser/builtins/DatabaseOperatorsParserTests.kt b/tests/parser/builtins/DatabaseOperatorsParserTests.kt new file mode 100644 index 0000000..9f13e57 --- /dev/null +++ b/tests/parser/builtins/DatabaseOperatorsParserTests.kt @@ -0,0 +1,65 @@ +package parser.builtins + +import com.github.h0tk3y.betterParse.grammar.Grammar +import com.github.h0tk3y.betterParse.grammar.parseToEnd +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.Test +import parser.grammars.TermsGrammar +import prolog.ast.terms.Atom +import prolog.ast.terms.Structure +import prolog.ast.terms.Term +import kotlin.test.assertEquals + +class DatabaseOperatorsParserTests { + private lateinit var parser: Grammar + + @BeforeEach + fun setup() { + parser = TermsGrammar() as Grammar + } + + @Test + fun `parse assert(rule)`() { + val input = "assert((a :- b))" + val expected = Structure(Atom("assert"), listOf( + Structure(Atom(":-"), listOf( + Atom("a"), + Atom("b") + )) + )) + + val result = parser.parseToEnd(input) + + assertEquals(expected, result) + } + + @Test + fun `parse assertA(rule)`() { + val input = "assertA((a :- b))" + val expected = Structure(Atom("assertA"), listOf( + Structure(Atom(":-"), listOf( + Atom("a"), + Atom("b") + )) + )) + + val result = parser.parseToEnd(input) + + assertEquals(expected, result) + } + + @Test + fun `parse assertZ(rule)`() { + val input = "assertZ((a :- b))" + val expected = Structure(Atom("assertZ"), listOf( + Structure(Atom(":-"), listOf( + Atom("a"), + Atom("b") + )) + )) + + val result = parser.parseToEnd(input) + + assertEquals(expected, result) + } +} diff --git a/tests/prolog/builtins/DatabaseOperatorsTests.kt b/tests/prolog/builtins/DatabaseOperatorsTests.kt new file mode 100644 index 0000000..a14453d --- /dev/null +++ b/tests/prolog/builtins/DatabaseOperatorsTests.kt @@ -0,0 +1,286 @@ +package prolog.builtins + +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.Nested +import org.junit.jupiter.api.Test +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.ValueSource +import prolog.Program +import prolog.ast.logic.Clause +import prolog.ast.logic.Fact +import prolog.ast.logic.Predicate +import prolog.ast.logic.Rule +import prolog.ast.terms.Atom +import prolog.ast.terms.Structure +import prolog.ast.terms.Variable +import kotlin.test.assertTrue + +class DatabaseOperatorsTests { + @BeforeEach + fun setup() { + Program.clear() + } + + abstract class AssertTestsBase { + protected abstract fun createAssert(clause: Clause): Structure + + @BeforeEach + fun setup() { + Program.clear() + } + + @ParameterizedTest + @ValueSource(classes = [AssertA::class, AssertZ::class, Assert::class]) + fun `assert(fact atom)`(assertKind: Class<*>) { + val fact = Fact(Atom("a")) + createAssert(fact).satisfy(emptyMap()) + + assertEquals(1, Program.internalDb.predicates.size, "Expected 1 predicate") + assertEquals(fact, Program.internalDb.predicates["a/_"]!!.clauses[0]) + } + + @Test + fun `assert(fact structure)`() { + val fact = Fact(Structure(Atom("a"), listOf(Atom("b")))) + createAssert(fact).satisfy(emptyMap()) + + assertEquals(1, Program.internalDb.predicates.size, "Expected 1 predicate") + assertEquals(fact, Program.internalDb.predicates["a/1"]!!.clauses[0]) + } + + @Test + fun `assert(rule)`() { + val rule = Rule( + Structure(Atom("a"), listOf(Atom("b"))), + Atom("c") + ) + createAssert(rule).satisfy(emptyMap()) + + assertEquals(1, Program.internalDb.predicates.size, "Expected 1 predicate") + assertEquals(rule, Program.internalDb.predicates["a/1"]!!.clauses[0]) + } + } + + @Nested + class AssertTests : AssertTestsBase() { + override fun createAssert(clause: Clause): Structure { + return Assert(clause) + } + } + + @Nested + class AssertATests : AssertTestsBase() { + override fun createAssert(clause: Clause): Structure { + return AssertA(clause) + } + + @Test + fun `asserta adds to the beginning`() { + val rule1 = Rule( + Structure(Atom("a"), listOf(Atom("b"))), + Atom("c") + ) + val rule2 = Rule( + Structure(Atom("a"), listOf(Atom("d"))), + Atom("e") + ) + AssertA(rule1).satisfy(emptyMap()) + AssertA(rule2).satisfy(emptyMap()) + + assertEquals(1, Program.internalDb.predicates.size, "Expected 1 predicate") + assertEquals(rule2, Program.internalDb.predicates["a/1"]!!.clauses[0]) + assertEquals(rule1, Program.internalDb.predicates["a/1"]!!.clauses[1]) + } + } + + @Nested + class AssertZTests : AssertTestsBase() { + override fun createAssert(clause: Clause): Structure { + return AssertZ(clause) + } + + @Test + fun `assertz adds to the end`() { + val rule1 = Rule( + Structure(Atom("a"), listOf(Atom("b"))), + Atom("c") + ) + val rule2 = Rule( + Structure(Atom("a"), listOf(Atom("d"))), + Atom("e") + ) + AssertZ(rule1).satisfy(emptyMap()) + AssertZ(rule2).satisfy(emptyMap()) + + assertEquals(1, Program.internalDb.predicates.size, "Expected 1 predicate") + assertEquals(rule1, Program.internalDb.predicates["a/1"]!!.clauses[0]) + assertEquals(rule2, Program.internalDb.predicates["a/1"]!!.clauses[1]) + } + } + + @Test + fun `retract fails silently for unknown predicates`() { + val retract = Retract(Atom("unknown")) + val result = retract.satisfy(emptyMap()) + + assertTrue(result.none(), "Expected no results") + } + + @Test + fun `simple retract`() { + val predicate = Predicate(listOf(Fact(Atom("a")))) + Program.internalDb.load(predicate) + + assertEquals(1, Program.query(Atom("a")).count()) + + val retract = Retract(Atom("a")) + + assertTrue(retract.satisfy(emptyMap()).any(), "Expected 1 result") + assertEquals(0, predicate.clauses.size, "Expected 0 clauses") + + assertTrue(retract.satisfy(emptyMap()).none()) + } + + @Test + fun `retract atom`() { + val predicate = Predicate(listOf( + Fact(Atom("a")), + Fact(Atom("a")), + Fact(Atom("a")) + )) + Program.internalDb.load(predicate) + + val control = Program.query(Atom("a")).toList() + + assertEquals(3, control.size, "Expected 3 results") + + val retract = Retract(Atom("a")) + + val result = retract.satisfy(emptyMap()) + + assertEquals(3, predicate.clauses.size, "Expected 3 clauses") + + var answer = result.first() + + assertTrue(answer.isSuccess, "Expected success") + var subs = answer.getOrNull()!! + assertTrue(subs.isEmpty(), "Expected no substitutions") + assertEquals(2, predicate.clauses.size, "Expected 2 clauses") + + assertTrue(result.first().isSuccess) + assertTrue(result.first().isSuccess) + + assertEquals(0, predicate.clauses.size, "Expected no remaining clauses") + } + + @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")))) + )) + Program.internalDb.load(predicate) + + val control = Program.query(Structure(Atom("a"), listOf(Variable("X")))).toList() + + assertEquals(3, control.size, "Expected 3 results") + + val retract = Retract(Structure(Atom("a"), listOf(Variable("X")))) + + val result = retract.satisfy(emptyMap()) + + assertEquals(3, predicate.clauses.size, "Expected 3 clauses") + + var answer = result.first() + + assertTrue(answer.isSuccess, "Expected success") + var subs = answer.getOrNull()!! + assertTrue(subs.isNotEmpty(), "Expected substitutions") + assertTrue(Variable("X") in subs, "Expected variable X") + assertEquals(Atom("b"), subs[Variable("X")], "Expected b") + assertEquals(2, predicate.clauses.size, "Expected 2 clauses") + + answer = result.first() + + assertTrue(answer.isSuccess, "Expected success") + subs = answer.getOrNull()!! + assertTrue(subs.isNotEmpty(), "Expected substitutions") + assertTrue(Variable("X") in subs, "Expected variable X") + assertEquals(Atom("c"), subs[Variable("X")], "Expected c") + assertEquals(1, predicate.clauses.size, "Expected 1 clause") + + answer = result.first() + + assertTrue(answer.isSuccess, "Expected success") + subs = answer.getOrNull()!! + 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") + + assertEquals(0, result.count(), "Expected no remaining results") + } + + @Test + fun `custom assert example`() { + var query = Structure(Atom("likes"), listOf(Atom("alice"), Atom("pizza"))) + + var result = Program.query(query).toList() + assertEquals(0, result.size, "Expected 0 results") + + var assert: Structure = Assert(Fact(query)) + assert.satisfy(emptyMap()) + + result = Program.query(query).toList() + assertEquals(1, result.size, "Expected 1 result") + assertTrue(result[0].getOrNull()!!.isEmpty()) + + assert = AssertZ(Fact(Structure(Atom("likes"), listOf(Atom("bob"), Atom("sushi"))))) + assert.satisfy(emptyMap()) + + query = Structure(Atom("likes"), listOf(Atom("bob"), Variable("X"))) + + result = Program.query(query).toList() + assertEquals(1, result.size, "Expected 1 result") + assertTrue(result[0].isSuccess, "Expected success") + assertEquals(Atom("sushi"), result[0].getOrNull()!![Variable("X")], "Expected sushi") + + query = Structure(Atom("likes"), listOf(Variable("X"), Variable("Y"))) + + result = Program.query(query).toList() + assertEquals(2, result.size, "Expected 2 results") + assertTrue(result[0].isSuccess, "Expected success") + var result0 = result[0].getOrNull()!! + assertEquals(Atom("alice"), result0[Variable("X")], "Expected alice") + assertEquals(Atom("pizza"), result0[Variable("Y")], "Expected pizza") + assertTrue(result[1].isSuccess, "Expected success") + var result1 = result[1].getOrNull()!! + assertEquals(Atom("bob"), result1[Variable("X")], "Expected bob") + assertEquals(Atom("sushi"), result1[Variable("Y")], "Expected sushi") + + assert = AssertA( + Rule( + Structure(Atom("likes"), listOf(Variable("X"), Atom("italian"))), + Structure(Atom("likes"), listOf(Variable("X"), Atom("pizza"))) + ) + ) + assert.satisfy(emptyMap()) + + result = Program.query(query).toList() + assertEquals(3, result.size, "Expected 3 results") + assertTrue(result[0].isSuccess, "Expected success") + result0 = result[0].getOrNull()!! + assertEquals(Atom("alice"), result0[Variable("X")], "Expected alice") + assertEquals(Atom("italian"), result0[Variable("Y")], "Expected italian") + assertTrue(result[1].isSuccess, "Expected success") + result1 = result[1].getOrNull()!! + assertEquals(Atom("alice"), result1[Variable("X")], "Expected alice") + assertEquals(Atom("pizza"), result1[Variable("Y")], "Expected pizza") + assertTrue(result[2].isSuccess, "Expected success") + val result2 = result[2].getOrNull()!! + assertEquals(Atom("bob"), result2[Variable("X")], "Expected bob") + assertEquals(Atom("sushi"), result2[Variable("Y")], "Expected sushi") + } +} \ No newline at end of file