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 myData = new HashMap(); + private Map myData = new IdentityHashMap(); 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 collectVars(Node n) { @@ -297,13 +306,6 @@ public class UnionFindTermGraphUnifier { return Collections.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); }