From d26b7197fdf301a365f804e5dc5d8a7b71f4ed52 Mon Sep 17 00:00:00 2001
From: Fedor Isakov <fisakov@gmail.com>
Date: Fri, 17 Aug 2018 23:12:52 +0200
Subject: [PATCH] Fix a bug in new matching algorithm that prevented correct
 matching of ref-ed metalogicals with terms.

---
 .../mps/logic/reactor/core/RuleMatcher.kt     | 15 ++++++-----
 reactor/Test/test/TestRuleMatcher.kt          | 27 +++++++++++++++++++
 2 files changed, 36 insertions(+), 6 deletions(-)

diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleMatcher.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleMatcher.kt
index 21816b52..6c2e7f0d 100644
--- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleMatcher.kt
+++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/RuleMatcher.kt
@@ -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
diff --git a/reactor/Test/test/TestRuleMatcher.kt b/reactor/Test/test/TestRuleMatcher.kt
index bb78cf58..9bbbf9c5 100644
--- a/reactor/Test/test/TestRuleMatcher.kt
+++ b/reactor/Test/test/TestRuleMatcher.kt
@@ -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() {