From 690e2929bbdc14e723d8e1192765902d89f2f7fb Mon Sep 17 00:00:00 2001
From: Fedor Isakov <fisakov@gmail.com>
Date: Sun, 22 Mar 2015 15:10:41 +0100
Subject: [PATCH] Ensure the data is associated with nodes using identity,
 except variables, which are identified by symbol

---
 .../UnionFindTermGraphUnifier.java            | 20 ++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java b/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java
index 4ed00562..5213efa0 100644
--- a/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java
+++ b/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java
@@ -42,7 +42,7 @@ import java.util.*;
  */
 public class UnionFindTermGraphUnifier {
 
-    private Map<Object, Data> myData = new HashMap<Object, Data>();
+    private Map<Object, Data> myData = new IdentityHashMap<Object, Data>();
 
     public Substitution unify(Node a, Node b) {
         if (!unifClosure(a, b)) {
@@ -287,7 +287,16 @@ public class UnionFindTermGraphUnifier {
     }
 
     private boolean hasData(Node n) {
-        return myData.containsKey(n);
+        Object key = n.is(Node.Kind.VAR) ? String.valueOf(n.symbol()).intern() : n;
+        return myData.containsKey(key);
+    }
+
+    private Data getData(Node n) {
+        Object key = n.is(Node.Kind.VAR) ? String.valueOf(n.symbol()).intern() : n;
+        if (myData.containsKey(key)) return myData.get(key);
+        Data data = new Data(n);
+        myData.put(key, data);
+        return data;
     }
 
     private List<Node> collectVars(Node n) {
@@ -297,13 +306,6 @@ public class UnionFindTermGraphUnifier {
         return Collections.<Node>emptyList();
     }
 
-    private Data getData(Node n) {
-        if (myData.containsKey(n)) return myData.get(n);
-        Data data = new Data(n);
-        myData.put(n, data);
-        return data;
-    }
-
     private boolean eq(Object a, Object b) {
         return a == null ? b == null : a.equals(b);
     }