diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt index 4b36614..c65efd5 100644 --- a/src/interpreter/Preprocessor.kt +++ b/src/interpreter/Preprocessor.kt @@ -48,70 +48,93 @@ open class Preprocessor { } protected open fun preprocess(term: Term, nested: Boolean = false): Term { - 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 -> { + // TODO Remove hardcoding by storing the functors as constants in operators? + + val prepped = when { + term == Variable("_") -> AnonymousVariable.create() + term is Atom || term is Structure -> { // Preprocess the arguments first to recognize builtins - val args = term.arguments.map { preprocess(it, nested = true) } + val args = if (term is Structure) { + term.arguments.map { preprocess(it, nested = true) } + } else emptyList() - 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) + 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) // 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 - 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) + 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) // 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" -> { + 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") -> { if (args[0] is Rule) { Assert(args[0] as Rule) } else { Assert(Fact(args[0] as Head)) } } - term.functor == "asserta/1" -> { + + Functor.of("asserta/1") -> { if (args[0] is Rule) { AssertA(args[0] as Rule) } else { AssertA(Fact(args[0] as Head)) } } - term.functor == "assertz/1" -> { + + Functor.of("assertz/1") -> { if (args[0] is Rule) { AssertZ(args[0] as Rule) } else { @@ -119,14 +142,25 @@ open class Preprocessor { } } + // IO + Functor.of("write/1") -> Write(args[0]) + Functor.of("nl/0") -> Nl + Functor.of("read/1") -> Read(args[0]) + // Other - 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) + 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) else -> { - term.arguments = args + if (term is Structure) term.arguments = args term } } diff --git a/src/prolog/ast/Database.kt b/src/prolog/ast/Database.kt index be2da7a..b309883 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 != "/_" } + predicates.filter { it.key != Functor.of("/_") } .forEach { (_, predicate) -> db.load(predicate, force = true) } } Logger.info("Initializing database from $sourceFile") - if (predicates.contains("/_")) { + if (predicates.contains(Functor.of("/_"))) { Logger.debug("Loading clauses from /_ predicate") - predicates["/_"]?.clauses?.forEach { + predicates[Functor.of("/_")]?.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 1080a9f..a2af1f3 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.ast.Database.Program import prolog.Substitutions +import prolog.ast.Database.Program import prolog.ast.terms.* import prolog.builtins.True import prolog.flags.AppliedCut @@ -45,7 +45,14 @@ 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 5bc2004..fccf9fc 100644 --- a/src/prolog/ast/terms/Atom.kt +++ b/src/prolog/ast/terms/Atom.kt @@ -4,9 +4,10 @@ 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 = "$name/_" + override val functor: Functor = Functor(this, Integer(0)) 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 new file mode 100644 index 0000000..98d764f --- /dev/null +++ b/src/prolog/ast/terms/Functor.kt @@ -0,0 +1,35 @@ +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 95f9016..4f98585 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.ast.Database.Program import prolog.Substitutions +import prolog.ast.Database.Program import prolog.ast.logic.LogicOperand /** diff --git a/src/prolog/ast/terms/Head.kt b/src/prolog/ast/terms/Head.kt index 71b4e8a..fe5048d 100644 --- a/src/prolog/ast/terms/Head.kt +++ b/src/prolog/ast/terms/Head.kt @@ -6,5 +6,3 @@ 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 afed37c..e17b987 100644 --- a/src/prolog/ast/terms/Structure.kt +++ b/src/prolog/ast/terms/Structure.kt @@ -5,13 +5,14 @@ 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 = "${name.name}/${arguments.size}" + override val functor: Functor = Functor(name, Integer(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 new file mode 100644 index 0000000..8982313 --- /dev/null +++ b/src/prolog/builtins/analysisOperators.kt @@ -0,0 +1,139 @@ +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 ea36376..ddfa471 100644 --- a/src/prolog/builtins/databaseOperators.kt +++ b/src/prolog/builtins/databaseOperators.kt @@ -3,26 +3,21 @@ package prolog.builtins import io.Logger 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.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.ast.Database.Program +import prolog.ast.arithmetic.Integer +import prolog.ast.logic.Clause +import prolog.ast.logic.Fact +import prolog.ast.logic.Predicate +import prolog.ast.terms.* 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 = "dynamic/1" +class Dynamic(private val dynamicFunctor: Functor) : Goal(), Body { + override val functor = Functor(Atom("dynamic"), Integer(1)) override fun satisfy(subs: Substitutions): Answers { val predicate = Program.db.predicates[dynamicFunctor] @@ -48,7 +43,7 @@ class Dynamic(private val dynamicFunctor: Functor): Goal(), Body { } class Assert(clause: Clause) : AssertZ(clause) { - override val functor: Functor = "assert/1" + override val functor = Functor(Atom("assert"), Integer(1)) } /** diff --git a/tests/interpreter/PreprocessorTests.kt b/tests/interpreter/PreprocessorTests.kt index bf54869..ace7862 100644 --- a/tests/interpreter/PreprocessorTests.kt +++ b/tests/interpreter/PreprocessorTests.kt @@ -6,7 +6,6 @@ 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.* @@ -612,7 +611,7 @@ class PreprocessorTests { Atom("declaration/1") ) ) - val expected = Dynamic("declaration/1") + val expected = Dynamic(Functor.of("declaration/1")) val result = preprocessor.preprocess(input) diff --git a/tests/parser/grammars/LogicGrammarTests.kt b/tests/parser/grammars/LogicGrammarTests.kt index 57a1f99..cbcb949 100644 --- a/tests/parser/grammars/LogicGrammarTests.kt +++ b/tests/parser/grammars/LogicGrammarTests.kt @@ -2,7 +2,6 @@ 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 @@ -14,7 +13,7 @@ import prolog.ast.logic.Rule import prolog.ast.terms.CompoundTerm import prolog.ast.terms.Structure import prolog.ast.terms.Variable -import prolog.builtins.Conjunction +import prolog.ast.terms.Functor class LogicGrammarTests { private lateinit var parser: Grammar> @@ -94,13 +93,13 @@ class LogicGrammarTests { assertTrue(rule.head is Structure, "Expected head to be a structure") val head = rule.head as Structure - assertEquals("parent/2", head.functor, "Expected functor 'parent/2'") + assertEquals(Functor.of("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("father/2", body.functor, "Expected functor 'father/2'") + assertEquals(Functor.of("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'") } @@ -125,12 +124,12 @@ class LogicGrammarTests { assertEquals(1, result.size, "Expected 1 rule") val rule = result[0] as Rule - assertEquals("guest/2", rule.head.functor, "Expected functor 'guest/2'") - assertEquals(",/2", (rule.body as CompoundTerm).functor, "Expected functor ',/2'") + assertEquals(Functor.of("guest/2"), rule.head.functor, "Expected functor 'guest/2'") + assertEquals(Functor.of(",/2"), (rule.body as CompoundTerm).functor, "Expected functor ',/2'") val l1 = (rule.body as CompoundTerm).arguments[0] as CompoundTerm - assertEquals(",/2", l1.functor, "Expected functor ',/2'") + assertEquals(Functor.of(",/2"), l1.functor, "Expected functor ',/2'") val l2 = l1.arguments[0] as CompoundTerm - assertEquals("invited/2", l2.functor, "Expected functor 'invited/2'") + assertEquals(Functor.of("invited/2"), l2.functor, "Expected functor 'invited/2'") } @Test @@ -157,6 +156,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("/_", rule.head.functor, "Expected a constraint") + assertEquals(Functor.of("/0"), 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 new file mode 100644 index 0000000..dbd3b03 --- /dev/null +++ b/tests/prolog/builtins/AnalysisOperatorsTests.kt @@ -0,0 +1,404 @@ +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 73cfef0..51a27c3 100644 --- a/tests/prolog/builtins/DatabaseOperatorsTests.kt +++ b/tests/prolog/builtins/DatabaseOperatorsTests.kt @@ -8,7 +8,6 @@ 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 @@ -40,7 +39,7 @@ class DatabaseOperatorsTests { createAssert(fact).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(fact, Program.db.predicates["a/_"]!!.clauses[0]) + assertEquals(fact, Program.db.predicates[Functor.of("a/_")]!!.clauses[0]) } @Test @@ -49,7 +48,7 @@ class DatabaseOperatorsTests { createAssert(fact).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(fact, Program.db.predicates["a/1"]!!.clauses[0]) + assertEquals(fact, Program.db.predicates[Functor.of("a/1")]!!.clauses[0]) } @Test @@ -61,7 +60,7 @@ class DatabaseOperatorsTests { createAssert(rule).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(rule, Program.db.predicates["a/1"]!!.clauses[0]) + assertEquals(rule, Program.db.predicates[Functor.of("a/1")]!!.clauses[0]) } } @@ -92,8 +91,8 @@ class DatabaseOperatorsTests { AssertA(rule2).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[0]) - assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[1]) + assertEquals(rule2, Program.db.predicates[Functor.of("a/1")]!!.clauses[0]) + assertEquals(rule1, Program.db.predicates[Functor.of("a/1")]!!.clauses[1]) } } @@ -117,8 +116,8 @@ class DatabaseOperatorsTests { AssertZ(rule2).satisfy(emptyMap()) assertEquals(1, Program.db.predicates.size, "Expected 1 predicate") - assertEquals(rule1, Program.db.predicates["a/1"]!!.clauses[0]) - assertEquals(rule2, Program.db.predicates["a/1"]!!.clauses[1]) + assertEquals(rule1, Program.db.predicates[Functor.of("a/1")]!!.clauses[0]) + assertEquals(rule2, Program.db.predicates[Functor.of("a/1")]!!.clauses[1]) } } @@ -309,20 +308,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["a/1"]!!.clauses.size, "Expected 3 clauses") + assertEquals(3, Program.db.predicates[Functor.of("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") + assertEquals(0, Program.db.predicates[Functor.of("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" + val predicateFunctor = Functor.of("$predicateName/1") assertFalse(predicateFunctor in Program.db.predicates, "Expected predicate to not exist before")