Typechecking for basic language done

diff --git a/src/tycheck.sml b/src/tycheck.sml
index 5eca71e..03ede40 100644 (file)
--- 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 (file)
--- 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