X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/blobdiff_plain/9b7ee2b22abce813120a633f5a4f5523a630a2ea..a92add469211c33a0820839dae449853cd427b66:/src/tycheck.sml

diff --git a/src/tycheck.sml b/src/tycheck.sml
index d486603..12efce3 100644
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -184,10 +184,21 @@ fun baseCondition t =
 			      | _ => 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 e) then
+	  | SOME rule => rule (simplifyKindOf e)) then
 	()
     else
 	subTyp (t1, t2)
@@ -237,7 +248,7 @@ fun envVarSetFrom v (e, _) =
 	    SOME e
 	else
 	    NONE
-      | EGet (_, _, e) => envVarSetFrom v e
+      | EGet (_, _, _, e) => envVarSetFrom v e
       | ESeq es => foldr (fn (e, found) =>
 			     case found of
 				 SOME _ => found
@@ -247,6 +258,8 @@ fun envVarSetFrom v (e, _) =
 
       | _ => NONE
 
+val ununify = Describe.ununify
+
 fun checkExp G (eAll as (e, loc)) =
     let
 	val dte = Describe.describe_type_error loc
@@ -346,14 +359,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, 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)
@@ -426,14 +443,14 @@ fun checkExp G (eAll as (e, loc)) =
 			     (TAction (p', d', r'), loc)
 			 end
 		       | (TError, _) => t2
-		       | _ => (dte (WrongForm ("Action to be sequenced",
+		       | _ => (dte (WrongForm ("First action to be sequenced",
 					       "action",
 					       e2,
 					       t2,
 					       NONE));
 			       (TError, loc)))
 		  | (TError, _) => t1
-		  | _ => (dte (WrongForm ("Action to be sequenced",
+		  | _ => (dte (WrongForm ("Second action to be sequenced",
 					  "action",
 					  e1,
 					  t1,
@@ -485,14 +502,14 @@ fun checkExp G (eAll as (e, loc)) =
 			     (TAction (p', d', r2), loc)
 			 end
 		       | (TError, _) => t2
-		       | _ => (dte (WrongForm ("Action to be sequenced",
+		       | _ => (dte (WrongForm ("Body of local settings",
 					       "action",
 					       e2,
 					       t2,
 					       NONE));
 			       (TError, loc)))
 		  | (TError, _) => t1
-		  | _ => (dte (WrongForm ("Action to be sequenced",
+		  | _ => (dte (WrongForm ("Local settings",
 					  "action",
 					  e1,
 					  t1,
@@ -551,6 +568,32 @@ fun checkExp G (eAll as (e, loc)) =
 
 	  | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
 			       SM.empty, SM.empty), loc)
+
+	  | EIf (e1, e2, e3) =>
+	    let
+		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, t3); t3)
+		       handle Unify _ =>
+			      ((subTyp (t3, t2); t2)
+			       handle Unify ue =>
+				      (dte (WrongType ("\"else\" case",
+						       eAll,
+						       t3,
+						       t2,
+						       SOME ue));
+				       (TError, loc)))
+	    end
     end
 
 exception Ununif
@@ -630,6 +673,56 @@ fun checkDecl G (d, _, loc) =
 	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
@@ -641,10 +734,11 @@ fun checkFile G tInit (_, ds, eo) =
 		val t = checkExp G' e
 	    in
 		hasTyp (e, 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))
+		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