diff --git a/src/prolog/components/Program.kt b/src/prolog/Program.kt similarity index 84% rename from src/prolog/components/Program.kt rename to src/prolog/Program.kt index 36760f7..9d8e126 100644 --- a/src/prolog/components/Program.kt +++ b/src/prolog/Program.kt @@ -1,12 +1,15 @@ -package prolog.components +package prolog -import prolog.Substituted +import prolog.logic.Substituted +import prolog.ast.logic.Clause +import prolog.ast.logic.Fact +import prolog.ast.logic.Predicate +import prolog.ast.logic.Resolvent +import prolog.ast.terms.Functor +import prolog.ast.terms.Goal import prolog.builtins.True -import prolog.components.expressions.Clause -import prolog.components.expressions.Fact -import prolog.components.expressions.Predicate -import prolog.components.terms.Functor -import prolog.components.terms.Goal + +typealias Database = Program /** * Prolog Program or database. @@ -29,7 +32,7 @@ object Program: Resolvent { * Queries the program with a goal. * @return true if the goal can be proven, false otherwise. */ - fun query(goal: Goal): Boolean = solve(goal, emptyMap()).toList().isNotEmpty() + fun query(goal: Goal): Sequence = solve(goal, emptyMap()) override fun solve(goal: Goal, subs: Substituted): Sequence { val functor = goal.functor @@ -74,6 +77,4 @@ object Program: Resolvent { predicates = emptyMap() setup() } -} - -typealias Database = Program +} \ No newline at end of file diff --git a/src/prolog/components/expressions/Clause.kt b/src/prolog/ast/logic/Clause.kt similarity index 78% rename from src/prolog/components/expressions/Clause.kt rename to src/prolog/ast/logic/Clause.kt index baedeea..e821ce0 100644 --- a/src/prolog/components/expressions/Clause.kt +++ b/src/prolog/ast/logic/Clause.kt @@ -1,18 +1,19 @@ -package prolog.components.expressions +package prolog.ast.logic -import prolog.Substituted +import prolog.logic.Substituted +import prolog.ast.terms.Body +import prolog.ast.terms.Functor +import prolog.ast.terms.Goal +import prolog.ast.terms.Head import prolog.builtins.True -import prolog.builtins.equivalent -import prolog.components.Resolvent -import prolog.components.terms.* -import prolog.unifyLazy +import prolog.logic.unifyLazy /** * ‘Sentence’ of a Prolog program. * - * A clause consists of a [Head] and body separated by the [neck][prolog.terms.Neck] operator, or it is a [Fact]. + * A clause consists of a [Head] and body separated by the neck operator, or it is a [Fact]. * - * @see [prolog.components.terms.Variable] + * @see [prolog.ast.terms.Variable] * @see [Predicate] */ abstract class Clause(private val head: Head, private val body: Body) : Resolvent { @@ -40,4 +41,4 @@ abstract class Clause(private val head: Head, private val body: Body) : Resolven else -> "$head :- $body" } } -} +} \ No newline at end of file diff --git a/src/prolog/ast/logic/Fact.kt b/src/prolog/ast/logic/Fact.kt new file mode 100644 index 0000000..3288836 --- /dev/null +++ b/src/prolog/ast/logic/Fact.kt @@ -0,0 +1,6 @@ +package prolog.ast.logic + +import prolog.ast.terms.Head +import prolog.builtins.True + +class Fact(head: Head) : Clause(head, True()) \ No newline at end of file diff --git a/src/prolog/components/expressions/Predicate.kt b/src/prolog/ast/logic/Predicate.kt similarity index 85% rename from src/prolog/components/expressions/Predicate.kt rename to src/prolog/ast/logic/Predicate.kt index 964fa67..6a8ec75 100644 --- a/src/prolog/components/expressions/Predicate.kt +++ b/src/prolog/ast/logic/Predicate.kt @@ -1,9 +1,8 @@ -package prolog.components.expressions +package prolog.ast.logic -import prolog.Substituted -import prolog.components.Resolvent -import prolog.components.terms.Functor -import prolog.components.terms.Goal +import prolog.logic.Substituted +import prolog.ast.terms.Functor +import prolog.ast.terms.Goal /** * Collection of [Clause]s with the same [Functor]. @@ -37,7 +36,7 @@ class Predicate : Resolvent { * Adds a clause to the predicate. */ fun add(clause: Clause) { - require (clause.functor == functor) { "Clause functor does not match predicate functor" } + require(clause.functor == functor) { "Clause functor does not match predicate functor" } clauses.add(clause) } diff --git a/src/prolog/components/Provable.kt b/src/prolog/ast/logic/Provable.kt similarity index 84% rename from src/prolog/components/Provable.kt rename to src/prolog/ast/logic/Provable.kt index 1f0c354..7bc4685 100644 --- a/src/prolog/components/Provable.kt +++ b/src/prolog/ast/logic/Provable.kt @@ -1,6 +1,6 @@ -package prolog.components +package prolog.ast.logic -import prolog.Substituted +import prolog.logic.Substituted interface Provable { /** diff --git a/src/prolog/components/Resolvent.kt b/src/prolog/ast/logic/Resolvent.kt similarity index 82% rename from src/prolog/components/Resolvent.kt rename to src/prolog/ast/logic/Resolvent.kt index aa87e33..5f6c1bb 100644 --- a/src/prolog/components/Resolvent.kt +++ b/src/prolog/ast/logic/Resolvent.kt @@ -1,7 +1,7 @@ -package prolog.components +package prolog.ast.logic -import prolog.Substituted -import prolog.components.terms.Goal +import prolog.logic.Substituted +import prolog.ast.terms.Goal /** * Can be instructed to solve a goal. diff --git a/src/prolog/ast/logic/Rule.kt b/src/prolog/ast/logic/Rule.kt new file mode 100644 index 0000000..9eba36e --- /dev/null +++ b/src/prolog/ast/logic/Rule.kt @@ -0,0 +1,6 @@ +package prolog.ast.logic + +import prolog.ast.terms.Body +import prolog.ast.terms.Head + +class Rule(head: Head, body: Body) : Clause(head, body) \ No newline at end of file diff --git a/src/prolog/components/terms/Atom.kt b/src/prolog/ast/terms/Atom.kt similarity index 58% rename from src/prolog/components/terms/Atom.kt rename to src/prolog/ast/terms/Atom.kt index 6b7baae..c711590 100644 --- a/src/prolog/components/terms/Atom.kt +++ b/src/prolog/ast/terms/Atom.kt @@ -1,8 +1,8 @@ -package prolog.components.terms +package prolog.ast.terms -import prolog.Substituted -import prolog.components.Resolvent -import prolog.unifyLazy +import prolog.ast.logic.Resolvent +import prolog.logic.Substituted +import prolog.logic.unifyLazy open class Atom(val name: String) : Goal(), Head, Body, Resolvent { override val functor: Functor = "$name/_" @@ -11,14 +11,14 @@ open class Atom(val name: String) : Goal(), Head, Body, Resolvent { override fun compareTo(other: Term): Int { return when (other) { - is Variable -> 1 - is Atom -> name.compareTo(other.name) + is Variable -> 1 + is Atom -> name.compareTo(other.name) is Structure -> -1 - else -> throw IllegalArgumentException("Cannot compare $this with $other") + else -> throw IllegalArgumentException("Cannot compare $this with $other") } } override fun toString(): String { return name } -} +} \ No newline at end of file diff --git a/src/prolog/ast/terms/Body.kt b/src/prolog/ast/terms/Body.kt new file mode 100644 index 0000000..b7b4469 --- /dev/null +++ b/src/prolog/ast/terms/Body.kt @@ -0,0 +1,5 @@ +package prolog.ast.terms + +import prolog.ast.logic.Provable + +interface Body : Provable \ No newline at end of file diff --git a/src/prolog/components/terms/Goal.kt b/src/prolog/ast/terms/Goal.kt similarity index 76% rename from src/prolog/components/terms/Goal.kt rename to src/prolog/ast/terms/Goal.kt index 1d39813..6d29ffb 100644 --- a/src/prolog/components/terms/Goal.kt +++ b/src/prolog/ast/terms/Goal.kt @@ -1,8 +1,8 @@ -package prolog.components.terms +package prolog.ast.terms -import prolog.Substituted -import prolog.components.Program -import prolog.components.Provable +import prolog.Program +import prolog.ast.logic.Provable +import prolog.logic.Substituted /** * Ask the Prolog engine. @@ -15,4 +15,4 @@ abstract class Goal : Term, Provable { abstract val functor: Functor override fun prove(subs: Substituted): Sequence = Program.solve(this, subs) -} +} \ No newline at end of file diff --git a/src/prolog/ast/terms/Head.kt b/src/prolog/ast/terms/Head.kt new file mode 100644 index 0000000..71b4e8a --- /dev/null +++ b/src/prolog/ast/terms/Head.kt @@ -0,0 +1,10 @@ +package prolog.ast.terms + +/** + * Part of a [Clause][prolog.ast.logic.Clause] before the neck operator. + */ +interface Head : Term { + val functor: Functor +} + +typealias Functor = String diff --git a/src/prolog/components/expressions/Operator.kt b/src/prolog/ast/terms/Operator.kt similarity index 70% rename from src/prolog/components/expressions/Operator.kt rename to src/prolog/ast/terms/Operator.kt index 5d7331e..20d8764 100644 --- a/src/prolog/components/expressions/Operator.kt +++ b/src/prolog/ast/terms/Operator.kt @@ -1,12 +1,7 @@ -package prolog.components.expressions +package prolog.ast.terms -import prolog.Substituted -import prolog.components.Provable -import prolog.components.terms.Atom -import prolog.components.terms.CompoundTerm -import prolog.components.terms.Goal - -typealias Operand = Goal +import prolog.ast.logic.Provable +import prolog.logic.Substituted abstract class Operator( private val symbol: Atom, @@ -22,3 +17,5 @@ abstract class Operator( } } } + +typealias Operand = Goal diff --git a/src/prolog/components/terms/Structure.kt b/src/prolog/ast/terms/Structure.kt similarity index 89% rename from src/prolog/components/terms/Structure.kt rename to src/prolog/ast/terms/Structure.kt index 2f74d78..26e3ae3 100644 --- a/src/prolog/components/terms/Structure.kt +++ b/src/prolog/ast/terms/Structure.kt @@ -1,13 +1,15 @@ -package prolog.components.terms +package prolog.ast.terms -import prolog.Substituted +import prolog.ast.logic.Resolvent import prolog.builtins.equivalent -import prolog.components.Resolvent -import prolog.unifyLazy +import prolog.logic.Substituted +import prolog.logic.unifyLazy typealias Argument = Term -open class Structure(val name: Atom, val arguments: List): Goal(), Head, Body, Resolvent { +typealias CompoundTerm = Structure + +open class Structure(val name: Atom, val arguments: List) : Goal(), Head, Body, Resolvent { override val functor: Functor = "${name.name}/${arguments.size}" override fun solve(goal: Goal, subs: Substituted): Sequence { @@ -38,6 +40,4 @@ open class Structure(val name: Atom, val arguments: List): Goal(), Hea else -> "${name.name}(${arguments.joinToString(", ")})" } } -} - -typealias CompoundTerm = Structure +} \ No newline at end of file diff --git a/src/prolog/ast/terms/Term.kt b/src/prolog/ast/terms/Term.kt new file mode 100644 index 0000000..80d338f --- /dev/null +++ b/src/prolog/ast/terms/Term.kt @@ -0,0 +1,9 @@ +package prolog.ast.terms + +/** + * Value in Prolog. + * + * A [Term] is either a [Variable], [Atom], integer, float or [CompoundTerm]. + * In addition, SWI-Prolog also defines the type string. + */ +interface Term : Comparable \ No newline at end of file diff --git a/src/prolog/components/terms/Variable.kt b/src/prolog/ast/terms/Variable.kt similarity index 82% rename from src/prolog/components/terms/Variable.kt rename to src/prolog/ast/terms/Variable.kt index 0da4ad8..429d408 100644 --- a/src/prolog/components/terms/Variable.kt +++ b/src/prolog/ast/terms/Variable.kt @@ -1,6 +1,6 @@ -package prolog.components.terms +package prolog.ast.terms -import java.util.Optional +import java.util.* data class Variable(val name: String) : Term { private var alias: Optional = Optional.empty() @@ -23,9 +23,9 @@ data class Variable(val name: String) : Term { override fun compareTo(other: Term): Int { return when (other) { - is Variable -> name.compareTo(other.name) + is Variable -> name.compareTo(other.name) // Variables are always less than atoms - else -> -1 + else -> -1 } } @@ -35,4 +35,4 @@ data class Variable(val name: String) : Term { else -> name } } -} +} \ No newline at end of file diff --git a/src/prolog/builtins/arithmetic.kt b/src/prolog/builtins/arithmetic.kt new file mode 100644 index 0000000..6021440 --- /dev/null +++ b/src/prolog/builtins/arithmetic.kt @@ -0,0 +1 @@ +package prolog.builtins diff --git a/src/prolog/builtins/control.kt b/src/prolog/builtins/control.kt index b2bb83a..c2eebea 100644 --- a/src/prolog/builtins/control.kt +++ b/src/prolog/builtins/control.kt @@ -1,15 +1,12 @@ package prolog.builtins -import prolog.Substituted -import prolog.components.expressions.Operand -import prolog.components.expressions.Operator -import prolog.components.terms.Atom -import prolog.components.terms.Body +import prolog.ast.terms.* +import prolog.logic.Substituted /** * Always fail. */ -class Fail: Atom("fail"), Body { +class Fail : Atom("fail"), Body { override fun prove(subs: Substituted): Sequence = emptySequence() } @@ -21,7 +18,7 @@ typealias False = Fail /** * Always succeed. */ -class True: Atom("true"), Body { +class True : Atom("true"), Body { override fun prove(subs: Substituted): Sequence = sequenceOf(emptyMap()) } @@ -49,7 +46,7 @@ class Conjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(" /** * Disjunction (or). True if either Goal1 or Goal2 succeeds. */ -class Disjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(";"), leftOperand, rightOperand) { +open class Disjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(";"), leftOperand, rightOperand) { override fun prove(subs: Substituted): Sequence = sequence { if (leftOperand != null) { yieldAll(leftOperand.prove(subs)) @@ -57,3 +54,24 @@ class Disjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(" yieldAll(rightOperand.prove(subs)) } } + +@Deprecated("Use Disjunction instead") +class Bar(leftOperand: Operand, rightOperand: Operand) : Disjunction(leftOperand, rightOperand) + +// TODO -> + +// TODO *-> + +/** + * True if 'Goal' cannot be proven. + */ +class Not(goal: Goal) : Operator(Atom("\\+"), rightOperand = goal) { + override fun prove(subs: Substituted): Sequence { + // If the goal can be proven, return an empty sequence + if (rightOperand.prove(subs).toList().isNotEmpty()) { + return emptySequence() + } + // If the goal cannot be proven, return a sequence with an empty map + return sequenceOf(emptyMap()) + } +} diff --git a/src/prolog/builtins/meta.kt b/src/prolog/builtins/meta.kt new file mode 100644 index 0000000..6021440 --- /dev/null +++ b/src/prolog/builtins/meta.kt @@ -0,0 +1 @@ +package prolog.builtins diff --git a/src/prolog/builtins/other.kt b/src/prolog/builtins/other.kt index b2a818b..3b3ed3d 100644 --- a/src/prolog/builtins/other.kt +++ b/src/prolog/builtins/other.kt @@ -1,9 +1,9 @@ package prolog.builtins -import prolog.Substituted -import prolog.components.expressions.Operand -import prolog.components.expressions.Operator -import prolog.components.terms.Atom +import prolog.ast.terms.Atom +import prolog.ast.terms.Operand +import prolog.ast.terms.Operator +import prolog.logic.Substituted class Query(rightOperand: Operand) : Operator(Atom("?-"), null, rightOperand) { override fun prove(subs: Substituted): Sequence = rightOperand.prove(subs) diff --git a/src/prolog/builtins/terms.kt b/src/prolog/builtins/terms.kt index d7a09c6..744e1b5 100644 --- a/src/prolog/builtins/terms.kt +++ b/src/prolog/builtins/terms.kt @@ -1,7 +1,7 @@ package prolog.builtins -import prolog.components.terms.Atom -import prolog.components.terms.Term +import prolog.ast.terms.Atom +import prolog.ast.terms.Term /** * True when Term is a term with functor Name/Arity. If Term is a variable it is unified with a new term whose diff --git a/src/prolog/builtins/unification.kt b/src/prolog/builtins/unification.kt index b4b1100..ffb75bc 100644 --- a/src/prolog/builtins/unification.kt +++ b/src/prolog/builtins/unification.kt @@ -1,9 +1,9 @@ package prolog.builtins -import prolog.components.terms.Atom -import prolog.components.terms.Structure -import prolog.components.terms.Term -import prolog.components.terms.Variable +import prolog.ast.terms.Atom +import prolog.ast.terms.Structure +import prolog.ast.terms.Term +import prolog.ast.terms.Variable /** * True if Term1 is equivalent to Term2. A variable is only identical to a sharing variable. @@ -18,3 +18,7 @@ fun equivalent(term1: Term, term2: Term): Boolean { else -> false } } + +/** + * + */ diff --git a/src/prolog/builtins/verification.kt b/src/prolog/builtins/verification.kt index 5b83659..8bb2cb1 100644 --- a/src/prolog/builtins/verification.kt +++ b/src/prolog/builtins/verification.kt @@ -1,8 +1,8 @@ package prolog.builtins -import prolog.components.terms.CompoundTerm -import prolog.components.terms.Term -import prolog.components.terms.Variable +import prolog.ast.terms.CompoundTerm +import prolog.ast.terms.Term +import prolog.ast.terms.Variable /** * True if [Term] is bound (i.e., not a variable) and is not compound. diff --git a/src/prolog/components/expressions/Fact.kt b/src/prolog/components/expressions/Fact.kt deleted file mode 100644 index 2a7ccc5..0000000 --- a/src/prolog/components/expressions/Fact.kt +++ /dev/null @@ -1,6 +0,0 @@ -package prolog.components.expressions - -import prolog.builtins.True -import prolog.components.terms.Head - -class Fact(head: Head) : Clause(head, True()) diff --git a/src/prolog/components/expressions/Rule.kt b/src/prolog/components/expressions/Rule.kt deleted file mode 100644 index ce4570b..0000000 --- a/src/prolog/components/expressions/Rule.kt +++ /dev/null @@ -1,6 +0,0 @@ -package prolog.components.expressions - -import prolog.components.terms.Body -import prolog.components.terms.Head - -class Rule(head: Head, body: Body): Clause(head, body) diff --git a/src/prolog/components/terms/Body.kt b/src/prolog/components/terms/Body.kt deleted file mode 100644 index 838b076..0000000 --- a/src/prolog/components/terms/Body.kt +++ /dev/null @@ -1,5 +0,0 @@ -package prolog.components.terms - -import prolog.components.Provable - -interface Body : Provable diff --git a/src/prolog/components/terms/Head.kt b/src/prolog/components/terms/Head.kt deleted file mode 100644 index fbd9b82..0000000 --- a/src/prolog/components/terms/Head.kt +++ /dev/null @@ -1,10 +0,0 @@ -package prolog.components.terms - -/** - * Part of a [Clause][prolog.components.expressions.Clause] before the [neck][prolog.terms.Neck] operator. - */ -interface Head : Term { - val functor: Functor -} - -typealias Functor = String diff --git a/src/prolog/components/terms/Term.kt b/src/prolog/components/terms/Term.kt deleted file mode 100644 index ec9c4aa..0000000 --- a/src/prolog/components/terms/Term.kt +++ /dev/null @@ -1,23 +0,0 @@ -package prolog.components.terms - -/** - * Value in Prolog. - * - * A [Term] is either a [Variable], [Atom], integer, float or [CompoundTerm]. - * In addition, SWI-Prolog also defines the type string. - */ -interface Term : Comparable - -/* - ::= | - ::= | - ::= . | :- . - ::= | , - ::= | ( ) - ::= | , - ::= | | | - ::= ( ) - ::= ?- . - ::= | - ::= | -*/ diff --git a/src/prolog/unify.kt b/src/prolog/logic/unify.kt similarity index 95% rename from src/prolog/unify.kt rename to src/prolog/logic/unify.kt index a5745bb..2a1e411 100644 --- a/src/prolog/unify.kt +++ b/src/prolog/logic/unify.kt @@ -1,12 +1,12 @@ -package prolog +package prolog.logic +import prolog.ast.terms.Structure +import prolog.ast.terms.Term +import prolog.ast.terms.Variable import prolog.builtins.atomic import prolog.builtins.compound import prolog.builtins.equivalent import prolog.builtins.variable -import prolog.components.terms.Term -import prolog.components.terms.Variable -import prolog.components.terms.Structure import java.util.* typealias Substituted = Map diff --git a/tests/prolog/EvaluationTest.kt b/tests/prolog/EvaluationTest.kt index 5a04c66..50ac65d 100644 --- a/tests/prolog/EvaluationTest.kt +++ b/tests/prolog/EvaluationTest.kt @@ -3,14 +3,15 @@ package prolog import org.junit.jupiter.api.Assertions.* import org.junit.jupiter.api.BeforeEach import org.junit.jupiter.api.Test +import prolog.ast.logic.Fact +import prolog.ast.logic.Rule import prolog.builtins.Conjunction import prolog.builtins.Disjunction -import prolog.components.Program -import prolog.components.expressions.Fact -import prolog.components.expressions.Rule -import prolog.components.terms.Atom -import prolog.components.terms.Structure -import prolog.components.terms.Variable +import prolog.builtins.Query +import prolog.builtins.equivalent +import prolog.ast.terms.Atom +import prolog.ast.terms.Structure +import prolog.ast.terms.Variable class EvaluationTest { @BeforeEach @@ -25,7 +26,7 @@ class EvaluationTest { val result = Program.query(Atom("a")) - assertTrue(result) + assertTrue(result.any()) } @Test @@ -35,7 +36,7 @@ class EvaluationTest { val result = Program.query(Atom("b")) - assertFalse(result) + assertFalse(result.any()) } @Test @@ -44,9 +45,9 @@ class EvaluationTest { val fact2 = Fact(Atom("b")) Program.load(listOf(fact1, fact2)) - assertTrue(Program.query(Atom("a"))) - assertTrue(Program.query(Atom("b"))) - assertFalse(Program.query(Atom("c"))) + assertTrue(Program.query(Atom("a")).any()) + assertTrue(Program.query(Atom("b")).any()) + assertFalse(Program.query(Atom("c")).any()) } @Test @@ -54,7 +55,7 @@ class EvaluationTest { val structure = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) Program.load(listOf(Fact(structure))) - assertTrue(Program.query(Structure(Atom("f"), listOf(Atom("a"), Atom("b"))))) + assertTrue(Program.query(Structure(Atom("f"), listOf(Atom("a"), Atom("b")))).any()) } @Test @@ -63,9 +64,9 @@ class EvaluationTest { val structure2 = Structure(Atom("g"), listOf(Atom("c"), Atom("d"))) Program.load(listOf(Fact(structure1), Fact(structure2))) - assertTrue(Program.query(Structure(Atom("f"), listOf(Atom("a"), Atom("b"))))) - assertTrue(Program.query(Structure(Atom("g"), listOf(Atom("c"), Atom("d"))))) - assertFalse(Program.query(Structure(Atom("h"), listOf(Atom("e"))))) + assertTrue(Program.query(Structure(Atom("f"), listOf(Atom("a"), Atom("b")))).any()) + assertTrue(Program.query(Structure(Atom("g"), listOf(Atom("c"), Atom("d")))).any()) + assertFalse(Program.query(Structure(Atom("h"), listOf(Atom("e")))).any()) } /** @@ -89,8 +90,8 @@ class EvaluationTest { Program.load(listOf(father, mother, parent1, parent2)) - assertTrue(Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy"))))) - assertTrue(Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy"))))) + assertTrue(Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy")))).any()) + assertTrue(Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy")))).any()) } /** @@ -110,19 +111,20 @@ class EvaluationTest { Structure(Atom("father"), listOf(variable1, variable2)), /* ; */ Structure(Atom("mother"), listOf(variable1, variable2)) - )) + ) + ) Program.load(listOf(father, mother, parent)) val result1 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy")))) - assertTrue(result1) + assertTrue(result1.toList().isNotEmpty()) val result2 = Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy")))) - assertTrue(result2) + assertTrue(result2.toList().isNotEmpty()) val result3 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jane")))) - assertFalse(result3) + assertFalse(result3.any()) val result4 = Program.query(Structure(Atom("father"), listOf(Atom("john"), Atom("jane")))) - assertFalse(result4) + assertFalse(result4.any()) } /** @@ -162,18 +164,55 @@ class EvaluationTest { Program.load(listOf(male, female, parent1, parent2, isFather, isMother)) val result1 = Program.query(Structure(Atom("isFather"), listOf(Atom("john"), Atom("jimmy")))) - assertTrue(result1) + assertTrue(result1.any()) val result2 = Program.query(Structure(Atom("isMother"), listOf(Atom("jane"), Atom("jimmy")))) - assertTrue(result2) + assertTrue(result2.any()) val result3 = Program.query(Structure(Atom("isFather"), listOf(Atom("jane"), Atom("jimmy")))) - assertFalse(result3) + assertFalse(result3.any()) val result4 = Program.query(Structure(Atom("isMother"), listOf(Atom("john"), Atom("jimmy")))) - assertFalse(result4) + assertFalse(result4.any()) val result5 = Program.query(Structure(Atom("parent"), listOf(Atom("trudy"), Atom("jimmy")))) - assertFalse(result5) + assertFalse(result5.any()) + } + + @Test + fun requires_backtracking() { + val fact1 = Fact(Structure(Atom("a"), listOf(Atom("b")))) + val fact2 = Fact(Structure(Atom("a"), listOf(Atom("c")))) + val fact3 = Fact(Structure(Atom("a"), listOf(Atom("d")))) + + Program.load(listOf(fact1, fact2, fact3)) + + assertTrue(Program.query(Structure(Atom("a"), listOf(Atom("b")))).any()) + assertTrue(Program.query(Structure(Atom("a"), listOf(Atom("c")))).any()) + assertTrue(Program.query(Structure(Atom("a"), listOf(Atom("d")))).any()) + } + + @Test + fun multiple_choices() { + val fact1 = Fact(Structure(Atom("a"), listOf(Atom("b")))) + val fact2 = Fact(Structure(Atom("a"), listOf(Atom("c")))) + val fact3 = Fact(Structure(Atom("a"), listOf(Atom("d")))) + + Program.load(listOf(fact1, fact2, fact3)) + + val results = Query(Structure(Atom("a"), listOf(Variable("X")))).prove(emptyMap()) + + val expectedResults = listOf( + mapOf(Variable("X") to Atom("b")), + mapOf(Variable("X") to Atom("c")), + mapOf(Variable("X") to Atom("d")) + ) + val actualResults = results.toList() + + assertEquals(expectedResults.size, actualResults.size, "Number of results should match") + for (i in expectedResults.indices) { + assertEquals(expectedResults[i].size, actualResults[i].size, "Substitution size should match") + assertTrue(expectedResults[i].all { actualResults[i][it.key]?.let { it1 -> equivalent(it.value, it1) } ?: false }, "Substitution values should match") + } } } \ No newline at end of file diff --git a/tests/prolog/builtins/ControlBuiltinsTest.kt b/tests/prolog/builtins/ControlBuiltinsTest.kt new file mode 100644 index 0000000..225f386 --- /dev/null +++ b/tests/prolog/builtins/ControlBuiltinsTest.kt @@ -0,0 +1,66 @@ +package prolog.builtins + +import org.junit.jupiter.api.Assertions.assertFalse +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.Test +import prolog.Program +import prolog.ast.logic.Fact +import prolog.ast.terms.Atom + +class ControlBuiltinsTest { + @BeforeEach + fun setUp() { + Program.clear() + } + + @Test + fun not_atom() { + val success = Fact(Atom("a")) + + Program.load(listOf(success)) + + val goal = Atom("a") + val notGoal = Not(goal) + + val result1 = Program.query(goal) + val result2 = Program.query(notGoal) + + assertTrue(result1.any(), "Expected query to succeed") + assertFalse(result2.any(), "Expected query to fail") + } + + @Test + fun not_compound() { + val success = Fact(Atom("f")) + val failure = Fact(Atom("g")) + + Program.load(listOf(success, failure)) + + val goal = Atom("f") + val notGoal = Not(Atom("g")) + + val result1 = Program.query(goal) + val result2 = Program.query(notGoal) + + assertTrue(result1.any(), "Expected query to succeed") + assertFalse(result2.any(), "Expected query to fail") + } + + @Test + fun fail_should_cause_fails() { + val success = Fact(Atom("a")) + val failure = Fact(Atom("b")) + + Program.load(listOf(success, failure)) + + val goal = Atom("a") + val failGoal = Fail() + + val result1 = Program.query(goal) + val result2 = Program.query(failGoal) + + assertTrue(result1.any(), "Expected query to succeed") + assertFalse(result2.any(), "Expected query to fail") + } +} \ No newline at end of file diff --git a/tests/prolog/builtins/TermAnalysisConstructionTest.kt b/tests/prolog/builtins/TermAnalysisConstructionTest.kt index a9c2a5f..a43b6cc 100644 --- a/tests/prolog/builtins/TermAnalysisConstructionTest.kt +++ b/tests/prolog/builtins/TermAnalysisConstructionTest.kt @@ -3,9 +3,8 @@ package prolog.builtins import org.junit.jupiter.api.Assertions.assertFalse import org.junit.jupiter.api.Assertions.assertTrue import org.junit.jupiter.api.Test -import org.junit.jupiter.api.assertThrows -import prolog.components.terms.Atom -import prolog.components.terms.Structure +import prolog.ast.terms.Atom +import prolog.ast.terms.Structure /** * Based on [Predicates for analyzing/constructing terms](https://github.com/dtonhofer/prolog_notes/blob/master/swipl_notes/about_term_analysis_and_construction/term_analysis_construction.png) diff --git a/tests/prolog/builtins/VerificationBuiltinsTest.kt b/tests/prolog/builtins/VerificationBuiltinsTest.kt index a6189ca..b8e5e9b 100644 --- a/tests/prolog/builtins/VerificationBuiltinsTest.kt +++ b/tests/prolog/builtins/VerificationBuiltinsTest.kt @@ -3,12 +3,12 @@ package prolog.builtins import org.junit.jupiter.api.Assertions.assertFalse import org.junit.jupiter.api.Assertions.assertTrue import org.junit.jupiter.api.Test -import prolog.components.terms.Atom -import prolog.components.terms.Structure -import prolog.components.terms.Variable +import prolog.ast.terms.Atom +import prolog.ast.terms.Structure +import prolog.ast.terms.Variable import kotlin.test.assertEquals -class BuiltinsTest { +class VerificationBuiltinsTest { @Test fun unbound_variable_is_var() { val variable = Variable("X") diff --git a/tests/prolog/UnifyTest.kt b/tests/prolog/logic/UnifyTest.kt similarity index 98% rename from tests/prolog/UnifyTest.kt rename to tests/prolog/logic/UnifyTest.kt index 104a7bb..0fe9d94 100644 --- a/tests/prolog/UnifyTest.kt +++ b/tests/prolog/logic/UnifyTest.kt @@ -1,12 +1,12 @@ -package prolog +package prolog.logic import org.junit.jupiter.api.Assertions.* import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test +import prolog.ast.terms.Atom +import prolog.ast.terms.Structure +import prolog.ast.terms.Variable import prolog.builtins.equivalent -import prolog.components.terms.Atom -import prolog.components.terms.Structure -import prolog.components.terms.Variable /* * Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms