src/tycheck.sml

   1 (* HCoop Domtool (http://hcoop.sourceforge.net/)
   2  * Copyright (c) 2006, Adam Chlipala
   3  *
   4  * This program is free software; you can redistribute it and/or
   5  * modify it under the terms of the GNU General Public License
   6  * as published by the Free Software Foundation; either version 2
   7  * of the License, or (at your option) any later version.
   8  *
   9  * This program is distributed in the hope that it will be useful,
  10  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  11  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  12  * GNU General Public License for more details.
  13  *
  14  * You should have received a copy of the GNU General Public License
  15  * along with this program; if not, write to the Free Software
  16  * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
  17  *)
  18
  19 (* Domtool configuration language type checking *)
  20
  21 structure Tycheck :> TYCHECK = struct
  22
  23 open Ast Print Env
  24
  25 structure SM = StringMap
  26
  27 local
  28     val unifCount = ref 0
  29 in
  30 fun resetUnif () = unifCount := 0
  31
  32 fun newUnif () =
  33     let
  34         val c = !unifCount
  35         val name =
  36             if c < 26 then
  37                 str (chr (ord #"A" + c))
  38             else
  39                 "UNIF" ^ Int.toString (c - 26)
  40     in
  41         unifCount := c + 1;
  42         TUnif (name, ref NONE)
  43     end
  44 end
  45
  46 exception UnequalDomains
  47
  48 fun eqRecord f (r1, r2) =
  49     (SM.appi (fn (k, v1) =>
  50                  case SM.find (r2, k) of
  51                      NONE => raise UnequalDomains
  52                    | SOME v2 =>
  53                      if f (v1, v2) then
  54                          ()
  55                      else
  56                          raise UnequalDomains) r1;
  57      SM.appi (fn (k, v2) =>
  58                  case SM.find (r1, k) of
  59                      NONE => raise UnequalDomains
  60                    | SOME v1 =>
  61                      if f (v1, v2) then
  62                          ()
  63                      else
  64                          raise UnequalDomains) r2;
  65      true)
  66     handle UnequalDomains => false
  67
  68 fun eqPred ((p1, _), (p2, _)) =
  69     case (p1, p2) of
  70         (CRoot, CRoot) => true
  71       | (CConst s1, CConst s2) => s1 = s2
  72       | (CPrefix p1, CPrefix p2) => eqPred (p1, p2)
  73       | (CNot p1, CNot p2) => eqPred (p1, p2)
  74       | (CAnd (p1, q1), CAnd (p2, q2)) =>
  75         eqPred (p1, p2) andalso eqPred (q1, q2)
  76
  77       | _ => false
  78
  79 fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
  80     case (t1, t2) of
  81         (TBase s1, TBase s2) => s1 = s2
  82       | (TList t1, TList t2) => eqTy (t1, t2)
  83       | (TArrow (d1, r1), TArrow (d2, r2)) =>
  84         eqTy (d1, d2) andalso eqTy (r1, r2)
  85
  86       | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
  87         eqPred (p1, p2) andalso eqRecord eqTy (d1, d2)
  88         andalso eqRecord eqTy (r1, r2)
  89
  90       | (TNested (p1, q1), TNested (p2, q2)) =>
  91         eqPred (p1, p2) andalso eqTy (q1, q2)
  92
  93       | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
  94       | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)
  95
  96       | (TUnif (_, r1), TUnif (_, r2)) => r1 = r2
  97
  98       | (TError, TError) => true
  99
 100       | _ => false
 101
 102 datatype unification_error =
 103          UnifyPred of pred * pred
 104        | UnifyTyp of typ * typ
 105        | UnifyOccurs of string * typ
 106
 107 exception Unify of unification_error
 108
 109 datatype type_error =
 110          WrongType of string * exp * typ * typ * unification_error option
 111        | WrongForm of string * string * exp * typ * unification_error option
 112        | UnboundVariable of string
 113        | WrongPred of string * pred * pred
 114
 115 fun describe_unification_error t ue =
 116     case ue of
 117         UnifyPred (p1, p2) =>
 118         (print "Reason: Incompatible contexts.\n";
 119          preface ("Have:", p_pred p1);
 120          preface ("Need:", p_pred p2))
 121       | UnifyTyp (t1, t2) =>
 122         if eqTy (t, t1) then
 123             ()
 124         else
 125             (print "Reason: Incompatible types.\n";
 126              preface ("Have:", p_typ t1);
 127              preface ("Need:", p_typ t2))
 128       | UnifyOccurs (name, t') =>
 129         if eqTy (t, t') then
 130             ()
 131         else
 132             (print "Reason: Occurs check failed for ";
 133              print name;
 134              print " in:\n";
 135              printd (p_typ t))
 136
 137 fun describe_type_error loc te =
 138     case te of
 139         WrongType (place, e, t1, t2, ueo) =>
 140         (ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
 141          preface (" Expression:", p_exp e);
 142          preface ("Actual type:", p_typ t1);
 143          preface ("Needed type:", p_typ t2);
 144          Option.app (describe_unification_error t1) ueo)
 145       | WrongForm (place, form, e, t, ueo) =>
 146         (ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
 147          preface ("Expression:", p_exp e);
 148          preface ("      Type:", p_typ t);
 149          Option.app (describe_unification_error t) ueo)
 150       | UnboundVariable name =>
 151         ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
 152       | WrongPred (place, p1, p2) =>
 153         (ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
 154          preface ("Have:", p_pred p1);
 155          preface ("Need:", p_pred p2))
 156
 157 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
 158     case (p1, p2) of
 159         (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
 160       | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
 161
 162       | (_, CPrefix (CRoot, _)) => true
 163       | (CNot (CPrefix (CRoot, _), _), _) => true
 164
 165       | (CRoot, CRoot) => true
 166
 167       | (CConst s1, CConst s2) => s1 = s2
 168
 169       | (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
 170       | (_, CPrefix p2) => predImplies (p1All, p2)
 171
 172       | (CNot p1, CNot p2) => predImplies (p2, p1)
 173       | (CRoot, CNot (CConst _, _)) => true
 174       | (CConst s1, CNot (CConst s2, _)) => s1 <> s2
 175
 176       | _ => false
 177
 178 fun predSimpl (pAll as (p, loc)) =
 179     case p of
 180         CRoot => pAll
 181       | CConst _ => pAll
 182       | CPrefix p => (CPrefix (predSimpl p), loc)
 183       | CNot p => (CNot (predSimpl p), loc)
 184       | CAnd (p1, p2) =>
 185         let
 186             val p1' = predSimpl p1
 187             val p2' = predSimpl p2
 188         in
 189             case p1' of
 190                 (CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
 191               | _ => if predImplies (p2', p1') then
 192                          p2'
 193                      else if predImplies (p1', p2') then
 194                          p1'
 195                      else
 196                          (CAnd (p1', p2'), loc)
 197         end
 198
 199 fun subPred (p1, p2) =
 200     if predImplies (p1, p2) then
 201         ()
 202     else
 203         raise (Unify (UnifyPred (p1, p2)))
 204
 205 fun subRecord f (r1, r2) =
 206     SM.appi (fn (k, v2) =>
 207                 case SM.find (r1, k) of
 208                     NONE => raise UnequalDomains
 209                   | SOME v1 => f (v1, v2)) r2
 210
 211 fun occurs u (t, _) =
 212     case t of
 213         TBase _ => false
 214       | TList t => occurs u t
 215       | TArrow (d, r) => occurs u d orelse occurs u r
 216       | TAction (_, d, r) =>
 217         List.exists (occurs u) (SM.listItems d)
 218         orelse List.exists (occurs u) (SM.listItems r)
 219       | TNested (_, t) => occurs u t
 220       | TError => false
 221       | TUnif (_, ref (SOME t)) => occurs u t
 222       | TUnif (_, u') => u = u'
 223
 224 fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
 225     case (t1, t2) of
 226         (TBase s1, TBase s2) =>
 227         if s1 = s2 then
 228             ()
 229         else
 230             raise Unify (UnifyTyp (t1All, t2All))
 231       | (TList t1, TList t2) => subTyp (t1, t2)
 232       | (TArrow (d1, r1), TArrow (d2, r2)) =>
 233         (subTyp (d2, d1);
 234          subTyp (r1, r2))
 235
 236       | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
 237         ((subPred (p2, p1);
 238           subRecord subTyp (d2, d1);
 239           subRecord subTyp (r1, r2);
 240           subRecord subTyp (r2, r1))
 241          handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
 242
 243       | (TNested (d1, r1), TNested (d2, r2)) =>
 244         (subPred (d2, d1);
 245          subTyp (r1, r2))
 246
 247       | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
 248       | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
 249
 250       | (TUnif (_, r1), TUnif (_, r2)) =>
 251         if r1 = r2 then
 252             ()
 253         else
 254             r1 := SOME t2All
 255
 256       | (TUnif (name, r), _) =>
 257         if occurs r t2All then
 258             raise (Unify (UnifyOccurs (name, t2All)))
 259         else
 260             r := SOME t2All
 261
 262       | (_, TUnif (name, r)) =>
 263         if occurs r t1All then
 264             raise (Unify (UnifyOccurs (name, t1All)))
 265         else
 266             r := SOME t1All
 267
 268       | (TError, _) => ()
 269       | (_, TError) => ()
 270
 271       | _ => raise Unify (UnifyTyp (t1All, t2All))
 272
 273 fun isError t =
 274     case t of
 275         (TError, _) => true
 276       | _ => false
 277
 278 fun whnorm (tAll as (t, loc)) =
 279     case t of
 280         TUnif (_, ref (SOME tAll)) => whnorm tAll
 281       | _ => tAll
 282
 283 fun baseCondition t =
 284     case whnorm t of
 285         (TBase name, _) => typeRule name
 286       | (TList t, _) =>
 287         (case baseCondition t of
 288              NONE => NONE
 289            | SOME f => SOME (fn (EList ls, _) => List.all f ls
 290                               | _ => false))
 291       | _ => NONE
 292
 293 fun hasTyp (e, t1, t2) =
 294     if (case baseCondition t2 of
 295             NONE => false
 296           | SOME rule => rule e) then
 297         ()
 298     else
 299         subTyp (t1, t2)
 300
 301 fun checkPred G (p, loc) =
 302     let
 303         val err = ErrorMsg.error (SOME loc)
 304     in
 305         case p of
 306             CRoot => ()
 307           | CConst s =>
 308             if lookupContext G s then
 309                 ()
 310             else
 311                 err ("Unbound context " ^ s)
 312           | CPrefix p => checkPred G p
 313           | CNot p => checkPred G p
 314           | CAnd (p1, p2) => (checkPred G p1; checkPred G p2)
 315     end
 316
 317 fun checkTyp G (tAll as (t, loc)) =
 318     let
 319         val err = ErrorMsg.error (SOME loc)
 320     in
 321         case t of
 322             TBase name =>
 323             if lookupType G name then
 324                 tAll
 325             else
 326                 (err ("Unbound type name " ^ name);
 327                  (TError, loc))
 328           | TList t => (TList (checkTyp G t), loc)
 329           | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
 330           | TAction (p, d, r) => (checkPred G p;
 331                                   (TAction (p, SM.map (checkTyp G) d,
 332                                             SM.map (checkTyp G) r), loc))
 333           | TNested (p, t) => (checkPred G p;
 334                                (TNested (p, checkTyp G t), loc))
 335           | TError => raise Fail "TError in parser-generated type"
 336           | TUnif _ => raise Fail "TUnif in parser-generated type"
 337     end
 338
 339 fun envVarSetFrom v (e, _) =
 340     case e of
 341         ESet (v', e) =>
 342         if v = v' then
 343             SOME e
 344         else
 345             NONE
 346       | EGet (_, _, e) => envVarSetFrom v e
 347       | ESeq es => foldr (fn (e, found) =>
 348                              case found of
 349                                  SOME _ => found
 350                                | NONE => envVarSetFrom v e)
 351                          NONE es
 352       | ELocal (_, e) => envVarSetFrom v e
 353
 354       | _ => NONE
 355
 356 fun checkExp G (eAll as (e, loc)) =
 357     let
 358         val dte = describe_type_error loc
 359     in
 360         case e of
 361             EInt _ => (TBase "int", loc)
 362           | EString _ => (TBase "string", loc)
 363           | EList es =>
 364             let
 365                 val t = (newUnif (), loc)
 366             in
 367                 foldl (fn (e', ret) =>
 368                           let
 369                               val t' = checkExp G e'
 370                           in
 371                               (hasTyp (eAll, t', t);
 372                                if isError t' then
 373                                    (TList (TError, loc), loc)
 374                                else
 375                                    ret)
 376                               handle Unify ue =>
 377                                      (dte (WrongType ("List element",
 378                                                       e',
 379                                                       t',
 380                                                       t,
 381                                                       SOME ue));
 382                                       (TError, loc))
 383                           end) (TList t, loc) es
 384             end
 385
 386           | ELam (x, to, e) =>
 387             let
 388                 val t =
 389                     case to of
 390                         NONE => (newUnif (), loc)
 391                       | SOME t => checkTyp G t
 392
 393                 val G' = bindVal G (x, t, NONE)
 394                 val t' = checkExp G' e
 395             in
 396                 (TArrow (t, t'), loc)
 397             end
 398           | EVar x =>
 399             (case lookupVal G x of
 400                  NONE => (dte (UnboundVariable x);
 401                           (TError, loc))
 402                | SOME t => t)
 403           | EApp (func, arg) =>
 404             let
 405                 val dom = (newUnif (), loc)
 406                 val ran = (newUnif (), loc)
 407
 408                 val tf = checkExp G func
 409                 val ta = checkExp G arg
 410             in
 411                 (hasTyp (func, tf, (TArrow (dom, ran), loc));
 412                  hasTyp (arg, ta, dom)
 413                  handle Unify ue =>
 414                         dte (WrongType ("Function argument",
 415                                         arg,
 416                                         ta,
 417                                         dom,
 418                                         SOME ue));
 419                  ran)
 420                 handle Unify ue =>
 421                        (dte (WrongForm ("Function to be applied",
 422                                         "function",
 423                                         func,
 424                                         tf,
 425                                         SOME ue));
 426                         (TError, loc))
 427             end
 428
 429           | EALam (x, p, e) =>
 430             let
 431                 val p' = checkPred G p
 432
 433                 val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
 434                 val t' = checkExp G' e
 435             in
 436                 case t' of
 437                     (TAction _, _) => (TNested (p, t'), loc)
 438                   | _ => (dte (WrongForm ("Body of nested configuration 'fn'",
 439                                           "action",
 440                                           e,
 441                                           t',
 442                                           NONE));
 443                           (TError, loc))
 444             end
 445
 446           | ESet (evar, e) =>
 447             let
 448                 val t = checkExp G e
 449             in
 450                 (TAction ((CPrefix (CRoot, loc), loc),
 451                           SM.empty,
 452                           SM.insert (SM.empty, evar, t)),
 453                  loc)
 454             end
 455           | EGet (x, evar, rest) =>
 456             let
 457                 val xt = (newUnif (), loc)
 458                 val G' = bindVal G (x, xt, NONE)
 459
 460                 val rt = whnorm (checkExp G' rest)
 461             in
 462                 case rt of
 463                     (TAction (p, d, r), _) =>
 464                     (case SM.find (d, evar) of
 465                          NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
 466                        | SOME xt' =>
 467                          (subTyp (xt', xt)
 468                                 handle Unify ue =>
 469                                        dte (WrongType ("Retrieved environment variable",
 470                                                        (EVar x, loc),
 471                                                        xt',
 472                                                        xt,
 473                                                        SOME ue));
 474                           rt))
 475                   | (TError, _) => rt
 476                   | _ => (dte (WrongForm ("Body of environment variable read",
 477                                           "action",
 478                                           rest,
 479                                           rt,
 480                                           NONE));
 481                           (TError, loc))
 482             end
 483
 484           | ESeq [] => raise Fail "Empty ESeq"
 485           | ESeq [e1] => checkExp G e1
 486           | ESeq (e1 :: rest) =>
 487             let
 488                 val e2 = (ESeq rest, loc)
 489
 490                 val t1 = whnorm (checkExp G e1)
 491                 val t2 = whnorm (checkExp G e2)
 492             in
 493                 case t1 of
 494                     (TAction (p1, d1, r1), _) =>
 495                     (case t2 of
 496                          (TAction (p2, d2, r2), _) =>
 497                          let
 498                              val p' = predSimpl (CAnd (p1, p2), loc)
 499
 500                              val d' = SM.foldli (fn (name, t, d') =>
 501                                                     case SM.find (r1, name) of
 502                                                         NONE =>
 503                                                         (case SM.find (d', name) of
 504                                                              NONE => SM.insert (d', name, t)
 505                                                            | SOME t' =>
 506                                                              ((case envVarSetFrom name e1 of
 507                                                                    NONE => subTyp (t, t')
 508                                                                  | SOME e => hasTyp (e, t, t'))
 509                                                               handle Unify ue =>
 510                                                                      dte (WrongType ("Shared environment variable",
 511                                                                                      (EVar name, loc),
 512                                                                                      t',
 513                                                                                      t,
 514                                                                                      SOME ue));
 515                                                               d'))
 516                                                       | SOME t' =>
 517                                                         ((case envVarSetFrom name e1 of
 518                                                                    NONE => subTyp (t, t')
 519                                                                  | SOME e => hasTyp (e, t, t'))
 520                                                          handle Unify ue =>
 521                                                                 dte (WrongType ("Shared environment variable",
 522                                                                                 (EVar name, loc),
 523                                                                                 t',
 524                                                                                 t,
 525                                                                                 SOME ue));
 526                                                          d'))
 527                                                 d1 d2
 528
 529                              val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
 530                                                 r1 r2
 531                          in
 532                              (TAction (p', d', r'), loc)
 533                          end
 534                        | (TError, _) => t2
 535                        | _ => (dte (WrongForm ("Action to be sequenced",
 536                                                "action",
 537                                                e2,
 538                                                t2,
 539                                                NONE));
 540                                (TError, loc)))
 541                   | (TError, _) => t1
 542                   | _ => (dte (WrongForm ("Action to be sequenced",
 543                                           "action",
 544                                           e1,
 545                                           t1,
 546                                           NONE));
 547                           (TError, loc))
 548             end
 549
 550           | ELocal (e1, e2) =>
 551             let
 552                 val t1 = whnorm (checkExp G e1)
 553                 val t2 = whnorm (checkExp G e2)
 554             in
 555                 case t1 of
 556                     (TAction (p1, d1, r1), _) =>
 557                     (case t2 of
 558                          (TAction (p2, d2, r2), _) =>
 559                          let
 560                              val p' = predSimpl (CAnd (p1, p2), loc)
 561
 562                              val d' = SM.foldli (fn (name, t, d') =>
 563                                                     case SM.find (r1, name) of
 564                                                         NONE =>
 565                                                         (case SM.find (d', name) of
 566                                                              NONE => SM.insert (d', name, t)
 567                                                            | SOME t' =>
 568                                                              ((case envVarSetFrom name e1 of
 569                                                                    NONE => subTyp (t', t)
 570                                                                  | SOME e => hasTyp (e, t', t))
 571                                                               handle Unify ue =>
 572                                                                      dte (WrongType ("Shared environment variable",
 573                                                                                      (EVar name, loc),
 574                                                                                      t',
 575                                                                                      t,
 576                                                                                      SOME ue));
 577                                                               d'))
 578                                                       | SOME t' =>
 579                                                         ((case envVarSetFrom name e1 of
 580                                                                    NONE => subTyp (t', t)
 581                                                                  | SOME e => hasTyp (e, t', t))
 582                                                          handle Unify ue =>
 583                                                                 dte (WrongType ("Shared environment variable",
 584                                                                                 (EVar name, loc),
 585                                                                                 t',
 586                                                                                 t,
 587                                                                                 SOME ue));
 588                                                          d'))
 589                                                 d1 d2
 590                          in
 591                              (TAction (p', d', r2), loc)
 592                          end
 593                        | (TError, _) => t2
 594                        | _ => (dte (WrongForm ("Action to be sequenced",
 595                                                "action",
 596                                                e2,
 597                                                t2,
 598                                                NONE));
 599                                (TError, loc)))
 600                   | (TError, _) => t1
 601                   | _ => (dte (WrongForm ("Action to be sequenced",
 602                                           "action",
 603                                           e1,
 604                                           t1,
 605                                           NONE));
 606                           (TError, loc))
 607             end
 608
 609
 610           | EWith (e1, e2) =>
 611             let
 612                 val t1 = whnorm (checkExp G e1)
 613                 val t2 = whnorm (checkExp G e2)
 614             in
 615                 case t1 of
 616                     (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
 617                     (case t2 of
 618                          (TAction (p, d, r), _) =>
 619                          if predImplies (pd, p) then
 620                              let
 621                                  val combineRecs =
 622                                      SM.unionWithi (fn (name, t1, t2) =>
 623                                                        (subTyp (t1, t2)
 624                                                         handle Unify ue =>
 625                                                                dte (WrongType ("Environment variable",
 626                                                                                (EVar name, loc),
 627                                                                                t1,
 628                                                                                t2,
 629                                                                                SOME ue));
 630                                                         t2))
 631                              in
 632                                  (TAction (pr, combineRecs (d, d1),
 633                                            combineRecs (r, r1)), loc)
 634                              end
 635                          else
 636                              (dte (WrongPred ("nested action",
 637                                               pd,
 638                                               p));
 639                               (TError, loc))
 640                        | (TError, _) => t2
 641                        | _ =>
 642                          (dte (WrongForm ("Body of nested action",
 643                                           "action",
 644                                           e2,
 645                                           t2,
 646                                           NONE));
 647                           (TError, loc)))
 648                   | (TError, _) => t1
 649                   | _ =>
 650                     (dte (WrongForm ("Container of nested action",
 651                                      "action",
 652                                      e1,
 653                                      t1,
 654                                      NONE));
 655                      (TError, loc))
 656             end
 657
 658           | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
 659                                SM.empty, SM.empty), loc)
 660     end
 661
 662 exception Ununif
 663
 664 fun ununif (tAll as (t, loc)) =
 665     case t of
 666         TBase _ => tAll
 667       | TList t => (TList (ununif t), loc)
 668       | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
 669       | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
 670       | TUnif (_, ref (SOME t)) => ununif t
 671       | TNested _ => tAll
 672       | TError => tAll
 673
 674       | TUnif (_, ref NONE) => raise Ununif
 675
 676 fun hasError (t, _) =
 677     case t of
 678         TBase _ => false
 679       | TList t => hasError t
 680       | TArrow (d, r) => hasError d orelse hasError r
 681       | TAction (p, d, r) => List.exists hasError (SM.listItems d)
 682                              orelse List.exists hasError (SM.listItems r)
 683       | TNested _ => false
 684       | TError => false
 685       | TUnif (_, ref (SOME t)) => hasError t
 686       | TUnif (_, ref NONE) => false
 687
 688
 689 fun checkUnit G (eAll as (_, loc)) =
 690     let
 691         val _ = resetUnif ()
 692         val t = checkExp G eAll
 693     in
 694         if hasError t then
 695             t
 696         else
 697             ununif t
 698             handle Ununif =>
 699                    (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
 700                     printd (p_typ t);
 701                     t)
 702     end
 703
 704 fun checkDecl G (d, _, loc) =
 705     case d of
 706         DExternType name => bindType G name
 707       | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
 708       | DVal (name, to, e) =>
 709         let
 710             val to =
 711                 case to of
 712                     NONE => (newUnif (), loc)
 713                   | SOME to => checkTyp G to
 714
 715             val t = checkExp G e
 716         in
 717             hasTyp (e, t, to)
 718             handle Unify ue =>
 719                    describe_type_error loc
 720                                        (WrongType ("Bound value",
 721                                                    e,
 722                                                    t,
 723                                                    to,
 724                                                    SOME ue));
 725             bindVal G (name, to, SOME e)
 726         end
 727       | DContext name => bindContext G name
 728
 729 fun checkFile G tInit (_, ds, eo) =
 730     let
 731         val G' = foldl (fn (d, G) => checkDecl G d) G ds
 732     in
 733         case eo of
 734             NONE => ()
 735           | SOME (e as (_, loc)) =>
 736             let
 737                 val t = checkExp G' e
 738             in
 739                 hasTyp (e, t, tInit)
 740                 handle Unify ue =>
 741                        (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
 742                         preface ("Actual:", p_typ t);
 743                         preface ("Needed:", p_typ tInit))
 744             end;
 745         G'
 746     end
 747
 748 end