Fix a bug in new matching algorithm that prevented correct matching of ref-ed metalogicals with terms.

This commit is contained in:
Fedor Isakov 2018-08-17 23:12:52 +02:00
parent ec38be682e
commit d26b7197fd
2 changed files with 36 additions and 6 deletions

View File

@ -184,13 +184,16 @@ class RuleMatcher(val rule: Rule) {
private fun matchLogical(ptn: Logical<*>,
trg: Any?,
subst: Subst): Subst? =
if (ptn.isBound) {
if (trg is Logical<*>) matchAny(ptn.value(), trg.findRoot().value(), subst) else null
} else {
if (trg is Logical<*> && ptn === trg.findRoot()) subst else null // reference equality!
when {
trg is Logical<*> -> when {
ptn.isBound -> matchAny(ptn.findRoot().value(), trg.findRoot().value(), subst)
ptn.findRoot() === trg.findRoot() -> subst // reference equality
else -> null
}
ptn.isBound -> matchAny(ptn.findRoot().value(), trg, subst)
else -> null
}
private fun resolve(obj: Any?): Any? =
when (obj) {
is LogicalOwner -> if (obj.logical().isBound) resolve(obj.logical()) else obj

View File

@ -330,6 +330,33 @@ class TestRuleMatcher {
}
}
@Test
fun testTermRefLogicalMetaLogical3() {
val (X, Y) = metaLogical<Term>("X", "Y")
val yLogical = Y.logical()
with(programWithRules(
rule("rule1",
headReplaced(
constraint("foo", term("f", ref(metaVar(X)), term("g"))),
constraint("bar", term("h", term("k"), metaVar(X)))
),
body(
constraint("qux")
))))
{
with(RuleMatcher(rules.first()).fringe()) {
expand(occurrence("foo", term("f", logicalVar(yLogical), term("g")))) }.apply {
matches().size shouldBe 0 }.run {
yLogical.set(parseTerm("p{q r}"))
val termh = logicalVar(yLogical)
expand(occurrence("bar", parseTerm("h{k p{q r}}"))) }.apply {
matches().size shouldBe 1
}
}
}
@Test
fun testTermLogical() {