X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/blobdiff_plain/6bb366c5a60247419dce5cbce4a5c034fa2f1e5c..411a85f26421358c20b11839310cce6caff8cf77:/src/tycheck.sml

diff --git a/src/tycheck.sml b/src/tycheck.sml
index f1c90dc..007a0fe 100644
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -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
@@ -431,7 +435,7 @@ fun checkExp G (eAll as (e, loc)) =
 		val p' = checkPred G p
 
 		val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
-		val t' = checkExp G' e
+		val t' = whnorm (checkExp G' e)
 	    in
 		case t' of
 		    (TAction _, _) => (TNested (p, t'), loc)
@@ -703,8 +707,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 =