Improve "Unification incomplete for case" diagnostics (#116)

src/edu/cmu/cs/sasylf/ast/DerivationByAnalysis.java

@@ -239,7 +239,11 @@ public static void caseAnalyze(Context ctx, final String targetName,
 							newSet = e.getKey().caseAnalyze(ctx, targetTerm, targetElement, source);
 							continue;
 						}
-						ErrorHandler.error(Errors.CASE_UNIFICATION_INCOMPLETE, e.getKey().getName(), source, "SASyLF tried to unify " + ex.term1 + " and " + ex.term2);
+						String hint = RuleCase.incompleteUnificationHint(ctx, ctx.getCurrentCaseAnalysisRoot(),
+								source.getLocation(), ex);
+						ErrorHandler.error(Errors.CASE_UNIFICATION_INCOMPLETE, hint, source,
+								"while merging saved case for rule " + e.getKey().getName() + "; SASyLF tried to unify "
+										+ ex.term1 + " and " + ex.term2);
 						continue;
 					} catch (UnificationFailed ex) {
 						Util.debug("case no longer feasible.");

src/edu/cmu/cs/sasylf/ast/Rule.java

@@ -435,7 +435,9 @@ private void checkCaseApplication(Context ctx, Set<Pair<Term,Substitution>> resu
 			Util.debug("found sub ", sub, " for case analyzing ", term, " with rule ", getName());
 		} catch (UnificationIncomplete e) {
 			Util.debug("unification incomplete on ", pattern, " and ", subject);
-			ErrorHandler.recoverableError(Errors.CASE_UNIFICATION_INCOMPLETE, source, "SASyLF tried to unify " + e.term1 + " and " + e.term2);
+			String hint = RuleCase.incompleteUnificationHint(ctx, ctx.getCurrentCaseAnalysisRoot(), source.getLocation(), e);
+			ErrorHandler.recoverableError(Errors.CASE_UNIFICATION_INCOMPLETE, hint, source,
+					"SASyLF tried to unify " + e.term1 + " and " + e.term2);
 		} catch (UnificationFailed e) {
 			Util.debug("failure: " + e.getMessage());
 			Util.debug("unification failed on ", pattern, " and ", subject);

src/edu/cmu/cs/sasylf/ast/RuleCase.java

@@ -348,8 +348,10 @@ public void typecheck(Context parent, Pair<Fact,Integer> isSubderivation) {
 
 				break;
 			} catch (UnificationIncomplete e) {
-				ErrorHandler.error(Errors.CASE_UNIFICATION_INCOMPLETE, this,
-						"(was checking " + candidate + " instance of " + caseTerm + ",\n got exception " + e);      
+				String hint = incompleteUnificationHint(ctx, subjectRoot, getLocation(), e);
+				ErrorHandler.error(Errors.CASE_UNIFICATION_INCOMPLETE, hint, this,
+						"(was checking " + candidate + " instance of " + caseTerm + ";\n SASyLF tried to unify "
+								+ e.term1 + " and " + e.term2 + ")");      
 				return; // tell Java we're gone.
 
 			} catch (UnificationFailed uf) {
@@ -421,6 +423,28 @@ public void typecheck(Context parent, Pair<Fact,Integer> isSubderivation) {
 	 * @param app
 	 * @return
 	 */
+	/**
+	 * Produce a short user-facing hint for {@link UnificationIncomplete} during case checking,
+	 * using the same heuristic as the first unification in {@link #typecheck(Context, Pair)}.
+	 * See <a href="https://github.com/boyland/sasylf/issues/116">issue #116</a>.
+	 */
+	static String incompleteUnificationHint(Context ctx, NonTerminal subjectRoot, Location loc, UnificationIncomplete uf) {
+		Term app = uf.term1;
+		if (app instanceof Application && !(((Application) app).getFunction() instanceof FreeVar)) {
+			app = uf.term2;
+		}
+		try {
+			TermPrinter tp = new TermPrinter(ctx, subjectRoot, loc, false);
+			String s = tp.toString(app, false);
+			if (app instanceof FreeVar && ctx.inputVars.contains(app)) {
+				return s + " (this metavariable is already fixed by an earlier premise)";
+			}
+			return s;
+		} catch (RuntimeException ex) {
+			return app.toString();
+		}
+	}
+
 	private Term canonRuleApp(Application app) {
 		if (app.getArguments().size() == 1 && app.getArguments().get(0) instanceof Abstraction) {
 			List<Abstraction> abs = new ArrayList<Abstraction>();

src/edu/cmu/cs/sasylf/util/Errors.java

@@ -238,7 +238,7 @@ public enum Errors {
 	SUGAR_SYNTAX_UNKNOWN ("unknown syntax"), // infeasible
 	SUGAR_ABSTRACT ("cannot define abstract syntactic sugar on concrete syntax"), // infeasible
 	NEVER_RIGID ("using rule is likely to lead to incomplete unification because the following variables are never used outside of a binding: "), // Warning
-	CASE_UNIFICATION_INCOMPLETE("Unification incomplete for case "),
+	CASE_UNIFICATION_INCOMPLETE("Unification incomplete for case; likely problem near "),
 	SOLVE_FAILED ("unable to find proof"),
 	SOLVE_UNRELIABLE ("proof by solve is not reliable"), // Warning
 	DERIVATION_NAME_REUSED ("reusing derivation identifier"), // Warning

visualizer/.gitignore

@@ -0,0 +1,5 @@
+node_modules/
+dist/
+.env
+.DS_Store
+coverage/