From e73e5cbfc837d4bb4dc54eceec326954f12618de Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Fri, 11 Apr 2025 19:27:01 +0200 Subject: [PATCH] Checkpoint --- {pl => examples}/scratchpad.pl | 0 src/prolog/Program.kt | 3 - .../ast/arithmetic/ArithmeticOperator.kt | 12 + src/prolog/ast/arithmetic/Expression.kt | 5 + src/prolog/ast/logic/Clause.kt | 4 +- src/prolog/ast/logic/Fact.kt | 2 +- src/prolog/ast/logic/LogicOperand.kt | 5 + src/prolog/ast/logic/LogicOperator.kt | 13 + src/prolog/ast/terms/Atom.kt | 5 + src/prolog/ast/terms/Goal.kt | 4 +- src/prolog/ast/terms/Integer.kt | 32 ++ src/prolog/ast/terms/Operator.kt | 15 +- src/prolog/ast/terms/Structure.kt | 10 +- src/prolog/ast/terms/Term.kt | 9 +- src/prolog/ast/terms/Variable.kt | 14 +- src/prolog/builtins/arithmetic.kt | 1 - src/prolog/builtins/arithmeticOperators.kt | 152 +++++++ .../{control.kt => controlOperators.kt} | 37 +- src/prolog/builtins/meta.kt | 1 - src/prolog/builtins/other.kt | 8 +- src/prolog/builtins/unification.kt | 34 +- src/prolog/logic/arithmetic.kt | 150 ++++++ src/prolog/logic/{unify.kt => unification.kt} | 55 ++- .../{builtins => logic}/verification.kt | 4 +- tests/prolog/EvaluationTest.kt | 2 +- .../builtins/ArithmeticOperatorsTests.kt | 426 ++++++++++++++++++ ...{ControlBuiltinsTest.kt => ControlTest.kt} | 4 +- .../builtins/TermAnalysisConstructionTest.kt | 2 + tests/prolog/builtins/UnificationTest.kt | 52 +++ ...ionBuiltinsTest.kt => VerificationTest.kt} | 5 +- tests/prolog/logic/ArithmeticTests.kt | 357 +++++++++++++++ tests/prolog/logic/UnifyTest.kt | 23 +- 32 files changed, 1354 insertions(+), 92 deletions(-) rename {pl => examples}/scratchpad.pl (100%) create mode 100644 src/prolog/ast/arithmetic/ArithmeticOperator.kt create mode 100644 src/prolog/ast/arithmetic/Expression.kt create mode 100644 src/prolog/ast/logic/LogicOperand.kt create mode 100644 src/prolog/ast/logic/LogicOperator.kt create mode 100644 src/prolog/ast/terms/Integer.kt delete mode 100644 src/prolog/builtins/arithmetic.kt create mode 100644 src/prolog/builtins/arithmeticOperators.kt rename src/prolog/builtins/{control.kt => controlOperators.kt} (54%) delete mode 100644 src/prolog/builtins/meta.kt create mode 100644 src/prolog/logic/arithmetic.kt rename src/prolog/logic/{unify.kt => unification.kt} (60%) rename src/prolog/{builtins => logic}/verification.kt (96%) create mode 100644 tests/prolog/builtins/ArithmeticOperatorsTests.kt rename tests/prolog/builtins/{ControlBuiltinsTest.kt => ControlTest.kt} (96%) create mode 100644 tests/prolog/builtins/UnificationTest.kt rename tests/prolog/builtins/{VerificationBuiltinsTest.kt => VerificationTest.kt} (98%) create mode 100644 tests/prolog/logic/ArithmeticTests.kt diff --git a/pl/scratchpad.pl b/examples/scratchpad.pl similarity index 100% rename from pl/scratchpad.pl rename to examples/scratchpad.pl diff --git a/src/prolog/Program.kt b/src/prolog/Program.kt index 9d8e126..1f36b17 100644 --- a/src/prolog/Program.kt +++ b/src/prolog/Program.kt @@ -2,12 +2,10 @@ package prolog 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 typealias Database = Program @@ -24,7 +22,6 @@ object Program: Resolvent { private fun setup() { // Initialize the program with built-in predicates load(listOf( - Fact(True()) )) } diff --git a/src/prolog/ast/arithmetic/ArithmeticOperator.kt b/src/prolog/ast/arithmetic/ArithmeticOperator.kt new file mode 100644 index 0000000..18ca16d --- /dev/null +++ b/src/prolog/ast/arithmetic/ArithmeticOperator.kt @@ -0,0 +1,12 @@ +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 +} diff --git a/src/prolog/ast/arithmetic/Expression.kt b/src/prolog/ast/arithmetic/Expression.kt new file mode 100644 index 0000000..cf5eb49 --- /dev/null +++ b/src/prolog/ast/arithmetic/Expression.kt @@ -0,0 +1,5 @@ +package prolog.ast.arithmetic + +import prolog.ast.terms.Term + +interface Expression : Term diff --git a/src/prolog/ast/logic/Clause.kt b/src/prolog/ast/logic/Clause.kt index e821ce0..0160600 100644 --- a/src/prolog/ast/logic/Clause.kt +++ b/src/prolog/ast/logic/Clause.kt @@ -37,8 +37,8 @@ abstract class Clause(private val head: Head, private val body: Body) : Resolven override fun toString(): String { return when { - body == True() -> head.toString() - else -> "$head :- $body" + body is True -> head.toString() + 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 index 3288836..a52990e 100644 --- a/src/prolog/ast/logic/Fact.kt +++ b/src/prolog/ast/logic/Fact.kt @@ -3,4 +3,4 @@ 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 +class Fact(head: Head) : Clause(head, True) \ No newline at end of file diff --git a/src/prolog/ast/logic/LogicOperand.kt b/src/prolog/ast/logic/LogicOperand.kt new file mode 100644 index 0000000..8732b8b --- /dev/null +++ b/src/prolog/ast/logic/LogicOperand.kt @@ -0,0 +1,5 @@ +package prolog.ast.logic + +import prolog.ast.terms.Operand + +abstract class LogicOperand : Operand, Provable diff --git a/src/prolog/ast/logic/LogicOperator.kt b/src/prolog/ast/logic/LogicOperator.kt new file mode 100644 index 0000000..632b1ea --- /dev/null +++ b/src/prolog/ast/logic/LogicOperator.kt @@ -0,0 +1,13 @@ +package prolog.ast.logic + +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 +} diff --git a/src/prolog/ast/terms/Atom.kt b/src/prolog/ast/terms/Atom.kt index c711590..fa8bc30 100644 --- a/src/prolog/ast/terms/Atom.kt +++ b/src/prolog/ast/terms/Atom.kt @@ -9,6 +9,11 @@ open class Atom(val name: String) : Goal(), Head, Body, Resolvent { 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 diff --git a/src/prolog/ast/terms/Goal.kt b/src/prolog/ast/terms/Goal.kt index 6d29ffb..342ecb5 100644 --- a/src/prolog/ast/terms/Goal.kt +++ b/src/prolog/ast/terms/Goal.kt @@ -1,7 +1,7 @@ package prolog.ast.terms import prolog.Program -import prolog.ast.logic.Provable +import prolog.ast.logic.LogicOperand import prolog.logic.Substituted /** @@ -11,7 +11,7 @@ import prolog.logic.Substituted * A goal either [succeeds][prolog.builtins.True], in which case the variables in the compound terms have a binding, * or it fails if Prolog fails to prove it. */ -abstract class Goal : Term, Provable { +abstract class Goal : LogicOperand(), Term { abstract val functor: Functor override fun prove(subs: Substituted): Sequence = Program.solve(this, subs) diff --git a/src/prolog/ast/terms/Integer.kt b/src/prolog/ast/terms/Integer.kt new file mode 100644 index 0000000..210566f --- /dev/null +++ b/src/prolog/ast/terms/Integer.kt @@ -0,0 +1,32 @@ +package prolog.ast.terms + +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 + } + } + + // Integers are already evaluated + override fun evaluate(subs: Substituted): Pair = Pair(this, emptyMap()) + + override fun toString(): String { + return value.toString() + } + + operator fun plus(other: Integer): Integer { + return Integer(value + other.value) + } + + operator fun minus(other: Integer): Integer { + return Integer(value - other.value) + } +} diff --git a/src/prolog/ast/terms/Operator.kt b/src/prolog/ast/terms/Operator.kt index 20d8764..9d0e067 100644 --- a/src/prolog/ast/terms/Operator.kt +++ b/src/prolog/ast/terms/Operator.kt @@ -1,21 +1,16 @@ package prolog.ast.terms -import prolog.ast.logic.Provable -import prolog.logic.Substituted +typealias Operand = Term abstract class Operator( private val symbol: Atom, - val leftOperand: Operand? = null, - val rightOperand: Operand -) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)), Provable { - abstract override fun prove(subs: Substituted): Sequence - + private val leftOperand: Operand? = null, + private val rightOperand: Operand +) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)) { override fun toString(): String { return when (leftOperand) { null -> "${symbol.name} $rightOperand" - else -> "$leftOperand ${symbol.name} $rightOperand" + else -> "($leftOperand ${symbol.name} $rightOperand)" } } } - -typealias Operand = Goal diff --git a/src/prolog/ast/terms/Structure.kt b/src/prolog/ast/terms/Structure.kt index 26e3ae3..e44b51c 100644 --- a/src/prolog/ast/terms/Structure.kt +++ b/src/prolog/ast/terms/Structure.kt @@ -1,7 +1,7 @@ package prolog.ast.terms import prolog.ast.logic.Resolvent -import prolog.builtins.equivalent +import prolog.logic.equivalent import prolog.logic.Substituted import prolog.logic.unifyLazy @@ -9,13 +9,19 @@ typealias Argument = Term typealias CompoundTerm = Structure -open class Structure(val name: Atom, val arguments: List) : Goal(), Head, Body, Resolvent { +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 { 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 -> { diff --git a/src/prolog/ast/terms/Term.kt b/src/prolog/ast/terms/Term.kt index 80d338f..47f3064 100644 --- a/src/prolog/ast/terms/Term.kt +++ b/src/prolog/ast/terms/Term.kt @@ -1,9 +1,16 @@ package prolog.ast.terms +import prolog.logic.Substituted + /** * 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 +interface Term : Comparable { + /** + * Returns the term that this expression evaluates to. (All the way down.) + */ + fun evaluate(subs: Substituted): Pair +} diff --git a/src/prolog/ast/terms/Variable.kt b/src/prolog/ast/terms/Variable.kt index 429d408..2968bab 100644 --- a/src/prolog/ast/terms/Variable.kt +++ b/src/prolog/ast/terms/Variable.kt @@ -1,8 +1,10 @@ package prolog.ast.terms +import prolog.ast.arithmetic.Expression +import prolog.logic.Substituted import java.util.* -data class Variable(val name: String) : Term { +data class Variable(val name: String) : Term, Expression { private var alias: Optional = Optional.empty() fun alias(): Optional { @@ -21,6 +23,16 @@ data class Variable(val name: String) : Term { alias = Optional.empty() } + override fun evaluate(subs: Substituted): Pair { + // 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()) + } + } + override fun compareTo(other: Term): Int { return when (other) { is Variable -> name.compareTo(other.name) diff --git a/src/prolog/builtins/arithmetic.kt b/src/prolog/builtins/arithmetic.kt deleted file mode 100644 index 6021440..0000000 --- a/src/prolog/builtins/arithmetic.kt +++ /dev/null @@ -1 +0,0 @@ -package prolog.builtins diff --git a/src/prolog/builtins/arithmeticOperators.kt b/src/prolog/builtins/arithmeticOperators.kt new file mode 100644 index 0000000..b78020c --- /dev/null +++ b/src/prolog/builtins/arithmeticOperators.kt @@ -0,0 +1,152 @@ +package prolog.builtins + +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.terms.* +import prolog.logic.* + +// TODO > + +// TODO < + +// TODO =< + +// TODO >= + +/** + * 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) + + // Should both be instantiated + if (!atomic(t1.first) || !atomic(t2.first)) { + throw IllegalArgumentException("Both operands must be instantiated") + } + + return if (equivalent(t1.first, t2.first)) { + Pair(False, emptyMap()) + } else { + Pair(True, t1.second + t2.second) + } + } + +} + +/** + * 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) + + // Should both be instantiated + if (!atomic(t1.first) || !atomic(t2.first)) { + throw IllegalArgumentException("Both operands must be instantiated") + } + + return if (equivalent(t1.first, t2.first)) { + Pair(True, t1.second + t2.second) + } else { + Pair(False, emptyMap()) + } + } +} + +/** + * 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) + + if (!atomic(t2.first)) { + throw IllegalArgumentException("Arguments are not sufficiently instantiated") + } + + return unifyLazy(t1.first, t2.first, subs).map{ it + t1.second + t2.second } + } +} + +/** + * Result = -Expr + */ +class Negate(operand: Expression) : Subtract(Integer(0), operand) + +/** + * Result = Expr + */ +class Positive(operand: Expression) : Add(Integer(0), operand) + +/** + * Result = Expr1 + Expr2 + */ +open class Add(private val expr1: Expression, private val expr2: Expression) : + ArithmeticOperator(Atom("+"), expr1, expr2) { + override fun evaluate(subs: Substituted): Pair { + val result = Variable("Result") + val map = plus(expr1, expr2, result, subs) + return result.evaluate(map.first()) + } +} + +/** + * Result = Expr1 - Expr2 + */ +open class Subtract(private val expr1: Expression, private val expr2: Expression) : + ArithmeticOperator(Atom("-"), expr1, expr2) { + override fun evaluate(subs: Substituted): Pair { + val result = Variable("Result") + val map = plus(expr2, result, expr1, subs) + return result.evaluate(map.first()) + } +} + +// TODO Expr * Expr +/** + * Result = Expr1 * Expr2 + */ +class Multiply(private val expr1: Expression, private val expr2: Expression) : + ArithmeticOperator(Atom("*"), expr1, expr2) { + override fun evaluate(subs: Substituted): Pair { + val result = Variable("Result") + val map = mul(expr1, expr2, result, subs) + return result.evaluate(map.first()) + } +} + +// TODO Expr / Expr + +// TODO Expr mod Expr + +// TODO Expr rem Expr + +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) + + require(e1.first is Integer && e2.first is Integer) { "Arguments must be integers" } + + val v1 = e1.first as Integer + val v2 = e2.first as Integer + + return if (variable(e3.first)) { + between(v1, v2, e3.first as Variable).map { it + e1.second + e2.second } + } else { + between(v1, v2, e3.first as Integer).map { it + e1.second + e2.second } + } + } +} diff --git a/src/prolog/builtins/control.kt b/src/prolog/builtins/controlOperators.kt similarity index 54% rename from src/prolog/builtins/control.kt rename to src/prolog/builtins/controlOperators.kt index c2eebea..4dfeef9 100644 --- a/src/prolog/builtins/control.kt +++ b/src/prolog/builtins/controlOperators.kt @@ -1,12 +1,16 @@ package prolog.builtins -import prolog.ast.terms.* +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. */ -class Fail : Atom("fail"), Body { +object Fail : Atom("fail"), Body { override fun prove(subs: Substituted): Sequence = emptySequence() } @@ -18,7 +22,7 @@ typealias False = Fail /** * Always succeed. */ -class True : Atom("true"), Body { +object True : Atom("true"), Body { override fun prove(subs: Substituted): Sequence = sequenceOf(emptyMap()) } @@ -29,16 +33,12 @@ class True : Atom("true"), Body { /** * Conjunction (and). True if both Goal1 and Goal2 are true. */ -class Conjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(","), leftOperand, rightOperand) { +class Conjunction(private val left: LogicOperand, private val right: LogicOperand) : LogicOperator(Atom(","), left, right) { override fun prove(subs: Substituted): Sequence = sequence { - if (leftOperand != null) { - leftOperand.prove(subs).forEach { left -> - rightOperand.prove(subs + left).forEach { right -> - yield(left + right) - } + left.prove(subs).forEach { left -> + right.prove(subs + left).forEach { right -> + yield(left + right) } - } else { - yieldAll(rightOperand.prove(subs)) } } } @@ -46,17 +46,16 @@ class Conjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(" /** * Disjunction (or). True if either Goal1 or Goal2 succeeds. */ -open class Disjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(";"), leftOperand, rightOperand) { +open class Disjunction(private val left: LogicOperand, private val right: LogicOperand) : + LogicOperator(Atom(";"), left, right) { override fun prove(subs: Substituted): Sequence = sequence { - if (leftOperand != null) { - yieldAll(leftOperand.prove(subs)) - } - yieldAll(rightOperand.prove(subs)) + yieldAll(left.prove(subs)) + yieldAll(right.prove(subs)) } } @Deprecated("Use Disjunction instead") -class Bar(leftOperand: Operand, rightOperand: Operand) : Disjunction(leftOperand, rightOperand) +class Bar(leftOperand: LogicOperand, rightOperand: LogicOperand) : Disjunction(leftOperand, rightOperand) // TODO -> @@ -65,10 +64,10 @@ class Bar(leftOperand: Operand, rightOperand: Operand) : Disjunction(leftOperand /** * True if 'Goal' cannot be proven. */ -class Not(goal: Goal) : Operator(Atom("\\+"), rightOperand = goal) { +class Not(private val goal: Goal) : LogicOperator(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()) { + if (goal.prove(subs).toList().isNotEmpty()) { return emptySequence() } // If the goal cannot be proven, return a sequence with an empty map diff --git a/src/prolog/builtins/meta.kt b/src/prolog/builtins/meta.kt deleted file mode 100644 index 6021440..0000000 --- a/src/prolog/builtins/meta.kt +++ /dev/null @@ -1 +0,0 @@ -package prolog.builtins diff --git a/src/prolog/builtins/other.kt b/src/prolog/builtins/other.kt index 3b3ed3d..defb38f 100644 --- a/src/prolog/builtins/other.kt +++ b/src/prolog/builtins/other.kt @@ -1,10 +1,10 @@ package prolog.builtins +import prolog.ast.logic.LogicOperand import prolog.ast.terms.Atom -import prolog.ast.terms.Operand -import prolog.ast.terms.Operator +import prolog.ast.logic.LogicOperator import prolog.logic.Substituted -class Query(rightOperand: Operand) : Operator(Atom("?-"), null, rightOperand) { - override fun prove(subs: Substituted): Sequence = rightOperand.prove(subs) +class Query(private val query: LogicOperand) : LogicOperator(Atom("?-"), null, query) { + override fun prove(subs: Substituted): Sequence = query.prove(subs) } diff --git a/src/prolog/builtins/unification.kt b/src/prolog/builtins/unification.kt index ffb75bc..a90616f 100644 --- a/src/prolog/builtins/unification.kt +++ b/src/prolog/builtins/unification.kt @@ -1,24 +1,24 @@ +/** + * Comparison and Unification of Terms + * + * [SWI Prolog Documentation](https://www.swi-prolog.org/pldoc/man?section=compare) + */ package prolog.builtins import prolog.ast.terms.Atom -import prolog.ast.terms.Structure +import prolog.ast.terms.Operator import prolog.ast.terms.Term -import prolog.ast.terms.Variable +import prolog.logic.Substituted +import prolog.logic.applySubstitution +import prolog.logic.equivalent -/** - * True if Term1 is equivalent to Term2. A variable is only identical to a sharing variable. - */ -fun equivalent(term1: Term, term2: Term): Boolean { - return when { - 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 Atom && term2 is Atom -> term1.compareTo(term2) == 0 - term1 is Structure && term2 is Structure -> term1.compareTo(term2) == 0 - else -> false +class Equivalent(private val term1: Term, private val term2: Term) : Operator(Atom("=="), term1, term2) { + override fun prove(subs: Substituted): Sequence = sequence { + val t1 = applySubstitution(term1, subs) + val t2 = applySubstitution(term2, subs) + + if (equivalent(t1, t2)) { + yield(emptyMap()) + } } } - -/** - * - */ diff --git a/src/prolog/logic/arithmetic.kt b/src/prolog/logic/arithmetic.kt new file mode 100644 index 0000000..dd00ba9 --- /dev/null +++ b/src/prolog/logic/arithmetic.kt @@ -0,0 +1,150 @@ +package prolog.logic + +import prolog.ast.arithmetic.Expression +import prolog.ast.terms.Integer +import prolog.ast.terms.Variable +import prolog.builtins.Is +import java.util.* + +/** + * Low and High are integers, High ≥Low. + * + * 1. If Value is an integer, Low ≤ Value ≤ High. + * 2. When Value is a variable it is successively bound to all integers between Low and High. + * If High is inf or infinite between/3 is true iff Value ≥ Low, a feature that is particularly interesting for + * generating integers from a certain value. + */ +fun between( + low: Integer, + high: Integer, + value: Integer +): Sequence { + return if (value.value in low.value..high.value) { + sequenceOf(emptyMap()) + } else { + emptySequence() + } +} + +fun between( + low: Integer, + high: Integer, + variable: Variable +): Sequence { + return sequence { + for (i in low.value..high.value) { + yield(mapOf(variable to Integer(i))) + } + } +} + +/** + * True if Int2 = Int1 + 1 and Int1 ≥ 0. + * + * At least one of the arguments must be instantiated to a natural number. + * + * @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 { + 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 -> + val t1 = applySubstitution(term1, newSubs) + 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 + } + } + yield(newSubs) + }} +} + +/** + * True if Int3 = Int1 + Int2. + * + * At least two of the three arguments must be instantiated to integers. + */ +fun plus(term1: Expression, term2: Expression, term3: Expression, subs: Substituted): Sequence = sequence { + val t1 = applySubstitution(term1, subs) + val t2 = applySubstitution(term2, subs) + val t3 = applySubstitution(term3, subs) + + // At least two arguments must be Integers + when { + nonvariable(t1) && nonvariable(t2) && nonvariable(t3) -> { + val e1 = t1.evaluate(subs) + val e2 = t2.evaluate(subs) + val e3 = t3.evaluate(subs) + + val int3Value = e1.first as Integer + e2.first as Integer + if (int3Value == e3.first as Integer) { + yield(e1.second + e2.second + e3.second) + } + } + nonvariable(t1) && nonvariable(t2) && variable(t3) -> { + val e1 = t1.evaluate(subs) + val e2 = t2.evaluate(subs) + + val int3Value = e1.first as Integer + e2.first as Integer + val int3 = t3 as Variable + int3.bind(int3Value) + yield(mapOf(int3 to int3Value) + e1.second + e2.second) + } + nonvariable(t1) && variable(t2) && nonvariable(t3) -> { + val e1 = t1.evaluate(subs) + val e3 = t3.evaluate(subs) + + val int2Value = e3.first as Integer - e1.first as Integer + val int2 = t2 as Variable + int2.bind(int2Value) + yield(mapOf(int2 to int2Value) + e1.second + e3.second) + } + variable(t1) && nonvariable(t2) && nonvariable(t3) -> { + val e2 = t2.evaluate(subs) + val e3 = t3.evaluate(subs) + + val int1Value = e3.first as Integer - e2.first as Integer + val int1 = t1 as Variable + int1.bind(int1Value) + yield(mapOf(int1 to int1Value) + e2.second + e3.second) + } + else -> { + throw IllegalArgumentException("At least two arguments must be instantiated to integers") + } + } +} + +/** + * Recursive implementation of the multiply operator, logical programming-wise. + */ +fun mul(term1: Expression, term2: Expression, term3: Expression, subs: Substituted): Sequence = sequence { + val t1 = applySubstitution(term1, subs) + val t2 = applySubstitution(term2, subs) + val t3 = applySubstitution(term3, subs) + + // Base case + if (equivalent(t2, Integer(0))) { + yieldAll(Is(t3, Integer(0)).prove(subs)) + } + + // Recursive case + try { + val decremented = Variable("Decremented") + succ(decremented, t2, subs).forEach { decrementMap -> + val multiplied = Variable("Multiplied") + mul(t1, decremented, multiplied, subs + decrementMap).forEach { multipliedMap -> + yieldAll(plus(t1, multiplied, t3, subs + decrementMap + multipliedMap)) + } + } + } catch(_: Exception) { + } +} + +// TODO divmod + +// TODO nth_integer_root_and_remainder \ No newline at end of file diff --git a/src/prolog/logic/unify.kt b/src/prolog/logic/unification.kt similarity index 60% rename from src/prolog/logic/unify.kt rename to src/prolog/logic/unification.kt index 2a1e411..aae0669 100644 --- a/src/prolog/logic/unify.kt +++ b/src/prolog/logic/unification.kt @@ -1,27 +1,33 @@ 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.ast.arithmetic.Expression +import prolog.ast.logic.LogicOperator +import prolog.ast.terms.* import java.util.* typealias Substituted = Map // Apply substitutions to a term -private fun applySubstitution(term: Term, substitution: Substituted): Term = when { - variable(term) -> substitution[(term as Variable)] ?: term +fun applySubstitution(term: Term, subs: Substituted): Term = when { + variable(term) -> subs[(term as Variable)] ?: term atomic(term) -> term compound(term) -> { val structure = term as Structure - Structure(structure.name, structure.arguments.map { applySubstitution(it, substitution) }) + 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 + expr is LogicOperator -> { + expr.arguments = expr.arguments.map { applySubstitution(it, subs) } + expr + } + else -> expr +} + // Check if a variable occurs in a term private fun occurs(variable: Variable, term: Term): Boolean = when { variable(term) -> term == variable @@ -33,8 +39,8 @@ private fun occurs(variable: Variable, term: Term): Boolean = when { else -> false } -// Generate possible substitutions -private fun generateSubstitutions(term1: Term, term2: Term, subs: Substituted): Sequence = sequence { +// Unify two terms with backtracking and lazy evaluation +fun unifyLazy(term1: Term, term2: Term, subs: Substituted): Sequence = sequence { val t1 = applySubstitution(term1, subs) val t2 = applySubstitution(term2, subs) @@ -59,7 +65,7 @@ private fun generateSubstitutions(term1: Term, term2: Term, subs: Substituted): val structure2 = t2 as Structure if (structure1.functor == structure2.functor) { val newSubstitution = structure1.arguments.zip(structure2.arguments).fold(subs) { acc, (arg1, arg2) -> - generateSubstitutions(arg1, arg2, acc).firstOrNull() ?: return@sequence + unifyLazy(arg1, arg2, acc).firstOrNull() ?: return@sequence } yield(newSubstitution) } @@ -68,14 +74,6 @@ private fun generateSubstitutions(term1: Term, term2: Term, subs: Substituted): } } -// Unify two terms with backtracking and lazy evaluation -fun unifyLazy(term1: Term, term2: Term, subs: Substituted): Sequence = sequence { - generateSubstitutions(term1, term2, subs).forEach { newSubs -> - // Return the new substitution - yield(newSubs) - } -} - fun unify(term1: Term, term2: Term): Optional { val substitutions = unifyLazy(term1, term2, emptyMap()).toList() return if (substitutions.isNotEmpty()) { @@ -84,3 +82,18 @@ fun unify(term1: Term, term2: Term): Optional { Optional.empty() } } + +/** + * True if Term1 is equivalent to Term2. A variable is only identical to a sharing variable. + */ +fun equivalent(term1: Term, term2: Term): 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 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) + else -> false + } +} diff --git a/src/prolog/builtins/verification.kt b/src/prolog/logic/verification.kt similarity index 96% rename from src/prolog/builtins/verification.kt rename to src/prolog/logic/verification.kt index 8bb2cb1..b89758e 100644 --- a/src/prolog/builtins/verification.kt +++ b/src/prolog/logic/verification.kt @@ -1,4 +1,4 @@ -package prolog.builtins +package prolog.logic import prolog.ast.terms.CompoundTerm import prolog.ast.terms.Term @@ -37,5 +37,5 @@ fun variable(term: Term): Boolean { return term.alias().isEmpty || term.alias().get() === term || variable(term.alias().get()) } - return false; + return false } diff --git a/tests/prolog/EvaluationTest.kt b/tests/prolog/EvaluationTest.kt index 50ac65d..7e7e4d7 100644 --- a/tests/prolog/EvaluationTest.kt +++ b/tests/prolog/EvaluationTest.kt @@ -8,7 +8,7 @@ import prolog.ast.logic.Rule import prolog.builtins.Conjunction import prolog.builtins.Disjunction import prolog.builtins.Query -import prolog.builtins.equivalent +import prolog.logic.equivalent import prolog.ast.terms.Atom import prolog.ast.terms.Structure import prolog.ast.terms.Variable diff --git a/tests/prolog/builtins/ArithmeticOperatorsTests.kt b/tests/prolog/builtins/ArithmeticOperatorsTests.kt new file mode 100644 index 0000000..77c6a10 --- /dev/null +++ b/tests/prolog/builtins/ArithmeticOperatorsTests.kt @@ -0,0 +1,426 @@ +package prolog.builtins + +import org.junit.jupiter.api.Assertions.* +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.assertThrows +import prolog.ast.terms.Integer +import prolog.ast.terms.Variable +import prolog.logic.between +import prolog.logic.equivalent + +class ArithmeticOperatorsTests { + @Test + fun `1 evaluates to 1`() { + val op1 = EvaluatesTo( + Integer(1), + Integer(1) + ) + + var result = op1.evaluate(emptyMap()).first + + assertEquals(True, result, "1 should be equal to 1") + + val op2 = EvaluatesToDifferent( + Integer(1), + Integer(1) + ) + + result = op2.evaluate(emptyMap()).first + + assertEquals(False, result, "1 should not be different from 1") + } + + @Test + fun `1 does not evaluate to 2`() { + val op1 = EvaluatesTo( + Integer(1), + Integer(2) + ) + + var result = op1.evaluate(emptyMap()).first + + assertEquals(False, result, "1 should not be equal to 2") + + val op2 = EvaluatesToDifferent( + Integer(1), + Integer(2) + ) + + result = op2.evaluate(emptyMap()).first + + assertEquals(True, result, "1 should be different from 2") + } + + @Test + fun `2 + 3 evaluates to 5`() { + val op = EvaluatesTo( + Add(Integer(2), Integer(3)), + Integer(5) + ) + + var result = op.evaluate(emptyMap()).first + + assertEquals(True, result, "2 + 3 should be equal to 5") + + val op2 = EvaluatesToDifferent( + Add(Integer(2), Integer(3)), + Integer(5) + ) + + result = op2.evaluate(emptyMap()).first + + assertEquals(False, result, "2 + 3 should not be different from 5") + } + + @Test + fun `2 + 3 evaluates to 4 + 1`() { + val op = EvaluatesTo( + Add(Integer(2), Integer(3)), + Add(Integer(4), Integer(1)) + ) + + var result = op.evaluate(emptyMap()).first + + assertEquals(True, result, "2 + 3 should be equal to 4 + 1") + + val op2 = EvaluatesToDifferent( + Add(Integer(2), Integer(3)), + Add(Integer(4), Integer(1)) + ) + + result = op2.evaluate(emptyMap()).first + + assertEquals(False, result, "2 + 3 should not be different from 4 + 1") + } + + @Test + fun `1 evaluates to variable not sufficiently instantiated`() { + val op = EvaluatesTo( + Integer(1), + Variable("X") + ) + + assertThrows { op.evaluate(emptyMap()) } + + val op2 = EvaluatesToDifferent( + Integer(1), + Variable("X") + ) + + assertThrows { op2.evaluate(emptyMap()) } + } + + @Test + fun `(1 + var) evaluates to 1 not sufficiently instantiated`() { + val op = EvaluatesTo( + Add(Integer(1), Variable("X")), + Integer(1) + ) + + assertThrows { op.evaluate(emptyMap()) } + + val op2 = EvaluatesToDifferent( + Add(Integer(1), Variable("X")), + Integer(1) + ) + + assertThrows { op2.evaluate(emptyMap()) } + } + + @Test + fun `1 is 1`() { + val op = Is( + Integer(1), + Integer(1) + ) + + val result = op.prove(emptyMap()) + + assertTrue(result.any(), "1 should be equal to 1") + } + + @Test + fun `1 is not 2`() { + val op = Is( + Integer(1), + Integer(2) + ) + + val result = op.prove(emptyMap()).toList() + + assertTrue(result.isEmpty(), "1 should not be equal to 2") + } + + @Test + fun `bound-to-1-var is 1`() { + val t1 = Variable("X") + val op = Is( + t1, + Integer(1) + ) + + t1.bind(Integer(1)) + + val result = op.prove(emptyMap()) + + assertTrue(result.any(), "X should be equal to 1") + assertTrue(result.first().isEmpty(), "X should not be rebound") + } + + @Test + fun `bound-to-2-var is not 1`() { + val t1 = Variable("X") + val op = Is( + t1, + Integer(1) + ) + + t1.bind(Integer(2)) + + val result = op.prove(emptyMap()) + + assertFalse(result.any(), "X should not be equal to 1") + } + + @Test + fun `variable is 1`() { + val op = Is( + Variable("X"), + Integer(1) + ) + + val result = op.prove(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") + } + + @Test + fun `variable is 1 + 2`() { + val op = Is( + Variable("X"), + Add(Integer(1), Integer(2)) + ) + + val result = op.prove(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") + } + + @Test + fun `var is var should throw`() { + val op = Is( + Variable("X"), + Variable("Y") + ) + + assertThrows { op.prove(emptyMap()) } + } + + @Test + fun `1 is var should throw`() { + val op = Is( + Integer(1), + Variable("X") + ) + + assertThrows { op.prove(emptyMap()) } + } + + @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 result = op.prove(emptyMap()).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") + } + + /** + * ?- between(1, 2, X), Y is 1 + X. + * X = 1, Y = 2 ; + * X = 2, Y = 3 . + */ + @Test + fun `between 1 and 2 plus 1 to get 2 and 3`() { + val t1 = Integer(1) + val t2 = Integer(2) + val t3 = Variable("X") + val t4 = Variable("Y") + + val op = Conjunction( + Between(t1, t2, t3), + Is(t4, Add(Integer(1), t3)) + ) + } + + @Test + fun `negate 1 to get -1`() { + val t1 = Integer(1) + + val result = Negate(t1).evaluate(emptyMap()).first + + assertEquals(Integer(-1), result, "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 + + assertEquals(Integer(0), result, "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 + + assertEquals(Integer(1), result, "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 result = Negate(t1).evaluate(emptyMap()).first + + 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") + } + + @Test + fun `negate 1 + 3 to get -4`() { + val t1 = Integer(1) + val t2 = Integer(3) + + val result = Negate(Add(t1, t2)).evaluate(emptyMap()).first + + assertEquals(Integer(-4), result, "negate(1 + 3) should be equal to -4") + } + + @Test + fun `Add 1 and 2 to get 3`() { + val t1 = Integer(1) + val t2 = Integer(2) + + 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`() { + val t1 = Integer(1) + val t2 = Variable("X") + + t2.bind(Integer(2)) + + 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") + } + + @Test + fun `Subtract 1 and 2 to get -1`() { + val t1 = Integer(1) + val t2 = Integer(2) + + val result = Subtract(t1, t2).evaluate(emptyMap()).first + + assertEquals(Integer(-1), result, "1 - 2 should be equal to -1") + } + + @Test + fun `Subtract 3 and 1 to get 2`() { + val t1 = Integer(3) + val t2 = Integer(1) + + val result = Subtract(t1, t2).evaluate(emptyMap()).first + + assertEquals(Integer(2), result, "3 - 1 should be equal to 2") + } + + @Test + fun `Multiply 0 and 0 to get 0`() { + val t1 = Integer(0) + val t2 = Integer(0) + + val result = Multiply(t1, t2).evaluate(emptyMap()).first + + assertEquals(Integer(0), result, "0 * 0 should be equal to 0") + } + + @Test + fun `Multiply 1 and 0 to get 0`() { + val t1 = Integer(1) + val t2 = Integer(0) + + val result = Multiply(t1, t2).evaluate(emptyMap()).first + + assertEquals(Integer(0), result, "1 * 0 should be equal to 0") + } + + @Test + fun `Multiply 0 and 1 to get 0`() { + val t1 = Integer(0) + val t2 = Integer(1) + + val result = Multiply(t1, t2).evaluate(emptyMap()).first + + assertEquals(Integer(0), result, "0 * 1 should be equal to 0") + } + + @Test + fun `Multiply 3 and 1 to get 3`() { + val t1 = Integer(3) + val t2 = Integer(1) + + val result = Multiply(t1, t2).evaluate(emptyMap()).first + + assertEquals(Integer(3), result, "3 * 1 should be equal to 3") + } + + @Test + fun `Multiply 2 and 3 to get 6`() { + val t1 = Integer(2) + val t2 = Integer(3) + + val result = Multiply(t1, t2).evaluate(emptyMap()).toList() + + assertEquals(1, result.size, "There should only be one solution") + assertEquals(Integer(6), result, "2 * 3 should be equal to 6") + } +} diff --git a/tests/prolog/builtins/ControlBuiltinsTest.kt b/tests/prolog/builtins/ControlTest.kt similarity index 96% rename from tests/prolog/builtins/ControlBuiltinsTest.kt rename to tests/prolog/builtins/ControlTest.kt index 225f386..11e835e 100644 --- a/tests/prolog/builtins/ControlBuiltinsTest.kt +++ b/tests/prolog/builtins/ControlTest.kt @@ -8,7 +8,7 @@ import prolog.Program import prolog.ast.logic.Fact import prolog.ast.terms.Atom -class ControlBuiltinsTest { +class ControlTest { @BeforeEach fun setUp() { Program.clear() @@ -55,7 +55,7 @@ class ControlBuiltinsTest { Program.load(listOf(success, failure)) val goal = Atom("a") - val failGoal = Fail() + val failGoal = Fail val result1 = Program.query(goal) val result2 = Program.query(failGoal) diff --git a/tests/prolog/builtins/TermAnalysisConstructionTest.kt b/tests/prolog/builtins/TermAnalysisConstructionTest.kt index a43b6cc..09c5a0a 100644 --- a/tests/prolog/builtins/TermAnalysisConstructionTest.kt +++ b/tests/prolog/builtins/TermAnalysisConstructionTest.kt @@ -5,6 +5,8 @@ import org.junit.jupiter.api.Assertions.assertTrue import org.junit.jupiter.api.Test import prolog.ast.terms.Atom import prolog.ast.terms.Structure +import prolog.logic.atomic +import prolog.logic.compound /** * 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/UnificationTest.kt b/tests/prolog/builtins/UnificationTest.kt new file mode 100644 index 0000000..267e41d --- /dev/null +++ b/tests/prolog/builtins/UnificationTest.kt @@ -0,0 +1,52 @@ +package prolog.builtins + +import org.junit.jupiter.api.Assertions.* +import org.junit.jupiter.api.Test +import prolog.ast.terms.Atom +import prolog.ast.terms.Integer +import prolog.ast.terms.Variable + +class UnificationTest { + /** + * ?- X == a. + * false. + */ + @Test + fun equivalent_variable_and_atom() { + val variable = Variable("X") + val atom = Atom("a") + + val result = Equivalent(variable, atom).prove(emptyMap()) + + assertFalse(result.any(), "Variable and atom should not be equivalent") + } + + /** + * ?- a == a. + * true. + */ + @Test + fun equivalent_atom_and_atom() { + val atom1 = Atom("a") + val atom2 = Atom("a") + + val result = Equivalent(atom1, atom2).prove(emptyMap()) + + assertTrue(result.any(), "Identical atoms should be equivalent") + assertEquals(0, result.first().size, "No substitutions should be made") + } + + /** + * ?- 1 + 2 == 3. + * false. + */ + @Test + fun simple_addition_equivalence() { + val addition = Add(Integer(1), Integer(2)) + val solution = Integer(3) + + val result = Equivalent(addition, solution).prove(emptyMap()) + + assertFalse(result.any(), "Addition should be equivalent") + } +} diff --git a/tests/prolog/builtins/VerificationBuiltinsTest.kt b/tests/prolog/builtins/VerificationTest.kt similarity index 98% rename from tests/prolog/builtins/VerificationBuiltinsTest.kt rename to tests/prolog/builtins/VerificationTest.kt index b8e5e9b..ce8af97 100644 --- a/tests/prolog/builtins/VerificationBuiltinsTest.kt +++ b/tests/prolog/builtins/VerificationTest.kt @@ -6,9 +6,12 @@ import org.junit.jupiter.api.Test 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 VerificationBuiltinsTest { +class VerificationTest { @Test fun unbound_variable_is_var() { val variable = Variable("X") diff --git a/tests/prolog/logic/ArithmeticTests.kt b/tests/prolog/logic/ArithmeticTests.kt new file mode 100644 index 0000000..fdf4c68 --- /dev/null +++ b/tests/prolog/logic/ArithmeticTests.kt @@ -0,0 +1,357 @@ +package prolog.logic + +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.assertThrows +import prolog.ast.terms.Integer +import prolog.ast.terms.Term +import prolog.ast.terms.Variable + +class ArithmeticTests { + @Test + fun `1_between_0_and_2`() { + 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") + } + + @Test + fun `3_not_between_0_and_2`() { + val result = between(Integer(0), Integer(2), Integer(3)) + + assertTrue(result.none(), "Expected 3 not to be between 0 and 2") + } + + @Test + fun numbers_between_0_and_2() { + val result = between(Integer(0), Integer(2), Variable("X")) + + val expectedResults = listOf( + mapOf(Variable("X") to Integer(0)), + mapOf(Variable("X") to Integer(1)), + mapOf(Variable("X") to Integer(2)) + ) + + val actualResults = result.toList() + assertEquals(expectedResults.size, actualResults.size, "Expected 3 results") + for ((expected, actual) in expectedResults.zip(actualResults)) { + for ((key, value) in expected) { + assertTrue(actual.containsKey(key), "Expected key $key to be present") + assertTrue( + equivalent(value, actual[key]!!), + "Expected value $value for key $key, but got ${actual[key]}" + ) + } + } + } + + @Test + fun `succ(0) is 1`() { + val t1 = Integer(0) + + val expected = Integer(1) + + val result = succ(t1, expected, emptyMap()) + + assertTrue(result.any(), "Expected 0 + 1 to be equal to 1") + assertTrue(result.first().isEmpty(), "Expected no substitutions") + } + + @Test + fun `succ(1) is 2`() { + val t1 = Integer(1) + + val expected = Integer(2) + + val result = succ(t1, expected, emptyMap()) + + assertTrue(result.any(), "Expected 1 + 1 to be equal to 2") + assertTrue(result.first().isEmpty(), "Expected no substitutions") + } + + @Test + fun `succ(1) is var`() { + val t1 = Integer(1) + val t2 = Variable("X") + + val expected = Integer(2) + + val result = succ(t1, t2, emptyMap()).toList() + + assertTrue(result.isNotEmpty(), "Expected 1 + 1 to be equal to X") + assertTrue(result[0][t2] == expected, "Expected X to be equal to 2") + } + + @Test + fun `succ(bound-to-1-var) is 2`() { + val t1 = Variable("X") + val t2 = Integer(2) + + t1.bind(Integer(1)) + + val result = succ(t1, t2, emptyMap()) + + assertTrue(result.any(), "Expected X + 1 to be equal to 2") + assertTrue(result.first().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))) + + assertTrue(result.any(), "Expected X + 1 to be equal to 2") + assertTrue(result.first().isEmpty(), "Expected no substitutions") + } + + @Test + fun `succ(bound-to-1-var) is var`() { + val t1 = Variable("X") + val t2 = Variable("Y") + + t1.bind(Integer(1)) + + val result = succ(t1, t2, emptyMap()).toList() + + assertTrue(result.isNotEmpty(), "Expected X + 1 to be equal to Y") + assertTrue(result[0][t2] == Integer(2), "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() + + assertTrue(result.isNotEmpty(), "Expected X + 1 to be equal to Y") + assertTrue(result[0][t2] == Integer(2), "Expected Y to be equal to 2") + } + + @Test + fun `succ(var, 0) fails silently`() { + val t1 = Variable("X") + val t2 = Integer(0) + + val result = succ(t1, t2, emptyMap()).toList() + + assertTrue(result.isEmpty(), "Expected X + 1 to fail") + } + + @Test + fun `1_plus_2_is_3`() { + val t1 = Integer(1) + val t2 = Integer(2) + val t3 = Integer(3) + + val result = plus(t1, t2, t3, emptyMap()) + + assertTrue(result.any(), "1 + 2 should be equal to 3") + assertTrue(result.first().isEmpty(), "1 + 2 should be equal to 3") + } + + @Test + fun `1_plus_2_is_not_4`() { + val t1 = Integer(1) + val t2 = Integer(2) + val t3 = Integer(4) + + val result = plus(t1, t2, t3, emptyMap()) + + assertTrue(result.none(), "1 + 2 should not be equal to 4") + } + + @Test + fun `1_plus_2_is_variable`() { + val t1 = Integer(1) + val t2 = Integer(2) + val t3 = Variable("X") + + val result = plus(t1, t2, t3, emptyMap()).toList() + + assertTrue(result.isNotEmpty(), "1 + 2 should be equal to X") + assertTrue(equivalent(result[0][t3]!!, Integer(3)), "X should be equal to 3") + } + + @Test + fun `1_plus_variable_is_3`() { + val t1 = Integer(1) + val t2 = Variable("X") + val t3 = Integer(3) + + val result = plus(t1, t2, t3, emptyMap()).toList() + + assertTrue(result.isNotEmpty(), "1 + X should be equal to 3") + assertTrue(equivalent(result[0][t2]!!, Integer(2)), "X should be equal to 2") + } + + @Test + fun variable_plus_2_is_3() { + val t1 = Variable("X") + val t2 = Integer(2) + val t3 = Integer(3) + + val result = plus(t1, t2, t3, emptyMap()).toList() + + assertTrue(result.isNotEmpty(), "X + 2 should be equal to 3") + assertTrue(equivalent(result[0][t1]!!, Integer(1)), "X should be equal to 1") + } + + @Test + fun `1 plus 2 is bound-to-3-var`() { + val t1 = Integer(1) + val t2 = Integer(2) + val t3 = Variable("X") + + t3.bind(Integer(3)) + + val result = plus(t1, t2, t3, emptyMap()) + + assertTrue(result.any(), "1 + 2 should be equal to X") + assertTrue(result.first().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))) + + assertTrue(result.any(), "1 + 2 should be equal to X") + assertTrue(result.first().isEmpty(), "t3 should not be rebound") + } + + @Test + fun `1 plus 2 is bound-to-4-var`() { + val t1 = Integer(1) + val t2 = Integer(2) + val t3 = Variable("X") + + t3.bind(Integer(4)) + + val result = plus(t1, t2, t3, emptyMap()) + + assertTrue(result.none(), "1 + 2 should not be equal to X") + } + + @Test + fun `1 plus bound-to-2-var is 3`() { + val t1 = Integer(1) + val t2 = Variable("X") + val t3 = Integer(3) + + t2.bind(Integer(2)) + + val result = plus(t1, t2, t3, emptyMap()) + + assertTrue(result.any(), "1 + X should be equal to 3") + assertTrue(result.first().isEmpty(), "t2 should not be rebound") + } + + @Test + fun `1 plus bound-to-2-var is not 4`() { + val t1 = Integer(1) + val t2 = Variable("X") + val t3 = Integer(4) + + t2.bind(Integer(2)) + + val result = plus(t1, t2, t3, emptyMap()) + + assertTrue(result.none(), "1 + X should not be equal to 4") + } + + @Test + fun `bound-to-1-var plus 2 is 3`() { + val t1 = Variable("X") + val t2 = Integer(2) + val t3 = Integer(3) + + t1.bind(Integer(1)) + + val result = plus(t1, t2, t3, emptyMap()) + + assertTrue(result.any(), "X + 2 should be equal to 3") + assertTrue(result.first().none(), "t1 should not be rebound") + } + + @Test + fun `bound-to-1-var plus 2 is not 4`() { + val t1 = Variable("X") + val t2 = Integer(2) + val t3 = Integer(4) + + t1.bind(Integer(1)) + + val result = plus(t1, t2, t3, emptyMap()) + + assertTrue(result.none(), "X + 2 should not be equal to 4") + } + + @Test + fun `two unbound vars plus should throw`() { + val t1 = Variable("X") + val t2 = Variable("Y") + val t3 = Integer(3) + + assertThrows { + plus(t1, t2, t3, emptyMap()) + } + } + + @Test + fun `bound-to-1-var plus bound-to-2-var is variable`() { + val t1 = Variable("X") + val t2 = Variable("Y") + val t3 = Variable("Z") + + t1.bind(Integer(1)) + t2.bind(Integer(2)) + + val result = plus(t1, t2, t3, emptyMap()).toList() + + assertTrue(result.isNotEmpty(), "X + Y should be equal to Z") + assertTrue(equivalent(result[0][t3]!!, Integer(3)), "Z should be equal to 3") + } + + @Test + fun `1 times 1 is 1`() { + val t1 = Integer(1) + val t2 = Integer(1) + val t3 = Integer(1) + + val result = mul(t1, t2, t3, emptyMap()).toList() + + assertEquals(1, result.size, "There should be one solution") + assertTrue(result[0].isEmpty(), "1 * 1 should already be equal to 1") + } + + @Test + fun `2 times 3 is 6`() { + val t1 = Integer(2) + val t2 = Integer(3) + val t3 = Integer(6) + + val result = mul(t1, t2, t3, emptyMap()).toList() + + assertEquals(1, result.size, "There should be one solution") + assertTrue(result[0].isEmpty(), "2 * 3 should already be equal to 6") + } + + @Test + fun `2 times 3 is not 4`() { + val t1 = Integer(2) + val t2 = Integer(3) + val t3 = Integer(4) + + val result = mul(t1, t2, t3, emptyMap()) + + assertTrue(result.none(), "2 * 3 should not be equal to 4") + } +} diff --git a/tests/prolog/logic/UnifyTest.kt b/tests/prolog/logic/UnifyTest.kt index 0fe9d94..4045744 100644 --- a/tests/prolog/logic/UnifyTest.kt +++ b/tests/prolog/logic/UnifyTest.kt @@ -3,10 +3,10 @@ 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.Integer import prolog.ast.terms.Atom import prolog.ast.terms.Structure import prolog.ast.terms.Variable -import prolog.builtins.equivalent /* * Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms @@ -260,4 +260,25 @@ class UnifyTest { assertFalse(result.isPresent, "Atom with different arity should not unify") } + + @Test + fun identical_integers_unify() { + val int1 = Integer(1) + val int2 = Integer(1) + + val result = unify(int1, int2) + + assertTrue(result.isPresent, "Identical integers should unify") + assertEquals(0, result.get().size, "No substitutions should be made") + } + + @Test + fun different_integers_do_not_unify() { + val int1 = Integer(1) + val int2 = Integer(2) + + val result = unify(int1, int2) + + assertFalse(result.isPresent, "Different integers should not unify") + } } \ No newline at end of file