From: Adam Chlipala <adamc@hcoop.net>
Date: Sat, 29 Jul 2006 20:33:22 +0000 (+0000)
Subject: Typechecking for basic language done
X-Git-Tag: release_2010-11-19~389
X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/commitdiff_plain/db427c6775f4d2babcabadbbea93117f593259c6

Typechecking for basic language done
---

diff --git a/src/tycheck.sml b/src/tycheck.sml
index 5eca71e..03ede40 100644
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -152,21 +152,48 @@ fun describe_type_error loc te =
       | UnboundVariable name =>
 	ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
 
-fun unifyPred (p1All as (p1, _), p2All as (p2, _)) =
+fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
     case (p1, p2) of
-	(CRoot, CRoot) => ()
-      | (CConst s1, CConst s2) =>
-	if s1 = s2 then
-	    ()
-	else
-	    raise (Unify (UnifyPred (p1All, p2All)))
-      | (CPrefix p1, CPrefix p2) => unifyPred (p1, p2)
-      | (CNot p1, CNot p2) => unifyPred (p1, p2)
-      | (CAnd (p1, q1), CAnd (p2, q2)) =>
-	(unifyPred (p1, p2);
-	 unifyPred (q1, q2))
+	(_, CPrefix (CRoot, _)) => true
+      | (CNot (CPrefix (CRoot, _), _), _) => true
+
+      | (CRoot, CRoot) => true
+
+      | (CConst s1, CConst s2) => s1 = s2
+
+      | (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
+
+      | (CNot p1, CNot p2) => predImplies (p2, p1)
 
-      | _ => raise (Unify (UnifyPred (p1All, p2All)))
+      | (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
+      | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
+
+      | _ => false
+
+fun predSimpl (pAll as (p, loc)) =
+    case p of
+	CRoot => pAll
+      | CConst _ => pAll
+      | CPrefix p => (CPrefix (predSimpl p), loc)
+      | CNot p => (CNot (predSimpl p), loc)
+      | CAnd (p1, p2) =>
+	let
+	    val p1' = predSimpl p1
+	    val p2' = predSimpl p2
+	in
+	    case p1' of
+		(CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
+	      | _ => if predImplies (p2', p1') then
+			 p2'
+		     else
+			 (CAnd (p1', p2'), loc)
+	end
+   
+fun unifyPred (p1, p2) =
+    if predImplies (p1, p2) then
+	()
+    else
+	raise (Unify (UnifyPred (p1, p2)))
 
 fun unifyRecord f (r1, r2) =
     (SM.appi (fn (k, v1) =>
@@ -239,6 +266,11 @@ fun isError t =
 	(TError, _) => true
       | _ => false
 
+fun whnorm (tAll as (t, loc)) =
+    case t of
+	TUnif (_, ref (SOME tAll)) => whnorm tAll
+      | _ => tAll
+
 fun checkExp G (eAll as (e, loc)) =
     let
 	val dte = describe_type_error loc
@@ -311,8 +343,118 @@ fun checkExp G (eAll as (e, loc)) =
 					SOME ue));
 			(TError, loc))
 	    end
-		     
-	  | _ => raise Fail "Not ready for that expression yet!"
+
+	  | ESet (evar, e) =>
+	    let
+		val t = checkExp G e
+	    in
+		(TAction ((CPrefix (CRoot, loc), loc),
+			  SM.empty,
+			  SM.insert (SM.empty, evar, t)),
+		 loc)
+	    end
+	  | EGet (x, evar, rest) =>
+	    let
+		val xt = (newUnif (), loc)
+		val G' = SM.insert (G, x, xt)
+
+		val rt = whnorm (checkExp G' rest)
+	    in
+		case rt of
+		    (TAction (p, d, r), _) =>
+		    (case SM.find (d, evar) of
+			 NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
+		       | SOME xt' =>
+			 (unify (xt', xt)
+				handle Unify ue =>
+				       dte (WrongType ("Retrieved environment variable",
+						       (EVar x, loc),
+						       xt',
+						       xt,
+						       SOME ue));
+			  rt))
+		  | _ => (dte (WrongForm ("Body of environment variable read",
+					  "action",
+					  rest,
+					  rt,
+					  NONE));
+			  (TError, loc))
+	    end
+
+	  | ESeq [] => raise Fail "Empty ESeq"
+	  | ESeq [e1] => checkExp G e1
+	  | ESeq (e1 :: rest) =>
+	    let
+		val e2 = (ESeq rest, loc)
+
+		val t1 = whnorm (checkExp G e1)
+		val t2 = whnorm (checkExp G e2)
+	    in
+		case t1 of
+		    (TAction (p1, d1, r1), _) =>
+		    (case t2 of
+			 (TAction (p2, d2, r2), _) =>
+			 let
+			     val p' = predSimpl (CAnd (p1, p2), loc)
+
+			     val d' = SM.foldli (fn (name, t, d') =>
+						    case SM.find (r1, name) of
+							NONE =>
+							(case SM.find (d', name) of
+							     NONE => SM.insert (d', name, t)
+							   | SOME t' =>
+							     (unify (t, t')
+							      handle Unify ue =>
+								     dte (WrongType ("Shared environment variable",
+										     (EVar name, loc),
+										     t,
+										     t',
+										     SOME ue));
+							      d'))
+						      | SOME t' =>
+							(unify (t, t')
+							 handle Unify ue =>
+								dte (WrongType ("Shared environment variable",
+										(EVar name, loc),
+										t,
+										t',
+										SOME ue));
+							 d'))
+						d1 d2
+
+			     val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
+						r1 r2
+			 in
+			     (TAction (p', d', r'), loc)
+			 end
+		       | _ => (dte (WrongForm ("Action to be sequenced",
+					       "action",
+					       e2,
+					       t2,
+					       NONE));
+			       (TError, loc)))
+		  | _ => (dte (WrongForm ("Action to be sequenced",
+					  "action",
+					  e1,
+					  t1,
+					  NONE));
+			  (TError, loc))
+	    end
+
+	  | ELocal e =>
+	    let
+		val rt = whnorm (checkExp G e)
+	    in
+		case rt of
+		    (TAction (p, d, _), _) =>
+		    (TAction (p, d, SM.empty), loc)
+		  | _ => (dte (WrongForm ("Body of local action",
+					  "action",
+					  e,
+					  rt,
+					  NONE));
+			  (TError, loc))
+	    end
     end
 
 exception Ununif
diff --git a/tests/test.dtl b/tests/test.dtl
index b23f578..38c1af7 100644
--- a/tests/test.dtl
+++ b/tests/test.dtl
@@ -1,3 +1,8 @@
-(\x -> [x, 7]) 13;
-0
+name <- Name;
+Name = (\x : (int) -> "Freddy") name;
+let
+	Name = 17
+in
+	Name = 13
+end