E-mail aliases

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

diff --git a/src/tycheck.sml b/src/tycheck.sml
index 5ce94c8..ac69a6d 100644 (file)
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -14,27 +14,16 @@
  * You should have received a copy of the GNU General Public License
  * along with this program; if not, write to the Free Software
  * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
-*)
+ *)
 
 (* Domtool configuration language type checking *)
 
 structure Tycheck :> TYCHECK = struct
 
-open Ast Print
+open Ast Print Env
 
-structure SS = StringSet
 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
@@ -123,9 +112,6 @@ datatype type_error =
        | UnboundVariable of string
        | WrongPred of string * pred * pred
 
-fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
-                                       [PD.string s, PD.space 1, d]))
-
 fun describe_unification_error t ue =
     case ue of
        UnifyPred (p1, p2) =>
@@ -292,6 +278,24 @@ fun whnorm (tAll as (t, loc)) =
        TUnif (_, ref (SOME tAll)) => whnorm tAll
       | _ => tAll
 
+fun baseCondition t =
+    case whnorm t of
+       (TBase name, _) => typeRule name
+      | (TList t, _) =>
+       (case baseCondition t of
+            NONE => NONE
+          | SOME f => SOME (fn (EList ls, _) => List.all f ls
+                             | _ => false))
+      | _ => NONE
+
+fun hasTyp (e, t1, t2) =
+    if (case baseCondition t2 of
+           NONE => false
+         | SOME rule => rule e) then
+       ()
+    else
+       subTyp (t1, t2)
+
 fun checkTyp G (tAll as (t, loc)) =
     let
        val err = ErrorMsg.error (SOME loc)
@@ -327,7 +331,7 @@ fun checkExp G (eAll as (e, loc)) =
                          let
                              val t' = checkExp G e'
                          in
-                             (subTyp (t', t);
+                             (hasTyp (eAll, t', t);
                               if isError t' then
                                   (TList (TError, loc), loc)
                               else
@@ -349,7 +353,7 @@ fun checkExp G (eAll as (e, loc)) =
                        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)
@@ -367,8 +371,8 @@ fun checkExp G (eAll as (e, loc)) =
                val tf = checkExp G func
                val ta = checkExp G arg
            in
-               (subTyp (tf, (TArrow (dom, ran), loc));
-                subTyp (ta, dom)
+               (hasTyp (func, tf, (TArrow (dom, ran), loc));
+                hasTyp (arg, ta, dom)
                 handle Unify ue =>
                        dte (WrongType ("Function argument",
                                        arg,
@@ -397,7 +401,7 @@ fun checkExp G (eAll as (e, 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
@@ -638,7 +642,26 @@ fun checkUnit G (eAll as (_, loc)) =
 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
+           hasTyp (e, 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
@@ -650,7 +673,7 @@ fun checkFile G tInit (ds, eo) =
            let
                val t = checkExp G' e
            in
-               subTyp (t, tInit)
+               hasTyp (e, t, tInit)
                handle Unify ue =>
                       (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
                        preface ("Actual:", p_typ t);