fix: Univ

This commit is contained in:
Tibo De Peuter 2025-05-18 20:28:58 +02:00
parent d50ec0f715
commit 61178cbeac
Signed by: tdpeuter
GPG key ID: 38297DE43F75FFE2
2 changed files with 40 additions and 19 deletions

View file

@ -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 {