Factor error message generation into a separate file; add '-tc' flag to domtool-client

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

diff --git a/src/tycheck.sml b/src/tycheck.sml
index 6d58e43..6f62a6c 100644 (file)
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -1,5 +1,5 @@
 (* HCoop Domtool (http://hcoop.sourceforge.net/)
- * Copyright (c) 2006, Adam Chlipala
+ * Copyright (c) 2006-2007, Adam Chlipala
  *
  * This program is free software; you can redistribute it and/or
  * modify it under the terms of the GNU General Public License
@@ -24,6 +24,10 @@ open Ast Print Env
 
 structure SM = StringMap
 
+val externFlag = ref false
+fun allowExterns () = externFlag := true
+fun disallowExterns () = externFlag := false
+
 local
     val unifCount = ref 0
 in
@@ -99,61 +103,6 @@ fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
 
       | _ => false
 
-datatype unification_error =
-        UnifyPred of pred * pred
-       | UnifyTyp of typ * typ
-       | UnifyOccurs of string * typ
-
-exception Unify of unification_error
-
-datatype type_error =
-        WrongType of string * exp * typ * typ * unification_error option
-       | WrongForm of string * string * exp * typ * unification_error option
-       | UnboundVariable of string
-       | WrongPred of string * pred * pred
-
-fun describe_unification_error t ue =
-    case ue of
-       UnifyPred (p1, p2) =>
-       (print "Reason: Incompatible contexts.\n";
-        preface ("Have:", p_pred p1);
-        preface ("Need:", p_pred p2))
-      | UnifyTyp (t1, t2) =>
-       if eqTy (t, t1) then
-           ()
-       else
-           (print "Reason: Incompatible types.\n";
-            preface ("Have:", p_typ t1);
-            preface ("Need:", p_typ t2))
-      | UnifyOccurs (name, t') =>
-       if eqTy (t, t') then
-           ()
-       else
-           (print "Reason: Occurs check failed for ";
-            print name;
-            print " in:\n";
-            printd (p_typ t))
-
-fun describe_type_error loc te =
-    case te of
-       WrongType (place, e, t1, t2, ueo) =>
-       (ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
-        preface (" Expression:", p_exp e);
-        preface ("Actual type:", p_typ t1);
-        preface ("Needed type:", p_typ t2);
-        Option.app (describe_unification_error t1) ueo)
-      |        WrongForm (place, form, e, t, ueo) =>
-       (ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
-        preface ("Expression:", p_exp e);
-        preface ("      Type:", p_typ t);
-        Option.app (describe_unification_error t) ueo)
-      | UnboundVariable name =>
-       ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
-      |        WrongPred (place, p1, p2) =>
-       (ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
-        preface ("Have:", p_pred p1);
-        preface ("Need:", p_pred p2))
-
 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
     case (p1, p2) of
        (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
@@ -170,6 +119,8 @@ fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
       | (_, CPrefix p2) => predImplies (p1All, p2)
 
       | (CNot p1, CNot p2) => predImplies (p2, p1)
+      | (CRoot, CNot (CConst _, _)) => true
+      | (CConst s1, CNot (CConst s2, _)) => s1 <> s2
 
       | _ => false
 
@@ -353,7 +304,7 @@ fun envVarSetFrom v (e, _) =
 
 fun checkExp G (eAll as (e, loc)) =
     let
-       val dte = describe_type_error loc
+       val dte = Describe.describe_type_error loc
     in
        case e of
            EInt _ => (TBase "int", loc)
@@ -424,6 +375,23 @@ fun checkExp G (eAll as (e, loc)) =
                        (TError, loc))
            end
 
+         | EALam (x, p, e) =>
+           let
+               val p' = checkPred G p
+
+               val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
+               val t' = whnorm (checkExp G' e)
+           in
+               case t' of
+                   (TAction _, _) => (TNested (p, t'), loc)
+                 | _ => (dte (WrongForm ("Body of nested configuration 'fn'",
+                                         "action",
+                                         e,
+                                         t',
+                                         NONE));
+                         (TError, loc))
+           end
+
          | ESet (evar, e) =>
            let
                val t = checkExp G e
@@ -684,8 +652,18 @@ fun checkUnit G (eAll as (_, loc)) =
 
 fun checkDecl G (d, _, loc) =
     case d of
-       DExternType name => bindType G name
-      | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
+       DExternType name =>
+       if !externFlag then
+           bindType G name
+       else
+           (ErrorMsg.error (SOME loc) "'extern type' not allowed in untrusted code";
+            G)
+      | DExternVal (name, t) =>
+       if !externFlag then
+           bindVal G (name, checkTyp G t, NONE)
+       else
+           (ErrorMsg.error (SOME loc) "'extern val' not allowed in untrusted code";
+            G)
       | DVal (name, to, e) =>
        let
            val to =
@@ -697,12 +675,12 @@ fun checkDecl G (d, _, loc) =
        in
            hasTyp (e, t, to)
            handle Unify ue =>
-                  describe_type_error loc
-                                      (WrongType ("Bound value",
-                                                  e,
-                                                  t,
-                                                  to,
-                                                  SOME ue));
+                  Describe.describe_type_error loc
+                                               (WrongType ("Bound value",
+                                                           e,
+                                                           t,
+                                                           to,
+                                                           SOME ue));
            bindVal G (name, to, SOME e)
        end
       | DContext name => bindContext G name