X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/blobdiff_plain/095de39e1be653dcb6438d19c719bd7797e0772a..b3159a7069504fe2fb2b781cd6f438decaf0937a:/src/tycheck.sml

diff --git a/src/tycheck.sml b/src/tycheck.sml
index ac9fad5..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
@@ -170,6 +174,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
 
@@ -334,6 +340,23 @@ fun checkTyp G (tAll as (t, loc)) =
 	  | TUnif _ => raise Fail "TUnif in parser-generated type"
     end
 
+fun envVarSetFrom v (e, _) =
+    case e of
+	ESet (v', e) =>
+	if v = v' then
+	    SOME e
+	else
+	    NONE
+      | EGet (_, _, e) => envVarSetFrom v e
+      | ESeq es => foldr (fn (e, found) =>
+			     case found of
+				 SOME _ => found
+			       | NONE => envVarSetFrom v e)
+			 NONE es
+      | ELocal (_, e) => envVarSetFrom v e
+
+      | _ => NONE
+
 fun checkExp G (eAll as (e, loc)) =
     let
 	val dte = describe_type_error loc
@@ -407,6 +430,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
@@ -467,21 +507,25 @@ fun checkExp G (eAll as (e, loc)) =
 							(case SM.find (d', name) of
 							     NONE => SM.insert (d', name, t)
 							   | SOME t' =>
-							     (subTyp (t, t')
+							     ((case envVarSetFrom name e1 of
+								   NONE => subTyp (t, t')
+								 | SOME e => hasTyp (e, t, t'))
 							      handle Unify ue =>
 								     dte (WrongType ("Shared environment variable",
 										     (EVar name, loc),
-										     t,
 										     t',
+										     t,
 										     SOME ue));
 							      d'))
 						      | SOME t' =>
-							(subTyp (t, t')
+							((case envVarSetFrom name e1 of
+								   NONE => subTyp (t, t')
+								 | SOME e => hasTyp (e, t, t'))
 							 handle Unify ue =>
 								dte (WrongType ("Shared environment variable",
 										(EVar name, loc),
-										t,
 										t',
+										t,
 										SOME ue));
 							 d'))
 						d1 d2
@@ -525,21 +569,25 @@ fun checkExp G (eAll as (e, loc)) =
 							(case SM.find (d', name) of
 							     NONE => SM.insert (d', name, t)
 							   | SOME t' =>
-							     (subTyp (t, t')
+							     ((case envVarSetFrom name e1 of
+								   NONE => subTyp (t', t)
+								 | SOME e => hasTyp (e, t', t))
 							      handle Unify ue =>
 								     dte (WrongType ("Shared environment variable",
 										     (EVar name, loc),
-										     t,
 										     t',
+										     t,
 										     SOME ue));
 							      d'))
 						      | SOME t' =>
-							(subTyp (t, t')
+							((case envVarSetFrom name e1 of
+								   NONE => subTyp (t', t)
+								 | SOME e => hasTyp (e, t', t))
 							 handle Unify ue =>
 								dte (WrongType ("Shared environment variable",
 										(EVar name, loc),
-										t,
 										t',
+										t,
 										SOME ue));
 							 d'))
 						d1 d2
@@ -659,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 =