diff --git a/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java b/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java index 91182f3f..c3a130e0 100644 --- a/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java +++ b/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java @@ -51,8 +51,6 @@ public class UnionFindTermGraphUnifier { private Map myData = new IdentityHashMap(); - private int myUnreconciledRefs = 0; - private FailureCause myFailureCause = UKNOWN; public Substitution unify(Node a, Node b) { @@ -190,7 +188,6 @@ public class UnionFindTermGraphUnifier { } private Substitution findSolution(Node s) { - myUnreconciledRefs = 0; return findSolution(s, EMPTY_SUBSTITUTION); } @@ -204,7 +201,6 @@ public class UnionFindTermGraphUnifier { return failedSubstitution(CYCLE_DETECTED); // there exists a cycle } - int unreconciled = myUnreconciledRefs; if (z.is(FUN)) { setVisited(z, true); @@ -223,20 +219,11 @@ public class UnionFindTermGraphUnifier { return substitution; } - if (isReferenced(z)) { - setReferenced(z, false); - myUnreconciledRefs--; - } - setAcyclic(z, true); SuccessfulSubstitution success = new SuccessfulSubstitution(substitution); for (Node var : getVars(find(z))) { if (var != z) { - if (myUnreconciledRefs != unreconciled) { - return failedSubstitution(UNRECONCILED_REF); // there's an unreconciled outward reference - } - Node val = z.is(REF) ? z.get() : z; // Keep the order of variables within a binding @@ -249,14 +236,10 @@ public class UnionFindTermGraphUnifier { } } - if (z.is(REF) && z.get().is(FUN)) { - setReferenced(z.get(), true); - myUnreconciledRefs++; - } - return success; } + private int getSize(Node n) { if (!hasData(n)) return 1; return getData(n).mySize; @@ -310,14 +293,6 @@ public class UnionFindTermGraphUnifier { getData(n).myVisited = visited; } - private boolean isReferenced(Node n) { - return hasData(n) && getData(n).myReferenced; - } - - private void setReferenced(Node n, boolean referenced) { - getData(n).myReferenced = referenced; - } - private boolean hasData(Node n) { Object key = n.is(VAR) ? String.valueOf(n.symbol()).intern() : n; return myData.containsKey(key); diff --git a/reactor/tests/src/jetbrains/mps/unification/test/AssertStructurallyEquivalent.java b/reactor/tests/src/jetbrains/mps/unification/test/AssertStructurallyEquivalent.java index 16f3d3b1..f622495c 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/AssertStructurallyEquivalent.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/AssertStructurallyEquivalent.java @@ -38,7 +38,18 @@ public class AssertStructurallyEquivalent { signature.label(term); return term.children(); } - }), + } + , + new NodeVisitor(Node.Kind.REF) { + @Override + public Collection visit(Node ref) throws Exception { + if (ref.get().is(Node.Kind.FUN)) { + return Collections.singletonList(ref.get()); + } + return Collections.emptyList(); + } + } + ), // second pass new NodeWalker( new NodeVisitor(Node.Kind.FUN) { @@ -59,9 +70,14 @@ public class AssertStructurallyEquivalent { public Collection visit(Node ref) throws Exception { if (ref.get().is(Node.Kind.FUN)) { Integer label = signature.getLabel(ref.get()); - assertNotNull("not found label for '"+ref.get() + "'", label); - signature.appendSignature("^").append(label); - return Collections.emptyList(); + assertNotNull("not found label for '" + ref.get() + "'", label); + if (signature.isTopLevel(ref.get())) { + signature.appendSignature("^").append(label); + return Collections.emptyList(); + } + else { + return Collections.singletonList(ref.get()); + } } else if (ref.get().is(Node.Kind.VAR)) { signature.appendSignature("^").append(ref.get().symbol()); @@ -98,6 +114,8 @@ public class AssertStructurallyEquivalent { return labels.get(node); } + protected boolean isTopLevel(Node node) { return labels.get(node) == 1; } + protected StringBuilder appendSignature(String str) { return signature.append(str); } @@ -133,12 +151,16 @@ public class AssertStructurallyEquivalent { return kind; } + + public abstract Collection visit(T t) throws Exception ; } private static class NodeWalker { + private static Object SINGLETON = new Object(); + private Map> visitorMap = new HashMap>(); public NodeWalker(NodeVisitor... visitors) { @@ -148,9 +170,19 @@ public class AssertStructurallyEquivalent { } public void walk(Node node) throws Exception { + walk(node, new IdentityHashMap()); + } + + private void walk(Node node, Map visited) throws Exception { + if (node.is(Node.Kind.FUN)) { + visited.put(node, SINGLETON); + } Collection children = switchClass(node); for (Node child : children) { - walk(child); + if (visited.containsKey(child)) { + continue; + } + walk(child, visited); } } diff --git a/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java b/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java index 2081f9d4..19618d5b 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java @@ -89,16 +89,25 @@ public class AssertUnification { } public static void assertUnificationFails(Node s, Node t) throws Exception { - Substitution subs = Unification.unify(s, t); + Substitution subs1 = Unification.unify(s, t); - assertFalse(subs.isSuccessful()); + assertFalse(subs1.isSuccessful()); + + Substitution subs2 = Unification.unify(s, t); + + assertFalse(subs2.isSuccessful()); } public static void assertUnificationFails(Node s, Node t, FailureCause failureCause) throws Exception { - Substitution subs = Unification.unify(s, t); + Substitution subs1 = Unification.unify(s, t); - assertFalse(subs.isSuccessful()); - assertSame(failureCause, subs.failureCause()); + assertFalse(subs1.isSuccessful()); + assertSame(failureCause, subs1.failureCause()); + + Substitution subs2 = Unification.unify(t, s); + + assertFalse(subs2.isSuccessful()); + assertSame(failureCause, subs2.failureCause()); } } \ No newline at end of file diff --git a/reactor/tests/src/jetbrains/mps/unification/test/MockTreeParser.java b/reactor/tests/src/jetbrains/mps/unification/test/MockTreeParser.java index 90bd80fa..d8a74d7b 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/MockTreeParser.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/MockTreeParser.java @@ -231,7 +231,7 @@ public class MockTreeParser { private void addRef(String ref) { final int label = Integer.parseInt(ref.substring(1)); - if (termRefs.containsKey(label)) { + if (termRefs.containsKey(label) && termRefs.get(label) != null) { childrenStack.peek().add(ref(termRefs.get(label))); } else { diff --git a/reactor/tests/src/jetbrains/mps/unification/test/ParserTests.java b/reactor/tests/src/jetbrains/mps/unification/test/ParserTests.java index 3f4dbc66..3b7c44bf 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/ParserTests.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/ParserTests.java @@ -136,22 +136,6 @@ public class ParserTests { term("a", ref(d), d)); } - @Test(expected = ComparisonFailure.class) - public void testNotEquivalent2() throws Exception { - Node b1 = term("b"); - Node b2 = term("b"); - assertEquivalent(parse("a{@2b ^1 @1b ^2}"), - term("a", b2, ref(b2), b1, ref(b1))); - } - - @Test(expected = ComparisonFailure.class) - public void testNotEquivalent3() throws Exception { - Node b1 = term("b"); - Node b2 = term("b"); - assertEquivalent(parse("a{@2b ^1 ^2 @1b}"), - term("a", b2, ref(b2), ref(b1), b1)); - } - @Test(expected = MockTreeParser.ParseException.class) public void testUnclosedFail() { parse("a{b "); diff --git a/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java b/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java index d168c873..dbb8556b 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java @@ -16,10 +16,12 @@ package jetbrains.mps.unification.test; +import jetbrains.mps.unification.Node; import org.junit.Test; import static jetbrains.mps.unification.Substitution.FailureCause.*; import static jetbrains.mps.unification.test.AssertUnification.*; +import static jetbrains.mps.unification.test.MockNode.ref; import static jetbrains.mps.unification.test.MockNode.term; import static jetbrains.mps.unification.test.MockNode.var; import static jetbrains.mps.unification.test.MockTreeParser.*; @@ -288,6 +290,77 @@ public class SolverTests { parse("@1 a{b ^1}"), parse("@2 a{b ^2}") ); + // the following tests are not very strict, but they suffice to convey a message + // that cyclic terms can be safely unified + assertUnifiesWithBindings( + parse("a{@1 b{c{^2}} @2 b{c{^1}}}"), + parse("a{ b{Y} b{Y} }"), + + // TODO: the innermost "b" must actually contain a ref to the top level + // FIXME: AssertStructurallyEquivalent + bind(var("Y"), parse("@1 c{b{c{b }}}")) + ); + assertUnifiesWithBindings( + parse("a{@1 b{c{^1}} @2 c{b{^2}}}"), + parse("a{ b{Y} Y }"), + + // TODO: the innermost "b" must actually contain a ref to the top level + // FIXME: AssertStructurallyEquivalent + bind(var("Y"), parse("c{b }")) + ); + assertUnifiesWithBindings( + parse("a{@1 b{c{@3 b{c{^3}}}} @2 c{b{^2}}}"), + parse("a{ b{Y} Y }"), + + // TODO: the innermost "c" must actually contain a ref to the top level + // FIXME: AssertStructurallyEquivalent + bind(var("Y"), parse("c{b{c }}")) + ); + assertUnifiesWithBindings( + parse("@1 a{c{d} b{e{^1 f}}}"), + parse(" a{c{X} b{Y}}"), + + bind(var("X"), parse("d")), + + // TODO: the innermost "b" must actually contain a ref to the top level + // FIXME: AssertStructurallyEquivalent + bind(var("Y"), parse("e{a{c{d} b } f}")) + ); + assertUnifiesWithBindings( + parse("@1 a{c{d} b{e{@2 a{c{d} b{e{^2 f}}} f}}}"), + parse(" a{c{X} b{Y}}"), + + bind(var("X"), parse("d")), + + // TODO: the innermost "e" must actually contain a ref to the top level + // FIXME: AssertStructurallyEquivalent + bind(var("Y"), parse("e{a{c{d} b{e{ f}}} f}")) + ); + } + + @Test + public void testCyclicExt() throws Exception { + Node left = parse("@1 j{^1}"); + Node right = term("j", term("j", ref(left))); + assertUnifiesWithBindings( + left, + right + ); + assertUnifiesWithBindings( + parse("a{@1 b{c{^1}} b{c{Z}} @2 c{b{^2}}}"), + parse("a{ Z b{Y} Y }"), + + bind(var("Y"), parse("@2 c{Z}")), + bind(var("Z"), parse("@1 b{c{^1}}")) + ); + assertUnifiesWithBindings( + parse("@1 a{c{d} b{e{Z f}} ^1}"), + parse(" a{c{X} b{Y} Z}"), + + bind(var("X"), parse("d")), + bind(var("Y"), parse("e{Z f}")), + bind(var("Z"), parse("@1 a{c{d} b{e{Z f}} ^1}")) + ); } @Test @@ -327,7 +400,6 @@ public class SolverTests { @Test public void testVarRef() throws Exception { - assertUnifiesWithBindings( parse("^X"), parse("Y"), @@ -358,7 +430,6 @@ public class SolverTests { bind(var("X"), parse("d")) ); - } @Test @@ -414,7 +485,7 @@ public class SolverTests { } @Test - public void testFailRecursive() throws Exception { + public void testFailCyclic() throws Exception { assertUnificationFails( parse("f{X}"), parse("X"), @@ -439,11 +510,13 @@ public class SolverTests { CYCLE_DETECTED ); - assertUnificationFails ( - parse("a{@1 b{c{^1}} @2 c{b{^2}}}"), - parse("a{ b{Y} Y }"), + assertUnificationFails( + parse("a{ b{c{b{c{b{c{^2}}}}}} @2 b{c{b{c{^2}}}}}"), + parse("a{ b{Y} b{Y} }"), - UNRECONCILED_REF + CYCLE_DETECTED ); } + + }