From 41077453e8ce7b5bbd33c01ba206ce6cb85e3107 Mon Sep 17 00:00:00 2001 From: Fedor Isakov Date: Tue, 24 Mar 2015 16:20:40 +0100 Subject: [PATCH] Reporting the cause of failed unification, some code cleanup --- .../mps/unification/Substitution.java | 51 +++++++++++++++++-- .../mps/unification/Unification.java | 49 ++++++------------ .../UnionFindTermGraphUnifier.java | 17 +++++-- .../unification/test/AssertUnification.java | 7 +++ .../mps/unification/test/SolverTests.java | 47 ++++++++++++----- 5 files changed, 115 insertions(+), 56 deletions(-) diff --git a/reactor/code/src/jetbrains/mps/unification/Substitution.java b/reactor/code/src/jetbrains/mps/unification/Substitution.java index 1e16b58c..180815ef 100644 --- a/reactor/code/src/jetbrains/mps/unification/Substitution.java +++ b/reactor/code/src/jetbrains/mps/unification/Substitution.java @@ -25,13 +25,38 @@ import java.util.Collections; * * @author Fedor Isakov */ -public interface Substitution { +public class Substitution { - boolean isSuccessful(); + private boolean mySuccessful; - Collection bindings() ; + private FailureCause myFailureCause; - public class Binding { + public Substitution(boolean successful) { + mySuccessful = successful; + } + + public Substitution(FailureCause failCause) { + myFailureCause = failCause; + mySuccessful = false; + } + + public boolean isSuccessful() { + return mySuccessful; + } + + public Collection bindings() { + return Collections.emptyList(); + } + + public FailureCause failureCause() { + return myFailureCause; + } + + public String toString() { + return myFailureCause != null ? "[" + myFailureCause + "]" : "[FAILED_SUBSTITUTION]"; + } + + public static class Binding { private Node myVar; private Node myNode; @@ -49,4 +74,22 @@ public interface Substitution { } } + public enum FailureCause { + CYCLE_DETECTED("cycle detected"), + UNRECONCILED_REF("unreconciled ref"), + SYMBOL_CLASH("symbol clash"), + UKNOWN("uknown"); + + private String myMessage; + + FailureCause(String message) { + myMessage = message; + } + + @Override + public String toString() { + return myMessage; + } + } + } diff --git a/reactor/code/src/jetbrains/mps/unification/Unification.java b/reactor/code/src/jetbrains/mps/unification/Unification.java index 01f4530a..cb1d31dd 100644 --- a/reactor/code/src/jetbrains/mps/unification/Unification.java +++ b/reactor/code/src/jetbrains/mps/unification/Unification.java @@ -16,6 +16,8 @@ package jetbrains.mps.unification; +import jetbrains.mps.unification.Substitution.FailureCause; + import java.util.*; /** @@ -32,53 +34,33 @@ public class Unification { return dagUnifier.unify(a, b); } - protected static final Substitution FAILED_SUBSTITUTION = new Substitution() { - @Override - public boolean isSuccessful() { - return false; - } - - @Override - public Collection bindings() { - return Collections.emptyList(); - } - - @Override - public String toString() { - return "[FAILED_SUBSTITUTION]"; - } - }; - - protected static final Substitution EMPTY_SUBSTITUTION = new Substitution() { - @Override - public boolean isSuccessful() { - return true; - } - - @Override - public Collection bindings() { - return Collections.emptyList(); - } + protected static Substitution failedSubstitution(FailureCause failCause) { + return new Substitution(failCause); + } + protected static final Substitution EMPTY_SUBSTITUTION = new Substitution(true) { @Override public String toString() { return "[]"; } }; - protected static class SuccessfulSubstitution implements Substitution { + protected static final Substitution FAILED_SUBSTITUTION = new Substitution(FailureCause.UKNOWN) { + @Override + public String toString() { + return "[FAILED_SUBSTITUTION]"; + } + }; + + protected static class SuccessfulSubstitution extends Substitution { private LinkedList myBindings; protected SuccessfulSubstitution(Substitution substitution) { + super(true); this.myBindings = new LinkedList(substitution.bindings()); } - @Override - public boolean isSuccessful() { - return true; - } - @Override public Collection bindings() { return Collections.unmodifiableCollection(myBindings); @@ -108,5 +90,4 @@ public class Unification { } } - } diff --git a/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java b/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java index af2d7231..91182f3f 100644 --- a/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java +++ b/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java @@ -16,11 +16,13 @@ package jetbrains.mps.unification; +import jetbrains.mps.unification.Substitution.FailureCause; import jetbrains.mps.unification.Unification.SuccessfulSubstitution; import java.util.*; import static jetbrains.mps.unification.Node.Kind.*; +import static jetbrains.mps.unification.Substitution.FailureCause.*; import static jetbrains.mps.unification.Unification.*; /** @@ -51,9 +53,11 @@ public class UnionFindTermGraphUnifier { private int myUnreconciledRefs = 0; + private FailureCause myFailureCause = UKNOWN; + public Substitution unify(Node a, Node b) { if (!unifClosure(a, b)) { - return FAILED_SUBSTITUTION; + return failedSubstitution(myFailureCause); } return findSolution(a); @@ -108,6 +112,7 @@ public class UnionFindTermGraphUnifier { if (zs.is(FUN) && zt.is(FUN)) { if (!eq(zs.symbol(), zt.symbol())) { + myFailureCause = SYMBOL_CLASH; return false; // symbol clash } @@ -119,7 +124,9 @@ public class UnionFindTermGraphUnifier { Iterator scit = zs.children().iterator(); Iterator tcit = zt.children().iterator(); while (scit.hasNext() && tcit.hasNext()) { - if (!unifClosure(scit.next(), tcit.next())) return false; + if (!unifClosure(scit.next(), tcit.next())) { + return false; // children mismatch + } } // fail if different children count @@ -127,7 +134,7 @@ public class UnionFindTermGraphUnifier { } else { // something's wrong with the input - return false; + throw new IllegalStateException("invalid input"); } } @@ -194,7 +201,7 @@ public class UnionFindTermGraphUnifier { return substitution; // not part of a cycle } if (isVisited(z)) { - return FAILED_SUBSTITUTION; // there exists a cycle + return failedSubstitution(CYCLE_DETECTED); // there exists a cycle } int unreconciled = myUnreconciledRefs; @@ -227,7 +234,7 @@ public class UnionFindTermGraphUnifier { for (Node var : getVars(find(z))) { if (var != z) { if (myUnreconciledRefs != unreconciled) { - return FAILED_SUBSTITUTION; // there's an unreconciled outward reference + return failedSubstitution(UNRECONCILED_REF); // there's an unreconciled outward reference } Node val = z.is(REF) ? z.get() : z; diff --git a/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java b/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java index 3f9fc4b8..2081f9d4 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java @@ -94,4 +94,11 @@ public class AssertUnification { assertFalse(subs.isSuccessful()); } + public static void assertUnificationFails(Node s, Node t, FailureCause failureCause) throws Exception { + Substitution subs = Unification.unify(s, t); + + assertFalse(subs.isSuccessful()); + assertSame(failureCause, subs.failureCause()); + } + } \ No newline at end of file diff --git a/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java b/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java index 06372b73..d168c873 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java @@ -16,12 +16,13 @@ package jetbrains.mps.unification.test; -import jetbrains.mps.unification.Node; import org.junit.Test; -import static jetbrains.mps.unification.test.MockNode.*; -import static jetbrains.mps.unification.test.MockTreeParser.*; +import static jetbrains.mps.unification.Substitution.FailureCause.*; import static jetbrains.mps.unification.test.AssertUnification.*; +import static jetbrains.mps.unification.test.MockNode.term; +import static jetbrains.mps.unification.test.MockNode.var; +import static jetbrains.mps.unification.test.MockTreeParser.*; /** * Created by fyodor on 09.06.2014. @@ -315,6 +316,13 @@ public class SolverTests { bind(var("X"), parse("@1 a{b ^1}")) ); + assertUnifiesWithBindings( + parse("a{X c{X} }"), + parse("a{b{Y} c{@1 b{@2 c{b{^2}}}}}"), + + bind(var("X"), parse("b{Y}")), + bind(var("Y"), parse("@1 c{b{^1}}")) + ); } @Test @@ -385,15 +393,15 @@ public class SolverTests { public void testFailConflict() throws Exception { assertUnificationFails( term("a"), - term("b") + term("b"), + + SYMBOL_CLASH ); assertUnificationFails( parse("node{name{X} child{abc}}"), - parse("node{name{foo} child{X}}") - ); - assertUnificationFails( - parse("f{a{X} Y }"), - parse("f{Y a{b{X}}}") + parse("node{name{foo} child{X}}"), + + SYMBOL_CLASH ); } @@ -409,20 +417,33 @@ public class SolverTests { public void testFailRecursive() throws Exception { assertUnificationFails( parse("f{X}"), - parse("X") + parse("X"), + + CYCLE_DETECTED ); assertUnificationFails( parse("f{f{X}}"), - parse("f{X}") + parse("f{X}"), + + CYCLE_DETECTED + ); + assertUnificationFails( + parse("f{a{X} Y }"), + parse("f{Y a{b{X}}}"), + + CYCLE_DETECTED ); assertUnificationFails( parse("a{X c{X}}"), - parse("a{b{Y} Y }") + parse("a{b{Y} Y }"), + CYCLE_DETECTED ); assertUnificationFails ( parse("a{@1 b{c{^1}} @2 c{b{^2}}}"), - parse("a{ b{Y} Y }") + parse("a{ b{Y} Y }"), + + UNRECONCILED_REF ); } }