diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt index 686139f..559a7b2 100644 --- a/src/interpreter/Preprocessor.kt +++ b/src/interpreter/Preprocessor.kt @@ -59,6 +59,7 @@ open class Preprocessor { Structure(Atom("!"), emptyList()) -> Cut() Atom("inf") -> Integer(Int.MAX_VALUE) Atom("nl") -> Nl + Variable("_") -> AnonymousVariable.create() is Structure -> { // Preprocess the arguments first to recognize builtins val args = term.arguments.map { preprocess(it, nested = true) } @@ -86,6 +87,10 @@ open class Preprocessor { Not(args[0] as Goal) } + term.functor == "==/2" -> { + Equivalent(args[0], args[1]) + } + term.functor == "=\\=/2" && args.all { it is Expression } -> { EvaluatesToDifferent(args[0] as Expression, args[1] as Expression) } @@ -133,7 +138,10 @@ open class Preprocessor { term.functor == "read/1" -> Read(args[0]) term.functor == "initialization/1" -> Initialization(args[0] as Goal) - else -> term + else -> { + term.arguments = args + term + } } } diff --git a/src/parser/grammars/TermsGrammar.kt b/src/parser/grammars/TermsGrammar.kt index 1d20fc1..487f9f7 100644 --- a/src/parser/grammars/TermsGrammar.kt +++ b/src/parser/grammars/TermsGrammar.kt @@ -36,8 +36,8 @@ import prolog.ast.terms.* open class TermsGrammar : Tokens() { // Basic named terms - protected val variable: Parser by variableToken use { Variable(text) } - protected val simpleAtom: Parser by nameToken use { Atom(text) } + protected val variable: Parser by (variableToken or anonymousVariableToken) use { Variable(text) } + protected val simpleAtom: Parser by (nameToken or exclamation) use { Atom(text) } protected val quotedAtom: Parser by (dummy or ticked or doubleTicked @@ -85,7 +85,7 @@ open class TermsGrammar : Tokens() { } // Level 700 - comparison operators - protected val op700: Parser by (equals or notEquals) use { text } + protected val op700: Parser by (equivalent or equals or notEquals or isOp) use { text } protected val term700: Parser by (term500 * optional(op700 * term500)) use { if (t2 == null) t1 else CompoundTerm(Atom(t2!!.t1), listOf(t1, t2!!.t2)) } diff --git a/src/parser/grammars/Tokens.kt b/src/parser/grammars/Tokens.kt index 83e7e33..bffc308 100644 --- a/src/parser/grammars/Tokens.kt +++ b/src/parser/grammars/Tokens.kt @@ -8,28 +8,32 @@ import com.github.h0tk3y.betterParse.lexer.regexToken import com.github.h0tk3y.betterParse.lexer.token abstract class Tokens : Grammar() { - // Prolog tokens - protected val nameToken: Token by regexToken("[a-z][a-zA-Z0-9_]*") - protected val variableToken: Token by regexToken("[A-Z][a-zA-Z0-9_]*") - - // Arithmetic tokens - protected val floatToken: Token by regexToken("-?[1-9][0-9]*\\.[0-9]+") - protected val integerToken: Token by regexToken("-?([1-9][0-9]*|0)") - // Special tokens protected val neck by literalToken(":-") protected val leftParenthesis: Token by literalToken("(") protected val rightParenthesis: Token by literalToken(")") protected val comma: Token by literalToken(",") protected val semicolon: Token by literalToken(";") + protected val equivalent: Token by literalToken("==") protected val equals: Token by literalToken("=") protected val notEquals: Token by literalToken("\\=") protected val plus: Token by literalToken("+") protected val minus: Token by literalToken("-") protected val multiply: Token by literalToken("*") protected val divide: Token by literalToken("/") + protected val exclamation: Token by literalToken("!") + protected val isOp: Token by literalToken("is") protected val dot by literalToken(".") + // Prolog tokens + protected val nameToken: Token by regexToken("[a-z][a-zA-Z0-9_]*") + protected val variableToken: Token by regexToken("[A-Z][a-zA-Z0-9_]*") + protected val anonymousVariableToken: Token by literalToken("_") + + // Arithmetic tokens + protected val floatToken: Token by regexToken("-?[1-9][0-9]*\\.[0-9]+") + protected val integerToken: Token by regexToken("-?([1-9][0-9]*|0)") + // Ignored tokens protected val whitespace: Token by regexToken("\\s+", ignore = true) protected val singleLineComment: Token by regexToken("%[^\\n]*", ignore = true) @@ -41,4 +45,4 @@ abstract class Tokens : Grammar() { // Helper protected val dummy by token { _, _ -> -1 } use { throw IllegalStateException("This parser should not be used") } -} \ No newline at end of file +} diff --git a/src/prolog/ast/terms/AnonymousVariable.kt b/src/prolog/ast/terms/AnonymousVariable.kt new file mode 100644 index 0000000..1bc0633 --- /dev/null +++ b/src/prolog/ast/terms/AnonymousVariable.kt @@ -0,0 +1,17 @@ +package prolog.ast.terms + +import io.Logger + +class AnonymousVariable(id: Int) : Variable("_$id") { + companion object { + private var counter = 0 + fun create(): AnonymousVariable { + val id = counter + counter++ + Logger.debug("Creating anonymous variable: _${id}") + return AnonymousVariable(id) + } + } + + override fun toString(): String = "_" +} \ No newline at end of file diff --git a/src/prolog/ast/terms/Variable.kt b/src/prolog/ast/terms/Variable.kt index f19ea86..2d23170 100644 --- a/src/prolog/ast/terms/Variable.kt +++ b/src/prolog/ast/terms/Variable.kt @@ -6,7 +6,7 @@ import prolog.ast.arithmetic.Expression import prolog.ast.arithmetic.Simplification import prolog.ast.logic.LogicOperand -data class Variable(val name: String) : Term, Body, Expression, LogicOperand() { +open class Variable(val name: String) : Term, Body, Expression, LogicOperand() { 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 @@ -28,5 +28,15 @@ data class Variable(val name: String) : Term, Body, Expression, LogicOperand() { return sequenceOf(Result.failure(IllegalArgumentException("Unbound variable: $this"))) } + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (other == null || other !is Variable) return false + return name == other.name + } + + override fun hashCode(): Int { + return name.hashCode() + } + override fun toString(): String = name } \ No newline at end of file diff --git a/src/prolog/builtins/controlOperators.kt b/src/prolog/builtins/controlOperators.kt index c1ebe63..01cd333 100644 --- a/src/prolog/builtins/controlOperators.kt +++ b/src/prolog/builtins/controlOperators.kt @@ -3,10 +3,10 @@ package prolog.builtins import prolog.Answers import prolog.Substitutions import prolog.ast.logic.LogicOperand +import prolog.ast.logic.LogicOperator import prolog.ast.terms.Atom import prolog.ast.terms.Body import prolog.ast.terms.Goal -import prolog.ast.logic.LogicOperator import prolog.flags.AppliedCut /** diff --git a/src/prolog/builtins/io.kt b/src/prolog/builtins/io.kt index 5806511..3f9aaae 100644 --- a/src/prolog/builtins/io.kt +++ b/src/prolog/builtins/io.kt @@ -18,12 +18,7 @@ import prolog.logic.unifyLazy */ class Write(private val term: Term) : Operator(Atom("write"), null, term), Satisfiable { override fun satisfy(subs: Substitutions): Answers { - var t = term - var temp = applySubstitution(t, subs) - while (t != temp) { - t = temp - temp = applySubstitution(t, subs) - } + val t = applySubstitution(term, subs) Terminal().say(t.toString()) diff --git a/src/prolog/logic/arithmetic.kt b/src/prolog/logic/arithmetic.kt index 0d4d341..36b903c 100644 --- a/src/prolog/logic/arithmetic.kt +++ b/src/prolog/logic/arithmetic.kt @@ -58,7 +58,7 @@ fun succ(term1: Expression, term2: Expression, subs: Substitutions): Answers { it.fold( onSuccess = { result -> val t1 = applySubstitution(term1, result) - if (t1 in result) { + if (t1 in result || t1 in result.values) { val e1 = t1.simplify(result) if (e1.to is Integer && e1.to.value < 0) { return@sequence diff --git a/src/prolog/logic/unification.kt b/src/prolog/logic/unification.kt index 68242b1..0cf1321 100644 --- a/src/prolog/logic/unification.kt +++ b/src/prolog/logic/unification.kt @@ -13,7 +13,15 @@ import prolog.ast.arithmetic.Float // Apply substitutions to a term fun applySubstitution(term: Term, subs: Substitutions): Term = when { - variable(term, emptyMap()) -> subs[(term as Variable)] ?: term + variable(term, emptyMap()) -> { + var result = subs[(term as Variable)] + + while (result != null && result is Variable && result in subs) { + result = subs[result] + } + + result ?: term + } atomic(term, subs) -> term compound(term, subs) -> { val structure = term as Structure @@ -25,7 +33,7 @@ fun applySubstitution(term: Term, subs: Substitutions): Term = when { //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 + variable(expr, emptyMap()) -> applySubstitution(expr as Term, subs) as Expression atomic(expr, subs) -> expr expr is LogicOperator -> { expr.arguments = expr.arguments.map { applySubstitution(it, subs) } diff --git a/tests/e2e/Examples.kt b/tests/e2e/Examples.kt index 9febe53..2b1f3fa 100644 --- a/tests/e2e/Examples.kt +++ b/tests/e2e/Examples.kt @@ -4,43 +4,43 @@ import interpreter.FileLoader import org.junit.jupiter.api.Test import org.junit.jupiter.api.Assertions.assertEquals import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.TestInstance +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.Arguments +import org.junit.jupiter.params.provider.MethodSource +import org.junit.jupiter.params.provider.ValueSource import prolog.Program import java.io.ByteArrayOutputStream import java.io.PrintStream +@TestInstance(TestInstance.Lifecycle.PER_CLASS) class Examples { private val loader = FileLoader() + private lateinit var outStream: ByteArrayOutputStream @BeforeEach fun setup() { Program.reset() - } - @Test - fun fraternity() { - val inputFile = "examples/basics/fraternity.pl" - - loader.load(inputFile) - } - - @Test - fun unification() { - val inputFile = "examples/basics/unification.pl" - - loader.load(inputFile) - } - - @Test - fun write() { - val expected = "gpl zegt: dag(wereld)\n" - - val outStream = ByteArrayOutputStream() + outStream = ByteArrayOutputStream() System.setOut(PrintStream(outStream)) + } - val inputFile = "examples/basics/write.pl" - - // Compare the stdio output with the expected output + @ParameterizedTest + @MethodSource("expectations") + fun test(inputFile: String, expected: String) { loader.load(inputFile) assertEquals(expected, outStream.toString()) } + + fun expectations() = listOf( + Arguments.of("examples/basics/arithmetics.pl", "gimli is a level 4 fighter with 35 hitpoints.\nlegolas is a level 5 ranger with 30 hitpoints.\ngandalf is a level 10 wizard with 25 hitpoints.\nfrodo is a level 2 rogue with 20 hitpoints.\nlegolas threw gimli, and gimli took 5 damage.\ngimli is a level 4 fighter with 30 hitpoints.\ngandalf casts aid.\ngimli is a level 4 fighter with 35 hitpoints.\nlegolas leveled up.\nlegolas is a level 6 ranger with 30 hitpoints"), + Arguments.of("examples/basics/backtracking.pl", "0\ns(0)\ns(s(0))\ns(s(s(0)))\n"), + Arguments.of("examples/basics/cut.pl", "0\n"), + Arguments.of("examples/basics/disjunction.pl", "Alice likes Italian food.\nBob likes Italian food.\n"), + Arguments.of("examples/basics/equality.pl", "X == Y failed\nX = Y succeeded\nX == Y succeeded\nX = Y succeeded\nX == Y succeeded\n"), + Arguments.of("examples/basics/fraternity.pl", "Citizen robespierre is eligible for the event.\nCitizen danton is eligible for the event.\nCitizen camus is eligible for the event.\n"), + Arguments.of("examples/basics/unification.pl", "While alice got an A, carol got an A, but bob did not get an A, dave did not get an A, unfortunately.\n"), + Arguments.of("examples/basics/write.pl", "gpl zegt: dag(wereld)\n"), + ) } \ No newline at end of file diff --git a/tests/interpreter/OpenPreprocessor.kt b/tests/interpreter/OpenPreprocessor.kt new file mode 100644 index 0000000..4e35b2a --- /dev/null +++ b/tests/interpreter/OpenPreprocessor.kt @@ -0,0 +1,9 @@ +package interpreter + +import prolog.ast.terms.Term + +class OpenPreprocessor : Preprocessor() { + public override fun preprocess(term: Term, nested: Boolean): Term { + return super.preprocess(term, nested) + } +} \ No newline at end of file diff --git a/tests/interpreter/ParserPreprocessorIntegrationTests.kt b/tests/interpreter/ParserPreprocessorIntegrationTests.kt new file mode 100644 index 0000000..a572686 --- /dev/null +++ b/tests/interpreter/ParserPreprocessorIntegrationTests.kt @@ -0,0 +1,93 @@ +package interpreter + +import com.github.h0tk3y.betterParse.grammar.parseToEnd +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Nested +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.ValueSource +import parser.grammars.TermsGrammar +import prolog.Program +import prolog.ast.arithmetic.Float +import prolog.ast.arithmetic.Integer +import prolog.ast.terms.Atom +import prolog.ast.terms.Goal +import prolog.ast.terms.Structure +import prolog.ast.terms.Term +import prolog.ast.terms.Variable +import prolog.builtins.Is +import prolog.builtins.Subtract + +class ParserPreprocessorIntegrationTests { + @Nested + class `Arithmetic`() { + val parser = TermsGrammar() + val preprocessor = OpenPreprocessor() + + @ParameterizedTest + @ValueSource(strings = ["-1", "-1.0", "-1.5"]) + fun `can parse negative numbers`(input: String) { + val number = if (input.contains('.')) { + Float(input.substring(1).toFloat()) + } else { + Integer(input.substring(1).toInt()) + } + val negativeNumber = if (input.contains('.')) { + Float(input.toFloat()) + } else { + Integer(input.toInt()) + } + + // Check if parser returns the same result + + val parsed = parser.parseToEnd("X is $input") as Term + + assertEquals( + Structure(Atom("is"), listOf( + Variable("X"), + Structure(Atom("-"), listOf(number)), + )), + parsed + ) + + // Check if preprocessor returns the same result + + val prepped = preprocessor.preprocess(parsed) + + val expected = Is( + Variable("X"), + Subtract(Integer(0), number) + ) + + assertEquals(expected, prepped) + assertEquals(expected.toString(), prepped.toString()) + + // Check if evaluation is correct + + val solutions = (prepped as Is).satisfy(emptyMap()).toList() + + assertEquals(1, solutions.size) + assertEquals(negativeNumber, solutions[0].getOrNull()!![Variable("X")]) + } + + @ParameterizedTest + @ValueSource(strings = ["X is 1 - 2", "X is 1-2"]) + fun `can add negative numbers`(input: String) { + val result = parser.parseToEnd(input) as Term + + assertEquals( + Structure(Atom("is"), listOf(Variable("X"), Structure(Atom("-"), listOf(Integer(1), Integer(2))))), + result + ) + + val prepped = preprocessor.preprocess(result) + + val expected = Is( + Variable("X"), + Subtract(Integer(1), Integer(2)) + ) + + assertEquals(expected, prepped) + assertEquals(expected.toString(), prepped.toString()) + } + } +} \ No newline at end of file diff --git a/tests/interpreter/PreprocessorTests.kt b/tests/interpreter/PreprocessorTests.kt index 3f3ad3f..d7d6c19 100644 --- a/tests/interpreter/PreprocessorTests.kt +++ b/tests/interpreter/PreprocessorTests.kt @@ -1,32 +1,80 @@ package interpreter -import org.junit.jupiter.api.Assertions.assertEquals +import com.github.h0tk3y.betterParse.grammar.parseToEnd +import org.junit.jupiter.api.Assertions.* import org.junit.jupiter.api.Nested import org.junit.jupiter.api.Test +import parser.grammars.TermsGrammar import prolog.ast.arithmetic.Integer -import prolog.ast.terms.Atom -import prolog.ast.terms.CompoundTerm -import prolog.ast.terms.Term -import prolog.ast.terms.Variable +import prolog.ast.terms.* import prolog.builtins.* class PreprocessorTests { - class OpenPreprocessor : Preprocessor() { - public override fun preprocess(term: Term, nested: Boolean): Term { - return super.preprocess(term, nested) - } - } + val preprocessor = OpenPreprocessor() companion object { + val preprocessor = OpenPreprocessor() + fun test(tests: Map) { for ((input, expected) in tests) { - val result = OpenPreprocessor().preprocess(input) + val result = preprocessor.preprocess(input) assertEquals(expected, result, "Expected preprocessed") assertEquals(expected::class, result::class, "Expected same class") } } } + @Test + fun `can preprocess anonymous variable`() { + val input = Variable("_") + + val result = preprocessor.preprocess(input) + + assertInstanceOf(AnonymousVariable::class.java, result, "Expected anonymous variable") + assertTrue((result as Variable).name.matches("_\\d+".toRegex()), "Expected anonymous variable name") + } + + @Test + fun `multiple anonymous variables should be unique`() { + val input = CompoundTerm(Atom("foo"), listOf(Variable("_"), Variable("_"))) + + val result = preprocessor.preprocess(input) + + assertInstanceOf(CompoundTerm::class.java, result, "Expected compound term") + assertEquals(2, (result as CompoundTerm).arguments.size, "Expected two terms") + for (argument in result.arguments) { + assertTrue( + (argument as Variable).name.matches("_\\d+".toRegex()), + "Expected anonymous variable name, but got ${argument.name}" + ) + } + val first = result.arguments[0] as Variable + val second = result.arguments[1] as Variable + assertNotEquals(first.name, second.name, "Expected different anonymous variable names") + } + + @Test + fun `can preprocess nested anonymous variables`() { + val input = TermsGrammar().parseToEnd("name(character(Name, _, _, _))") as Term + + val result = preprocessor.preprocess(input) + + assertInstanceOf(CompoundTerm::class.java, result, "Expected compound term") + assertEquals(1, (result as CompoundTerm).arguments.size, "Expected one term") + assertInstanceOf(CompoundTerm::class.java, result.arguments[0], "Expected compound term") + val inner = result.arguments[0] as CompoundTerm + assertEquals(4, inner.arguments.size, "Expected four terms") + for (argument in inner.arguments) { + if ((argument as Variable).name != "Name") { + assertTrue( + (argument as Variable).name.matches("_\\d+".toRegex()), + "Expected anonymous variable name, but got ${argument.name}" + ) + } + } + + } + @Nested class `Arithmetic operators` { @Test @@ -432,5 +480,22 @@ class PreprocessorTests { ) ) } + + @Test + fun `is`() { + test( + mapOf( + CompoundTerm(Atom("is"), listOf(Variable("T"), Integer(1))) to Is(Variable("T"), Integer(1)), + CompoundTerm(Atom("is"), listOf(Variable("T"), Add(Variable("HP"), Integer(5)))) to Is( + Variable("T"), + Add(Variable("HP"), Integer(5)) + ), + CompoundTerm(Atom("is"), listOf(Variable("T"), Subtract(Variable("HP"), Integer(5)))) to Is( + Variable("T"), + Subtract(Variable("HP"), Integer(5)) + ), + ) + ) + } } } diff --git a/tests/parser/grammars/LogicGrammarTests.kt b/tests/parser/grammars/LogicGrammarTests.kt index ba0143d..57a1f99 100644 --- a/tests/parser/grammars/LogicGrammarTests.kt +++ b/tests/parser/grammars/LogicGrammarTests.kt @@ -133,6 +133,21 @@ class LogicGrammarTests { assertEquals("invited/2", l2.functor, "Expected functor 'invited/2'") } + @Test + fun `parse check_identical(X, Y)`() { + var input = "check_identical(X, Y) :- X == Y." + + assertDoesNotThrow { + val result = parser.parseToEnd(input) + } + + input = "check_identical(X, Y) :- X = Y, !, write('X == Y succeeded'), nl." + + assertDoesNotThrow { + val result = parser.parseToEnd(input) + } + } + @Test fun `parse constraints`() { val input = ":- a." diff --git a/tests/parser/grammars/TermsGrammarTests.kt b/tests/parser/grammars/TermsGrammarTests.kt index 5166856..d3b45e2 100644 --- a/tests/parser/grammars/TermsGrammarTests.kt +++ b/tests/parser/grammars/TermsGrammarTests.kt @@ -17,6 +17,7 @@ import prolog.ast.terms.Atom import prolog.ast.terms.Structure import prolog.ast.terms.Term import prolog.ast.terms.Variable +import prolog.builtins.Is import prolog.logic.equivalent class TermsGrammarTests { @@ -60,7 +61,16 @@ class TermsGrammarTests { fun `parse variable`(name: String) { val result = parser.parseToEnd(name) - assertEquals(Variable(name), result, "Expected atom '$name'") + assertEquals(Variable(name), result) + } + + @Test + fun `parse anonymous variable`() { + val input = "_" + + val result = parser.parseToEnd(input) + + assertEquals(Variable("_"), result, "Expected anonymous variable") } @Test @@ -100,24 +110,33 @@ class TermsGrammarTests { val result = parser.parseToEnd(input) - assertTrue( - equivalent(Structure(Atom("f"), listOf(Atom("a"), Variable("X"))), result, emptyMap()), + assertEquals( + Structure(Atom("f"), listOf(Atom("a"), Variable("X"))), + result, "Expected atom 'f(a, X)'" ) } + @Test + fun `parse compound term with var and int`() { + val input = "check_identical(A, 13)" + val result = parser.parseToEnd(input) + assertEquals( + Structure(Atom("check_identical"), listOf(Variable("A"), Integer(13))), + result, + "Expected atom 'check_identical(A, 13)'" + ) + } + @Test fun `parse nested compound term f(a, g(b))`() { val input = "f(a, g(b))" val result = parser.parseToEnd(input) - Assertions.assertTrue( - equivalent( - Structure(Atom("f"), listOf(Atom("a"), Structure(Atom("g"), listOf(Atom("b"))))), - result, - emptyMap() - ), + assertEquals( + Structure(Atom("f"), listOf(Atom("a"), Structure(Atom("g"), listOf(Atom("b"))))), + result, "Expected atom 'f(a, g(b))'" ) } @@ -128,24 +147,63 @@ class TermsGrammarTests { val result = parser.parseToEnd(input) - Assertions.assertTrue( - equivalent( - Structure(Atom("f"), listOf(Atom("a"), Structure(Atom("g"), listOf(Variable("X"))))), - result, - emptyMap() - ), + assertEquals( + Structure(Atom("f"), listOf(Atom("a"), Structure(Atom("g"), listOf(Variable("X"))))), + result, "Expected atom 'f(a, g(X))'" ) } + @Test + fun `parse nested compound term with variables`() { + val input = "hit(character(Name, Class, Level, HP), character(Name, Class, Level, T))" + + val result = parser.parseToEnd(input) + + assertEquals( + Structure( + Atom("hit"), + listOf( + Structure(Atom("character"), listOf(Variable("Name"), Variable("Class"), Variable("Level"), Variable("HP"))), + Structure(Atom("character"), listOf(Variable("Name"), Variable("Class"), Variable("Level"), Variable("T"))) + ) + ), + result, + "Expected atom 'hit(character(Name, Class, Level, HP), character(Name, Class, Level, T))'" + ) + } + + @Test + fun `parse compound term with anonymous variables`() { + val input = "f(a, _, g(X))" + + val result = parser.parseToEnd(input) + + assertEquals( + Structure(Atom("f"), listOf(Atom("a"), Variable("_"), Structure(Atom("g"), listOf(Variable("X"))))), + result, + "Expected atom 'f(a, _, g(X))'" + ) + } + @ParameterizedTest - @ValueSource(ints = [-987654321, -543, -21, -1, 0, 1, 5, 12, 345, 123456789]) - fun `parse integer`(number: Int) { + @ValueSource(ints = [0, 1, 5, 12, 345, 123456789]) + fun `parse positive integer`(number: Int) { val input = number.toString() val result = parser.parseToEnd(input) - Assertions.assertEquals(Integer(number), result, "Expected integer '$number'") + assertEquals(Integer(number), result, "Expected integer '$number'") + } + + @ParameterizedTest + @ValueSource(ints = [-987654321, -543, -21, -1]) + fun `parse negative integer`(number: Int) { + val input = number.toString() + + val result = parser.parseToEnd(input) + + assertEquals(Structure(Atom("-"), listOf(Integer(0 - number))), result, "Expected integer '$number'") } @Test @@ -154,10 +212,7 @@ class TermsGrammarTests { val result = parser.parseToEnd(input) - Assertions.assertTrue( - equivalent(Float(42.0f), result, emptyMap()), - "Expected float '42.0'" - ) + assertEquals(Float(42.0f), result, "Expected float '42.0'") } @Test @@ -166,7 +221,7 @@ class TermsGrammarTests { val result = parser.parseToEnd(input) - assertEquals(Float(-42.0f), result, "Expected float '-42.0'") + assertEquals(Structure(Atom("-"), listOf(Float(42.0f))), result, "Expected float '-42.0'") } @ParameterizedTest @@ -176,7 +231,7 @@ class TermsGrammarTests { } @Nested - class `Operator precedence` { + class `Operators and precedence` { private lateinit var parser: Grammar @BeforeEach @@ -184,6 +239,74 @@ class TermsGrammarTests { parser = TermsGrammar() as Grammar } + @Test + fun `can parse equivalent`() { + val input = "X == Y" + + val result = parser.parseToEnd(input) + + assertEquals( + Structure(Atom("=="), listOf(Variable("X"), Variable("Y"))), + result, + "Expected equivalent operator" + ) + } + + @Test + fun `can parse cut`() { + val input = "!" + val result = parser.parseToEnd(input) + assertEquals(Atom("!"), result, "Expected cut operator") + } + + @Test + fun `can parse 'is'`() { + val input = "T is 1" + val result = parser.parseToEnd(input) + assertEquals( + Structure(Atom("is"), listOf(Variable("T"), Integer(1))), + result + ) + } + + @Test + fun `can parse 'is' with addition`() { + val input = "T is 1 + 2" + val result = parser.parseToEnd(input) + assertEquals( + Structure(Atom("is"), listOf(Variable("T"), Structure(Atom("+"), listOf(Integer(1), Integer(2))))), + result + ) + } + + @ParameterizedTest + @ValueSource(strings = ["+", "-", "*", "/"]) + fun `can parse with spaces`(operator: String) { + val input = "1 $operator 2" + + val result = parser.parseToEnd(input) + + assertEquals( + Structure(Atom(operator), listOf(Integer(1), Integer(2))), + result, + "Expected operator '$operator'" + ) + } + + @ParameterizedTest + @ValueSource(strings = ["+", "-", "*", "/"]) + fun `can parse without spaces`(operator: String) { + val input = "1${operator}2" + + val result = parser.parseToEnd(input) + + assertEquals( + Structure(Atom(operator), listOf(Integer(1), Integer(2))), + result, + "Expected operator '$operator' without spaces" + ) + } + @Test fun `parse addition and multiplication`() { val input = "1 + 2 * 3" diff --git a/tests/prolog/logic/ArithmeticTests.kt b/tests/prolog/logic/ArithmeticTests.kt index 83fa8c7..ac532f3 100644 --- a/tests/prolog/logic/ArithmeticTests.kt +++ b/tests/prolog/logic/ArithmeticTests.kt @@ -583,10 +583,23 @@ class ArithmeticTests { assertTrue(equivalent(result[0].getOrThrow()[t3]!!, Float(6.0f), result[0].getOrNull()!!), "X should be equal to 6.0") } + @Test + fun `addition with negative`() { + val t1 = Integer(1) + val t2 = Integer(-1) + val t3 = Integer(0) + + val result = plus(t1, t2, t3, emptyMap()).toList() + + assertEquals(1, result.size, "There should be one solution") + assertTrue(result[0].isSuccess, "Expected success") + assertTrue(result[0].getOrNull()!!.isEmpty(), "1 + -1 should already be equal to 0") + } + @RepeatedTest(100) fun `random test for mul`() { - val t1 = Integer((0..1000).random()) - val t2 = Integer((0..1000).random()) + val t1 = Integer((-1000..1000).random()) + val t2 = Integer((-1000..1000).random()) val t3 = Variable("X") val result = mul(t1, t2, t3, emptyMap()).toList() diff --git a/tests/prolog/logic/UnificationTests.kt b/tests/prolog/logic/UnificationTests.kt new file mode 100644 index 0000000..10a37e7 --- /dev/null +++ b/tests/prolog/logic/UnificationTests.kt @@ -0,0 +1,370 @@ +package prolog.logic + +import org.junit.jupiter.api.Assertions.* +import org.junit.jupiter.api.Test +import prolog.Substitutions +import prolog.ast.arithmetic.Integer +import prolog.ast.terms.Atom +import prolog.ast.terms.Structure +import prolog.ast.terms.Variable +import prolog.builtins.Add +import org.junit.jupiter.api.Disabled +import org.junit.jupiter.api.Nested + +/* + * Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms + */ +class UnificationTests { + @Nested + class `unify` { + @Test + fun identical_atoms_unify() { + val atom1 = Atom("a") + val atom2 = Atom("a") + + val result = unify(atom1, atom2) + + assertTrue(result.isSuccess, "Identical atoms should unify") + assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made") + } + + @Test + fun different_atoms_do_not_unify() { + val atom1 = Atom("a") + val atom2 = Atom("b") + + val result = unify(atom1, atom2) + + assertFalse(result.isSuccess, "Different atoms should not unify") + } + + /** + * ?- X = X. + * true. + */ + @Test + fun identical_variables_unify() { + val variable1 = Variable("X") + val variable2 = Variable("X") + + val result = unify(variable1, variable2) + + assertTrue(result.isSuccess, "Identical variables should unify") + assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made") + } + + @Test + fun variable_unifies_with_atom() { + val variable = Variable("X") + val atom = Atom("a") + + val result = unify(atom, variable) + + 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 + fun variables_alias_when_unified() { + val variable1 = Variable("X") + val variable2 = Variable("Y") + + val result = unify(variable1, variable2) + + assertTrue(result.isSuccess) + assertEquals(1, result.getOrNull()!!.size) + assertEquals(variable2, result.getOrNull()!![variable1], "Variable 1 should alias to variable 2") + } + + @Test + fun identical_compound_terms_unify() { + val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) + val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) + + val result = unify(structure1, structure2) + + assertTrue(result.isSuccess, "Identical compound terms should unify") + assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made") + } + + @Test + fun compound_terms_with_different_arguments_do_not_unify() { + val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) + val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("c"))) + + val result = unify(structure1, structure2) + + assertFalse(result.isSuccess, "Different compound terms should not unify") + } + + @Test + fun compound_terms_with_different_functors_do_not_unify() { + val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) + val structure2 = Structure(Atom("g"), listOf(Atom("a"), Atom("b"))) + + val result = unify(structure1, structure2) + + assertFalse(result.isSuccess, "Compound terms with different functors should not unify") + } + + /** + * ?- X = f(a, b). + * X = f(a, b). + */ + @Test + fun variable_unifies_with_compound_term() { + val variable = Variable("X") + val structure = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) + + val result = unify(variable, structure) + + 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"))), subs[variable]!!, subs), + "Variable should be substituted with compound term" + ) + } + + @Test + fun compound_term_with_variable_unifies_with_part() { + val variable = Variable("X") + val structure1 = Structure(Atom("f"), listOf(Atom("a"), variable)) + val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) + + val result = unify(structure1, structure2) + + 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") + } + + @Test + fun compound_terms_with_variable_arguments_lists_alias_variables() { + val variable1 = Variable("X") + val variable2 = Variable("Y") + + val structure1 = Structure(Atom("f"), listOf(variable1)) + val structure2 = Structure(Atom("f"), listOf(variable2)) + + val result = unify(structure1, structure2) + + 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") + } + + /** + * f(X) = f(Y, Z) + */ + @Test + fun compound_terms_with_different_arity_do_not_unify() { + val structure1 = Structure(Atom("f"), listOf(Variable("X"))) + val structure2 = Structure(Atom("f"), listOf(Variable("Y"), Variable("Z"))) + + val result = unify(structure1, structure2) + + assertFalse(result.isSuccess, "Compound terms with different arity should not unify") + } + + /** + * ?- f(g(X)) = f(Y). + * Y = g(X). + */ + @Test + fun nested_compound_terms_with_variables_unify() { + val variable2 = Variable("Y") + + val structure1 = Structure(Atom("f"), listOf(Structure(Atom("g"), listOf(Variable("X"))))) + val structure2 = Structure(Atom("f"), listOf(variable2)) + + val result = unify(structure1, structure2) + + 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"))), subs[variable2]!!, subs), + "Variable should be substituted with compound term" + ) + } + + /** + * ?- f(g(X), X) = f(Y, a). + * X = a, + * Y = g(a). + */ + @Test + fun compound_terms_with_more_variables() { + val variable1 = Variable("X") + val variable2 = Variable("Y") + + val structure1 = Structure(Atom("f"), listOf(Structure(Atom("g"), listOf(variable1)), variable1)) + val structure2 = Structure(Atom("f"), listOf(variable2, Atom("a"))) + + val result = unify(structure1, structure2) + + 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"), subs[variable1]!!, subs), + "Variable 1 should be substituted with atom" + ) + 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" + + ) + } + + /** + * ?- X = f(X). + * X = f(f(X)). + */ + @Test + @Disabled("If the occurs check is applied, this should fail") + fun recursive_unification() { + val variable1 = Variable("X") + val structure2 = Structure(Atom("f"), listOf(Variable("X"))) + + val result = unifyLazy(variable1, structure2, emptyMap()).toList() + + 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") + } + + /** + * ?- X = bar, Y = bar, X = Y. + * X = Y, Y = bar. + */ + @Test + fun multiple_unification() { + val variable1 = Variable("X") + val variable2 = Variable("Y") + val atom = Atom("bar") + + val map: Substitutions = mapOf( + variable1 to atom, + variable2 to atom + ) + val result = unifyLazy(variable1, variable2, map).toList() + + 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") + } + + /** + * ?- a = a(). + * false. + */ + @Test + fun atom_with_different_arity() { + val atom1 = Atom("a") + val structure2 = Structure(Atom("a"), emptyList()) + + val result = unify(atom1, structure2) + + assertFalse(result.isSuccess, "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.isSuccess, "Identical integers should unify") + assertEquals(0, result.getOrNull()!!.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.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") + } + } + + @Nested + class `applySubstitution` { + @Test + fun `apply substitution without sub`() { + val term = Variable("X") + val subs: Substitutions = emptyMap() + + val result = applySubstitution(term, subs) + + assertEquals(term, result) + } + + @Test + fun `apply single substitution`() { + val sub = Variable("X") to Integer(5) + val subs: Substitutions = mapOf(sub) + + val term = Variable("X") + + val result = applySubstitution(term, subs) + + assertEquals(Integer(5), result) + } + + @Test + fun `apply chained substitution`() { + val sub1 = Variable("HP") to Variable("HP(19)") + val sub2 = Variable("HP(19)") to Integer(35) + + val subs: Substitutions = mapOf(sub1, sub2) + + val term = Variable("HP") + + val result = applySubstitution(term, subs) + + assertEquals(Integer(35), result) + } + } +} \ No newline at end of file diff --git a/tests/prolog/logic/UnifyTests.kt b/tests/prolog/logic/UnifyTests.kt deleted file mode 100644 index 0f0199f..0000000 --- a/tests/prolog/logic/UnifyTests.kt +++ /dev/null @@ -1,328 +0,0 @@ -package prolog.logic - -import org.junit.jupiter.api.Assertions.* -import org.junit.jupiter.api.Test -import prolog.Substitutions -import prolog.ast.arithmetic.Integer -import prolog.ast.terms.Atom -import prolog.ast.terms.Structure -import prolog.ast.terms.Variable -import prolog.builtins.Add -import org.junit.jupiter.api.Disabled -import org.junit.jupiter.api.fail - -/* - * Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms - */ -class UnifyTests { - @Test - fun identical_atoms_unify() { - val atom1 = Atom("a") - val atom2 = Atom("a") - - val result = unify(atom1, atom2) - - assertTrue(result.isSuccess, "Identical atoms should unify") - assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made") - } - - @Test - fun different_atoms_do_not_unify() { - val atom1 = Atom("a") - val atom2 = Atom("b") - - val result = unify(atom1, atom2) - - assertFalse(result.isSuccess, "Different atoms should not unify") - } - - /** - * ?- X = X. - * true. - */ - @Test - fun identical_variables_unify() { - val variable1 = Variable("X") - val variable2 = Variable("X") - - val result = unify(variable1, variable2) - - assertTrue(result.isSuccess, "Identical variables should unify") - assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made") - } - - @Test - fun variable_unifies_with_atom() { - val variable = Variable("X") - val atom = Atom("a") - - val result = unify(atom, variable) - - 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 - fun variables_alias_when_unified() { - val variable1 = Variable("X") - val variable2 = Variable("Y") - - val result = unify(variable1, variable2) - - assertTrue(result.isSuccess) - assertEquals(1, result.getOrNull()!!.size) - assertEquals(variable2, result.getOrNull()!![variable1], "Variable 1 should alias to variable 2") - } - - @Test - fun identical_compound_terms_unify() { - val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) - val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) - - val result = unify(structure1, structure2) - - assertTrue(result.isSuccess, "Identical compound terms should unify") - assertEquals(0, result.getOrNull()!!.size, "No substitutions should be made") - } - - @Test - fun compound_terms_with_different_arguments_do_not_unify() { - val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) - val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("c"))) - - val result = unify(structure1, structure2) - - assertFalse(result.isSuccess, "Different compound terms should not unify") - } - - @Test - fun compound_terms_with_different_functors_do_not_unify() { - val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) - val structure2 = Structure(Atom("g"), listOf(Atom("a"), Atom("b"))) - - val result = unify(structure1, structure2) - - assertFalse(result.isSuccess, "Compound terms with different functors should not unify") - } - - /** - * ?- X = f(a, b). - * X = f(a, b). - */ - @Test - fun variable_unifies_with_compound_term() { - val variable = Variable("X") - val structure = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) - - val result = unify(variable, structure) - - 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"))), subs[variable]!!, subs), - "Variable should be substituted with compound term" - ) - } - - @Test - fun compound_term_with_variable_unifies_with_part() { - val variable = Variable("X") - val structure1 = Structure(Atom("f"), listOf(Atom("a"), variable)) - val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("b"))) - - val result = unify(structure1, structure2) - - 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") - } - - @Test - fun compound_terms_with_variable_arguments_lists_alias_variables() { - val variable1 = Variable("X") - val variable2 = Variable("Y") - - val structure1 = Structure(Atom("f"), listOf(variable1)) - val structure2 = Structure(Atom("f"), listOf(variable2)) - - val result = unify(structure1, structure2) - - 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") - } - - /** - * f(X) = f(Y, Z) - */ - @Test - fun compound_terms_with_different_arity_do_not_unify() { - val structure1 = Structure(Atom("f"), listOf(Variable("X"))) - val structure2 = Structure(Atom("f"), listOf(Variable("Y"), Variable("Z"))) - - val result = unify(structure1, structure2) - - assertFalse(result.isSuccess, "Compound terms with different arity should not unify") - } - - /** - * ?- f(g(X)) = f(Y). - * Y = g(X). - */ - @Test - fun nested_compound_terms_with_variables_unify() { - val variable2 = Variable("Y") - - val structure1 = Structure(Atom("f"), listOf(Structure(Atom("g"), listOf(Variable("X"))))) - val structure2 = Structure(Atom("f"), listOf(variable2)) - - val result = unify(structure1, structure2) - - 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"))), subs[variable2]!!, subs), - "Variable should be substituted with compound term" - ) - } - - /** - * ?- f(g(X), X) = f(Y, a). - * X = a, - * Y = g(a). - */ - @Test - fun compound_terms_with_more_variables() { - val variable1 = Variable("X") - val variable2 = Variable("Y") - - val structure1 = Structure(Atom("f"), listOf(Structure(Atom("g"), listOf(variable1)), variable1)) - val structure2 = Structure(Atom("f"), listOf(variable2, Atom("a"))) - - val result = unify(structure1, structure2) - - 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"), subs[variable1]!!, subs), - "Variable 1 should be substituted with atom" - ) - 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" - - ) - } - - /** - * ?- X = f(X). - * X = f(f(X)). - */ - @Test - @Disabled("If the occurs check is applied, this should fail") - fun recursive_unification() { - val variable1 = Variable("X") - val structure2 = Structure(Atom("f"), listOf(Variable("X"))) - - val result = unifyLazy(variable1, structure2, emptyMap()).toList() - - 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") - } - - /** - * ?- X = bar, Y = bar, X = Y. - * X = Y, Y = bar. - */ - @Test - fun multiple_unification() { - val variable1 = Variable("X") - val variable2 = Variable("Y") - val atom = Atom("bar") - - val map: Substitutions = mapOf( - variable1 to atom, - variable2 to atom - ) - val result = unifyLazy(variable1, variable2, map).toList() - - 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") - } - - /** - * ?- a = a(). - * false. - */ - @Test - fun atom_with_different_arity() { - val atom1 = Atom("a") - val structure2 = Structure(Atom("a"), emptyList()) - - val result = unify(atom1, structure2) - - assertFalse(result.isSuccess, "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.isSuccess, "Identical integers should unify") - assertEquals(0, result.getOrNull()!!.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.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