Reduction

[hcoop/domtool2.git] / src / tycheck.sml

diff --git a/src/tycheck.sml b/src/tycheck.sml
index 854b575..fa006df 100644 (file)
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -20,21 +20,10 @@
 
 structure Tycheck :> TYCHECK = struct
 
 
 structure Tycheck :> TYCHECK = struct
 

-open Ast Print
+open Ast Print Env

 
 

-structure SS = StringSet

 structure SM = StringMap
 
 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))
-

 local
     val unifCount = ref 0
 in
 local
     val unifCount = ref 0
 in


@@ -99,7 +88,7 @@ fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
        andalso eqRecord eqTy (r1, r2)
 
       | (TNested (p1, q1), TNested (p2, q2)) =>
        andalso eqRecord eqTy (r1, r2)
 
       | (TNested (p1, q1), TNested (p2, q2)) =>

-       eqPred (p1, p2) andalso eqPred (q1, q2)
+       eqPred (p1, p2) andalso eqTy (q1, q2)

 
       | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
       | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)
 
       | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
       | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)


@@ -170,7 +159,10 @@ fun describe_type_error loc te =
 
 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
     case (p1, p2) of
 
 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
     case (p1, p2) of

-       (_, CPrefix (CRoot, _)) => true
+       (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
+      | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
+
+      | (_, CPrefix (CRoot, _)) => true

       | (CNot (CPrefix (CRoot, _), _), _) => true
 
       | (CRoot, CRoot) => true
       | (CNot (CPrefix (CRoot, _), _), _) => true
 
       | (CRoot, CRoot) => true


@@ -182,9 +174,6 @@ fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
 
       | (CNot p1, CNot p2) => predImplies (p2, p1)
 
 
       | (CNot p1, CNot p2) => predImplies (p2, p1)
 

-      | (_, 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)) =
       | _ => false
 
 fun predSimpl (pAll as (p, loc)) =


@@ -202,6 +191,8 @@ fun predSimpl (pAll as (p, loc)) =
                (CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
              | _ => if predImplies (p2', p1') then
                         p2'
                (CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
              | _ => if predImplies (p2', p1') then
                         p2'

+                    else if predImplies (p1', p2') then
+                        p1'

                     else
                         (CAnd (p1', p2'), loc)
        end
                     else
                         (CAnd (p1', p2'), loc)
        end


@@ -226,7 +217,7 @@ fun occurs u (t, _) =
       | TAction (_, d, r) =>
        List.exists (occurs u) (SM.listItems d)
        orelse List.exists (occurs u) (SM.listItems r)
       | TAction (_, d, r) =>
        List.exists (occurs u) (SM.listItems d)
        orelse List.exists (occurs u) (SM.listItems r)

-      | TNested _ => false
+      | TNested (_, t) => occurs u t

       | TError => false
       | TUnif (_, ref (SOME t)) => occurs u t
       | TUnif (_, u') => u = u'
       | TError => false
       | TUnif (_, ref (SOME t)) => occurs u t
       | TUnif (_, u') => u = u'


@@ -252,7 +243,7 @@ fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
 
       | (TNested (d1, r1), TNested (d2, r2)) =>
        (subPred (d2, d1);
 
       | (TNested (d1, r1), TNested (d2, r2)) =>
        (subPred (d2, d1);

-        subPred (r1, r2))
+        subTyp (r1, r2))

 
       | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
       | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
 
       | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
       | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)


@@ -305,7 +296,7 @@ fun checkTyp G (tAll as (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)
          | 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 _ => tAll
+         | TNested (p, t) => (TNested (p, checkTyp G t), loc)

          | TError => raise Fail "TError in parser-generated type"
          | TUnif _ => raise Fail "TUnif in parser-generated type"
     end
          | TError => raise Fail "TError in parser-generated type"
          | TUnif _ => raise Fail "TUnif in parser-generated type"
     end


@@ -347,7 +338,7 @@ fun checkExp G (eAll as (e, loc)) =
                        NONE => (newUnif (), loc)
                      | SOME t => checkTyp G t
 
                        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)
                val t' = checkExp G' e
            in
                (TArrow (t, t'), loc)


@@ -395,7 +386,7 @@ fun checkExp G (eAll as (e, loc)) =
          | EGet (x, evar, rest) =>
            let
                val xt = (newUnif (), loc)
          | EGet (x, 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
 
                val rt = whnorm (checkExp G' rest)
            in


@@ -483,33 +474,87 @@ fun checkExp G (eAll as (e, loc)) =
                          (TError, loc))
            end
 
                          (TError, loc))
            end
 

-         | ELocal e =>
+         | ELocal (e1, e2) =>

            let
            let

-               val rt = whnorm (checkExp G e)
+               val t1 = whnorm (checkExp G e1)
+               val t2 = whnorm (checkExp G e2)

            in
            in

-               case rt of
-                   (TAction (p, d, _), _) =>
-                   (TAction (p, d, SM.empty), loc)
-                 | (TError, _) => rt
-                 | _ => (dte (WrongForm ("Body of local action",
+               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' =>
+                                                            (subTyp (t, t')
+                                                             handle Unify ue =>
+                                                                    dte (WrongType ("Shared environment variable",
+                                                                                    (EVar name, loc),
+                                                                                    t,
+                                                                                    t',
+                                                                                    SOME ue));
+                                                             d'))
+                                                     | SOME t' =>
+                                                       (subTyp (t, t')
+                                                        handle Unify ue =>
+                                                               dte (WrongType ("Shared environment variable",
+                                                                               (EVar name, loc),
+                                                                               t,
+                                                                               t',
+                                                                               SOME ue));
+                                                        d'))
+                                               d1 d2
+                        in
+                            (TAction (p', d', r2), loc)
+                        end
+                      | (TError, _) => t2
+                      | _ => (dte (WrongForm ("Action to be sequenced",
+                                              "action",
+                                              e2,
+                                              t2,
+                                              NONE));
+                              (TError, loc)))
+                 | (TError, _) => t1
+                 | _ => (dte (WrongForm ("Action to be sequenced",

                                          "action",
                                          "action",

-                                         e,
-                                         rt,
+                                         e1,
+                                         t1,

                                          NONE));
                          (TError, loc))
            end
 
                                          NONE));
                          (TError, loc))
            end
 

+

          | EWith (e1, e2) =>
            let
                val t1 = whnorm (checkExp G e1)
                val t2 = whnorm (checkExp G e2)
            in
                case t1 of
          | EWith (e1, e2) =>
            let
                val t1 = whnorm (checkExp G e1)
                val t2 = whnorm (checkExp G e2)
            in
                case t1 of

-                   (TNested (pd, pr), _) =>
+                   (TNested (pd, (TAction (pr, d1, r1), _)), _) =>

                    (case t2 of
                         (TAction (p, d, r), _) =>
                         if predImplies (pd, p) then
                    (case t2 of
                         (TAction (p, d, r), _) =>
                         if predImplies (pd, p) then

-                            (TAction (pr, d, r), loc)
+                            let
+                                val combineRecs =
+                                    SM.unionWithi (fn (name, t1, t2) =>
+                                                      (subTyp (t1, t2)
+                                                       handle Unify ue =>
+                                                              dte (WrongType ("Environment variable",
+                                                                              (EVar name, loc),
+                                                                              t1,
+                                                                              t2,
+                                                                              SOME ue));
+                                                       t2))
+                            in
+                                (TAction (pr, combineRecs (d, d1),
+                                          combineRecs (r, r1)), loc)
+                            end

                         else
                             (dte (WrongPred ("nested action",
                                              pd,
                         else
                             (dte (WrongPred ("nested action",
                                              pd,


@@ -582,7 +627,26 @@ fun checkUnit G (eAll as (_, loc)) =
 fun checkDecl G (d, _, loc) =
     case d of
        DExternType name => bindType G name
 fun checkDecl G (d, _, loc) =
     case d of
        DExternType name => bindType G name

-      | DExternVal (name, t) => bindVal G (name, checkTyp G t)
+      | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
+      | DVal (name, to, e) =>
+       let
+           val to =
+               case to of
+                   NONE => (newUnif (), loc)
+                 | SOME to => checkTyp G to
+
+           val t = checkExp G e
+       in
+           subTyp (t, to)
+           handle Unify ue =>
+                  describe_type_error loc
+                                      (WrongType ("Bound value",
+                                                  e,
+                                                  t,
+                                                  to,
+                                                  SOME ue));
+           bindVal G (name, to, SOME e)
+       end

 
 fun checkFile G tInit (ds, eo) =
     let
 
 fun checkFile G tInit (ds, eo) =
     let