structure SM = StringMap
+val externFlag = ref false
+fun allowExterns () = externFlag := true
+fun disallowExterns () = externFlag := false
+
local
val unifCount = ref 0
in
(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
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 =