Improved Easy_domain, with boolean env vars

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

diff --git a/src/tycheck.sml b/src/tycheck.sml
index e2feb90..d5b3f1e 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)
@@ -562,6 +571,32 @@ fun checkExp G (eAll as (e, loc)) =
 
          | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
                               SM.empty, SM.empty), loc)
+
+         | EIf (e1, e2, e3) =>
+           let
+               val t1 = checkExp G e1
+               val t2 = checkExp G e2
+               val t3 = checkExp G e3
+               val bool = (TBase "bool", loc)
+           in
+               (subTyp (t1, bool))
+               handle Unify ue =>
+                      dte (WrongType ("\"if\" test",
+                                      e1,
+                                      t1,
+                                      bool,
+                                      SOME ue));
+               (subTyp (t2, t3); t3)
+                      handle Unify _ =>
+                             ((subTyp (t3, t2); t2)
+                              handle Unify ue =>
+                                     (dte (WrongType ("\"else\" case",
+                                                      eAll,
+                                                      t3,
+                                                      t2,
+                                                      SOME ue));
+                                      (TError, loc)))
+           end
     end
 
 exception Ununif
@@ -641,6 +676,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 +737,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