Limit 'extern' to trusted code
[hcoop/domtool2.git] / src / tycheck.sml
index 152eaf7..007a0fe 100644 (file)
@@ -24,6 +24,10 @@ open Ast Print Env
 
 structure SM = StringMap
 
 
 structure SM = StringMap
 
+val externFlag = ref false
+fun allowExterns () = externFlag := true
+fun disallowExterns () = externFlag := false
+
 local
     val unifCount = ref 0
 in
 local
     val unifCount = ref 0
 in
@@ -426,6 +430,23 @@ fun checkExp G (eAll as (e, loc)) =
                        (TError, loc))
            end
 
                        (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
          | ESet (evar, e) =>
            let
                val t = checkExp G e
@@ -686,8 +707,18 @@ fun checkUnit G (eAll as (_, loc)) =
 
 fun checkDecl G (d, _, loc) =
     case d of
 
 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 =
       | DVal (name, to, e) =>
        let
            val to =