X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/blobdiff_plain/a356587aacf682b584fbbebf7b999154755e80c7..b5a575f0cd0d94db4e3cea6aba0fa904d127d044:/src/tycheck.sml

diff --git a/src/tycheck.sml b/src/tycheck.sml
index d5b3f1e..38ef822 100644
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -1,5 +1,6 @@
 (* HCoop Domtool (http://hcoop.sourceforge.net/)
  * Copyright (c) 2006-2007, Adam Chlipala
+ * Copyright (c) 2014 Clinton Ebadi <clinton@unknownlamer.org>
  *
  * This program is free software; you can redistribute it and/or
  * modify it under the terms of the GNU General Public License
@@ -258,10 +259,7 @@ fun envVarSetFrom v (e, _) =
 
       | _ => NONE
 
-fun ununify (tAll as (t, _)) =
-    case t of
-	TUnif (_, ref (SOME t)) => ununify t
-      | _ => tAll
+val ununify = Describe.ununify
 
 fun checkExp G (eAll as (e, loc)) =
     let
@@ -446,14 +444,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,
@@ -505,14 +503,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,
@@ -674,6 +672,25 @@ fun checkDecl G (d, _, loc) =
 							    SOME ue));
 	    bindVal G (name, to, SOME e)
 	end
+      | DEnv (name, to, e) =>
+	let
+	    val to =
+		case to of
+		    NONE => (newUnif (), loc)
+		  | SOME to => checkTyp G to
+
+	    val t = checkExp G e
+	in
+	    hasTyp (e, t, to)
+	    handle Unify ue =>
+		   Describe.describe_type_error loc
+						(WrongType ("Dynamically bound value",
+							    e,
+							    t,
+							    to,
+							    SOME ue));
+	    bindInitialDynEnvVal G (name, to, e)
+	end
       | DContext name => bindContext G name
 
 fun printActionDiffs {have, need} =
@@ -726,15 +743,42 @@ fun printActionDiffs {have, need} =
 	
       | _ => false
 
-fun checkFile G tInit (_, ds, eo) =
+fun checkFile G (prog as (_, ds, eo)) =
     let
 	val G' = foldl (fn (d, G) => checkDecl G d) G ds
+
+	fun tInitial prog env =
+	    (* This should likely only take the dynamic env as an argument *)
+	    let
+		fun allSets (e, _) =
+		    case e of
+			ESkip => true
+		      | ESet _ => true
+		      | ESeq es => List.all allSets es
+		      | _ => false
+
+		val dmy = ErrorMsg.dummyLoc
+
+		fun bodyType (_, _, SOME e) =
+		    if allSets e then
+			(CPrefix (CRoot, dmy), dmy)
+		    else
+			(CRoot, dmy)
+		  | bodyType _ = (CRoot, dmy)
+	    in
+		(TAction (bodyType prog,
+			  Env.initialDynEnvTypes env,
+			  StringMap.empty),
+		 dmy)
+	    end
+
     in
 	case eo of
 	    NONE => ()
 	  | SOME (e as (_, loc)) =>
 	    let
 		val t = checkExp G' e
+		val tInit = tInitial prog G'
 	    in
 		hasTyp (e, t, tInit)
 		handle Unify _ =>