Report details if the unification failed

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"),

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() {

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
             }
 

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());
     }
 
-}
+    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
+    }
+
+}
+

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"
         );
     }