From 27a42d9841cf98d306897b9b3918d867ee1fbec2 Mon Sep 17 00:00:00 2001 From: Fedor Isakov Date: Wed, 12 Aug 2015 16:13:27 +0200 Subject: [PATCH] Report details if the unification failed --- .../mps/unification/Substitution.java | 50 +++++++++++++++++-- .../mps/unification/Unification.java | 4 ++ .../UnionFindTermGraphUnifier.java | 5 +- .../unification/test/AssertUnification.java | 18 ++++++- .../mps/unification/test/SolverTests.java | 8 ++- 5 files changed, 77 insertions(+), 8 deletions(-) diff --git a/reactor/code/src/jetbrains/mps/unification/Substitution.java b/reactor/code/src/jetbrains/mps/unification/Substitution.java index beafdbd7..7d34256b 100644 --- a/reactor/code/src/jetbrains/mps/unification/Substitution.java +++ b/reactor/code/src/jetbrains/mps/unification/Substitution.java @@ -16,6 +16,7 @@ package jetbrains.mps.unification; +import java.util.Arrays; import java.util.Collection; import java.util.Collections; @@ -29,14 +30,19 @@ public class Substitution { private boolean mySuccessful; - private FailureCause myFailureCause; + private Failure myFailure; public Substitution(boolean successful) { mySuccessful = successful; } public Substitution(FailureCause failCause) { - myFailureCause = failCause; + myFailure = new Failure(failCause); + mySuccessful = false; + } + + public Substitution(FailureCause failCause, Object... details) { + myFailure = new Failure(failCause, details); mySuccessful = false; } @@ -49,15 +55,21 @@ public class Substitution { } public FailureCause failureCause() { - return myFailureCause; + return myFailure != null ? myFailure.getCause() : null; + } + + public Object[] failureDetails() { + return myFailure != null ? myFailure.getDetails() : null; } public String toString() { - return myFailureCause != null ? "[" + myFailureCause + "]" : "[FAILED_SUBSTITUTION]"; + return myFailure != null ? "[" + String.valueOf(myFailure) + "]" : "[FAILED_SUBSTITUTION]"; } public static class Binding { + private Term myVar; + private Term myTerm; public Binding(Term myVar, Term myTerm) { @@ -74,6 +86,36 @@ public class Substitution { } } + + public static class Failure { + + private FailureCause myCause; + + private Object[] myDetails; + + public Failure(FailureCause cause) { + this.myCause = cause; + } + + public Failure(FailureCause cause, Object... details) { + this.myCause = cause; + this.myDetails = details; + } + + public FailureCause getCause() { + return myCause; + } + + public Object[] getDetails() { + return myDetails; + } + + @Override + public String toString() { + return String.valueOf(myCause) + (myDetails != null ? Arrays.asList(myDetails) : ""); + } + } + public enum FailureCause { CYCLE_DETECTED("cycle detected"), UNRECONCILED_REF("unreconciled ref"), diff --git a/reactor/code/src/jetbrains/mps/unification/Unification.java b/reactor/code/src/jetbrains/mps/unification/Unification.java index a2136593..70dea80d 100644 --- a/reactor/code/src/jetbrains/mps/unification/Unification.java +++ b/reactor/code/src/jetbrains/mps/unification/Unification.java @@ -38,6 +38,10 @@ public class Unification { return new Substitution(failCause); } + protected static Substitution failedSubstitution(FailureCause failCause, Object... details) { + return new Substitution(failCause, details); + } + protected static final Substitution EMPTY_SUBSTITUTION = new Substitution(true) { @Override public String toString() { diff --git a/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java b/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java index 50758b15..10fcffbd 100644 --- a/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java +++ b/reactor/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java @@ -53,9 +53,11 @@ public class UnionFindTermGraphUnifier { private FailureCause myFailureCause = UKNOWN; + private Object[] myFailureDetails = null; + public Substitution unify(Term a, Term b) { if (!unifClosure(a, b)) { - return failedSubstitution(myFailureCause); + return failedSubstitution(myFailureCause, myFailureDetails); } return findSolution(a); @@ -111,6 +113,7 @@ public class UnionFindTermGraphUnifier { { if (!eq(zs.symbol(), zt.symbol())) { myFailureCause = SYMBOL_CLASH; + myFailureDetails = new Object[]{zs.symbol(), zt.symbol()}; return false; // symbol clash } diff --git a/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java b/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java index 3c2c31d7..d1efd057 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/AssertUnification.java @@ -25,6 +25,7 @@ import java.util.*; import static jetbrains.mps.unification.test.AssertStructurallyEquivalent.assertEquivalent; import static org.junit.Assert.*; +import static org.junit.Assert.assertArrayEquals; /** @@ -110,4 +111,19 @@ public class AssertUnification { assertSame(failureCause, subs2.failureCause()); } -} \ No newline at end of file + public static void assertUnificationFails(Term s, Term t, FailureCause failureCause, Object... details) throws Exception { + Substitution subs1 = Unification.unify(s, t); + + assertFalse(subs1.isSuccessful()); + assertSame(failureCause, subs1.failureCause()); + assertArrayEquals(details, subs1.failureDetails()); + + Substitution subs2 = Unification.unify(t, s); + + assertFalse(subs2.isSuccessful()); + assertSame(failureCause, subs1.failureCause()); + // dont test for details: may be in different order + } + +} + diff --git a/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java b/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java index 3c5f8eae..16124f9d 100644 --- a/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java +++ b/reactor/tests/src/jetbrains/mps/unification/test/SolverTests.java @@ -464,13 +464,17 @@ public class SolverTests { term("a"), term("b"), - SYMBOL_CLASH + SYMBOL_CLASH, + "a", + "b" ); assertUnificationFails( parse("node{name{X} child{abc}}"), parse("node{name{foo} child{X}}"), - SYMBOL_CLASH + SYMBOL_CLASH, + "abc", + "foo" ); }