Dropped check for unreconciled refs, adapted the tests
This commit is contained in:
parent
41077453e8
commit
2fb992ead3
|
|
@ -51,8 +51,6 @@ public class UnionFindTermGraphUnifier {
|
|||
|
||||
private Map<Object, Data> myData = new IdentityHashMap<Object, Data>();
|
||||
|
||||
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);
|
||||
|
|
|
|||
|
|
@ -38,7 +38,18 @@ public class AssertStructurallyEquivalent {
|
|||
signature.label(term);
|
||||
return term.children();
|
||||
}
|
||||
}),
|
||||
}
|
||||
,
|
||||
new NodeVisitor<Node>(Node.Kind.REF) {
|
||||
@Override
|
||||
public Collection<? extends Node> 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>(Node.Kind.FUN) {
|
||||
|
|
@ -59,9 +70,14 @@ public class AssertStructurallyEquivalent {
|
|||
public Collection<? extends Node> 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<? extends Node> visit(T t) throws Exception ;
|
||||
|
||||
}
|
||||
|
||||
private static class NodeWalker {
|
||||
|
||||
private static Object SINGLETON = new Object();
|
||||
|
||||
private Map<Node.Kind, NodeVisitor<? extends Node>> visitorMap = new HashMap<Node.Kind, NodeVisitor<? extends Node>>();
|
||||
|
||||
public NodeWalker(NodeVisitor<? extends Node>... visitors) {
|
||||
|
|
@ -148,9 +170,19 @@ public class AssertStructurallyEquivalent {
|
|||
}
|
||||
|
||||
public void walk(Node node) throws Exception {
|
||||
walk(node, new IdentityHashMap<Node, Object>());
|
||||
}
|
||||
|
||||
private void walk(Node node, Map<Node, Object> visited) throws Exception {
|
||||
if (node.is(Node.Kind.FUN)) {
|
||||
visited.put(node, SINGLETON);
|
||||
}
|
||||
Collection<? extends Node> children = switchClass(node);
|
||||
for (Node child : children) {
|
||||
walk(child);
|
||||
if (visited.containsKey(child)) {
|
||||
continue;
|
||||
}
|
||||
walk(child, visited);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -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 {
|
||||
|
|
|
|||
|
|
@ -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 ");
|
||||
|
|
|
|||
|
|
@ -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
|
||||
);
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue