Dereference all refs within term on unification.

Method findSolution now walks all refs inside a term.
This guarantees no "hidden" cycles, but also breaks the
"cyclic term" feature.

reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt

@@ -58,7 +58,7 @@ typealias IntAnyHashMap<V> = TIntObjectHashMap<V>
 class TermGraphUnifier {
 
     companion object {
-        val EMPTY =TIntArrayList.wrap(kotlin.IntArray(0))
+        val EMPTY_LIST = TIntArrayList.wrap(kotlin.IntArray(0))
     }
 
     private var wrapper: TermWrapper
@@ -97,7 +97,8 @@ class TermGraphUnifier {
     }
 
     private fun findSolution(s: Int, defSubs: Substitution) : Substitution {
-        val z = innerSchema[find(s)]
+        val (_, z) = findSchema(s)
+        val vars = innerVars[find(z)]
 
         if (innerAcyclic[z]) { return defSubs } // not part of a cycle
         if (innerVisited[z]) { return failedSubstitution(CYCLE_DETECTED) } // there exists a cycle
@@ -105,22 +106,21 @@ class TermGraphUnifier {
         var subs = defSubs
         if (origin[z].`is`(FUN)) {
             innerVisited.set(z)
-
             for (c in origin[z].arguments()) {
-                subs = findSolution(toInner(c), subs)
+                val (_, zc) = findSchema(toInner(c))
+                subs = findSolution(zc, subs)
                 if (!subs.isSuccessful) break
             }
-
-            innerVisited.set(z)
+            innerVisited.clear(z)
         }
 
         if (subs.isSuccessful) {
             innerAcyclic.set(z)
 
             // avoid unnecessary instatiation
-            val success = if (subs is SuccessfulSubstitution) subs else SuccessfulSubstitution(subs)
+            val success = if (subs is SuccessfulSubstitution) subs as SuccessfulSubstitution
+                            else SuccessfulSubstitution(subs)
 
-            val vars = innerVars[find(z)]
             if (vars != null) {
                 for (v in vars) {
                    if (v != z) {
@@ -143,23 +143,10 @@ class TermGraphUnifier {
 
 
     private fun unifClosure(a: Int, b: Int): Boolean {
-        var s = find(a)
-        var t = find(b)
+        if (find(a) == find(b)) { return true }
 
-        if (s == t) { return true }
-
-        var zs = innerSchema[s]
-        var zt = innerSchema[t]
-
-        while (origin[zs].`is`(REF)) {
-            s = union(s, getRef(zs))
-            zs = innerSchema[s]
-        }
-
-        while (origin[zt].`is`(REF)) {
-            t = union(t, getRef(zt))
-            zt = innerSchema[t]
-        }
+        val (s, zs) = findSchema(a)
+        val (t, zt) = findSchema(b)
 
         // a VAR always matches another term
         if (origin[zs].`is`(VAR) || origin[zt].`is`(VAR)) {
@@ -188,14 +175,13 @@ class TermGraphUnifier {
 
             // fail if different arguments count
             return zsit.hasNext() == ztit.hasNext()
-            
+
         }  else {
             // something's wrong with the input
             throw IllegalStateException("invalid input")
         }
     }
 
-
     private fun union(a: Int, b: Int): Int {
         var s = find(a)
         var t = find(b)
@@ -230,13 +216,14 @@ class TermGraphUnifier {
         if (origin[zs].`is`(REF)) {
             innerSchema[s] = zt
 
-        } else if (origin[zs].`is`(VAR) && !(origin[zt].`is`(VAR))) {
+        } else if (origin[zs].`is`(VAR) && (origin[zt].`is`(FUN))) {
             innerSchema[s] = zt
         }
 
         return s
     }
 
+
     private fun find(t: Int): Int  {
         var repr = innerClass[t]
         if (repr == t) { return repr }
@@ -257,19 +244,31 @@ class TermGraphUnifier {
         return repr
     }
 
-
     private fun prependVars(t: Int, vars: TIntArrayList?) {
         if (vars?.isEmpty ?: true) { return }
 
-        val newVars = IntList(innerVars[t] ?: EMPTY)
+        val newVars = IntList(innerVars[t] ?: EMPTY_LIST)
         newVars.addAll(vars)
         innerVars.put (t, newVars)
     }
 
-    private fun getRef(zs: Int): Int {
-        return if (origin[zs].`is`(REF)) toInner(origin[zs].get()) else zs
+
+    private fun findSchema(s: Int): Pair<Int, Int> {
+        var t = find(s)
+        var zt = innerSchema[t]
+        while (origin[zt].`is`(REF)) {
+            t = union(t, getRef(zt))
+            zt = innerSchema[t]
+        }
+        return t to zt
     }
 
+    private fun getRef(zs: Int): Int =
+        if (origin[zs].`is`(REF))
+            toInner(origin[zs].get())
+        else
+            zs
+
     private fun toInner(term: Term): Int {
         // Variables with matching symbols are all treated as a single term.
         val key = if (term.`is`(VAR)) idSymbol(term.symbol()) else term
@@ -298,7 +297,7 @@ class TermGraphUnifier {
     private fun idSymbol(symbol: Any): Any =
         when (symbol) {
             is String       -> symbol.intern()
-            is Logical<*> -> symbol.findRoot()
+            is Logical<*>   -> symbol.findRoot()
             else            -> symbol
         }
 

reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java

@@ -23,6 +23,7 @@ import jetbrains.mps.unification.Substitution;
 import jetbrains.mps.unification.Term;
 import jetbrains.mps.unification.TermWrapper;
 import org.jetbrains.annotations.NotNull;
+import org.junit.Ignore;
 import org.junit.Test;
 
 import java.util.Collection;
@@ -288,7 +289,9 @@ public class SolverTests {
         );
     }
 
+    // FIXME cyclic terms are no longer supported
     @Test
+    @Ignore
     public void testCyclicVar() throws Exception {
         assertUnifiesWithBindings(
                 MockTermsParser.parseTerm("@1 a{b ^1}"),
@@ -576,32 +579,36 @@ public class SolverTests {
 
     @Test
     public void testFailCyclicVarRef() throws Exception {
-//        assertUnificationFails(
-//                MockTermsParser.parseTerm("X"),
-//                MockTermsParser.parseTerm("f{^X}"),
-//
-//                CYCLE_DETECTED
-//        );
-//        assertUnificationFails(
-//                MockTermsParser.parseTerm("f{X}"),
-//                MockTermsParser.parseTerm("f{f{^X}}"),
-//
-//                CYCLE_DETECTED
-//        );
-//        assertUnificationFails(
-//                MockTermsParser.parseTerm("t {@1 f{X} g{^1}}"),
-//                MockTermsParser.parseTerm("t {   f{X} X    }"),
-//
-//                CYCLE_DETECTED
-//        );
-//        assertUnificationFails(
-//                MockTermsParser.parseTerm("t { f{^X} X     }"),
-//                MockTermsParser.parseTerm("t { Y     g{^Y} }"),
-//
-//                CYCLE_DETECTED
-//        );
+        assertUnificationFails(
+                MockTermsParser.parseTerm("X"),
+                MockTermsParser.parseTerm("f{^X}"),
 
-        // pass
+                CYCLE_DETECTED
+        );
+        assertUnificationFails(
+                MockTermsParser.parseTerm("f{X}"),
+                MockTermsParser.parseTerm("f{f{^X}}"),
+
+                CYCLE_DETECTED
+        );
+        assertUnificationFails(
+                MockTermsParser.parseTerm("t {@1 f{X} g{^1}}"),
+                MockTermsParser.parseTerm("t {   f{X} X    }"),
+
+                CYCLE_DETECTED
+        );
+        assertUnificationFails(
+                MockTermsParser.parseTerm("t {@1 f{X} g{^1}}"),
+                MockTermsParser.parseTerm("t {   f{Y} Y    }"),
+
+                CYCLE_DETECTED
+        );
+        assertUnificationFails(
+                MockTermsParser.parseTerm("t { f{^X} X     }"),
+                MockTermsParser.parseTerm("t { Y     g{^Y} }"),
+
+                CYCLE_DETECTED
+        );
         assertUnificationFails(
                 MockTermsParser.parseTerm("t { ^X Y    }"),
                 MockTermsParser.parseTerm("t {  Y f{X} }"),
@@ -620,7 +627,6 @@ public class SolverTests {
 
                 CYCLE_DETECTED
         );
-        // fixme: infinitely cycles !!
         assertUnificationFails(
                 MockTermsParser.parseTerm("t { ^X ^Y    }"),
                 MockTermsParser.parseTerm("t {  Y f{X} }"),