Unification feature: term wrapper to facilitate modal unification (such as b/w different meta levels).

reactor/unification/code/src/jetbrains/mps/unification/TermWrapper.java

@@ -0,0 +1,30 @@
+package jetbrains.mps.unification;
+
+/**
+ * Used by the unifier to wrap original terms in order to alter the unification behaviour.
+ *
+ * For example, one might want to represent a (term) variable as a constant in order to avoid unwanted matches.
+ *
+ * @author Fedor Isakov
+ */
+public interface TermWrapper {
+
+    Term wrap(Term orig);
+
+    Term unwrap(Term wrapper);
+
+    TermWrapper ID = new TermWrapper() {
+
+        @Override
+        public Term wrap(Term orig) {
+            return orig;
+        }
+
+        @Override
+        public Term unwrap(Term wrapper) {
+            return wrapper;
+        }
+
+    };
+
+}

reactor/unification/code/src/jetbrains/mps/unification/Unification.java

@@ -34,6 +34,12 @@ public class Unification {
         return dagUnifier.unify(a, b);
     }
 
+    public static Substitution unify(Term a, Term b, TermWrapper wrapper) {
+        UnionFindTermGraphUnifier dagUnifier = new UnionFindTermGraphUnifier(wrapper);
+
+        return dagUnifier.unify(a, b);
+    }
+
     protected static Substitution failedSubstitution(FailureCause failCause) {
         return new Substitution(failCause);
     }

reactor/unification/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java

@@ -49,6 +49,12 @@ import static jetbrains.mps.unification.Unification.*;
  */
 public class UnionFindTermGraphUnifier {
 
+    public UnionFindTermGraphUnifier() {}
+
+    public UnionFindTermGraphUnifier(TermWrapper wrapper) {
+        this.wrapper = wrapper;
+    }
+
     public Substitution unify(Term a, Term b) {
         if (unifClosure(toInner(a), toInner(b))) {
             Substitution solution = findSolution(toInner(a));
@@ -241,10 +247,10 @@ public class UnionFindTermGraphUnifier {
 
                 // Keep the order of variables within a binding
                 if (trg.myOrigin.is(VAR) && trg.myOrigin.compareTo(var.myOrigin) < 0) {
-                    success.addBinding(trg.myOrigin, var.myOrigin);
+                    success.addBinding(fromInner(trg), fromInner(var));
                 }
                 else {
-                    success.addBinding(var.myOrigin, trg.myOrigin);
+                    success.addBinding(fromInner(var), fromInner(trg));
                 }
             }
         }
@@ -273,11 +279,17 @@ public class UnionFindTermGraphUnifier {
         Object key = term.is(VAR) ? String.valueOf(term.symbol()).intern() : term;
         InnerTerm innerTerm = myTermCache.get(key);
         if (innerTerm == null) {
-            myTermCache.put(key, (innerTerm = new InnerTerm(term)));
+            myTermCache.put(key, (innerTerm = new InnerTerm(wrapper.wrap(term))));
         }
         return innerTerm;
     }
 
+    private Term fromInner(InnerTerm innerTerm) {
+        return wrapper.unwrap(innerTerm.myOrigin);
+    }
+
+    private TermWrapper wrapper = TermWrapper.ID;
+
     private Map<Object, InnerTerm> myTermCache = new IdentityHashMap<Object, InnerTerm>();
 
     private FailureCause myFailureCause = UKNOWN;

reactor/unification/tests/test/jetbrains/mps/unification/test/AssertUnification.java

@@ -18,6 +18,8 @@ package jetbrains.mps.unification.test;
 
 import jetbrains.mps.unification.Substitution;
 import static jetbrains.mps.unification.Substitution.*;
+
+import jetbrains.mps.unification.TermWrapper;
 import jetbrains.mps.unification.Unification;
 import jetbrains.mps.unification.Term;
 
@@ -78,6 +80,22 @@ public class AssertUnification {
         assertSameBindings(subs.bindings(), subs2.bindings());
     }
 
+    public static void assertUnifiesWithBindings(Term s, Term t, TermWrapper wrapper, Substitution.Binding ... bindings) throws Exception{
+        Substitution subs = Unification.unify(s, t, wrapper);
+
+        assertTrue(subs.isSuccessful());
+        assertSameBindings(
+                Arrays.asList(
+                        bindings
+                ),
+                subs.bindings());
+
+        Substitution subs2 = Unification.unify(t, s, wrapper);
+
+        assertTrue(subs2.isSuccessful());
+        assertSameBindings(subs.bindings(), subs2.bindings());
+    }
+
     public static void assertUnifiesWithBindingsAsymm(Term s, Term t, Substitution.Binding ... bindings) throws Exception{
         Substitution subs = Unification.unify(s, t);
 
@@ -99,6 +117,16 @@ public class AssertUnification {
         assertFalse(subs2.isSuccessful());
     }
 
+    public static void assertUnificationFails(Term s, Term t, TermWrapper wrapper) throws Exception {
+        Substitution subs1 = Unification.unify(s, t, wrapper);
+
+        assertFalse(subs1.isSuccessful());
+
+        Substitution subs2 = Unification.unify(s, t, wrapper);
+
+        assertFalse(subs2.isSuccessful());
+    }
+
     public static void assertUnificationFails(Term s, Term t, FailureCause failureCause) throws Exception {
         Substitution subs1 = Unification.unify(s, t);
 

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

@@ -17,8 +17,13 @@
 package jetbrains.mps.unification.test;
 
 import jetbrains.mps.unification.Term;
+import jetbrains.mps.unification.TermWrapper;
+import org.jetbrains.annotations.NotNull;
 import org.junit.Test;
 
+import java.util.Collection;
+import java.util.Collections;
+
 import static jetbrains.mps.unification.Substitution.FailureCause.*;
 import static jetbrains.mps.unification.test.AssertUnification.*;
 import static jetbrains.mps.unification.test.MockTerm.*;
@@ -504,6 +509,55 @@ public class SolverTests {
         );
     }
 
+    @Test
+    public void testWrapper() throws Exception {
+        Term t1 = parse("a{b c{X}}");
+        Term t2 = parse("a{X c{Y}}");
+        Term p1 = parse("a{META c{d}}");
+        Term p2 = parse("a{b c{META}}");
+
+        class Wrapper implements Term {
+            Term wrapped;
+
+            Wrapper(Term term)                                          { this.wrapped = term; }
+            @Override public Object symbol()                            { return wrapped; }
+            @Override public Collection<? extends Term> arguments()     { return Collections.emptyList(); }
+            @Override public Term get()                                 {  return this; }
+            @Override public boolean is(Kind kind)                      { return Kind.FUN == kind; }
+            @Override public int compareTo(@NotNull Term other) {
+                return String.valueOf(symbol()).compareTo(String.valueOf(other.symbol()));
+            }
+
+        }
+
+        TermWrapper wrapper = new TermWrapper() {
+            @Override
+            public Term wrap(Term orig) {
+                return (orig.is(Kind.VAR) && "META".equals(orig.symbol())) ? new Wrapper(orig) : orig;
+            }
+
+            @Override
+            public Term unwrap(Term maybeWrapper) {
+                return maybeWrapper instanceof Wrapper ? ((Wrapper)maybeWrapper).wrapped : maybeWrapper;
+            }
+        };
+
+        assertUnifiesWithBindings(t1, p1,
+                bind(var("META"), parse("b")),
+                bind(var("X"), parse("d"))
+        );
+        assertUnificationFails(t1, p1, wrapper);
+
+        assertUnifiesWithBindings(t1, p2, wrapper,
+                bind(var("X"), parse("META"))
+        );
+
+        assertUnifiesWithBindings(t2, p2, wrapper,
+                bind(var("X"), parse("b")),
+                bind(var("Y"), parse("META"))
+        );
+    }
+
     @Test
     public void testFailConflict() throws Exception {
         assertUnificationFails(