X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/blobdiff_plain/1a4e5a6c9a8fbbdc980cf0661c444ddc2910544a..75d4c2d6fb7996625d062f5949ceb2e66c0a70ab:/src/tycheck.sml

diff --git a/src/tycheck.sml b/src/tycheck.sml
index 5ce94c8..f68100f 100644
--- 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
@@ -14,26 +14,19 @@
  * You should have received a copy of the GNU General Public License
  * along with this program; if not, write to the Free Software
  * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
-*)
+ *)
 
 (* Domtool configuration language type checking *)
 
 structure Tycheck :> TYCHECK = struct
 
-open Ast Print
+open Ast Print Env
 
-structure SS = StringSet
 structure SM = StringMap
 
-type env = SS.set * typ SM.map
-val empty : env = (SS.add (SS.singleton "int", "string"),
-		   SM.empty)
-
-fun lookupType (ts, _) name = SS.member (ts, name)
-fun lookupVal (_, vs) name = SM.find (vs, name)
-
-fun bindType (ts, vs) name = (SS.add (ts, name), vs)
-fun bindVal (ts, vs) (name, t) = (ts, SM.insert (vs, name, t))
+val externFlag = ref false
+fun allowExterns () = externFlag := true
+fun disallowExterns () = externFlag := false
 
 local
     val unifCount = ref 0
@@ -54,119 +47,6 @@ fun newUnif () =
     end
 end
 	    
-exception UnequalDomains
-	  
-fun eqRecord f (r1, r2) =
-    (SM.appi (fn (k, v1) =>
-		 case SM.find (r2, k) of
-		     NONE => raise UnequalDomains
-		   | SOME v2 =>
-		     if f (v1, v2) then
-			 ()
-		     else
-			 raise UnequalDomains) r1;
-     SM.appi (fn (k, v2) =>
-		 case SM.find (r1, k) of
-		     NONE => raise UnequalDomains
-		   | SOME v1 =>
-		     if f (v1, v2) then
-			 ()
-		     else
-			 raise UnequalDomains) r2;
-     true)
-    handle UnequalDomains => false
-
-fun eqPred ((p1, _), (p2, _)) =
-    case (p1, p2) of
-	(CRoot, CRoot) => true
-      | (CConst s1, CConst s2) => s1 = s2
-      | (CPrefix p1, CPrefix p2) => eqPred (p1, p2)
-      | (CNot p1, CNot p2) => eqPred (p1, p2)
-      | (CAnd (p1, q1), CAnd (p2, q2)) =>
-	eqPred (p1, p2) andalso eqPred (q1, q2)
-
-      | _ => false
-
-fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
-    case (t1, t2) of
-	(TBase s1, TBase s2) => s1 = s2
-      | (TList t1, TList t2) => eqTy (t1, t2)
-      | (TArrow (d1, r1), TArrow (d2, r2)) =>
-	eqTy (d1, d2) andalso eqTy (r1, r2)
-
-      | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
-	eqPred (p1, p2) andalso eqRecord eqTy (d1, d2)
-	andalso eqRecord eqTy (r1, r2)
-
-      | (TNested (p1, q1), TNested (p2, q2)) =>
-	eqPred (p1, p2) andalso eqTy (q1, q2)
-
-      | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
-      | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)
-
-      | (TUnif (_, r1), TUnif (_, r2)) => r1 = r2
-
-      | (TError, TError) => true
-
-      | _ => 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 preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
-					[PD.string s, PD.space 1, d]))
-
-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
@@ -184,6 +64,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
 
@@ -217,7 +99,7 @@ fun subPred (p1, p2) =
 fun subRecord f (r1, r2) =
     SM.appi (fn (k, v2) =>
 		case SM.find (r1, k) of
-		    NONE => raise UnequalDomains
+		    NONE => raise Describe.UnequalDomains
 		  | SOME v1 => f (v1, v2)) r2
 
 fun occurs u (t, _) =
@@ -292,6 +174,51 @@ fun whnorm (tAll as (t, loc)) =
 	TUnif (_, ref (SOME tAll)) => whnorm tAll
       | _ => tAll
 
+fun baseCondition t =
+    case whnorm t of
+	(TBase name, _) => typeRule name
+      | (TList t, _) =>
+	(case baseCondition t of
+	     NONE => NONE
+	   | SOME f => SOME (fn (EList ls, _) => List.all f ls
+			      | _ => false))
+      | _ => NONE
+
+fun simplifyKindOf e =
+    case e of
+	(EApp ((EVar s, _), e'), _) =>
+	(case Env.function s of
+	     NONE => e
+	   | SOME f =>
+	     case f [e'] of
+		 NONE => e
+	       | SOME e => e)
+      | _ => e
+
+fun hasTyp (e, t1, t2) =
+    if (case baseCondition t2 of
+	    NONE => false
+	  | SOME rule => rule (simplifyKindOf e)) then
+	()
+    else
+	subTyp (t1, t2)
+
+fun checkPred G (p, loc) =
+    let
+	val err = ErrorMsg.error (SOME loc)
+    in
+	case p of
+	    CRoot => ()
+	  | CConst s =>
+	    if lookupContext G s then
+		()
+	    else
+		err ("Unbound context " ^ s)
+	  | CPrefix p => checkPred G p
+	  | CNot p => checkPred G p
+	  | CAnd (p1, p2) => (checkPred G p1; checkPred G p2)
+    end
+
 fun checkTyp G (tAll as (t, loc)) =
     let
 	val err = ErrorMsg.error (SOME loc)
@@ -305,16 +232,40 @@ fun checkTyp G (tAll as (t, loc)) =
 		 (TError, loc))
 	  | TList t => (TList (checkTyp G t), loc)
 	  | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
-	  | TAction (p, d, r) => (TAction (p, SM.map (checkTyp G) d,
-					   SM.map (checkTyp G) r), loc)
-	  | TNested (p, t) => (TNested (p, checkTyp G t), loc)
+	  | TAction (p, d, r) => (checkPred G p;
+				  (TAction (p, SM.map (checkTyp G) d,
+					    SM.map (checkTyp G) r), loc))
+	  | TNested (p, t) => (checkPred G p;
+			       (TNested (p, checkTyp G t), loc))
 	  | TError => raise Fail "TError in parser-generated type"
 	  | 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 ununify (tAll as (t, _)) =
+    case t of
+	TUnif (_, ref (SOME t)) => ununify t
+      | _ => tAll
+
 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)
@@ -327,7 +278,7 @@ fun checkExp G (eAll as (e, loc)) =
 			  let
 			      val t' = checkExp G e'
 			  in
-			      (subTyp (t', t);
+			      (hasTyp (eAll, t', t);
 			       if isError t' then
 				   (TList (TError, loc), loc)
 			       else
@@ -349,7 +300,7 @@ fun checkExp G (eAll as (e, loc)) =
 			NONE => (newUnif (), loc)
 		      | SOME t => checkTyp G t
 
-		val G' = bindVal G (x, t)
+		val G' = bindVal G (x, t, NONE)
 		val t' = checkExp G' e
 	    in
 		(TArrow (t, t'), loc)
@@ -367,8 +318,8 @@ fun checkExp G (eAll as (e, loc)) =
 		val tf = checkExp G func
 		val ta = checkExp G arg
 	    in
-		(subTyp (tf, (TArrow (dom, ran), loc));
-		 subTyp (ta, dom)
+		(hasTyp (func, tf, (TArrow (dom, ran), loc));
+		 hasTyp (arg, ta, dom)
 		 handle Unify ue =>
 			dte (WrongType ("Function argument",
 					arg,
@@ -385,6 +336,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
@@ -394,14 +362,18 @@ fun checkExp G (eAll as (e, loc)) =
 			  SM.insert (SM.empty, evar, t)),
 		 loc)
 	    end
-	  | EGet (x, evar, rest) =>
+	  | EGet (x, topt, evar, rest) =>
 	    let
 		val xt = (newUnif (), loc)
-		val G' = bindVal G (x, xt)
+		val G' = bindVal G (x, xt, NONE)
 
 		val rt = whnorm (checkExp G' rest)
 	    in
-		case rt of
+		case topt of
+		    NONE => ()
+		  | SOME t => subTyp (xt, checkTyp G t);
+
+		case ununify rt of
 		    (TAction (p, d, r), _) =>
 		    (case SM.find (d, evar) of
 			 NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
@@ -445,21 +417,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
@@ -503,21 +479,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
@@ -591,6 +571,33 @@ fun checkExp G (eAll as (e, loc)) =
 
 	  | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
 			       SM.empty, SM.empty), loc)
+
+	  | EIf (e1, e2, e3) =>
+	    let
+		val t = (newUnif (), loc)
+
+		val t1 = checkExp G e1
+		val t2 = checkExp G e2
+		val t3 = checkExp G e3
+		val bool = (TBase "bool", loc)
+	    in
+		(subTyp (t1, bool))
+		handle Unify ue =>
+		       dte (WrongType ("\"If\" test",
+				       e1,
+				       t1,
+				       bool,
+				       SOME ue));
+		subTyp (t2, t);
+		(subTyp (t3, t))
+		handle Unify ue =>
+		       dte (WrongType ("\"Else\" case",
+				       eAll,
+				       t3,
+				       t2,
+				       SOME ue));
+		t
+	    end
     end
 
 exception Ununif
@@ -631,16 +638,96 @@ fun checkUnit G (eAll as (_, loc)) =
 	    ununif t
 	    handle Ununif =>
 		   (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
-		    printd (p_typ t);
+		    output (p_typ t);
 		    t)
     end
 
 fun checkDecl G (d, _, loc) =
     case d of
-	DExternType name => bindType G name
-      | DExternVal (name, t) => bindVal G (name, checkTyp G t)
+	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 =
+		case to of
+		    NONE => (newUnif (), loc)
+		  | SOME to => checkTyp G to
 
-fun checkFile G tInit (ds, eo) =
+	    val t = checkExp G e
+	in
+	    hasTyp (e, t, to)
+	    handle Unify 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
+
+fun printActionDiffs {have, need} =
+    case (ununif have, ununif need) of
+	((TAction (p1, in1, out1), loc), (TAction (p2, in2, out2), _)) =>
+	let
+	    fun checkPreds () =
+		if predImplies (p1, p2) then
+		    ()
+		else
+		    (ErrorMsg.error (SOME loc) "Files provides the wrong kind of configuration.";
+		     preface ("Have:", p_pred p1);
+		     preface ("Need:", p_pred p2))
+
+	    fun checkIn () =
+		SM.appi (fn (name, t) =>
+			    case SM.find (in2, name) of
+				NONE => (ErrorMsg.error (SOME loc) "An unavailable environment variable is used.";
+					 print ("Name: " ^ name ^ "\n");
+					 preface ("Type:", p_typ t))
+			      | SOME t' =>
+				subTyp (t', t)
+				handle Unify _ =>
+				       (ErrorMsg.error (SOME loc) "Wrong type for environment variable.";
+					print ("          Name: " ^ name ^ "\n");
+					preface ("      Has type:", p_typ t');
+					preface ("Used with type:", p_typ t)))
+			in1
+			
+	    fun checkOut () =
+		SM.appi (fn (name, t) =>
+			    case SM.find (out1, name) of
+				NONE => (ErrorMsg.error (SOME loc) "Missing an output environment variable.";
+					 print ("Name: " ^ name ^ "\n");
+					 preface ("Type:", p_typ t))
+			      | SOME t' =>
+				subTyp (t', t)
+				handle Unify _ =>
+				       (ErrorMsg.error (SOME loc) "Wrong type for output environment variable.";
+					print ("     Name: " ^ name ^ "\n");
+					preface (" Has type:", p_typ t');
+					preface ("Need type:", p_typ t)))
+			out2
+	in
+	    checkPreds ();
+	    checkIn ();
+	    checkOut ();
+	    true
+	end
+	
+      | _ => false
+
+fun checkFile G tInit (_, ds, eo) =
     let
 	val G' = foldl (fn (d, G) => checkDecl G d) G ds
     in
@@ -650,11 +737,12 @@ fun checkFile G tInit (ds, eo) =
 	    let
 		val t = checkExp G' e
 	    in
-		subTyp (t, tInit)
-		handle Unify ue =>
-		       (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
-			preface ("Actual:", p_typ t);
-			preface ("Needed:", p_typ tInit))
+		hasTyp (e, t, tInit)
+		handle Unify _ =>
+		       if printActionDiffs {have = t, need = tInit} then
+			   ()
+		       else
+			   ErrorMsg.error (SOME loc) "File ends in something that isn't a directive."			   
 	    end;
 	G'
     end