Better messages for top-level unification errors

[hcoop/domtool2.git] / src / tycheck.sml

diff --git a/src/tycheck.sml b/src/tycheck.sml
index e2feb90..def1463 100644 (file)
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -248,7 +248,7 @@ fun envVarSetFrom v (e, _) =
            SOME e
        else
            NONE
-      | EGet (_, _, e) => envVarSetFrom v e
+      | EGet (_, _, _, e) => envVarSetFrom v e
       | ESeq es => foldr (fn (e, found) =>
                             case found of
                                 SOME _ => found
@@ -258,6 +258,11 @@ fun envVarSetFrom v (e, _) =
 
       | _ => NONE
 
+fun ununify (tAll as (t, _)) =
+    case t of
+       TUnif (_, ref (SOME t)) => ununify t
+      | _ => tAll
+
 fun checkExp G (eAll as (e, loc)) =
     let
        val dte = Describe.describe_type_error loc
@@ -357,14 +362,18 @@ fun checkExp G (eAll as (e, loc)) =
                          SM.insert (SM.empty, evar, t)),
                 loc)
            end
-         | EGet (x, evar, rest) =>
+         | EGet (x, topt, evar, rest) =>
            let
                val xt = (newUnif (), loc)
                val G' = bindVal G (x, xt, NONE)
 
                val rt = whnorm (checkExp G' rest)
            in
-               case rt of
+               case topt of
+                   NONE => ()
+                 | SOME t => subTyp (xt, checkTyp G t);
+
+               case ununify rt of
                    (TAction (p, d, r), _) =>
                    (case SM.find (d, evar) of
                         NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
@@ -641,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
@@ -652,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