From: Adam Chlipala <adamc@hcoop.net>
Date: Sun, 18 Nov 2007 18:42:36 +0000 (+0000)
Subject: Better messages for top-level unification errors
X-Git-Tag: release_2010-11-19~115
X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/commitdiff_plain/f8fd0d2a07ae8b80fb2a39c82c6214e94076c7e8

Better messages for top-level unification errors
---

diff --git a/src/tycheck.sml b/src/tycheck.sml
index 8889540..def1463 100644
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -650,6 +650,56 @@ fun checkDecl G (d, _, loc) =
 	end
       | DContext name => bindContext G name
 
+fun printActionDiffs {have, need} =
+    case (ununif have, ununif need) of
+	((TAction (p1, in1, out1), loc), (TAction (p2, in2, out2), _)) =>
+	let
+	    fun checkPreds () =
+		if predImplies (p1, p2) then
+		    ()
+		else
+		    (ErrorMsg.error (SOME loc) "Files provides the wrong kind of configuration.";
+		     preface ("Have:", p_pred p1);
+		     preface ("Need:", p_pred p2))
+
+	    fun checkIn () =
+		SM.appi (fn (name, t) =>
+			    case SM.find (in2, name) of
+				NONE => (ErrorMsg.error (SOME loc) "An unavailable environment variable is used.";
+					 print ("Name: " ^ name ^ "\n");
+					 preface ("Type:", p_typ t))
+			      | SOME t' =>
+				subTyp (t', t)
+				handle Unify _ =>
+				       (ErrorMsg.error (SOME loc) "Wrong type for environment variable.";
+					print ("          Name: " ^ name ^ "\n");
+					preface ("      Has type:", p_typ t');
+					preface ("Used with type:", p_typ t)))
+			in1
+			
+	    fun checkOut () =
+		SM.appi (fn (name, t) =>
+			    case SM.find (out1, name) of
+				NONE => (ErrorMsg.error (SOME loc) "Missing an output environment variable.";
+					 print ("Name: " ^ name ^ "\n");
+					 preface ("Type:", p_typ t))
+			      | SOME t' =>
+				subTyp (t', t)
+				handle Unify _ =>
+				       (ErrorMsg.error (SOME loc) "Wrong type for output environment variable.";
+					print ("     Name: " ^ name ^ "\n");
+					preface (" Has type:", p_typ t');
+					preface ("Need type:", p_typ t)))
+			out2
+	in
+	    checkPreds ();
+	    checkIn ();
+	    checkOut ();
+	    true
+	end
+	
+      | _ => false
+
 fun checkFile G tInit (_, ds, eo) =
     let
 	val G' = foldl (fn (d, G) => checkDecl G d) G ds
@@ -661,10 +711,11 @@ fun checkFile G tInit (_, ds, eo) =
 		val t = checkExp G' e
 	    in
 		hasTyp (e, t, tInit)
-		handle Unify ue =>
-		       (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
-			preface ("Actual:", p_typ t);
-			preface ("Needed:", p_typ tInit))
+		handle Unify _ =>
+		       if printActionDiffs {have = t, need = tInit} then
+			   ()
+		       else
+			   ErrorMsg.error (SOME loc) "File ends in something that isn't a directive."			   
 	    end;
 	G'
     end