From 7daae860fcfe5d5e9ca9fb477c4a0af7b578cfa0 Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Thu, 8 May 2025 17:47:13 +0200 Subject: [PATCH] Checkpoint --- src/interpreter/Preprocessor.kt | 2 +- src/parser/grammars/TermsGrammar.kt | 18 +++++++ src/parser/grammars/Tokens.kt | 2 + src/prolog/builtins/unificationOperators.kt | 4 +- src/prolog/logic/unification.kt | 7 ++- tests/prolog/EvaluationTests.kt | 19 +++++++ tests/prolog/builtins/ListOperatorsTests.kt | 17 +++++- tests/prolog/logic/UnificationTests.kt | 59 +++++++++++++++++++-- 8 files changed, 119 insertions(+), 9 deletions(-) diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt index 5049fe3..226af60 100644 --- a/src/interpreter/Preprocessor.kt +++ b/src/interpreter/Preprocessor.kt @@ -65,7 +65,7 @@ open class Preprocessor { Functor.of("clause/2") -> ClauseOp(args[0] as Head, args[1] as Body) Functor.of("atomic/1") -> AtomicOp(args[0]) Functor.of("compound/1") -> CompoundOp(args[0]) - Functor.of("univ/2") -> Univ(args[0], args[1]) + Functor.of("=../2") -> Univ(args[0], args[1]) // Arithmetic Functor.of("inf/0") -> Integer(Int.MAX_VALUE) diff --git a/src/parser/grammars/TermsGrammar.kt b/src/parser/grammars/TermsGrammar.kt index 98a7147..8db42e9 100644 --- a/src/parser/grammars/TermsGrammar.kt +++ b/src/parser/grammars/TermsGrammar.kt @@ -5,8 +5,11 @@ import com.github.h0tk3y.betterParse.grammar.parser import com.github.h0tk3y.betterParse.parser.Parser import prolog.ast.arithmetic.Float import prolog.ast.arithmetic.Integer +import prolog.ast.lists.List import prolog.ast.terms.* import prolog.builtins.Dynamic +import prolog.ast.lists.List.Empty +import prolog.ast.lists.List.Cons /** * Precedence is based on the following table: @@ -65,6 +68,7 @@ open class TermsGrammar : Tokens() { // Base terms (atoms, compounds, variables, numbers) protected val baseTerm: Parser by (dummy or (-leftParenthesis * parser(::term) * -rightParenthesis) + or parser(::list) or compound or atom or variable @@ -112,6 +116,20 @@ open class TermsGrammar : Tokens() { t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) } } + // Lists + protected val list: Parser by (-leftBracket * separated( + parser(::termNoConjunction), + comma, + acceptZero = true + ) * -rightBracket) use { + var list: List = Empty + // Construct the list in reverse order + for (term in this.terms.reversed()) { + list = Cons(term, list) + } + list + } + // Term - highest level expression protected val term: Parser by term1200 protected val termNoConjunction: Parser by term700 diff --git a/src/parser/grammars/Tokens.kt b/src/parser/grammars/Tokens.kt index 3f54cba..b998fee 100644 --- a/src/parser/grammars/Tokens.kt +++ b/src/parser/grammars/Tokens.kt @@ -10,6 +10,8 @@ import com.github.h0tk3y.betterParse.lexer.token abstract class Tokens : Grammar() { protected val leftParenthesis: Token by literalToken("(") protected val rightParenthesis: Token by literalToken(")") + protected val leftBracket: Token by literalToken("[") + protected val rightBracket: Token by literalToken("]") protected val exclamation: Token by literalToken("!") // 1200 protected val neck by literalToken(":-") diff --git a/src/prolog/builtins/unificationOperators.kt b/src/prolog/builtins/unificationOperators.kt index ad55acf..5ebeed3 100644 --- a/src/prolog/builtins/unificationOperators.kt +++ b/src/prolog/builtins/unificationOperators.kt @@ -22,7 +22,7 @@ class Unify(private val term1: Term, private val term2: Term): Operator(Atom("=" val t1 = applySubstitution(term1, subs) val t2 = applySubstitution(term2, subs) - yieldAll(unifyLazy(t1, t2, subs)) + yieldAll(unifyLazy(t1, t2, emptyMap())) } override fun applySubstitution(subs: Substitutions): Unify = Unify( @@ -45,7 +45,7 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator(At val t1 = applySubstitution(term1, subs) val t2 = applySubstitution(term2, subs) - if (equivalent(t1, t2, subs)) { + if (equivalent(t1, t2, emptyMap())) { yield(Result.success(emptyMap())) } } diff --git a/src/prolog/logic/unification.kt b/src/prolog/logic/unification.kt index 23467c4..2fa6e23 100644 --- a/src/prolog/logic/unification.kt +++ b/src/prolog/logic/unification.kt @@ -85,6 +85,7 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence val args1 = structure1.arguments val args2 = structure2.arguments if (args1.size == args2.size) { + // Keep track of the substitutions so far val results = args1.zip(args2).map { (arg1, arg2) -> unifyLazy(arg1, arg2, subs) } @@ -145,7 +146,11 @@ fun unify(term1: Term, term2: Term): Answer { fun equivalent(term1: Term, term2: Term, subs: Substitutions): Boolean { return when { term1 is Atom && term2 is Atom -> compare(term1, term2, subs) == 0 - term1 is Structure && term2 is Structure -> compare(term1, term2, subs) == 0 + term1 is Structure && term2 is Structure -> { + term1.functor == term2.functor && term1.arguments.zip(term2.arguments).all { (arg1, arg2) -> + equivalent(arg1, arg2, subs) + } + } term1 is Integer && term2 is Integer -> compare(term1, term2, subs) == 0 term1 is Number && term2 is Number -> compare(term1, term2, subs) == 0 term1 is Variable && term2 is Variable -> term1 == term2 diff --git a/tests/prolog/EvaluationTests.kt b/tests/prolog/EvaluationTests.kt index 1a62390..8392eae 100644 --- a/tests/prolog/EvaluationTests.kt +++ b/tests/prolog/EvaluationTests.kt @@ -15,7 +15,10 @@ import prolog.ast.terms.Structure import prolog.ast.terms.Variable import prolog.ast.Database.Program import prolog.ast.arithmetic.Integer +import prolog.ast.lists.List.Empty +import prolog.ast.lists.List.Cons import prolog.ast.terms.AnonymousVariable +import prolog.builtins.Unify class EvaluationTests { @BeforeEach @@ -479,4 +482,20 @@ class EvaluationTests { assertEquals(1, subs3c.size, "Expected 1 substitution") assertEquals(Structure(Atom("s"), listOf(Structure(Atom("s"), listOf(Integer(0))))), subs3c[Variable("X")], "Expected X to be s(s(0))") } + + @Test + fun `foo(emptyList) = foo(X)`() { + val list = Empty + val left = Structure(Atom("foo"), listOf(list)) + val right = Structure(Atom("foo"), listOf(Variable("X"))) + + val unific = Unify(left, right) + val result = unific.satisfy(emptyMap()).toList() + + assertEquals(1, result.size, "Expected 1 result") + assertTrue(result[0].isSuccess, "Expected success") + val subs = result[0].getOrNull()!! + assertEquals(1, subs.size, "Expected 1 substitution") + assertEquals(list, subs[Variable("X")], "Expected X to be list(1, 2)") + } } diff --git a/tests/prolog/builtins/ListOperatorsTests.kt b/tests/prolog/builtins/ListOperatorsTests.kt index be1e521..d0c44c2 100644 --- a/tests/prolog/builtins/ListOperatorsTests.kt +++ b/tests/prolog/builtins/ListOperatorsTests.kt @@ -7,6 +7,7 @@ import org.junit.jupiter.api.Test import prolog.ast.lists.List.Cons import prolog.ast.lists.List.Empty import prolog.ast.terms.Atom +import prolog.ast.terms.Variable class ListOperatorsTests { @Test @@ -42,11 +43,23 @@ class ListOperatorsTests { assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map") } - @Disabled("Not required functionality") + @Test + fun `member should only check shallow`() { + val list = Cons(Atom("a"), Cons(Cons(Atom("b"), Empty), Empty)) + + var result = Member(Atom("a"), list).satisfy(emptyMap()).toList() + assertEquals(1, result.size, "Expected one solution") + assertTrue(result[0].isSuccess, "Expected success") + assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map") + + result = Member(Atom("b"), list).satisfy(emptyMap()).toList() + assertEquals(0, result.size, "Expected no solution") + } + @Test fun `member with variable in list`() { val atom = Atom("a") - val variable = Atom("X") + val variable = Variable("X") val list = Cons(variable, Empty) val member = Member(atom, list) diff --git a/tests/prolog/logic/UnificationTests.kt b/tests/prolog/logic/UnificationTests.kt index 242ab85..1324a12 100644 --- a/tests/prolog/logic/UnificationTests.kt +++ b/tests/prolog/logic/UnificationTests.kt @@ -375,8 +375,16 @@ class UnificationTests { class `equivalent logic` { @Test fun `empty lists are equivalent`() { - val eq = equivalent(Empty, Empty, emptyMap()) + var eq = equivalent(Empty, Empty, emptyMap()) assertTrue(eq, "Empty lists should be equivalent") + + val variable = Variable("X") + + eq = equivalent(Empty, variable, mapOf(variable to Empty)) + assertTrue(eq, "Empty list and variable should be equivalent") + + eq = equivalent(variable, Empty, mapOf(variable to Empty)) + assertTrue(eq, "Variable and empty list should be equivalent") } @Test @@ -385,9 +393,16 @@ class UnificationTests { val list1 = Cons(atom, Empty) val list2 = Cons(atom, Empty) - val eq = equivalent(list1, list2, emptyMap()) - + var eq = equivalent(list1, list2, emptyMap()) assertTrue(eq, "Singleton lists should be equivalent") + + val variable = Variable("X") + + eq = equivalent(list1, variable, mapOf(variable to list2)) + assertTrue(eq, "Singleton list and variable should be equivalent") + + eq = equivalent(variable, list1, mapOf(variable to list2)) + assertTrue(eq, "Variable and singleton list should be equivalent") } @Test @@ -401,6 +416,14 @@ class UnificationTests { eq = equivalent(list2, list1, emptyMap()) assertFalse(eq, "Empty and singleton lists should not be equivalent") + + val variable = Variable("X") + + eq = equivalent(list1, variable, mapOf(variable to list2)) + assertFalse(eq, "Singleton list and variable should not be equivalent") + + eq = equivalent(variable, list1, mapOf(variable to list2)) + assertFalse(eq, "Variable and singleton list should not be equivalent") } @Test @@ -413,6 +436,14 @@ class UnificationTests { eq = equivalent(list2, list1, emptyMap()) assertTrue(eq, "Identical lists should be equivalent") + + val variable = Variable("X") + + eq = equivalent(list1, variable, mapOf(variable to list2)) + assertTrue(eq, "Identical lists should be equivalent") + + eq = equivalent(variable, list2, mapOf(variable to list1)) + assertTrue(eq, "Identical lists should be equivalent") } @Test @@ -422,6 +453,17 @@ class UnificationTests { var eq = equivalent(list1, list2, emptyMap()) assertTrue(eq, "Identical nested lists should be equivalent") + + eq = equivalent(list2, list1, emptyMap()) + assertTrue(eq, "Identical nested lists should be equivalent") + + val variable = Variable("X") + + eq = equivalent(list1, variable, mapOf(variable to list2)) + assertTrue(eq, "Identical nested lists should be equivalent") + + eq = equivalent(variable, list2, mapOf(variable to list1)) + assertTrue(eq, "Identical nested lists should be equivalent") } @Test @@ -431,6 +473,17 @@ class UnificationTests { var eq = equivalent(list1, list2, emptyMap()) assertFalse(eq, "Lists with different nests should not be equivalent") + + eq = equivalent(list2, list1, emptyMap()) + assertFalse(eq, "Lists with different nests should not be equivalent") + + val variable = Variable("X") + + eq = equivalent(list1, variable, mapOf(variable to list2)) + assertFalse(eq, "Lists with different nests should not be equivalent") + + eq = equivalent(variable, list2, mapOf(variable to list1)) + assertFalse(eq, "Lists with different nests should not be equivalent") } } } \ No newline at end of file