diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt index c65efd5..4b36614 100644 --- a/src/interpreter/Preprocessor.kt +++ b/src/interpreter/Preprocessor.kt @@ -48,93 +48,70 @@ open class Preprocessor { } protected open fun preprocess(term: Term, nested: Boolean = false): Term { - // TODO Remove hardcoding by storing the functors as constants in operators? - - val prepped = when { - term == Variable("_") -> AnonymousVariable.create() - term is Atom || term is Structure -> { + val prepped = when (term) { + Atom("true") -> True + Structure(Atom("true"), emptyList()) -> True + Atom("false") -> False + Structure(Atom("false"), emptyList()) -> False + Atom("fail") -> Fail + Structure(Atom("fail"), emptyList()) -> Fail + Atom("!") -> Cut() + Structure(Atom("!"), emptyList()) -> Cut() + Atom("inf") -> Integer(Int.MAX_VALUE) + Atom("nl") -> Nl + Variable("_") -> AnonymousVariable.create() + is Structure -> { // Preprocess the arguments first to recognize builtins - val args = if (term is Structure) { - term.arguments.map { preprocess(it, nested = true) } - } else emptyList() + val args = term.arguments.map { preprocess(it, nested = true) } - when (term.functor) { - // Analysis - Functor.of("functor/3") -> FunctorOp(args[0], args[1], args[2]) - Functor.of("arg/3") -> Arg(args[0], args[1], args[2]) - Functor.of("clause/2") -> ClauseOp(args[0] as Head, args[1] as Body) + 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" -> 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" -> 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) + 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 - Functor.of("inf/0") -> Integer(Int.MAX_VALUE) - Functor.of("=\\=/2") -> if (args.all { it is Expression }) { - EvaluatesToDifferent(args[0] as Expression, args[1] as Expression) - } else term - Functor.of("=:=/2") -> if (args.all { it is Expression }) { - EvaluatesTo(args[0] as Expression, args[1] as Expression) - } else term - - Functor.of("is/2") -> if (args.all { it is Expression }) { - Is(args[0] as Expression, args[1] as Expression) - } else term - - Functor.of("-/1") -> if (args.all { it is Expression }) Negate(args[0] as Expression) else term - Functor.of("+/1") -> if (args.all { it is Expression }) Positive(args[0] as Expression) else term - Functor.of("+/2") -> if (args.all { it is Expression }) { - Add(args[0] as Expression, args[1] as Expression) - } else term - - Functor.of("-/2") -> if (args.all { it is Expression }) { - Subtract(args[0] as Expression, args[1] as Expression) - } else term - - Functor.of("*/2") -> if (args.all { it is Expression }) { - Multiply(args[0] as Expression, args[1] as Expression) - } else term - - Functor.of("//2") -> if (args.all { it is Expression }) { - Divide(args[0] as Expression, args[1] as Expression) - } else term - - Functor.of("between/3") -> if (args.all { it is Expression }) { - Between(args[0] as Expression, args[1] as Expression, args[2] as Expression) - } else term - - Functor.of("succ/2") -> if (args.all { it is Expression }) { - Successor(args[0] as Expression, args[1] as Expression) - } else term - - // Control - Functor.of("fail/0") -> Fail - Functor.of("false/0") -> False - Functor.of("true/0") -> True - Functor.of("!/0") -> Cut() - Functor.of(",/2") -> Conjunction(args[0] as LogicOperand, args[1] as LogicOperand) - Functor.of(";/2") -> Disjunction(args[0] as LogicOperand, args[1] as LogicOperand) - Functor.of("|/2") -> Bar(args[0] as LogicOperand, args[1] as LogicOperand) - Functor.of("\\+/1") -> Not(args[0] as Goal) + 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 == "succ/2" && args.all { it is Expression } -> Successor(args[0] as Expression, args[1] as Expression) // Database - Functor.of("dynamic/1") -> Dynamic(Functor.of((args[0] as Atom).name)) - Functor.of("retract/1") -> Retract(args[0]) - Functor.of("retractall/1") -> RetractAll(args[0]) - Functor.of("assert/1") -> { + 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) } else { Assert(Fact(args[0] as Head)) } } - - Functor.of("asserta/1") -> { + term.functor == "asserta/1" -> { if (args[0] is Rule) { AssertA(args[0] as Rule) } else { AssertA(Fact(args[0] as Head)) } } - - Functor.of("assertz/1") -> { + term.functor == "assertz/1" -> { if (args[0] is Rule) { AssertZ(args[0] as Rule) } else { @@ -142,25 +119,14 @@ open class Preprocessor { } } - // IO - Functor.of("write/1") -> Write(args[0]) - Functor.of("nl/0") -> Nl - Functor.of("read/1") -> Read(args[0]) - // Other - Functor.of("initialization/1") -> Initialization(args[0] as Goal) - Functor.of("forall/2") -> ForAll(args[0] as LogicOperand, args[1] as Goal) - - // Unification - Functor.of("=/2") -> Unify(args[0], args[1]) - Functor.of("\\=/2") -> NotUnify(args[0], args[1]) - Functor.of("==/2") -> Equivalent(args[0], args[1]) - Functor.of("\\==/2") -> NotEquivalent(args[0], args[1]) - - Functor.of(":-/2") -> Rule(args[0] as Head, args[1] as Body) + term.functor == "write/1" -> Write(args[0]) + term.functor == "read/1" -> Read(args[0]) + term.functor == "initialization/1" -> Initialization(args[0] as Goal) + term.functor == "forall/2" -> ForAll(args[0] as LogicOperand, args[1] as Goal) else -> { - if (term is Structure) term.arguments = args + term.arguments = args term } } diff --git a/src/prolog/ast/Database.kt b/src/prolog/ast/Database.kt index b309883..be2da7a 100644 --- a/src/prolog/ast/Database.kt +++ b/src/prolog/ast/Database.kt @@ -23,14 +23,14 @@ open class Database(val sourceFile: String) { if (sourceFile !== "") { Logger.debug("Moving clauses from $sourceFile to main database") - predicates.filter { it.key != Functor.of("/_") } + predicates.filter { it.key != "/_" } .forEach { (_, predicate) -> db.load(predicate, force = true) } } Logger.info("Initializing database from $sourceFile") - if (predicates.contains(Functor.of("/_"))) { + if (predicates.contains("/_")) { Logger.debug("Loading clauses from /_ predicate") - predicates[Functor.of("/_")]?.clauses?.forEach { + predicates["/_"]?.clauses?.forEach { Logger.debug("Loading clause $it") val goal = it.body as Goal goal.satisfy(emptyMap()).toList() diff --git a/src/prolog/ast/logic/Clause.kt b/src/prolog/ast/logic/Clause.kt index a2af1f3..1080a9f 100644 --- a/src/prolog/ast/logic/Clause.kt +++ b/src/prolog/ast/logic/Clause.kt @@ -1,8 +1,8 @@ package prolog.ast.logic import prolog.Answers -import prolog.Substitutions import prolog.ast.Database.Program +import prolog.Substitutions import prolog.ast.terms.* import prolog.builtins.True import prolog.flags.AppliedCut @@ -45,14 +45,7 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent { onSuccess = { bodySubs -> // If the body can be proven, yield the (combined) substitutions val goalToHeadResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) } - val headResult = headToGoalSubs.filterKeys { key -> - goalToHeadSubs.any { - occurs( - key as Variable, - it.value - ) - } - } + val headResult = headToGoalSubs.filterKeys { key -> goalToHeadSubs.any { occurs(key as Variable, it.value) } } yield(Result.success(goalToHeadResult + headResult)) }, onFailure = { error -> diff --git a/src/prolog/ast/terms/Atom.kt b/src/prolog/ast/terms/Atom.kt index fccf9fc..5bc2004 100644 --- a/src/prolog/ast/terms/Atom.kt +++ b/src/prolog/ast/terms/Atom.kt @@ -4,10 +4,9 @@ import prolog.Answers import prolog.Substitutions import prolog.ast.logic.Resolvent import prolog.logic.unifyLazy -import prolog.ast.arithmetic.Integer open class Atom(val name: String) : Goal(), Head, Body, Resolvent { - override val functor: Functor = Functor(this, Integer(0)) + override val functor: Functor = "$name/_" override fun solve(goal: Goal, subs: Substitutions): Answers = unifyLazy(goal, this, subs) diff --git a/src/prolog/ast/terms/Functor.kt b/src/prolog/ast/terms/Functor.kt deleted file mode 100644 index 98d764f..0000000 --- a/src/prolog/ast/terms/Functor.kt +++ /dev/null @@ -1,35 +0,0 @@ -package prolog.ast.terms - -import prolog.Substitutions -import prolog.ast.arithmetic.Integer - -data class Functor(val name: Atom, val arity: Integer) : Term { - companion object { - fun of(functor: String): Functor { - // Split the functor string into name and arity, by splitting the last "/" - val lastSlash = functor.lastIndexOf('/') - val name = Atom(functor.substring(0, lastSlash)) - val arity = Integer(functor.substring(lastSlash + 1).toIntOrNull() ?: 0) - return Functor(name, arity) - } - } - - override fun toString(): String = "${name.name}/$arity" - override fun applySubstitution(subs: Substitutions) : Functor = this - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (other == null) return false - if (other !is Functor && other !is String) return false - if (other is Functor) { - return this.name.toString() == other.name.toString() && this.arity == other.arity - } - return this.toString() == other - } - - override fun hashCode(): Int { - var result = name.hashCode() - result = 31 * result + arity.hashCode() - return result - } -} diff --git a/src/prolog/ast/terms/Goal.kt b/src/prolog/ast/terms/Goal.kt index 4f98585..95f9016 100644 --- a/src/prolog/ast/terms/Goal.kt +++ b/src/prolog/ast/terms/Goal.kt @@ -1,8 +1,8 @@ package prolog.ast.terms import prolog.Answers -import prolog.Substitutions import prolog.ast.Database.Program +import prolog.Substitutions import prolog.ast.logic.LogicOperand /** diff --git a/src/prolog/ast/terms/Head.kt b/src/prolog/ast/terms/Head.kt index fe5048d..71b4e8a 100644 --- a/src/prolog/ast/terms/Head.kt +++ b/src/prolog/ast/terms/Head.kt @@ -6,3 +6,5 @@ package prolog.ast.terms interface Head : Term { val functor: Functor } + +typealias Functor = String diff --git a/src/prolog/ast/terms/Structure.kt b/src/prolog/ast/terms/Structure.kt index e17b987..afed37c 100644 --- a/src/prolog/ast/terms/Structure.kt +++ b/src/prolog/ast/terms/Structure.kt @@ -5,14 +5,13 @@ import prolog.Substitutions import prolog.ast.logic.Resolvent import prolog.logic.applySubstitution import prolog.logic.unifyLazy -import prolog.ast.arithmetic.Integer typealias Argument = Term typealias CompoundTerm = Structure open class Structure(val name: Atom, var arguments: List) : Goal(), Head, Body, Resolvent { - override val functor: Functor = Functor(name, Integer(arguments.size)) + override val functor: Functor = "${name.name}/${arguments.size}" override fun solve(goal: Goal, subs: Substitutions): Answers { return unifyLazy(goal, this, subs) diff --git a/src/prolog/builtins/analysisOperators.kt b/src/prolog/builtins/analysisOperators.kt deleted file mode 100644 index 8982313..0000000 --- a/src/prolog/builtins/analysisOperators.kt +++ /dev/null @@ -1,139 +0,0 @@ -package prolog.builtins - -import prolog.Answers -import prolog.Substitutions -import prolog.ast.Database.Program -import prolog.ast.arithmetic.Integer -import prolog.ast.terms.* -import prolog.ast.logic.Clause -import prolog.logic.* - -/** - * [True] when [Term] is a term with [Functor] Name/Arity. - * - * If Term is a [Variable] it is unified with a new term whose arguments are all different variables. - * If Term is [atomic], Arity will be unified with the integer 0, and Name will be unified with Term. - */ -class FunctorOp(private val term: Term, private val functorName: Term, private val functorArity: Term) : - Structure(Atom("functor"), listOf(term, functorName, functorArity)) { - override fun satisfy(subs: Substitutions): Answers { - return when { - nonvariable(term, subs) -> { - val t = applySubstitution(term, subs) as Head - - Conjunction( - Unify(t.functor.arity, functorArity), - Unify(t.functor.name, functorName) - ).satisfy(subs) - } - - variable(term, subs) -> { - require(atomic(functorName, subs) && atomic(functorArity, subs)) { - "Arguments are not sufficiently instantiated" - } - - val name = applySubstitution(functorName, subs) as Atom - val arity = applySubstitution(functorArity, subs) as Integer - val result = Structure(name, List(arity.value) { AnonymousVariable.create() }) - sequenceOf(Result.success(mapOf(term to result))) - } - - else -> throw IllegalStateException() - } - } - - override fun applySubstitution(subs: Substitutions): FunctorOp = FunctorOp( - term.applySubstitution(subs), - functorName.applySubstitution(subs), - functorArity.applySubstitution(subs) - ) -} - -class Arg(private val arg: Term, private val term: Term, private val value: Term) : - Structure(Atom("arg"), listOf(arg, term, value)) { - override fun satisfy(subs: Substitutions): Answers = sequence { - require(nonvariable(term, subs)) { "Arguments are not sufficiently instantiated" } - require(compound(term, subs)) { - val expected = CompoundTerm::class.simpleName?.lowercase() - val actual = term::class.simpleName?.lowercase() - "Type error: `$expected' expected, found `$term' ($actual)" - } - - val t = applySubstitution(term, subs) as Structure - - when { - variable(arg, subs) -> { - // Value will be unified with the successive arguments of term. - // On successful unification, arg is unified with the argument number. - // Backtracking yields alternative solutions. - var count = 0 - for (argument in t.arguments) { - unifyLazy(value, argument, subs).forEach { result -> - result.map { - val sub = arg to Integer(count + 1) - yield(Result.success(it + sub)) - } - } - count++ - } - - } - - else -> { - val a = applySubstitution(arg, subs) as Integer - - require(0 <= a.value) { "Domain error: not_less_than_zero" } - - // Fail silently if the argument is out of bounds - if (0 == a.value || t.arguments.size < a.value) { - return@sequence - } - - val argument = t.arguments[a.value - 1] - yieldAll(unifyLazy(argument, value, subs)) - } - } - } -} - -/** - * [True] if [Head] can be unified with a [Clause] and [Body] with the corresponding Clause Body. - * - * Gives alternative clauses on backtracking. For facts, Body is unified with the atom [True]. - * - * When accessing builtins (static predicates, private procedures), the program will act as if the builtins do not - * exist. Head can only match with dynamic or imported predicates. - * - * [SWI-Prolog Operator clause/2](https://www.swi-prolog.org/pldoc/doc_for?object=clause/2) - */ -class ClauseOp(private val head: Head, private val body: Body) : - Structure(Atom("clause"), listOf(head, body)) { - override fun satisfy(subs: Substitutions): Answers = sequence { - require(nonvariable(head, subs)) { "Arguments are not sufficiently instantiated" } - - val predicate = Program.db.predicates[head.functor] - - if (predicate != null) { - for (clause in predicate.clauses) { - val clauseHead = clause.head - val clauseBody = clause.body - - // Unify the head of the clause with the head of the goal - unifyLazy(clauseHead, head, subs).forEach { result -> - result.map { headSubs -> - // Unify the body of the clause with the body of the goal - unifyLazy(clauseBody, body, headSubs).forEach { bodyResult -> - bodyResult.map { bodySubs -> - // Combine the substitutions from the head and body - val combinedSubs = headSubs + bodySubs - yield(Result.success(combinedSubs)) - } - } - } - } - } - } else { - yield(Result.success(emptyMap())) - } - } -} diff --git a/src/prolog/builtins/databaseOperators.kt b/src/prolog/builtins/databaseOperators.kt index ddfa471..ea36376 100644 --- a/src/prolog/builtins/databaseOperators.kt +++ b/src/prolog/builtins/databaseOperators.kt @@ -3,21 +3,26 @@ package prolog.builtins import io.Logger import prolog.Answers import prolog.Substitutions -import prolog.ast.Database -import prolog.ast.Database.Program -import prolog.ast.arithmetic.Integer import prolog.ast.logic.Clause -import prolog.ast.logic.Fact +import prolog.ast.terms.Atom +import prolog.ast.terms.Structure import prolog.ast.logic.Predicate -import prolog.ast.terms.* +import prolog.ast.Database.Program +import prolog.ast.terms.Functor +import prolog.ast.terms.Term +import prolog.ast.logic.Fact +import prolog.ast.Database +import prolog.ast.terms.Body +import prolog.ast.terms.Goal +import prolog.ast.terms.Operator import prolog.logic.applySubstitution import prolog.logic.unifyLazy /** * (Make) the [Predicate] with the corresponding [Functor] dynamic. */ -class Dynamic(private val dynamicFunctor: Functor) : Goal(), Body { - override val functor = Functor(Atom("dynamic"), Integer(1)) +class Dynamic(private val dynamicFunctor: Functor): Goal(), Body { + override val functor: Functor = "dynamic/1" override fun satisfy(subs: Substitutions): Answers { val predicate = Program.db.predicates[dynamicFunctor] @@ -43,7 +48,7 @@ class Dynamic(private val dynamicFunctor: Functor) : Goal(), Body { } class Assert(clause: Clause) : AssertZ(clause) { - override val functor = Functor(Atom("assert"), Integer(1)) + override val functor: Functor = "assert/1" } /** diff --git a/tests/interpreter/PreprocessorTests.kt b/tests/interpreter/PreprocessorTests.kt index ace7862..bf54869 100644 --- a/tests/interpreter/PreprocessorTests.kt +++ b/tests/interpreter/PreprocessorTests.kt @@ -6,6 +6,7 @@ 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.* @@ -611,7 +612,7 @@ class PreprocessorTests { Atom("declaration/1") ) ) - val expected = Dynamic(Functor.of("declaration/1")) + val expected = Dynamic("declaration/1") val result = preprocessor.preprocess(input) diff --git a/tests/parser/grammars/LogicGrammarTests.kt b/tests/parser/grammars/LogicGrammarTests.kt index cbcb949..57a1f99 100644 --- a/tests/parser/grammars/LogicGrammarTests.kt +++ b/tests/parser/grammars/LogicGrammarTests.kt @@ -2,6 +2,7 @@ package parser.grammars import com.github.h0tk3y.betterParse.grammar.Grammar import com.github.h0tk3y.betterParse.grammar.parseToEnd +import org.junit.jupiter.api.Assertions import org.junit.jupiter.api.Assertions.* import org.junit.jupiter.api.BeforeEach import org.junit.jupiter.api.Test @@ -13,7 +14,7 @@ import prolog.ast.logic.Rule import prolog.ast.terms.CompoundTerm import prolog.ast.terms.Structure import prolog.ast.terms.Variable -import prolog.ast.terms.Functor +import prolog.builtins.Conjunction class LogicGrammarTests { private lateinit var parser: Grammar> @@ -93,13 +94,13 @@ class LogicGrammarTests { assertTrue(rule.head is Structure, "Expected head to be a structure") val head = rule.head as Structure - assertEquals(Functor.of("parent/2"), head.functor, "Expected functor 'parent/2'") + assertEquals("parent/2", head.functor, "Expected functor 'parent/2'") assertEquals(Variable("X"), head.arguments[0], "Expected first argument 'X'") assertEquals(Variable("Y"), head.arguments[1], "Expected second argument 'Y'") assertTrue(rule.body is Structure, "Expected body to be a structure") val body = rule.body as Structure - assertEquals(Functor.of("father/2"), body.functor, "Expected functor 'father/2'") + assertEquals("father/2", body.functor, "Expected functor 'father/2'") assertEquals(Variable("X"), body.arguments[0], "Expected first argument 'X'") assertEquals(Variable("Y"), body.arguments[1], "Expected second argument 'Y'") } @@ -124,12 +125,12 @@ class LogicGrammarTests { assertEquals(1, result.size, "Expected 1 rule") val rule = result[0] as Rule - assertEquals(Functor.of("guest/2"), rule.head.functor, "Expected functor 'guest/2'") - assertEquals(Functor.of(",/2"), (rule.body as CompoundTerm).functor, "Expected functor ',/2'") + assertEquals("guest/2", rule.head.functor, "Expected functor 'guest/2'") + assertEquals(",/2", (rule.body as CompoundTerm).functor, "Expected functor ',/2'") val l1 = (rule.body as CompoundTerm).arguments[0] as CompoundTerm - assertEquals(Functor.of(",/2"), l1.functor, "Expected functor ',/2'") + assertEquals(",/2", l1.functor, "Expected functor ',/2'") val l2 = l1.arguments[0] as CompoundTerm - assertEquals(Functor.of("invited/2"), l2.functor, "Expected functor 'invited/2'") + assertEquals("invited/2", l2.functor, "Expected functor 'invited/2'") } @Test @@ -156,6 +157,6 @@ class LogicGrammarTests { assertEquals(1, result.size, "Expected 1 rule") assertTrue(result[0] is Rule, "Expected a rule") val rule = result[0] as Rule - assertEquals(Functor.of("/0"), rule.head.functor, "Expected a constraint") + assertEquals("/_", rule.head.functor, "Expected a constraint") } } \ No newline at end of file diff --git a/tests/prolog/builtins/AnalysisOperatorsTests.kt b/tests/prolog/builtins/AnalysisOperatorsTests.kt deleted file mode 100644 index dbd3b03..0000000 --- a/tests/prolog/builtins/AnalysisOperatorsTests.kt +++ /dev/null @@ -1,404 +0,0 @@ -package prolog.builtins - -import org.junit.jupiter.api.Assertions.* -import org.junit.jupiter.api.BeforeEach -import org.junit.jupiter.api.Nested -import org.junit.jupiter.api.Test -import org.junit.jupiter.api.assertThrows -import prolog.ast.Database.Program -import prolog.ast.arithmetic.Integer -import prolog.ast.logic.Fact -import prolog.ast.logic.Rule -import prolog.ast.terms.CompoundTerm -import prolog.ast.terms.AnonymousVariable -import prolog.ast.terms.Atom -import prolog.ast.terms.Structure -import prolog.ast.terms.Variable - -class AnalysisOperatorsTests { - @Test - fun `functor(foo, foo, 0)`() { - val functor = FunctorOp(Atom("foo"), Atom("foo"), Integer(0)) - - val result = functor.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitutions") - } - - @Test - fun `functor(foo(X), foo, Y)`() { - val functor = FunctorOp( - Structure(Atom("foo"), listOf(Variable("X"))), - Atom("foo"), - Variable("Y") - ) - - val result = functor.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(Integer(1), subs[Variable("Y")]) - } - - @Test - fun `functor(foo, X, Y)`() { - val atom = Atom("foo") - val functor = FunctorOp(atom, Variable("X"), Variable("Y")) - - val result = functor.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(2, subs.size, "Expected 2 substitutions") - assertEquals(atom.functor.name, subs[Variable("X")]) - assertEquals(atom.functor.arity, subs[Variable("Y")]) - } - - @Test - fun `functor(X, foo, 1)`() { - val functor = FunctorOp(Variable("X"), Atom("foo"), Integer(1)) - - val result = functor.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertInstanceOf(Structure::class.java, subs[Variable("X")]) - val structure = subs[Variable("X")] as Structure - assertEquals(Atom("foo"), structure.name) - assertEquals(1, structure.arguments.size) - assertInstanceOf(AnonymousVariable::class.java, structure.arguments[0]) - } - - @Test - fun `functor(foo(a), foo, 0)`() { - val functor = FunctorOp(Structure(Atom("foo"), listOf(Atom("a"))), Atom("foo"), Integer(0)) - - val result = functor.satisfy(emptyMap()).toList() - - assertTrue(result.isEmpty(), "Expected no results") - } - - @Test - fun `functor(foo(X), foo, 0)`() { - val functor = FunctorOp(Structure(Atom("foo"), listOf(Variable("X"))), Atom("foo"), Integer(0)) - - val result = functor.satisfy(emptyMap()).toList() - - assertTrue(result.isEmpty(), "Expected no results") - } - - @Test - fun `functor(X, Y, 1)`() { - val functor = FunctorOp(Variable("X"), Variable("Y"), Integer(1)) - - val exception = assertThrows { - functor.satisfy(emptyMap()).toList() - } - assertEquals("Arguments are not sufficiently instantiated", exception.message) - } - - @Test - fun `arg without variables`() { - val arg = Arg( - Integer(1), - Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))), - Atom("a") - ) - - val result = arg.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertTrue(subs.isEmpty(), "Expected no substitutions") - } - - @Test - fun `arg with variable value`() { - val arg = Arg( - Integer(1), - Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))), - Variable("Term") - ) - - val result = arg.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(Atom("a"), subs[Variable("Term")]) - } - - @Test - fun `arg with variable arg`() { - val arguments = listOf(Atom("a"), Atom("b"), Atom("c")) - for (i in arguments.indices) { - val arg = Arg( - Variable("Arg"), - Structure(Atom("f"), arguments), - arguments[i] - ) - - val result = arg.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result for arg $i") - assertTrue(result[0].isSuccess, "Expected success for arg $i") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution for arg $i") - assertEquals(Integer(i + 1), subs[Variable("Arg")], "Expected arg to be $i + 1") - } - } - - @Test - fun `arg with backtracking`() { - val arg = Arg( - Variable("Position"), - Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))), - Variable("Term") - ) - - val result = arg.satisfy(emptyMap()).toList() - - assertEquals(3, result.size, "Expected 3 results") - - assertTrue(result[0].isSuccess, "Expected success") - val subs1 = result[0].getOrNull()!! - assertEquals(2, subs1.size, "Expected 2 substitutions") - assertEquals(Integer(1), subs1[Variable("Position")]) - assertEquals(Atom("a"), subs1[Variable("Term")]) - - assertTrue(result[1].isSuccess, "Expected success") - val subs2 = result[1].getOrNull()!! - assertEquals(2, subs2.size, "Expected 2 substitutions") - assertEquals(Integer(2), subs2[Variable("Position")]) - assertEquals(Atom("b"), subs2[Variable("Term")]) - - assertTrue(result[2].isSuccess, "Expected success") - val subs3 = result[2].getOrNull()!! - assertEquals(2, subs3.size, "Expected 2 substitutions") - assertEquals(Integer(3), subs3[Variable("Position")]) - assertEquals(Atom("c"), subs3[Variable("Term")]) - } - - @Test - fun `arg raises error if Arg is not compound`() { - val arg = Arg(Integer(1), Atom("foo"), Variable("X")) - - val exception = assertThrows { - arg.satisfy(emptyMap()).toList() - } - assertEquals("Type error: `structure' expected, found `foo' (atom)", exception.message) - } - - @Test - fun `arg fails silently if arg = 0`() { - val arg = Arg( - Integer(0), - Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))), - Variable("Term") - ) - - val result = arg.satisfy(emptyMap()).toList() - - assertTrue(result.isEmpty(), "Expected no results") - } - - @Test - fun `arg fails silently if arg gt arity`() { - val arg = Arg( - Integer(4), - Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))), - Variable("Term") - ) - - val result = arg.satisfy(emptyMap()).toList() - - assertTrue(result.isEmpty(), "Expected no results") - } - - @Test - fun `arg raises error if arg lt 0`() { - val arg = Arg( - Integer(-1), - Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))), - Variable("Term") - ) - - val exception = assertThrows { - arg.satisfy(emptyMap()).toList() - } - assertEquals("Domain error: not_less_than_zero", exception.message) - } - - @Nested - class `Clause operator` { - @BeforeEach - fun setup() { - Program.reset() - } - - @Test - fun `clause fact atom without variables`() { - Program.load(listOf(Fact(Atom("foo")))) - - val result = ClauseOp( - Atom("foo"), - True - ).satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertTrue(subs.isEmpty(), "Expected empty substitutions") - } - - @Test - fun `clause fact compound without variables`() { - Program.load( - listOf( - Fact(CompoundTerm(Atom("foo"), listOf(Atom("a"), Atom("b")))) - ) - ) - - val result = ClauseOp( - CompoundTerm(Atom("foo"), listOf(Atom("a"), Atom("b"))), - True - ).satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertTrue(subs.isEmpty(), "Expected empty substitutions") - } - - @Test - fun `clause rule without variables`() { - Program.load(listOf(Rule(Atom("foo"), Atom("bar")))) - - val result = ClauseOp( - Atom("foo"), - Atom("bar") - ).satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertTrue(subs.isEmpty(), "Expected empty substitutions") - } - - @Test - fun `clause fact variable body`() { - Program.load(listOf(Fact(Atom("foo")))) - - val variable = Variable("Term") - val result = ClauseOp( - Atom("foo"), - variable - ).satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(True, subs[variable]) - } - - @Test - fun `clause fact with variable head`() { - Program.load( - listOf( - Fact(CompoundTerm(Atom("foo"), listOf(Atom("a")))) - ) - ) - - val result = ClauseOp( - CompoundTerm(Atom("foo"), listOf(Variable("X"))), - True - ).satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(Atom("a"), subs[Variable("X")]) - } - - @Test - fun `clause rule with variable body`() { - Program.load(listOf(Rule(Atom("foo"), Atom("bar")))) - - val result = ClauseOp( - Atom("foo"), - Variable("Term") - ).satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected 1 result") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected 1 substitution") - assertEquals(Atom("bar"), subs[Variable("Term")]) - } - - @Test - fun `clause fact variable value with backtracking`() { - Program.load( - listOf( - Fact(CompoundTerm(Atom("bar"), listOf(Atom("d")))), - Fact(CompoundTerm(Atom("bar"), listOf(Atom("e")))), - Fact(CompoundTerm(Atom("foo"), listOf(Atom("a")))), - Fact(CompoundTerm(Atom("foo"), listOf(Atom("b")))), - Fact(CompoundTerm(Atom("foo"), listOf(Atom("c")))), - Rule( - CompoundTerm(Atom("foo"), listOf(Variable("X"))), - CompoundTerm(Atom("bar"), listOf(Variable("X"))) - ) - ) - ) - - val x = Variable("X") - val term = Variable("Term") - - val result = ClauseOp( - CompoundTerm(Atom("foo"), listOf(x)), - term - ).satisfy(emptyMap()).toList() - - assertEquals(4, result.size, "Expected 4 results") - - assertTrue(result[0].isSuccess, "Expected success") - val subs1 = result[0].getOrNull()!! - assertEquals(2, subs1.size, "Expected 2 substitutions") - assertEquals(Atom("a"), subs1[x], "Expected a") - assertEquals(True, subs1[term], "Expected True") - - assertTrue(result[1].isSuccess, "Expected success") - val subs2 = result[1].getOrNull()!! - assertEquals(2, subs2.size, "Expected 2 substitutions") - assertEquals(Atom("b"), subs2[x], "Expected b") - assertEquals(True, subs2[term], "Expected True") - - assertTrue(result[2].isSuccess, "Expected success") - val subs3 = result[2].getOrNull()!! - assertEquals(2, subs3.size, "Expected 2 substitutions") - assertEquals(Atom("c"), subs3[x], "Expected c") - assertEquals(True, subs3[term], "Expected True") - - assertTrue(result[3].isSuccess, "Expected success") - val subs4 = result[3].getOrNull()!! - assertEquals(1, subs4.size, "Expected 2 substitutions") - assertEquals( - CompoundTerm(Atom("bar"), listOf(Variable("X"))), - subs4[term], - "Expected bar(X)" - ) - } - } -} diff --git a/tests/prolog/builtins/DatabaseOperatorsTests.kt b/tests/prolog/builtins/DatabaseOperatorsTests.kt index 51a27c3..73cfef0 100644 --- a/tests/prolog/builtins/DatabaseOperatorsTests.kt +++ b/tests/prolog/builtins/DatabaseOperatorsTests.kt @@ -8,6 +8,7 @@ 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.ast.Database import prolog.ast.Database.Program import prolog.ast.logic.Clause import prolog.ast.logic.Fact @@ -39,7 +40,7 @@ class DatabaseOperatorsTests { createAssert(fact).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(fact, Program.db.predicates[Functor.of("a/_")]!!.clauses[0]) + assertEquals(fact, Program.db.predicates["a/_"]!!.clauses[0]) } @Test @@ -48,7 +49,7 @@ class DatabaseOperatorsTests { createAssert(fact).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(fact, Program.db.predicates[Functor.of("a/1")]!!.clauses[0]) + assertEquals(fact, Program.db.predicates["a/1"]!!.clauses[0]) } @Test @@ -60,7 +61,7 @@ class DatabaseOperatorsTests { createAssert(rule).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(rule, Program.db.predicates[Functor.of("a/1")]!!.clauses[0]) + assertEquals(rule, Program.db.predicates["a/1"]!!.clauses[0]) } } @@ -91,8 +92,8 @@ class DatabaseOperatorsTests { AssertA(rule2).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(rule2, Program.db.predicates[Functor.of("a/1")]!!.clauses[0]) - assertEquals(rule1, Program.db.predicates[Functor.of("a/1")]!!.clauses[1]) + assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[0]) + assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[1]) } } @@ -116,8 +117,8 @@ class DatabaseOperatorsTests { AssertZ(rule2).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(rule1, Program.db.predicates[Functor.of("a/1")]!!.clauses[0]) - assertEquals(rule2, Program.db.predicates[Functor.of("a/1")]!!.clauses[1]) + assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[0]) + assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[1]) } } @@ -308,20 +309,20 @@ class DatabaseOperatorsTests { val control = Program.query(Structure(Atom("a"), listOf(Variable("X")))).toList() assertEquals(3, control.size, "Expected 3 results") - assertEquals(3, Program.db.predicates[Functor.of("a/1")]!!.clauses.size, "Expected 3 clauses") + 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[Functor.of("a/1")]!!.clauses.size, "Expected 0 clauses") + 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 = Functor.of("$predicateName/1") + val predicateFunctor = "$predicateName/1" assertFalse(predicateFunctor in Program.db.predicates, "Expected predicate to not exist before")