diff --git a/src/prolog/builtins/analysisOperators.kt b/src/prolog/builtins/analysisOperators.kt index 7f83ab0..75b7711 100644 --- a/src/prolog/builtins/analysisOperators.kt +++ b/src/prolog/builtins/analysisOperators.kt @@ -159,27 +159,31 @@ class ClauseOp(private val head: Head, private val body: Body) : open class Univ(private val term: Term, private val list: Term) : Operator("=..", term, list) { override fun satisfy(subs: Substitutions): Answers { - return when { - nonvariable(term, subs) && nonvariable(list, subs) -> { - val t = applySubstitution(term, subs) - val l = applySubstitution(list, subs) as List - unifyLazy(t, listToTerm(l), subs) - } + if (variable(term, subs)) { + require(nonvariable(list, subs)) { "Arguments are not sufficiently instantiated" } + val l = applySubstitution(list, subs) as List + require(nonvariable(l.head, subs)) { "Arguments are not sufficiently instantiated" } - variable(term, subs) && nonvariable(list, subs) -> { - val l = applySubstitution(list, subs) as List - val t = listToTerm(l) - unifyLazy(term, t, subs) - } - - nonvariable(term, subs) && variable(list, subs) -> { - val t = applySubstitution(term, subs) - val l = termToList(t) - unifyLazy(l, list, subs) - } - - else -> throw Exception("Arguments are not sufficiently instantiated") + val t = listToTerm(l) + return unifyLazy(term, t, subs) } + + if (nonvariable(list, subs)) { + val l = applySubstitution(list, subs) as List + + if (nonvariable(l.head, subs)) { + val t = applySubstitution(term, subs) + return unifyLazy(t, listToTerm(l), subs) + } + + val t = applySubstitution(term, subs) + val expectedL = termToList(t) + return unifyLazy(expectedL, l, subs) + } + + val t = applySubstitution(term, subs) + val l = termToList(t) + return unifyLazy(l, list, subs) } protected open fun listToTerm(list: List): Term { diff --git a/tests/prolog/builtins/AnalysisOperatorsTests.kt b/tests/prolog/builtins/AnalysisOperatorsTests.kt index a6866c3..1f4981a 100644 --- a/tests/prolog/builtins/AnalysisOperatorsTests.kt +++ b/tests/prolog/builtins/AnalysisOperatorsTests.kt @@ -568,6 +568,23 @@ class AnalysisOperatorsTests { assertEquals(0, result.size, "Expected 0 results") } + @Test + fun `univ extra debugging`() { + val univ = Univ( + Structure("baz", Variable("Foo")), + Cons(Variable("Baz"), Cons(Structure("foo", Integer(1)), Empty)) + ) + + val result = univ.satisfy(emptyMap()).toList() + + assertEquals(1, result.size, "Expected 1 result") + assertTrue(result[0].isSuccess, "Expected success") + val subs = result[0].getOrNull()!! + assertEquals(2, subs.size, "Expected 2 substitutions") + assertEquals(Atom("baz"), subs[Variable("Baz")], "Expected Baz to be baz") + assertEquals(Structure("foo", Integer(1)), subs[Variable("Foo")], "Expected Foo to be foo(1)") + } + @Test fun `univ with two vars should throw`() { val univ = Univ(Variable("X"), Variable("Y"))