From 6469dd6ced84010d4421163d60e56c23d320d35e Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Tue, 15 Apr 2025 12:32:59 +0200 Subject: [PATCH] refactor: Rework --- src/prolog/Program.kt | 5 +- src/prolog/Substitution.kt | 11 + .../ast/arithmetic/ArithmeticOperator.kt | 7 +- src/prolog/ast/arithmetic/Expression.kt | 8 +- src/prolog/ast/arithmetic/Simplification.kt | 6 + src/prolog/ast/logic/Clause.kt | 23 +- src/prolog/ast/logic/LogicOperand.kt | 2 +- src/prolog/ast/logic/LogicOperator.kt | 7 +- src/prolog/ast/logic/Predicate.kt | 5 +- src/prolog/ast/logic/Provable.kt | 14 -- src/prolog/ast/logic/Resolvent.kt | 5 +- src/prolog/ast/logic/Satisfiable.kt | 14 ++ src/prolog/ast/terms/Atom.kt | 19 +- src/prolog/ast/terms/Body.kt | 4 +- src/prolog/ast/terms/Goal.kt | 5 +- src/prolog/ast/terms/Integer.kt | 18 +- src/prolog/ast/terms/Operator.kt | 2 + src/prolog/ast/terms/Structure.kt | 30 +-- src/prolog/ast/terms/Term.kt | 9 +- src/prolog/ast/terms/Variable.kt | 48 +--- src/prolog/ast/terms/VariableBinding.kt | 5 + src/prolog/builtins/arithmeticOperators.kt | 100 +++++---- src/prolog/builtins/controlOperators.kt | 31 +-- src/prolog/builtins/other.kt | 5 +- ...unification.kt => unificationOperators.kt} | 9 +- src/prolog/logic/arithmetic.kt | 89 ++++---- src/prolog/logic/unification.kt | 146 ++++++++---- src/prolog/logic/verification.kt | 13 +- tests/prolog/EvaluationTest.kt | 6 +- .../builtins/ArithmeticOperatorsTests.kt | 211 ++++++++++-------- tests/prolog/builtins/UnificationTest.kt | 9 +- tests/prolog/builtins/VerificationTest.kt | 57 ++--- tests/prolog/logic/ArithmeticTests.kt | 85 ++----- tests/prolog/logic/UnifyTest.kt | 137 ++++++++---- 34 files changed, 593 insertions(+), 552 deletions(-) create mode 100644 src/prolog/Substitution.kt create mode 100644 src/prolog/ast/arithmetic/Simplification.kt delete mode 100644 src/prolog/ast/logic/Provable.kt create mode 100644 src/prolog/ast/logic/Satisfiable.kt create mode 100644 src/prolog/ast/terms/VariableBinding.kt rename src/prolog/builtins/{unification.kt => unificationOperators.kt} (72%) diff --git a/src/prolog/Program.kt b/src/prolog/Program.kt index 1f36b17..46adef1 100644 --- a/src/prolog/Program.kt +++ b/src/prolog/Program.kt @@ -1,6 +1,5 @@ package prolog -import prolog.logic.Substituted import prolog.ast.logic.Clause import prolog.ast.logic.Predicate import prolog.ast.logic.Resolvent @@ -29,9 +28,9 @@ object Program: Resolvent { * Queries the program with a goal. * @return true if the goal can be proven, false otherwise. */ - fun query(goal: Goal): Sequence = solve(goal, emptyMap()) + fun query(goal: Goal): Answers = solve(goal, emptyMap()) - override fun solve(goal: Goal, subs: Substituted): Sequence { + override fun solve(goal: Goal, subs: Substitutions): Answers { val functor = goal.functor // If the predicate does not exist, return false val predicate = predicates[functor] ?: return emptySequence() diff --git a/src/prolog/Substitution.kt b/src/prolog/Substitution.kt new file mode 100644 index 0000000..e9fb28b --- /dev/null +++ b/src/prolog/Substitution.kt @@ -0,0 +1,11 @@ +package prolog + +import prolog.ast.terms.Term + +abstract class Substitution(val from: Term, val to: Term) { + val mapped: Pair? = if (from != to) from to to else null + override fun toString(): String = "$from -> $to" +} +typealias Substitutions = Map +typealias Answer = Result +typealias Answers = Sequence \ No newline at end of file diff --git a/src/prolog/ast/arithmetic/ArithmeticOperator.kt b/src/prolog/ast/arithmetic/ArithmeticOperator.kt index 18ca16d..61550a9 100644 --- a/src/prolog/ast/arithmetic/ArithmeticOperator.kt +++ b/src/prolog/ast/arithmetic/ArithmeticOperator.kt @@ -2,11 +2,6 @@ package prolog.ast.arithmetic import prolog.ast.terms.Atom import prolog.ast.terms.Operator -import prolog.ast.terms.Term -import prolog.logic.Substituted abstract class ArithmeticOperator(symbol: Atom, leftOperand: Expression, rightOperand: Expression) : - Operator(symbol, leftOperand, rightOperand), Expression { - // Operators should overload the evaluate method to perform the operation - abstract override fun evaluate(subs: Substituted): Pair -} + Operator(symbol, leftOperand, rightOperand), Expression diff --git a/src/prolog/ast/arithmetic/Expression.kt b/src/prolog/ast/arithmetic/Expression.kt index cf5eb49..aa57f1a 100644 --- a/src/prolog/ast/arithmetic/Expression.kt +++ b/src/prolog/ast/arithmetic/Expression.kt @@ -1,5 +1,11 @@ package prolog.ast.arithmetic +import prolog.Substitutions import prolog.ast.terms.Term -interface Expression : Term +interface Expression : Term { + /** + * Returns the term that this expression evaluates to. (All the way down.) + */ + fun simplify(subs: Substitutions): Simplification +} diff --git a/src/prolog/ast/arithmetic/Simplification.kt b/src/prolog/ast/arithmetic/Simplification.kt new file mode 100644 index 0000000..c5689d7 --- /dev/null +++ b/src/prolog/ast/arithmetic/Simplification.kt @@ -0,0 +1,6 @@ +package prolog.ast.arithmetic + +import prolog.Substitution +import prolog.ast.terms.Term + +class Simplification(from: Expression, to: Term) : Substitution(from, to) \ No newline at end of file diff --git a/src/prolog/ast/logic/Clause.kt b/src/prolog/ast/logic/Clause.kt index 0160600..b899dd8 100644 --- a/src/prolog/ast/logic/Clause.kt +++ b/src/prolog/ast/logic/Clause.kt @@ -1,6 +1,7 @@ package prolog.ast.logic -import prolog.logic.Substituted +import prolog.Answers +import prolog.Substitutions import prolog.ast.terms.Body import prolog.ast.terms.Functor import prolog.ast.terms.Goal @@ -19,26 +20,26 @@ import prolog.logic.unifyLazy abstract class Clause(private val head: Head, private val body: Body) : Resolvent { val functor: Functor = head.functor - override fun solve(goal: Goal, subs: Substituted): Sequence = sequence { + override fun solve (goal: Goal, subs: Substitutions): Answers = sequence { // If the clause is a rule, unify the goal with the head and then try to prove the body. // Only if the body can be proven, the substitutions should be returned. // Do this in a lazy way. - unifyLazy(goal, head, subs).forEach { newHeadSubs -> - // If the body can be proven, yield the (combined) substitutions - body.prove(subs + newHeadSubs).forEach { newBodySubs -> - yield(newHeadSubs + newBodySubs) - // Unbind the newly bound variables, so they can be reused. - newBodySubs.keys.forEach { it.unbind() } + unifyLazy(goal, head, subs).forEach { headAnswer -> + headAnswer.map { newHeadSubs -> + // If the body can be proven, yield the (combined) substitutions + body.satisfy(subs + newHeadSubs).forEach { bodyAnswer -> + bodyAnswer.map { newBodySubs -> + yield(Result.success(newHeadSubs + newBodySubs)) + } + } } - // Unbind the newly bound variables, so they can be reused. - newHeadSubs.keys.forEach { it.unbind() } } } override fun toString(): String { return when { body is True -> head.toString() - else -> "$head :- $body" + else -> "$head :- $body" } } } \ No newline at end of file diff --git a/src/prolog/ast/logic/LogicOperand.kt b/src/prolog/ast/logic/LogicOperand.kt index 8732b8b..c53bc0d 100644 --- a/src/prolog/ast/logic/LogicOperand.kt +++ b/src/prolog/ast/logic/LogicOperand.kt @@ -2,4 +2,4 @@ package prolog.ast.logic import prolog.ast.terms.Operand -abstract class LogicOperand : Operand, Provable +abstract class LogicOperand : Operand, Satisfiable diff --git a/src/prolog/ast/logic/LogicOperator.kt b/src/prolog/ast/logic/LogicOperator.kt index 632b1ea..5353f0d 100644 --- a/src/prolog/ast/logic/LogicOperator.kt +++ b/src/prolog/ast/logic/LogicOperator.kt @@ -1,13 +1,14 @@ package prolog.ast.logic +import prolog.Answers +import prolog.Substitutions import prolog.ast.terms.Atom import prolog.ast.terms.Operator -import prolog.logic.Substituted abstract class LogicOperator( symbol: Atom, leftOperand: LogicOperand? = null, rightOperand: LogicOperand -) : Operator(symbol, leftOperand, rightOperand), Provable { - abstract override fun prove(subs: Substituted): Sequence +) : Operator(symbol, leftOperand, rightOperand), Satisfiable { + abstract override fun satisfy(subs: Substitutions): Answers } diff --git a/src/prolog/ast/logic/Predicate.kt b/src/prolog/ast/logic/Predicate.kt index 6a8ec75..3a1e3aa 100644 --- a/src/prolog/ast/logic/Predicate.kt +++ b/src/prolog/ast/logic/Predicate.kt @@ -1,6 +1,7 @@ package prolog.ast.logic -import prolog.logic.Substituted +import prolog.Answers +import prolog.Substitutions import prolog.ast.terms.Functor import prolog.ast.terms.Goal @@ -48,7 +49,7 @@ class Predicate : Resolvent { this.clauses.addAll(clauses) } - override fun solve(goal: Goal, subs: Substituted): Sequence = sequence { + override fun solve(goal: Goal, subs: Substitutions): Answers = sequence { require(goal.functor == functor) { "Goal functor does not match predicate functor" } // Try to unify the goal with the clause // If the unification is successful, yield the substitutions diff --git a/src/prolog/ast/logic/Provable.kt b/src/prolog/ast/logic/Provable.kt deleted file mode 100644 index c587f39..0000000 --- a/src/prolog/ast/logic/Provable.kt +++ /dev/null @@ -1,14 +0,0 @@ -package prolog.ast.logic - -import prolog.logic.Substituted - - -interface Provable { - /** - * Proves the current [Provable] instance. - * - * @return a sequence of [Substituted] instances representing the results of the proof. - * If the proof fails, an empty sequence is returned. - */ - fun prove(subs: Substituted): Sequence -} diff --git a/src/prolog/ast/logic/Resolvent.kt b/src/prolog/ast/logic/Resolvent.kt index 5f6c1bb..ad60dae 100644 --- a/src/prolog/ast/logic/Resolvent.kt +++ b/src/prolog/ast/logic/Resolvent.kt @@ -1,6 +1,7 @@ package prolog.ast.logic -import prolog.logic.Substituted +import prolog.Answers +import prolog.Substitutions import prolog.ast.terms.Goal /** @@ -13,5 +14,5 @@ interface Resolvent { * @return A sequence of substitutions that can be applied to the goal to unify it with this resolvent. * If the goal cannot be unified with this resolvent, an empty sequence is returned. */ - fun solve(goal: Goal, subs: Substituted): Sequence + fun solve(goal: Goal, subs: Substitutions): Answers } diff --git a/src/prolog/ast/logic/Satisfiable.kt b/src/prolog/ast/logic/Satisfiable.kt new file mode 100644 index 0000000..d391550 --- /dev/null +++ b/src/prolog/ast/logic/Satisfiable.kt @@ -0,0 +1,14 @@ +package prolog.ast.logic + +import prolog.Answers +import prolog.Substitutions + +interface Satisfiable { + /** + * Proves the current [Satisfiable] instance. + * + * @return a sequence of [Substitutions] instances representing the results of the proof. + * If the proof fails, an empty sequence is returned. + */ + fun satisfy(subs: Substitutions): Answers +} diff --git a/src/prolog/ast/terms/Atom.kt b/src/prolog/ast/terms/Atom.kt index fa8bc30..3c252e5 100644 --- a/src/prolog/ast/terms/Atom.kt +++ b/src/prolog/ast/terms/Atom.kt @@ -1,27 +1,14 @@ package prolog.ast.terms +import prolog.Answers +import prolog.Substitutions 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/_" - override fun solve(goal: Goal, subs: Substituted): Sequence = unifyLazy(goal, this, subs) - - override fun evaluate(subs: Substituted): Pair = Pair(this, emptyMap()) - - /** - * See also [SWI Prolog Standard Order of Terms](https://www.swi-prolog.org/pldoc/man?section=standardorder) - */ - override fun compareTo(other: Term): Int { - return when (other) { - is Variable -> 1 - is Atom -> name.compareTo(other.name) - is Structure -> -1 - else -> throw IllegalArgumentException("Cannot compare $this with $other") - } - } + override fun solve(goal: Goal, subs: Substitutions): Answers = unifyLazy(goal, this, subs) override fun toString(): String { return name diff --git a/src/prolog/ast/terms/Body.kt b/src/prolog/ast/terms/Body.kt index b7b4469..dc61c7d 100644 --- a/src/prolog/ast/terms/Body.kt +++ b/src/prolog/ast/terms/Body.kt @@ -1,5 +1,5 @@ package prolog.ast.terms -import prolog.ast.logic.Provable +import prolog.ast.logic.Satisfiable -interface Body : Provable \ No newline at end of file +interface Body : Satisfiable \ No newline at end of file diff --git a/src/prolog/ast/terms/Goal.kt b/src/prolog/ast/terms/Goal.kt index 342ecb5..e0a5c49 100644 --- a/src/prolog/ast/terms/Goal.kt +++ b/src/prolog/ast/terms/Goal.kt @@ -1,8 +1,9 @@ package prolog.ast.terms +import prolog.Answers import prolog.Program +import prolog.Substitutions import prolog.ast.logic.LogicOperand -import prolog.logic.Substituted /** * Ask the Prolog engine. @@ -14,5 +15,5 @@ import prolog.logic.Substituted abstract class Goal : LogicOperand(), Term { abstract val functor: Functor - override fun prove(subs: Substituted): Sequence = Program.solve(this, subs) + override fun satisfy(subs: Substitutions): Answers = Program.solve(this, subs) } \ No newline at end of file diff --git a/src/prolog/ast/terms/Integer.kt b/src/prolog/ast/terms/Integer.kt index f3f9fcf..d0c96c9 100644 --- a/src/prolog/ast/terms/Integer.kt +++ b/src/prolog/ast/terms/Integer.kt @@ -1,22 +1,12 @@ package prolog.ast.terms +import prolog.Substitutions import prolog.ast.arithmetic.Expression -import prolog.logic.Substituted - -data class Integer(val value: Int): Term, Expression { - /** - * See also [SWI Prolog Standard Order of Terms](https://www.swi-prolog.org/pldoc/man?section=standardorder) - */ - override fun compareTo(other: Term): Int { - return when (other) { - is Variable -> 1 - is Integer -> value.compareTo(other.value) - else -> -1 - } - } +import prolog.ast.arithmetic.Simplification +data class Integer(val value: Int): Expression { // Integers are already evaluated - override fun evaluate(subs: Substituted): Pair = Pair(this, emptyMap()) + override fun simplify(subs: Substitutions): Simplification = Simplification(this, this) override fun toString(): String { return value.toString() diff --git a/src/prolog/ast/terms/Operator.kt b/src/prolog/ast/terms/Operator.kt index 9d0e067..8a5af51 100644 --- a/src/prolog/ast/terms/Operator.kt +++ b/src/prolog/ast/terms/Operator.kt @@ -1,5 +1,7 @@ package prolog.ast.terms +import prolog.ast.arithmetic.Expression + typealias Operand = Term abstract class Operator( diff --git a/src/prolog/ast/terms/Structure.kt b/src/prolog/ast/terms/Structure.kt index e44b51c..0585de9 100644 --- a/src/prolog/ast/terms/Structure.kt +++ b/src/prolog/ast/terms/Structure.kt @@ -1,8 +1,8 @@ package prolog.ast.terms +import prolog.Answers +import prolog.Substitutions import prolog.ast.logic.Resolvent -import prolog.logic.equivalent -import prolog.logic.Substituted import prolog.logic.unifyLazy typealias Argument = Term @@ -12,34 +12,10 @@ 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 fun solve(goal: Goal, subs: Substituted): Sequence { + override fun solve(goal: Goal, subs: Substitutions): Answers { return unifyLazy(goal, this, subs) } - // A structure does not need to be evaluated, so return an empty sequence. - override fun evaluate(subs: Substituted): Pair = Pair(this, emptyMap()) - - /** - * See also [SWI Prolog Standard Order of Terms](https://www.swi-prolog.org/pldoc/man?section=standardorder) - */ - override fun compareTo(other: Term): Int { - when (other) { - is Structure -> { - val arityComparison = arguments.size.compareTo(other.arguments.size) - if (arityComparison != 0) return arityComparison - val nameComparison = name.compareTo(other.name) - if (nameComparison != 0) return nameComparison - arguments.zip(other.arguments).forEach { (arg1, arg2) -> - val argsComparison = equivalent(arg1, arg2) - if (!argsComparison) return arg1.compareTo(arg2) - } - return 0 - } - // Structure is always greater than other terms - else -> return 1 - } - } - override fun toString(): String { return when { arguments.isEmpty() -> name.name diff --git a/src/prolog/ast/terms/Term.kt b/src/prolog/ast/terms/Term.kt index 47f3064..ad5981f 100644 --- a/src/prolog/ast/terms/Term.kt +++ b/src/prolog/ast/terms/Term.kt @@ -1,16 +1,13 @@ package prolog.ast.terms -import prolog.logic.Substituted +import prolog.logic.compare /** * Value in Prolog. * - * A [Term] is either a [Variable], [Atom], integer, float or [CompoundTerm]. + * A [Term] is either a [Variable], [Atom], [Integer], float or [CompoundTerm]. * In addition, SWI-Prolog also defines the type string. */ interface Term : Comparable { - /** - * Returns the term that this expression evaluates to. (All the way down.) - */ - fun evaluate(subs: Substituted): Pair + override fun compareTo(other: Term): Int = compare(this, other, emptyMap()) } diff --git a/src/prolog/ast/terms/Variable.kt b/src/prolog/ast/terms/Variable.kt index 2968bab..713c44d 100644 --- a/src/prolog/ast/terms/Variable.kt +++ b/src/prolog/ast/terms/Variable.kt @@ -1,50 +1,20 @@ package prolog.ast.terms +import prolog.Substitutions import prolog.ast.arithmetic.Expression -import prolog.logic.Substituted -import java.util.* +import prolog.ast.arithmetic.Simplification data class Variable(val name: String) : Term, Expression { - private var alias: Optional = Optional.empty() - - fun alias(): Optional { - return alias - } - - fun bind(term: Term): Optional { - if (alias.isEmpty) { - alias = Optional.of(term) - } - - return alias - } - - fun unbind() { - alias = Optional.empty() - } - - override fun evaluate(subs: Substituted): Pair { + override fun simplify(subs: Substitutions): Simplification { // If the variable is bound, return the value of the binding // If the variable is not bound, return the variable itself - return if (alias.isPresent) { - alias.get().evaluate(subs) - } else { - Pair(this, emptyMap()) + var result = this as Term + if (this in subs) { + val boundTerm = subs[this]!! + result = if (boundTerm is Expression) boundTerm.simplify(subs).to else boundTerm } + return Simplification(this, result) } - override fun compareTo(other: Term): Int { - return when (other) { - is Variable -> name.compareTo(other.name) - // Variables are always less than atoms - else -> -1 - } - } - - override fun toString(): String { - return when { - alias.isPresent -> "$name: ${alias.get()}" - else -> name - } - } + override fun toString(): String = name } \ No newline at end of file diff --git a/src/prolog/ast/terms/VariableBinding.kt b/src/prolog/ast/terms/VariableBinding.kt new file mode 100644 index 0000000..eb51b79 --- /dev/null +++ b/src/prolog/ast/terms/VariableBinding.kt @@ -0,0 +1,5 @@ +package prolog.ast.terms + +import prolog.Substitution + +class VariableBinding(from: Variable, to: Term) : Substitution(from, to) diff --git a/src/prolog/builtins/arithmeticOperators.kt b/src/prolog/builtins/arithmeticOperators.kt index 4b2ac2f..8e44df8 100644 --- a/src/prolog/builtins/arithmeticOperators.kt +++ b/src/prolog/builtins/arithmeticOperators.kt @@ -1,10 +1,11 @@ package prolog.builtins +import prolog.Answers +import prolog.Substitutions import prolog.ast.arithmetic.ArithmeticOperator import prolog.ast.arithmetic.Expression -import prolog.ast.logic.LogicOperand -import prolog.ast.logic.LogicOperator -import prolog.ast.logic.Provable +import prolog.ast.arithmetic.Simplification +import prolog.ast.logic.Satisfiable import prolog.ast.terms.* import prolog.logic.* @@ -20,20 +21,20 @@ import prolog.logic.* * True if expression Expr1 evaluates to a number non-equal to Expr2. */ class EvaluatesToDifferent(private val left: Expression, private val right: Expression) : - ArithmeticOperator(Atom("=\\="), left, right) { - override fun evaluate(subs: Substituted): Pair { - val t1 = left.evaluate(subs) - val t2 = right.evaluate(subs) + Operator(Atom("=\\="), left, right), Satisfiable { + override fun satisfy(subs: Substitutions): Answers { + val t1 = left.simplify(subs) + val t2 = right.simplify(subs) // Should both be instantiated - if (!atomic(t1.first) || !atomic(t2.first)) { - throw IllegalArgumentException("Both operands must be instantiated") + if (!atomic(t1.to, subs) || !atomic(t2.to, subs)) { + return sequenceOf(Result.failure(IllegalArgumentException("Both operands must be instantiated"))) } - return if (equivalent(t1.first, t2.first)) { - Pair(False, emptyMap()) + return if (equivalent(t1.to, t2.to, subs)) { + emptySequence() } else { - Pair(True, t1.second + t2.second) + sequenceOf(Result.success(emptyMap())) } } @@ -43,21 +44,17 @@ class EvaluatesToDifferent(private val left: Expression, private val right: Expr * True if Expr1 evaluates to a number equal to Expr2. */ class EvaluatesTo(private val left: Expression, private val right: Expression) : - ArithmeticOperator(Atom("=:="), left, right) { - override fun evaluate(subs: Substituted): Pair { - val t1 = left.evaluate(subs) - val t2 = right.evaluate(subs) + Operator(Atom("=:="), left, right) { + override fun satisfy(subs: Substitutions): Answers { + val t1 = left.simplify(subs) + val t2 = right.simplify(subs) // Should both be instantiated - if (!atomic(t1.first) || !atomic(t2.first)) { - throw IllegalArgumentException("Both operands must be instantiated") + if (!atomic(t1.to, subs) || !atomic(t2.to, subs)) { + return sequenceOf(Result.failure(IllegalArgumentException("Both operands must be instantiated"))) } - return if (equivalent(t1.first, t2.first)) { - Pair(True, t1.second + t2.second) - } else { - Pair(False, emptyMap()) - } + return if (equivalent(t1.to, t2.to, subs)) sequenceOf(Result.success(emptyMap())) else emptySequence() } } @@ -65,16 +62,20 @@ class EvaluatesTo(private val left: Expression, private val right: Expression) : * True when Number is the value to which Expr evaluates. */ class Is(private val left: Expression, private val right: Expression) : - Operator(Atom("is"), left, right), Provable { - override fun prove(subs: Substituted): Sequence { - val t1 = left.evaluate(subs) - val t2 = right.evaluate(subs) + Operator(Atom("is"), left, right), Satisfiable { + override fun satisfy(subs: Substitutions): Answers { + val t1 = left.simplify(subs) + val t2 = right.simplify(subs) - if (!atomic(t2.first)) { - throw IllegalArgumentException("Arguments are not sufficiently instantiated") + if (!atomic(t2.to, subs)) { + return sequenceOf(Result.failure(IllegalArgumentException("Right operand must be instantiated"))) } - return unifyLazy(t1.first, t2.first, subs).map{ it + t1.second + t2.second } + if (!variable(t1.to, subs) && equivalent(t1.to, t2.to, subs + listOfNotNull(t1.mapped, t2.mapped))) { + return sequenceOf(Result.success(emptyMap())) + } + + return unifyLazy(t1.to, t2.to, subs) } } @@ -93,10 +94,11 @@ class Positive(operand: Expression) : Add(Integer(0), operand) */ open class Add(private val expr1: Expression, private val expr2: Expression) : ArithmeticOperator(Atom("+"), expr1, expr2) { - override fun evaluate(subs: Substituted): Pair { + override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = plus(expr1, expr2, result, subs) - return result.evaluate(map.first().getOrThrow()) + val simplification = result.simplify(map.first().getOrThrow()) + return Simplification(this, simplification.to) } } @@ -105,10 +107,11 @@ open class Add(private val expr1: Expression, private val expr2: Expression) : */ open class Subtract(private val expr1: Expression, private val expr2: Expression) : ArithmeticOperator(Atom("-"), expr1, expr2) { - override fun evaluate(subs: Substituted): Pair { + override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = plus(expr2, result, expr1, subs) - return result.evaluate(map.first().getOrThrow()) + val simplification = result.simplify(map.first().getOrThrow()) + return Simplification(this, simplification.to) } } @@ -118,10 +121,11 @@ open class Subtract(private val expr1: Expression, private val expr2: Expression */ class Multiply(private val expr1: Expression, private val expr2: Expression) : ArithmeticOperator(Atom("*"), expr1, expr2) { - override fun evaluate(subs: Substituted): Pair { + override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = mul(expr1, expr2, result, subs) - return result.evaluate(map.first().getOrThrow()) + val simplification = result.simplify(map.first().getOrThrow()) + return Simplification(this, simplification.to) } } @@ -133,20 +137,24 @@ class Multiply(private val expr1: Expression, private val expr2: Expression) : class Between(private val expr1: Expression, private val expr2: Expression, private val expr3: Expression) : Operator(Atom("between"), expr1, expr2) { - override fun prove(subs: Substituted): Sequence { - val e1 = expr1.evaluate(subs) - val e2 = expr2.evaluate(subs) - val e3 = expr3.evaluate(subs) + override fun satisfy(subs: Substitutions): Answers { + val e1 = expr1.simplify(subs) + val e2 = expr2.simplify(subs) + val e3 = expr3.simplify(subs) - require(e1.first is Integer && e2.first is Integer) { "Arguments must be integers" } + require(e1.to is Integer && e2.to is Integer) { "Arguments must be integers" } - val v1 = e1.first as Integer - val v2 = e2.first as Integer + val v1 = e1.to as Integer + val v2 = e2.to as Integer - return if (variable(e3.first)) { - between(v1, v2, e3.first as Variable).map { it + e1.second + e2.second } + return if (variable(e3.to, subs)) { + between(v1, v2, e3.to as Variable).map { answer -> + answer.mapCatching { it + listOfNotNull(e1.mapped, e2.mapped) } + } } else { - between(v1, v2, e3.first as Integer).map { it + e1.second + e2.second } + between(v1, v2, e3.to as Integer).map { answer -> + answer.mapCatching { it + listOfNotNull(e1.mapped, e2.mapped) } + } } } } diff --git a/src/prolog/builtins/controlOperators.kt b/src/prolog/builtins/controlOperators.kt index 4dfeef9..8f193b9 100644 --- a/src/prolog/builtins/controlOperators.kt +++ b/src/prolog/builtins/controlOperators.kt @@ -1,17 +1,18 @@ package prolog.builtins +import prolog.Answers +import prolog.Substitutions import prolog.ast.logic.LogicOperand import prolog.ast.terms.Atom import prolog.ast.terms.Body import prolog.ast.terms.Goal import prolog.ast.logic.LogicOperator -import prolog.logic.Substituted /** * Always fail. */ object Fail : Atom("fail"), Body { - override fun prove(subs: Substituted): Sequence = emptySequence() + override fun satisfy(subs: Substitutions): Answers = emptySequence() } /** @@ -23,7 +24,7 @@ typealias False = Fail * Always succeed. */ object True : Atom("true"), Body { - override fun prove(subs: Substituted): Sequence = sequenceOf(emptyMap()) + override fun satisfy(subs: Substitutions): Answers = sequenceOf(Result.success(emptyMap())) } // TODO Repeat/0 @@ -34,10 +35,14 @@ object True : Atom("true"), Body { * Conjunction (and). True if both Goal1 and Goal2 are true. */ class Conjunction(private val left: LogicOperand, private val right: LogicOperand) : LogicOperator(Atom(","), left, right) { - override fun prove(subs: Substituted): Sequence = sequence { - left.prove(subs).forEach { left -> - right.prove(subs + left).forEach { right -> - yield(left + right) + override fun satisfy(subs: Substitutions): Answers = sequence { + left.satisfy(subs).forEach { leftResult -> + leftResult.mapCatching { left -> + right.satisfy(subs + left).forEach { rightResult -> + rightResult.map { right -> + yield(Result.success(left + right)) + } + } } } } @@ -48,9 +53,9 @@ class Conjunction(private val left: LogicOperand, private val right: LogicOperan */ open class Disjunction(private val left: LogicOperand, private val right: LogicOperand) : LogicOperator(Atom(";"), left, right) { - override fun prove(subs: Substituted): Sequence = sequence { - yieldAll(left.prove(subs)) - yieldAll(right.prove(subs)) + override fun satisfy(subs: Substitutions): Answers = sequence { + yieldAll(left.satisfy(subs)) + yieldAll(right.satisfy(subs)) } } @@ -65,12 +70,12 @@ class Bar(leftOperand: LogicOperand, rightOperand: LogicOperand) : Disjunction(l * True if 'Goal' cannot be proven. */ class Not(private val goal: Goal) : LogicOperator(Atom("\\+"), rightOperand = goal) { - override fun prove(subs: Substituted): Sequence { + override fun satisfy(subs: Substitutions): Answers { // If the goal can be proven, return an empty sequence - if (goal.prove(subs).toList().isNotEmpty()) { + if (goal.satisfy(subs).toList().isNotEmpty()) { return emptySequence() } // If the goal cannot be proven, return a sequence with an empty map - return sequenceOf(emptyMap()) + return sequenceOf(Result.success(emptyMap())) } } diff --git a/src/prolog/builtins/other.kt b/src/prolog/builtins/other.kt index defb38f..b34d3e0 100644 --- a/src/prolog/builtins/other.kt +++ b/src/prolog/builtins/other.kt @@ -1,10 +1,11 @@ package prolog.builtins +import prolog.Answers +import prolog.Substitutions import prolog.ast.logic.LogicOperand import prolog.ast.terms.Atom import prolog.ast.logic.LogicOperator -import prolog.logic.Substituted class Query(private val query: LogicOperand) : LogicOperator(Atom("?-"), null, query) { - override fun prove(subs: Substituted): Sequence = query.prove(subs) + override fun satisfy(subs: Substitutions): Answers = query.satisfy(subs) } diff --git a/src/prolog/builtins/unification.kt b/src/prolog/builtins/unificationOperators.kt similarity index 72% rename from src/prolog/builtins/unification.kt rename to src/prolog/builtins/unificationOperators.kt index a90616f..c45de52 100644 --- a/src/prolog/builtins/unification.kt +++ b/src/prolog/builtins/unificationOperators.kt @@ -5,20 +5,21 @@ */ package prolog.builtins +import prolog.Answers +import prolog.Substitutions import prolog.ast.terms.Atom import prolog.ast.terms.Operator import prolog.ast.terms.Term -import prolog.logic.Substituted import prolog.logic.applySubstitution import prolog.logic.equivalent class Equivalent(private val term1: Term, private val term2: Term) : Operator(Atom("=="), term1, term2) { - override fun prove(subs: Substituted): Sequence = sequence { + override fun satisfy(subs: Substitutions): Answers = sequence { val t1 = applySubstitution(term1, subs) val t2 = applySubstitution(term2, subs) - if (equivalent(t1, t2)) { - yield(emptyMap()) + if (equivalent(t1, t2, subs)) { + yield(Result.success(emptyMap())) } } } diff --git a/src/prolog/logic/arithmetic.kt b/src/prolog/logic/arithmetic.kt index 979d8f3..8a26a52 100644 --- a/src/prolog/logic/arithmetic.kt +++ b/src/prolog/logic/arithmetic.kt @@ -1,10 +1,12 @@ package prolog.logic +import prolog.Answers +import prolog.Substitution +import prolog.Substitutions import prolog.ast.arithmetic.Expression import prolog.ast.terms.Integer +import prolog.ast.terms.Term import prolog.ast.terms.Variable -import prolog.builtins.Is -import java.util.* /** * Low and High are integers, High ≥Low. @@ -18,9 +20,9 @@ fun between( low: Integer, high: Integer, value: Integer -): Sequence { +): Answers { return if (value.value in low.value..high.value) { - sequenceOf(emptyMap()) + sequenceOf(Result.success(emptyMap())) } else { emptySequence() } @@ -30,10 +32,10 @@ fun between( low: Integer, high: Integer, variable: Variable -): Sequence { +): Answers { return sequence { for (i in low.value..high.value) { - yield(mapOf(variable to Integer(i))) + yield(Result.success(mapOf(variable to Integer(i)))) } } } @@ -46,24 +48,26 @@ fun between( * @throws IllegalArgumentException the domain error not_less_than_zero if called with a negative integer. * E.g. succ(X, 0) fails silently and succ(X, -1) raises a domain error.125 */ -fun succ(term1: Expression, term2: Expression, subs: Substituted): Sequence> { +fun succ(term1: Expression, term2: Expression, subs: Substitutions): Answers { if (term2 is Integer) { require(term2.value >= 0) { "Domain error: not_less_than_zero" } } - val result = plus(term1, Integer(1), term2, subs) // If term1 is a variable, we need to check if it is bound to a negative integer return sequence { - result.forEach { newSubs -> - if (newSubs.isSuccess) { - val t1 = applySubstitution(term1, newSubs.getOrNull()!!) - if (t1 is Variable && t1.alias().isPresent) { - val e1 = t1.evaluate(subs) - if (e1.first is Integer && (e1.first as Integer).value < 0) { - return@sequence + plus(term1, Integer(1), term2, subs).forEach { + it.fold( + onSuccess = { result -> + val t1 = applySubstitution(term1, result) + if (t1 in result) { + val e1 = t1.simplify(result) + if (e1.to is Integer && e1.to.value < 0) { + return@sequence + } } - } - } - yield(newSubs) + yield(Result.success(result)) + }, + onFailure = { yield(Result.success(emptyMap())) } + ) } } } @@ -73,55 +77,56 @@ fun succ(term1: Expression, term2: Expression, subs: Substituted): Sequence> = +fun plus(term1: Expression, term2: Expression, term3: Expression, subs: Substitutions): Answers = operate(term1, term2, term3, subs, Integer::plus, Integer::minus) -fun mul(term1: Expression, term2: Expression, term3: Expression, subs: Substituted): Sequence> = +fun mul(term1: Expression, term2: Expression, term3: Expression, subs: Substitutions): Answers = operate(term1, term2, term3, subs, Integer::times, Integer::div) fun operate( term1: Expression, term2: Expression, term3: Expression, - subs: Substituted, + subs: Substitutions, op: (Integer, Integer) -> Integer, inverseOp: (Integer, Integer) -> Integer -): Sequence> = sequence { +): Answers = sequence { val t1 = applySubstitution(term1, subs) val t2 = applySubstitution(term2, subs) val t3 = applySubstitution(term3, subs) when { - nonvariable(t1) && nonvariable(t2) && nonvariable(t3) -> { - val e1 = t1.evaluate(subs) - val e2 = t2.evaluate(subs) - val e3 = t3.evaluate(subs) + nonvariable(t1, subs) && nonvariable(t2, subs) && nonvariable(t3, subs) -> { + val e1 = t1.simplify(subs) + val e2 = t2.simplify(subs) + val e3 = t3.simplify(subs) - val int3Value = op(e1.first as Integer, e2.first as Integer) - if (int3Value == e3.first as Integer) { - yield(Result.success(e1.second + e2.second + e3.second)) + val int3Value = op(e1.to as Integer, e2.to as Integer) + if (int3Value == e3.to as Integer) { + val opSubs: Substitutions = listOfNotNull(e1.mapped, e2.mapped, e3.mapped) + .filter{ pair: Pair? -> pair != null && !subs.contains(pair.first) } + .toMap() + yield(Result.success(opSubs)) } } - nonvariable(t1) && nonvariable(t2) && variable(t3) -> { - val e1 = t1.evaluate(subs) - val e2 = t2.evaluate(subs) + nonvariable(t1, subs) && nonvariable(t2, subs) && variable(t3, subs) -> { + val e1 = t1.simplify(subs) + val e2 = t2.simplify(subs) - val int3Value = op(e1.first as Integer, e2.first as Integer) + val int3Value = op(e1.to as Integer, e2.to as Integer) val int3 = t3 as Variable - int3.bind(int3Value) - yield(Result.success(mapOf(int3 to int3Value) + e1.second + e2.second)) + yield(Result.success(mapOf(int3 to int3Value) + listOfNotNull(e1.mapped, e2.mapped))) } - ((nonvariable(t1) && variable(t2)) || (variable(t1) && nonvariable(t2))) && nonvariable(t3) -> { - val t = if (nonvariable(t1)) t2 else t1 - val e = if (nonvariable(t1)) t1.evaluate(subs) else t2.evaluate(subs) - val e3 = t3.evaluate(subs) + ((nonvariable(t1, subs) && variable(t2, subs)) || (variable(t1, subs) && nonvariable(t2, subs))) && nonvariable(t3, subs) -> { + val t = if (nonvariable(t1, subs)) t2 else t1 + val e = if (nonvariable(t1, subs)) t1.simplify(subs) else t2.simplify(subs) + val e3 = t3.simplify(subs) - val value = inverseOp(e3.first as Integer, e.first as Integer) + val value = inverseOp(e3.to as Integer, e.to as Integer) val int = t as Variable - int.bind(value) - yield(Result.success(mapOf(int to value) + e.second + e3.second)) + yield(Result.success(mapOf(int to value) + listOfNotNull(e.mapped, e3.mapped))) } else -> { diff --git a/src/prolog/logic/unification.kt b/src/prolog/logic/unification.kt index aae0669..a7b6274 100644 --- a/src/prolog/logic/unification.kt +++ b/src/prolog/logic/unification.kt @@ -1,26 +1,27 @@ package prolog.logic +import prolog.Answer +import prolog.Answers +import prolog.Substitutions import prolog.ast.arithmetic.Expression import prolog.ast.logic.LogicOperator import prolog.ast.terms.* -import java.util.* - -typealias Substituted = Map +import kotlin.NoSuchElementException // Apply substitutions to a term -fun applySubstitution(term: Term, subs: Substituted): Term = when { - variable(term) -> subs[(term as Variable)] ?: term - atomic(term) -> term - compound(term) -> { +fun applySubstitution(term: Term, subs: Substitutions): Term = when { + variable(term, emptyMap()) -> subs[(term as Variable)] ?: term + atomic(term, subs) -> term + compound(term, subs) -> { val structure = term as Structure Structure(structure.name, structure.arguments.map { applySubstitution(it, subs) }) } else -> term } - -fun applySubstitution(expr: Expression, subs: Substituted): Expression = when { - variable(expr) -> applySubstitution(expr as Term, subs) as Expression - atomic(expr) -> expr +//TODO Combine with the other applySubstitution function +fun applySubstitution(expr: Expression, subs: Substitutions): Expression = when { + variable(expr, subs) -> applySubstitution(expr as Term, subs) as Expression + atomic(expr, subs) -> expr expr is LogicOperator -> { expr.arguments = expr.arguments.map { applySubstitution(it, subs) } expr @@ -29,71 +30,138 @@ fun applySubstitution(expr: Expression, subs: Substituted): Expression = when { } // Check if a variable occurs in a term -private fun occurs(variable: Variable, term: Term): Boolean = when { - variable(term) -> term == variable - atomic(term) -> false - compound(term) -> { +private fun occurs(variable: Variable, term: Term, subs: Substitutions): Boolean = when { + variable(term, subs) -> term == variable + atomic(term, subs) -> false + compound(term, subs) -> { val structure = term as Structure - structure.arguments.any { occurs(variable, it) } + structure.arguments.any { occurs(variable, it, subs) } } else -> false } // Unify two terms with backtracking and lazy evaluation -fun unifyLazy(term1: Term, term2: Term, subs: Substituted): Sequence = sequence { +fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence { val t1 = applySubstitution(term1, subs) val t2 = applySubstitution(term2, subs) when { - equivalent(t1, t2) -> yield(subs) - variable(t1) -> { + equivalent(t1, t2, subs) -> yield(Result.success(subs)) + variable(t1, subs) -> { val variable = t1 as Variable - if (!occurs(variable, t2)) { - variable.bind(t2) - yield(subs + (variable to t2)) + if (!occurs(variable, t2, subs)) { + yield(Result.success(subs + (variable to t2))) } } - variable(t2) -> { + variable(t2, subs) -> { val variable = t2 as Variable - if (!occurs(variable, t1)) { - variable.bind(t1) - yield(subs + (variable to t1)) + if (!occurs(variable, t1, subs)) { + yield(Result.success(subs + (variable to t1))) } } - compound(t1) && compound(t2) -> { + compound(t1, subs) && compound(t2, subs) -> { val structure1 = t1 as Structure val structure2 = t2 as Structure if (structure1.functor == structure2.functor) { - val newSubstitution = structure1.arguments.zip(structure2.arguments).fold(subs) { acc, (arg1, arg2) -> - unifyLazy(arg1, arg2, acc).firstOrNull() ?: return@sequence + // Unify each argument at the same time, and yield the result + val args1 = structure1.arguments + val args2 = structure2.arguments + if (args1.size == args2.size) { + val results = args1.zip(args2).map { (arg1, arg2) -> + unifyLazy(arg1, arg2, subs) + } + // Combine the results of all unifications + val combinedResults = results.reduce { acc, result -> + acc.flatMap { a -> result.map { b -> + if (a.isSuccess && b.isSuccess) a.getOrThrow() + b.getOrThrow() else emptyMap() + } }.map { Result.success(it) } + } + yieldAll(combinedResults) } - yield(newSubstitution) } } else -> {} } } -fun unify(term1: Term, term2: Term): Optional { +fun unify(term1: Term, term2: Term): Answer { val substitutions = unifyLazy(term1, term2, emptyMap()).toList() return if (substitutions.isNotEmpty()) { - Optional.of(substitutions.first()) + substitutions.first() } else { - Optional.empty() + Result.failure(NoSuchElementException()) } } /** * True if Term1 is equivalent to Term2. A variable is only identical to a sharing variable. */ -fun equivalent(term1: Term, term2: Term): Boolean { +fun equivalent(term1: Term, term2: Term, subs: Substitutions): Boolean { return when { - term1 is Atom && term2 is Atom -> term1.compareTo(term2) == 0 - term1 is Structure && term2 is Structure -> term1.compareTo(term2) == 0 - term1 is Integer && term2 is Integer -> term1.compareTo(term2) == 0 + term1 is Atom && term2 is Atom -> compare(term1, term2, subs) == 0 + term1 is Structure && term2 is Structure -> compare(term1, term2, subs) == 0 + term1 is Integer && term2 is Integer -> compare(term1, term2, subs) == 0 term1 is Variable && term2 is Variable -> term1 == term2 - term1 is Variable -> term1.alias().isPresent && equivalent(term1.alias().get(), term2) - term2 is Variable -> term2.alias().isPresent && equivalent(term2.alias().get(), term1) + term1 is Variable -> term1 in subs && equivalent(subs[term1]!!, term2, subs) + term2 is Variable -> term2 in subs && equivalent(subs[term2]!!, term1, subs) else -> false } } + +/** + * See also [SWI Prolog Standard Order of Terms](https://www.swi-prolog.org/pldoc/man?section=standardorder) + */ +fun compare(term1: Term, term2: Term, subs: Substitutions): Int { + val t1 = applySubstitution(term1, subs) + val t2 = applySubstitution(term2, subs) + + return when (t1) { + is Variable -> { + when (t2) { + is Variable -> t1.name.compareTo(t2.name) + is Integer -> -1 + is Atom -> -1 + is Structure -> -1 + else -> throw IllegalArgumentException("Cannot compare $t1 with $t2") + } + } + is Integer -> { + when (t2) { + is Variable -> 1 + is Integer -> t1.value.compareTo(t2.value) + is Atom -> -1 + is Structure -> -1 + else -> throw IllegalArgumentException("Cannot compare $t1 with $t2") + } + } + is Atom -> { + when (t2) { + is Variable -> 1 + is Integer -> 1 + is Atom -> t1.name.compareTo(t2.name) + is Structure -> -1 + else -> throw IllegalArgumentException("Cannot compare $t1 with $t2") + } + } + is Structure -> { + when (t2) { + is Variable -> 1 + is Integer -> 1 + is Atom -> 1 + is Structure -> { + val arityComparison = t1.arguments.size.compareTo(t2.arguments.size) + if (arityComparison != 0) return arityComparison + val nameComparison = t1.name.compareTo(t2.name) + if (nameComparison != 0) return nameComparison + t1.arguments.zip(t2.arguments).forEach { (arg1, arg2) -> + val argsComparison = equivalent(arg1, arg2, emptyMap()) + if (!argsComparison) return compare(arg1, arg2, subs) + } + return 0 + } + else -> throw IllegalArgumentException("Cannot compare $t1 with $t2") + } + } + else -> throw IllegalArgumentException("Cannot compare $t1 with $t2") + } +} diff --git a/src/prolog/logic/verification.kt b/src/prolog/logic/verification.kt index b89758e..79db149 100644 --- a/src/prolog/logic/verification.kt +++ b/src/prolog/logic/verification.kt @@ -1,5 +1,6 @@ package prolog.logic +import prolog.Substitutions import prolog.ast.terms.CompoundTerm import prolog.ast.terms.Term import prolog.ast.terms.Variable @@ -12,29 +13,29 @@ import prolog.ast.terms.Variable * nonvar(Term), * \+ compound(Term). */ -fun atomic(term: Term): Boolean = nonvariable(term) && !compound(term) +fun atomic(term: Term, subs: Substitutions = emptyMap()): Boolean = nonvariable(term, subs) && !compound(term, subs) /** * True if [Term] is bound to a compound term. * See also functor/3 =../2, compound_name_arity/3 and compound_name_arguments/3. */ -fun compound(term: Term): Boolean { +fun compound(term: Term, subs: Substitutions = emptyMap()): Boolean { val isCompound = term is CompoundTerm - val isVariableCompound = term is Variable && term.alias().isPresent && compound(term.alias().get()) + val isVariableCompound = term is Variable && term in subs && compound(subs[term]!!, subs) return isCompound || isVariableCompound } /** * True if [Term] currently is not a free variable. */ -fun nonvariable(term: Term): Boolean = !variable(term) +fun nonvariable(term: Term, subs: Substitutions = emptyMap()): Boolean = !variable(term, subs) /** * True if [Term] currently is a free variable. */ -fun variable(term: Term): Boolean { +fun variable(term: Term, subs: Substitutions = emptyMap()): Boolean { if (term is Variable) { - return term.alias().isEmpty || term.alias().get() === term || variable(term.alias().get()) + return term !in subs || subs[term] === term || variable(subs[term]!!, subs) } return false diff --git a/tests/prolog/EvaluationTest.kt b/tests/prolog/EvaluationTest.kt index 7e7e4d7..de58432 100644 --- a/tests/prolog/EvaluationTest.kt +++ b/tests/prolog/EvaluationTest.kt @@ -200,7 +200,7 @@ class EvaluationTest { Program.load(listOf(fact1, fact2, fact3)) - val results = Query(Structure(Atom("a"), listOf(Variable("X")))).prove(emptyMap()) + val results = Query(Structure(Atom("a"), listOf(Variable("X")))).satisfy(emptyMap()) val expectedResults = listOf( mapOf(Variable("X") to Atom("b")), @@ -211,8 +211,8 @@ class EvaluationTest { 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") + assertEquals(expectedResults[i].size, actualResults[i].getOrNull()!!.size, "Substitution size should match") + assertTrue(expectedResults[i].all { actualResults[i].getOrNull()!![it.key]?.let { it1 -> equivalent(it.value, it1, emptyMap()) } ?: false }, "Substitution values should match") } } } \ No newline at end of file diff --git a/tests/prolog/builtins/ArithmeticOperatorsTests.kt b/tests/prolog/builtins/ArithmeticOperatorsTests.kt index b27b222..af5fbbb 100644 --- a/tests/prolog/builtins/ArithmeticOperatorsTests.kt +++ b/tests/prolog/builtins/ArithmeticOperatorsTests.kt @@ -3,9 +3,10 @@ package prolog.builtins import org.junit.jupiter.api.Assertions.* import org.junit.jupiter.api.Test import org.junit.jupiter.api.assertThrows +import prolog.Substitutions import prolog.ast.terms.Integer +import prolog.ast.terms.Term import prolog.ast.terms.Variable -import prolog.logic.between import prolog.logic.equivalent class ArithmeticOperatorsTests { @@ -16,18 +17,21 @@ class ArithmeticOperatorsTests { Integer(1) ) - var result = op1.evaluate(emptyMap()).first + var result = op1.satisfy(emptyMap()).toList() - assertEquals(True, result, "1 should be equal to 1") + assertEquals(1, result.size, "1 should be equal to 1") + assertTrue(result[0].isSuccess, "1 should be equal to 1") + val subs = result[0].getOrNull()!! + assertTrue(subs.isEmpty(), "1 should not be rebound") val op2 = EvaluatesToDifferent( Integer(1), Integer(1) ) - result = op2.evaluate(emptyMap()).first + result = op2.satisfy(emptyMap()).toList() - assertEquals(False, result, "1 should not be different from 1") + assertEquals(0, result.size, "1 should not be different from 1") } @Test @@ -37,18 +41,21 @@ class ArithmeticOperatorsTests { Integer(2) ) - var result = op1.evaluate(emptyMap()).first + var result = op1.satisfy(emptyMap()).toList() + + assertEquals(0, result.size, "1 should not be equal to 2") - assertEquals(False, result, "1 should not be equal to 2") - val op2 = EvaluatesToDifferent( Integer(1), Integer(2) ) - result = op2.evaluate(emptyMap()).first + result = op2.satisfy(emptyMap()).toList() - assertEquals(True, result, "1 should be different from 2") + assertEquals(1, result.size, "1 should be different from 2") + assertTrue(result[0].isSuccess, "1 should be different from 2") + val subs = result[0].getOrNull()!! + assertTrue(subs.isEmpty(), "1 should not be rebound") } @Test @@ -58,18 +65,21 @@ class ArithmeticOperatorsTests { Integer(5) ) - var result = op.evaluate(emptyMap()).first + var result = op.satisfy(emptyMap()).toList() - assertEquals(True, result, "2 + 3 should be equal to 5") + assertEquals(1, result.size, "2 + 3 should be equal to 5") + assertTrue(result[0].isSuccess, "2 + 3 should be equal to 5") + val subs = result[0].getOrNull()!! + assertTrue(subs.isEmpty(), "2 + 3 should not be rebound") val op2 = EvaluatesToDifferent( Add(Integer(2), Integer(3)), Integer(5) ) - result = op2.evaluate(emptyMap()).first + result = op2.satisfy(emptyMap()).toList() - assertEquals(False, result, "2 + 3 should not be different from 5") + assertEquals(0, result.size, "2 + 3 should not be different from 5") } @Test @@ -79,18 +89,21 @@ class ArithmeticOperatorsTests { Add(Integer(4), Integer(1)) ) - var result = op.evaluate(emptyMap()).first + var result = op.satisfy(emptyMap()).toList() - assertEquals(True, result, "2 + 3 should be equal to 4 + 1") + assertEquals(1, result.size, "2 + 3 should be equal to 4 + 1") + assertTrue(result[0].isSuccess, "2 + 3 should be equal to 4 + 1") + val subs = result[0].getOrNull()!! + assertTrue(subs.isEmpty(), "2 + 3 should not be rebound") val op2 = EvaluatesToDifferent( Add(Integer(2), Integer(3)), Add(Integer(4), Integer(1)) ) - result = op2.evaluate(emptyMap()).first + result = op2.satisfy(emptyMap()).toList() - assertEquals(False, result, "2 + 3 should not be different from 4 + 1") + assertEquals(0, result.size, "2 + 3 should not be different from 4 + 1") } @Test @@ -100,14 +113,24 @@ class ArithmeticOperatorsTests { Variable("X") ) - assertThrows { op.evaluate(emptyMap()) } + var result = op.satisfy(emptyMap()).toList() + + assertEquals(1, result.size, "One exception should be thrown") + assertTrue(result[0].isFailure, "One exception should be thrown") + var exceptions = result[0].exceptionOrNull() + assertTrue(exceptions is IllegalArgumentException, "One exception should be thrown") val op2 = EvaluatesToDifferent( Integer(1), Variable("X") ) - assertThrows { op2.evaluate(emptyMap()) } + result = op2.satisfy(emptyMap()).toList() + + assertEquals(1, result.size, "One exception should be thrown") + assertTrue(result[0].isFailure, "One exception should be thrown") + exceptions = result[0].exceptionOrNull() + assertTrue(exceptions is IllegalArgumentException, "One exception should be thrown") } @Test @@ -117,14 +140,14 @@ class ArithmeticOperatorsTests { Integer(1) ) - assertThrows { op.evaluate(emptyMap()) } + assertThrows { op.satisfy(emptyMap()) } val op2 = EvaluatesToDifferent( Add(Integer(1), Variable("X")), Integer(1) ) - assertThrows { op2.evaluate(emptyMap()) } + assertThrows { op2.satisfy(emptyMap()) } } @Test @@ -134,7 +157,7 @@ class ArithmeticOperatorsTests { Integer(1) ) - val result = op.prove(emptyMap()) + val result = op.satisfy(emptyMap()) assertTrue(result.any(), "1 should be equal to 1") } @@ -146,7 +169,7 @@ class ArithmeticOperatorsTests { Integer(2) ) - val result = op.prove(emptyMap()).toList() + val result = op.satisfy(emptyMap()).toList() assertTrue(result.isEmpty(), "1 should not be equal to 2") } @@ -159,12 +182,11 @@ class ArithmeticOperatorsTests { Integer(1) ) - t1.bind(Integer(1)) + val result = op.satisfy(mapOf(t1 to Integer(1))).toList() - val result = op.prove(emptyMap()) - - assertTrue(result.any(), "X should be equal to 1") - assertTrue(result.first().isEmpty(), "X should not be rebound") + assertEquals(1, result.size, "X should be equal to 1") + assertTrue(result.first().isSuccess, "X should be equal to 1") + assertTrue(result.first().getOrNull()!!.isEmpty(), "X should not be rebound") } @Test @@ -175,9 +197,7 @@ class ArithmeticOperatorsTests { Integer(1) ) - t1.bind(Integer(2)) - - val result = op.prove(emptyMap()) + val result = op.satisfy(mapOf(t1 to Integer(2))) assertFalse(result.any(), "X should not be equal to 1") } @@ -189,11 +209,12 @@ class ArithmeticOperatorsTests { Integer(1) ) - val result = op.prove(emptyMap()).toList() + val result = op.satisfy(emptyMap()).toList() assertFalse(result.isEmpty(), "X should be equal to 1") - assertEquals(1, result[0].size, "X should be rebound") - assertTrue(equivalent(Integer(1), result[0][Variable("X")]!!), "X should be equal to 1") + assertTrue(result.first().isSuccess, "X should be equal to 1") + assertEquals(1, result[0].getOrNull()!!.size, "X should be rebound") + assertTrue(equivalent(Integer(1), result[0].getOrNull()!![Variable("X")]!!, emptyMap()), "X should be equal to 1") } @Test @@ -203,11 +224,18 @@ class ArithmeticOperatorsTests { Add(Integer(1), Integer(2)) ) - val result = op.prove(emptyMap()).toList() + val result = op.satisfy(emptyMap()).toList() assertFalse(result.isEmpty(), "X should be equal to 3") - assertEquals(1, result[0].size, "X should be rebound") - assertTrue(equivalent(Integer(3), result[0][Variable("X")]!!), "X should be equal to 3") + assertTrue(result.first().isSuccess, "X should be equal to 3") + + val subs = result[0].getOrNull()!! + + assertEquals(1, subs.size, "X should be rebound") + assertTrue( + equivalent(Integer(3), subs[Variable("X")]!!, emptyMap()), + "X should be equal to 3" + ) } @Test @@ -217,7 +245,12 @@ class ArithmeticOperatorsTests { Variable("Y") ) - assertThrows { op.prove(emptyMap()) } + val result = op.satisfy(emptyMap()).toList() + + assertEquals(1, result.size, "One exception should be thrown") + assertTrue(result[0].isFailure, "One exception should be thrown") + val exceptions = result[0].exceptionOrNull() + assertTrue(exceptions is IllegalArgumentException, "One exception should be thrown") } @Test @@ -227,23 +260,29 @@ class ArithmeticOperatorsTests { Variable("X") ) - assertThrows { op.prove(emptyMap()) } + val result = op.satisfy(emptyMap()).toList() + + assertEquals(1, result.size, "One exception should be thrown") + assertTrue(result[0].isFailure, "One exception should be thrown") + val exceptions = result[0].exceptionOrNull() + assertTrue(exceptions is IllegalArgumentException, "One exception should be thrown") } + /** + * ?- X = 1, Y = 1 + 2, X is Y. + * false. + */ @Test fun `var is bound-to-sum-var`() { val t1 = Variable("X") val t2 = Variable("Y") - t2.bind(Add(Integer(1), Integer(2))) - val op = Is(t1, t2) + val map: Substitutions = mapOf(t1 to Integer(1), t2 to Add(Integer(1), Integer(2))) - val result = op.prove(emptyMap()).toList() + val result = op.satisfy(map).toList() - assertTrue(result.isNotEmpty(), "X should be equal to 3") - assertEquals(1, result[0].size, "X should be rebound, Y should not") - assertTrue(equivalent(Integer(3), result[0][t1]!!), "X should be equal to 3") + assertEquals(0, result.size, "X should not be equal to Y") } /** @@ -268,47 +307,38 @@ class ArithmeticOperatorsTests { fun `negate 1 to get -1`() { val t1 = Integer(1) - val result = Negate(t1).evaluate(emptyMap()).first + val result = Negate(t1).simplify(emptyMap()) - assertEquals(Integer(-1), result, "negate(1) should be equal to -1") + assertEquals(Integer(-1), result.to, "negate(1) should be equal to -1") } @Test fun `negate 0 to get 0`() { val t1 = Integer(0) - val result = Negate(t1).evaluate(emptyMap()).first + val result = Negate(t1).simplify(emptyMap()) - assertEquals(Integer(0), result, "negate(0) should be equal to 0") + assertEquals(Integer(0), result.to, "negate(0) should be equal to 0") } @Test fun `negate -1 to get 1`() { val t1 = Integer(-1) - val result = Negate(t1).evaluate(emptyMap()).first + val result = Negate(t1).simplify(emptyMap()) - assertEquals(Integer(1), result, "negate(-1) should be equal to 1") + assertEquals(Integer(1), result.to, "negate(-1) should be equal to 1") } @Test fun `negate bound-to-1-var to get -1`() { val t1 = Variable("X") - t1.bind(Integer(1)) + val map: Substitutions = mapOf(t1 to Integer(1)) - val result = Negate(t1).evaluate(emptyMap()).first + val result = Negate(t1).simplify(map) - assertEquals(Integer(-1), result, "negate(1) should be equal to -1") - } - - @Test - fun `negate bound-to-1-var to get -1 by map`() { - val t1 = Variable("X") - - val result = Negate(t1).evaluate(mapOf(t1 to Integer(1))).first - - assertEquals(Integer(-1), result, "negate(1) should be equal to -1") + assertEquals(Integer(-1), result.to, "negate(1) should be equal to -1") } @Test @@ -316,9 +346,9 @@ class ArithmeticOperatorsTests { val t1 = Integer(1) val t2 = Integer(3) - val result = Negate(Add(t1, t2)).evaluate(emptyMap()).first + val result = Negate(Add(t1, t2)).simplify(emptyMap()) - assertEquals(Integer(-4), result, "negate(1 + 3) should be equal to -4") + assertEquals(Integer(-4), result.to, "negate(1 + 3) should be equal to -4") } @Test @@ -326,9 +356,9 @@ class ArithmeticOperatorsTests { val t1 = Integer(1) val t2 = Integer(2) - val result = Add(t1, t2).evaluate(emptyMap()).first + val result = Add(t1, t2).simplify(emptyMap()) - assertEquals(Integer(3), result, "1 + 2 should be equal to 3") + assertEquals(Integer(3), result.to, "1 + 2 should be equal to 3") } @Test @@ -336,21 +366,10 @@ class ArithmeticOperatorsTests { val t1 = Integer(1) val t2 = Variable("X") - t2.bind(Integer(2)) + val subs: Substitutions = mapOf(t2 to Integer(2)) + val result = Add(t1, t2).simplify(subs) - val result = Add(t1, t2).evaluate(emptyMap()).first - - assertEquals(Integer(3), result, "1 + 2 should be equal to 3") - } - - @Test - fun `Add 1 and bound-to-2-var to get 3 by map`() { - val t1 = Integer(1) - val t2 = Variable("X") - - val result = Add(t1, t2).evaluate(mapOf(t2 to Integer(2))).first - - assertEquals(Integer(3), result, "1 + 2 should be equal to 3") + assertEquals(Integer(3), result.to, "1 + 2 should be equal to 3") } @Test @@ -358,9 +377,9 @@ class ArithmeticOperatorsTests { val t1 = Integer(1) val t2 = Integer(2) - val result = Subtract(t1, t2).evaluate(emptyMap()).first + val result = Subtract(t1, t2).simplify(emptyMap()) - assertEquals(Integer(-1), result, "1 - 2 should be equal to -1") + assertEquals(Integer(-1), result.to, "1 - 2 should be equal to -1") } @Test @@ -368,9 +387,9 @@ class ArithmeticOperatorsTests { val t1 = Integer(3) val t2 = Integer(1) - val result = Subtract(t1, t2).evaluate(emptyMap()).first + val result = Subtract(t1, t2).simplify(emptyMap()) - assertEquals(Integer(2), result, "3 - 1 should be equal to 2") + assertEquals(Integer(2), result.to, "3 - 1 should be equal to 2") } @Test @@ -378,9 +397,9 @@ class ArithmeticOperatorsTests { val t1 = Integer(0) val t2 = Integer(0) - val result = Multiply(t1, t2).evaluate(emptyMap()).first + val result = Multiply(t1, t2).simplify(emptyMap()) - assertEquals(Integer(0), result, "0 * 0 should be equal to 0") + assertEquals(Integer(0), result.to, "0 * 0 should be equal to 0") } @Test @@ -388,9 +407,9 @@ class ArithmeticOperatorsTests { val t1 = Integer(1) val t2 = Integer(0) - val result = Multiply(t1, t2).evaluate(emptyMap()).first + val result = Multiply(t1, t2).simplify(emptyMap()) - assertEquals(Integer(0), result, "1 * 0 should be equal to 0") + assertEquals(Integer(0), result.to, "1 * 0 should be equal to 0") } @Test @@ -398,9 +417,9 @@ class ArithmeticOperatorsTests { val t1 = Integer(0) val t2 = Integer(1) - val result = Multiply(t1, t2).evaluate(emptyMap()).first + val result = Multiply(t1, t2).simplify(emptyMap()) - assertEquals(Integer(0), result, "0 * 1 should be equal to 0") + assertEquals(Integer(0), result.to, "0 * 1 should be equal to 0") } @Test @@ -408,9 +427,9 @@ class ArithmeticOperatorsTests { val t1 = Integer(3) val t2 = Integer(1) - val result = Multiply(t1, t2).evaluate(emptyMap()).first + val result = Multiply(t1, t2).simplify(emptyMap()) - assertEquals(Integer(3), result, "3 * 1 should be equal to 3") + assertEquals(Integer(3), result.to, "3 * 1 should be equal to 3") } @Test @@ -418,8 +437,8 @@ class ArithmeticOperatorsTests { val t1 = Integer(2) val t2 = Integer(3) - val result = Multiply(t1, t2).evaluate(emptyMap()) + val result = Multiply(t1, t2).simplify(emptyMap()) - assertEquals(Integer(6), result.first, "2 * 3 should be equal to 6") + assertEquals(Integer(6), result.to, "2 * 3 should be equal to 6") } } diff --git a/tests/prolog/builtins/UnificationTest.kt b/tests/prolog/builtins/UnificationTest.kt index 267e41d..6c92206 100644 --- a/tests/prolog/builtins/UnificationTest.kt +++ b/tests/prolog/builtins/UnificationTest.kt @@ -16,7 +16,7 @@ class UnificationTest { val variable = Variable("X") val atom = Atom("a") - val result = Equivalent(variable, atom).prove(emptyMap()) + val result = Equivalent(variable, atom).satisfy(emptyMap()) assertFalse(result.any(), "Variable and atom should not be equivalent") } @@ -30,10 +30,11 @@ class UnificationTest { val atom1 = Atom("a") val atom2 = Atom("a") - val result = Equivalent(atom1, atom2).prove(emptyMap()) + val result = Equivalent(atom1, atom2).satisfy(emptyMap()) assertTrue(result.any(), "Identical atoms should be equivalent") - assertEquals(0, result.first().size, "No substitutions should be made") + assertTrue(result.first().isSuccess, "Result should be successful") + assertEquals(0, result.first().getOrNull()!!.size, "No substitutions should be made") } /** @@ -45,7 +46,7 @@ class UnificationTest { val addition = Add(Integer(1), Integer(2)) val solution = Integer(3) - val result = Equivalent(addition, solution).prove(emptyMap()) + val result = Equivalent(addition, solution).satisfy(emptyMap()) assertFalse(result.any(), "Addition should be equivalent") } diff --git a/tests/prolog/builtins/VerificationTest.kt b/tests/prolog/builtins/VerificationTest.kt index ce8af97..632808d 100644 --- a/tests/prolog/builtins/VerificationTest.kt +++ b/tests/prolog/builtins/VerificationTest.kt @@ -3,20 +3,19 @@ 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.Substitutions import prolog.ast.terms.Atom import prolog.ast.terms.Structure import prolog.ast.terms.Variable import prolog.logic.compound import prolog.logic.nonvariable import prolog.logic.variable -import kotlin.test.assertEquals class VerificationTest { @Test fun unbound_variable_is_var() { val variable = Variable("X") assertTrue(variable(variable)) - assertTrue(variable.alias().isEmpty) } @Test @@ -26,10 +25,8 @@ class VerificationTest { assertTrue(variable(variable)) val atom = Atom("a") - variable.bind(atom) - assertFalse(variable(variable)) - assertEquals(atom, variable.alias().get()) + assertFalse(variable(variable, mapOf(variable to atom))) } @Test @@ -39,10 +36,8 @@ class VerificationTest { assertTrue(variable(variable)) val structure = Structure(Atom("a"), listOf(Atom("b"))) - variable.bind(structure) - assertFalse(variable(variable)) - assertEquals(structure, variable.alias().get()) + assertFalse(variable(variable, mapOf(variable to structure))) } /** @@ -52,8 +47,7 @@ class VerificationTest { @Test fun variable_bound_to_itself_is_var() { val variable = Variable("X") - variable.bind(variable) - assertTrue(variable(variable)) + assertTrue(variable(variable, mapOf(variable to variable))) } /** @@ -64,9 +58,7 @@ class VerificationTest { fun variable_bound_to_another_variable_is_var() { val variable1 = Variable("X") val variable2 = Variable("Y") - variable1.bind(variable2) - assertTrue(variable(variable1)) - assertEquals(variable2, variable1.alias().get()) + assertTrue(variable(variable1, mapOf(variable1 to variable2))) } /** @@ -77,9 +69,11 @@ class VerificationTest { fun variable_bound_to_bound_variable_is_not_var() { val variable1 = Variable("X") val variable2 = Variable("Y") - variable2.bind(Atom("a")) - variable1.bind(variable2) - assertFalse(variable(variable1)) + val map: Substitutions = mapOf( + variable1 to variable2, + variable2 to Atom("a") + ) + assertFalse(variable(variable1, map)) } @Test @@ -117,10 +111,8 @@ class VerificationTest { assertFalse(nonvariable(variable)) val atom = Atom("a") - variable.bind(atom) - assertTrue(nonvariable(variable)) - assertEquals(atom, variable.alias().get()) + assertTrue(nonvariable(variable, mapOf(variable to atom))) } /** @@ -134,10 +126,8 @@ class VerificationTest { assertFalse(nonvariable(variable)) val structure = Structure(Atom("a"), listOf(Atom("b"))) - variable.bind(structure) - assertTrue(nonvariable(variable)) - assertEquals(structure, variable.alias().get()) + assertTrue(nonvariable(variable, mapOf(variable to structure))) } /** @@ -147,8 +137,7 @@ class VerificationTest { @Test fun variable_bound_to_itself_is_not_nonvar() { val variable = Variable("X") - variable.bind(variable) - assertFalse(nonvariable(variable)) + assertFalse(nonvariable(variable, mapOf(variable to variable))) } /** @@ -159,8 +148,7 @@ class VerificationTest { fun variable_bound_to_another_variable_is_not_nonvar() { val variable1 = Variable("X") val variable2 = Variable("Y") - variable1.bind(variable2) - assertFalse(nonvariable(variable1)) + assertFalse(nonvariable(variable1, mapOf(variable1 to variable2))) } @Test @@ -195,8 +183,7 @@ class VerificationTest { fun bound_variable_to_atom_is_not_compound() { val variable = Variable("X") val atom = Atom("a") - variable.bind(atom) - assertFalse(compound(variable)) + assertFalse(compound(variable, mapOf(variable to atom))) } /** @@ -207,8 +194,7 @@ class VerificationTest { fun bound_variable_to_compound_term_is_compound() { val variable = Variable("X") val structure = Structure(Atom("a"), listOf(Atom("b"))) - variable.bind(structure) - assertTrue(compound(variable)) + assertTrue(compound(variable, mapOf(variable to structure))) } /** @@ -221,13 +207,12 @@ class VerificationTest { val variable2 = Variable("Y") val structure = Structure(Atom("a"), listOf(Atom("b"))) - variable2.bind(structure) - variable1.bind(variable2) + val subs: Substitutions = mapOf( + variable1 to variable2, + variable2 to structure + ) - assertTrue(compound(variable1)) - - assertEquals(structure, variable2.alias().get()) - assertEquals(variable2, variable1.alias().get()) + assertTrue(compound(variable1, subs)) } @Test diff --git a/tests/prolog/logic/ArithmeticTests.kt b/tests/prolog/logic/ArithmeticTests.kt index d79e3b7..81b5f67 100644 --- a/tests/prolog/logic/ArithmeticTests.kt +++ b/tests/prolog/logic/ArithmeticTests.kt @@ -4,7 +4,7 @@ import org.junit.jupiter.api.Assertions.assertEquals import org.junit.jupiter.api.Assertions.assertTrue import org.junit.jupiter.api.RepeatedTest import org.junit.jupiter.api.Test -import org.junit.jupiter.api.assertThrows +import prolog.Substitutions import prolog.ast.terms.Integer import prolog.ast.terms.Term import prolog.ast.terms.Variable @@ -15,7 +15,11 @@ class ArithmeticTests { val result = between(Integer(0), Integer(2), Integer(1)) assertTrue(result.any(), "Expected 1 to be between 0 and 2") - assertEquals(emptyMap(), result.first(), "Expected no substitutions") + assertTrue(result.first().isSuccess, "Expected success") + + val subs = result.first().getOrNull()!! + + assertEquals(emptyMap(), subs, "Expected no substitutions") } @Test @@ -39,9 +43,11 @@ class ArithmeticTests { assertEquals(expectedResults.size, actualResults.size, "Expected 3 results") for ((expected, actual) in expectedResults.zip(actualResults)) { for ((key, value) in expected) { + assertTrue(actual.isSuccess, "Expected success") + val actual = actual.getOrNull()!! assertTrue(actual.containsKey(key), "Expected key $key to be present") assertTrue( - equivalent(value, actual[key]!!), + equivalent(value, actual[key]!!, emptyMap()), "Expected value $value for key $key, but got ${actual[key]}" ) } @@ -93,20 +99,6 @@ class ArithmeticTests { val t1 = Variable("X") val t2 = Integer(2) - t1.bind(Integer(1)) - - val result = succ(t1, t2, emptyMap()).toList() - - assertEquals(1, result.size, "Expected X + 1 to be equal to 2") - assertTrue(result[0].isSuccess, "Expected success") - assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected no substitutions") - } - - @Test - fun `succ(bound-to-1-var) is 2 by map`() { - val t1 = Variable("X") - val t2 = Integer(2) - val result = succ(t1, t2, mapOf(t1 to Integer(1))).toList() assertEquals(1, result.size, "Expected X + 1 to be equal to 2") @@ -119,20 +111,6 @@ class ArithmeticTests { val t1 = Variable("X") val t2 = Variable("Y") - t1.bind(Integer(1)) - - val result = succ(t1, t2, emptyMap()).toList() - - assertEquals(1, result.size, "Expected X + 1 to be equal to Y") - assertTrue(result[0].isSuccess, "Expected success") - assertEquals(Integer(2), result[0].getOrNull()!![t2], "Expected Y to be equal to 2") - } - - @Test - fun `succ(bound-to-1-var) is var by map`() { - val t1 = Variable("X") - val t2 = Variable("Y") - val result = succ(t1, t2, mapOf(t1 to Integer(1))).toList() assertEquals(1, result.size, "Expected X + 1 to be equal to Y") @@ -219,21 +197,6 @@ class ArithmeticTests { val t2 = Integer(2) val t3 = Variable("X") - t3.bind(Integer(3)) - - val result = plus(t1, t2, t3, emptyMap()).toList() - - assertEquals(1, result.size, "1 + 2 should be equal to X") - assertTrue(result[0].isSuccess, "Expected success") - assertTrue(result[0].getOrNull()!!.isEmpty(), "t3 should not be rebound") - } - - @Test - fun `1 plus 2 is bound-to-3-var by map`() { - val t1 = Integer(1) - val t2 = Integer(2) - val t3 = Variable("X") - val result = plus(t1, t2, t3, mapOf(Variable("X") to Integer(3))).toList() assertEquals(1, result.size, "1 + 2 should be equal to X") @@ -247,9 +210,7 @@ class ArithmeticTests { val t2 = Integer(2) val t3 = Variable("X") - t3.bind(Integer(4)) - - val result = plus(t1, t2, t3, emptyMap()) + val result = plus(t1, t2, t3, mapOf(t3 to Integer(4))) assertTrue(result.none(), "1 + 2 should not be equal to X") } @@ -260,9 +221,7 @@ class ArithmeticTests { val t2 = Variable("X") val t3 = Integer(3) - t2.bind(Integer(2)) - - val result = plus(t1, t2, t3, emptyMap()).toList() + val result = plus(t1, t2, t3, mapOf(t2 to Integer(2))).toList() assertEquals(1, result.size, "1 + X should be equal to 3") assertTrue(result[0].isSuccess, "Expected success") @@ -275,9 +234,7 @@ class ArithmeticTests { val t2 = Variable("X") val t3 = Integer(4) - t2.bind(Integer(2)) - - val result = plus(t1, t2, t3, emptyMap()) + val result = plus(t1, t2, t3, mapOf(t2 to Integer(2))) assertTrue(result.none(), "1 + X should not be equal to 4") } @@ -288,9 +245,7 @@ class ArithmeticTests { val t2 = Integer(2) val t3 = Integer(3) - t1.bind(Integer(1)) - - val result = plus(t1, t2, t3, emptyMap()).toList() + val result = plus(t1, t2, t3, mapOf(t1 to Integer(1))).toList() assertEquals(1, result.size, "X + 2 should be equal to 3") assertTrue(result[0].isSuccess, "Expected success") @@ -303,9 +258,7 @@ class ArithmeticTests { val t2 = Integer(2) val t3 = Integer(4) - t1.bind(Integer(1)) - - val result = plus(t1, t2, t3, emptyMap()) + val result = plus(t1, t2, t3, mapOf(t1 to Integer(1))) assertTrue(result.none(), "X + 2 should not be equal to 4") } @@ -329,14 +282,16 @@ class ArithmeticTests { val t2 = Variable("Y") val t3 = Variable("Z") - t1.bind(Integer(1)) - t2.bind(Integer(2)) + val map: Substitutions = mapOf( + t1 to Integer(1), + t2 to Integer(2), + ) - val result = plus(t1, t2, t3, emptyMap()).toList() + val result = plus(t1, t2, t3, map).toList() assertTrue(result.isNotEmpty(), "X + Y should be equal to Z") assertTrue(result[0].isSuccess, "Expected success") - assertTrue(equivalent(result[0].getOrThrow()[t3]!!, Integer(3)), "Z should be equal to 3") + assertTrue(equivalent(result[0].getOrThrow()[t3]!!, Integer(3), result[0].getOrNull()!!), "Z should be equal to 3") } @Test diff --git a/tests/prolog/logic/UnifyTest.kt b/tests/prolog/logic/UnifyTest.kt index 4045744..5e40c5e 100644 --- a/tests/prolog/logic/UnifyTest.kt +++ b/tests/prolog/logic/UnifyTest.kt @@ -3,10 +3,12 @@ package prolog.logic import org.junit.jupiter.api.Assertions.* import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test +import prolog.Substitutions import prolog.ast.terms.Integer import prolog.ast.terms.Atom import prolog.ast.terms.Structure import prolog.ast.terms.Variable +import prolog.builtins.Add /* * Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms @@ -19,8 +21,8 @@ class UnifyTest { val result = unify(atom1, atom2) - assertTrue(result.isPresent, "Identical atoms should unify") - assertEquals(0, result.get().size, "No substitutions should be made") + assertTrue(result.isSuccess, "Identical atoms should unify") + assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made") } @Test @@ -30,7 +32,7 @@ class UnifyTest { val result = unify(atom1, atom2) - assertFalse(result.isPresent, "Different atoms should not unify") + assertFalse(result.isSuccess, "Different atoms should not unify") } /** @@ -44,8 +46,8 @@ class UnifyTest { val result = unify(variable1, variable2) - assertTrue(result.isPresent, "Identical variables should unify") - assertEquals(0, result.get().size, "No substitutions should be made") + assertTrue(result.isSuccess, "Identical variables should unify") + assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made") } @Test @@ -55,9 +57,9 @@ class UnifyTest { val result = unify(atom, variable) - assertTrue(result.isPresent, "Variable should unify with atom") - assertEquals(1, result.get().size, "There should be one substitution") - assertEquals(atom, variable.alias().get(), "Variable should be substituted with atom") + assertTrue(result.isSuccess, "Variable should unify with atom") + assertEquals(1, result.getOrNull()!!.size, "There should be one substitution") + assertEquals(atom, result.getOrNull()!![variable], "Variable should be substituted with atom") } @Test @@ -67,9 +69,9 @@ class UnifyTest { val result = unify(variable1, variable2) - assertTrue(result.isPresent) - assertEquals(1, result.get().size) - assertEquals(variable2, variable1.alias().get(), "Variable 1 should alias to variable 2") + assertTrue(result.isSuccess) + assertEquals(1, result.getOrNull()!!.size) + assertEquals(variable2, result.getOrNull()!![variable1], "Variable 1 should alias to variable 2") } @Test @@ -79,8 +81,8 @@ class UnifyTest { val result = unify(structure1, structure2) - assertTrue(result.isPresent, "Identical compound terms should unify") - assertEquals(0, result.get().size, "No substitutions should be made") + assertTrue(result.isSuccess, "Identical compound terms should unify") + assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made") } @Test @@ -90,7 +92,7 @@ class UnifyTest { val result = unify(structure1, structure2) - assertFalse(result.isPresent, "Different compound terms should not unify") + assertFalse(result.isSuccess, "Different compound terms should not unify") } @Test @@ -100,7 +102,7 @@ class UnifyTest { val result = unify(structure1, structure2) - assertFalse(result.isPresent, "Compound terms with different functors should not unify") + assertFalse(result.isSuccess, "Compound terms with different functors should not unify") } /** @@ -114,10 +116,14 @@ class UnifyTest { val result = unify(variable, structure) - assertTrue(result.isPresent, "Variable should unify with compound term") - assertEquals(1, result.get().size, "There should be one substitution") + assertTrue(result.isSuccess, "Variable should unify with compound term") + + val subs = result.getOrNull()!! + + assertEquals(1, subs.size, "There should be one substitution") + assertTrue(subs.containsKey(variable), "Variable should be in the substitution map") assertTrue( - equivalent(Structure(Atom("f"), listOf(Atom("a"), Atom("b"))), variable.alias().get()), + equivalent(Structure(Atom("f"), listOf(Atom("a"), Atom("b"))), subs[variable]!!, subs), "Variable should be substituted with compound term" ) } @@ -130,9 +136,13 @@ class UnifyTest { val result = unify(structure1, structure2) - assertTrue(result.isPresent, "Compound term with variable should unify with part") - assertEquals(1, result.get().size, "There should be one substitution") - val equivalence = equivalent(Atom("b"), variable.alias().get()) + assertTrue(result.isSuccess, "Compound term with variable should unify with part") + + val subs = result.getOrNull()!! + + assertEquals(1, subs.size, "There should be one substitution") + assertTrue(subs.containsKey(variable), "Variable should be in the substitution map") + val equivalence = equivalent(Atom("b"), subs[variable]!!, subs) assertTrue(equivalence, "Variable should be substituted with atom") } @@ -146,9 +156,13 @@ class UnifyTest { val result = unify(structure1, structure2) - assertTrue(result.isPresent, "Compound terms with variable arguments should unify") - assertEquals(1, result.get().size, "There should be one substitution") - assertEquals(variable2, variable1.alias().get(), "Variable 1 should alias to variable 2") + assertTrue(result.isSuccess, "Compound terms with variable arguments should unify") + + val subs = result.getOrNull()!! + + assertEquals(1, subs.size, "There should be one substitution") + assertTrue(subs.containsKey(variable1), "Variable 1 should be in the substitution map") + assertEquals(variable2, subs[variable1], "Variable 1 should alias to variable 2") } /** @@ -161,7 +175,7 @@ class UnifyTest { val result = unify(structure1, structure2) - assertFalse(result.isPresent, "Compound terms with different arity should not unify") + assertFalse(result.isSuccess, "Compound terms with different arity should not unify") } /** @@ -177,10 +191,14 @@ class UnifyTest { val result = unify(structure1, structure2) - assertTrue(result.isPresent, "Nested compound terms with variables should unify") - assertEquals(1, result.get().size, "There should be one substitution") + assertTrue(result.isSuccess, "Nested compound terms with variables should unify") + + val subs = result.getOrNull()!! + + assertEquals(1, subs.size, "There should be one substitution") + assertTrue(subs.containsKey(variable2), "Variable 2 should be in the substitution map") assertTrue( - equivalent(Structure(Atom("g"), listOf(Variable("X"))), variable2.alias().get()), + equivalent(Structure(Atom("g"), listOf(Variable("X"))), subs[variable2]!!, subs), "Variable should be substituted with compound term" ) } @@ -200,15 +218,22 @@ class UnifyTest { val result = unify(structure1, structure2) - assertTrue(result.isPresent, "Compound terms with more variables should unify") - assertEquals(2, result.get().size, "There should be two substitutions") + assertTrue(result.isSuccess, "Compound terms with more variables should unify") + val subs = result.getOrNull()!! + + assertEquals(2, subs.size, "There should be two substitutions") + assertTrue(subs.containsKey(variable1), "Variable 1 should be in the substitution map") assertTrue( - equivalent(Atom("a"), variable1.alias().get()), + equivalent(Atom("a"), subs[variable1]!!, subs), "Variable 1 should be substituted with atom" ) - val equivalence = equivalent(Structure(Atom("g"), listOf(Atom("a"))), variable2.alias().get()) - assertTrue(equivalence, "Variable 2 should be substituted with compound term") + assertTrue(subs.containsKey(variable2), "Variable 2 should be in the substitution map") + assertTrue( + equivalent(Structure(Atom("g"), listOf(Atom("a"))), subs[variable2]!!, subs), + "Variable 2 should be substituted with compound term" + + ) } /** @@ -220,11 +245,16 @@ class UnifyTest { val variable1 = Variable("X") val structure2 = Structure(Atom("f"), listOf(Variable("X"))) - val result = unify(variable1, structure2) + val result = unifyLazy(variable1, structure2, emptyMap()).toList() - assertTrue(result.isPresent, "Recursive unification should succeed") - assertEquals(1, result.get().size, "There should be one substitution") - assertEquals(structure2, variable1.alias().get(), "Variable should be substituted with compound term") + assertEquals(1, result.size, "There should be one result") + assertTrue(result[0].isSuccess, "Recursive unification should succeed") + + val subs = result[0].getOrNull()!! + + assertEquals(1, subs.size, "There should be one substitution") + assertTrue(subs.containsKey(variable1), "Variable should be in the substitution map") + assertEquals(structure2, subs[variable1], "Variable should be substituted with compound term") } /** @@ -238,13 +268,15 @@ class UnifyTest { val variable2 = Variable("Y") val atom = Atom("bar") - variable1.bind(atom) - variable2.bind(atom) + val map: Substitutions = mapOf( + variable1 to atom, + variable2 to atom + ) + val result = unifyLazy(variable1, variable2, map).toList() - val result = unify(variable1, variable2) - - assertTrue(result.isPresent, "Multiple unification should succeed") - assertEquals(0, result.get().size, "No substitutions should be made") + assertEquals(1, result.size, "There should be one substitution") + assertTrue(result[0].isSuccess, "Multiple unification should succeed") + assertEquals(0, result[0].getOrNull()!!.size, "No (additional) substitutions should be made") } /** @@ -258,7 +290,7 @@ class UnifyTest { val result = unify(atom1, structure2) - assertFalse(result.isPresent, "Atom with different arity should not unify") + assertFalse(result.isSuccess, "Atom with different arity should not unify") } @Test @@ -268,8 +300,8 @@ class UnifyTest { val result = unify(int1, int2) - assertTrue(result.isPresent, "Identical integers should unify") - assertEquals(0, result.get().size, "No substitutions should be made") + assertTrue(result.isSuccess, "Identical integers should unify") + assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made") } @Test @@ -279,6 +311,17 @@ class UnifyTest { val result = unify(int1, int2) - assertFalse(result.isPresent, "Different integers should not unify") + assertFalse(result.isSuccess, "Different integers should not unify") + } + + + @Test + fun `1 + 2 does not unify with 3`() { + val expr1 = Add(Integer(1), Integer(2)) + val expr2 = Integer(3) + + val result = unify(expr1, expr2) + + assertFalse(result.isSuccess, "1 + 2 should not unify with 3") } } \ No newline at end of file