diff --git a/reactor/unification/code/src/jetbrains/mps/unification/TermWrapper.java b/reactor/unification/code/src/jetbrains/mps/unification/TermWrapper.java new file mode 100644 index 00000000..63fc64f8 --- /dev/null +++ b/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; + } + + }; + +} diff --git a/reactor/unification/code/src/jetbrains/mps/unification/Unification.java b/reactor/unification/code/src/jetbrains/mps/unification/Unification.java index 5228c708..4e46a178 100644 --- a/reactor/unification/code/src/jetbrains/mps/unification/Unification.java +++ b/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); } diff --git a/reactor/unification/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java b/reactor/unification/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java index 00cec251..08554b82 100644 --- a/reactor/unification/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java +++ b/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 myTermCache = new IdentityHashMap(); private FailureCause myFailureCause = UKNOWN; diff --git a/reactor/unification/tests/test/jetbrains/mps/unification/test/AssertUnification.java b/reactor/unification/tests/test/jetbrains/mps/unification/test/AssertUnification.java index d1efd057..5741a40d 100644 --- a/reactor/unification/tests/test/jetbrains/mps/unification/test/AssertUnification.java +++ b/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); diff --git a/reactor/unification/tests/test/jetbrains/mps/unification/test/SolverTests.java b/reactor/unification/tests/test/jetbrains/mps/unification/test/SolverTests.java index 647074e1..c04f0221 100644 --- a/reactor/unification/tests/test/jetbrains/mps/unification/test/SolverTests.java +++ b/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 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(