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           | ESet (evar, e) =>
 430             let
 431                 val t = checkExp G e
 432             in
 433                 (TAction ((CPrefix (CRoot, loc), loc),
 434                           SM.empty,
 435                           SM.insert (SM.empty, evar, t)),
 436                  loc)
 437             end
 438           | EGet (x, evar, rest) =>
 439             let
 440                 val xt = (newUnif (), loc)
 441                 val G' = bindVal G (x, xt, NONE)
 442
 443                 val rt = whnorm (checkExp G' rest)
 444             in
 445                 case rt of
 446                     (TAction (p, d, r), _) =>
 447                     (case SM.find (d, evar) of
 448                          NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
 449                        | SOME xt' =>
 450                          (subTyp (xt', xt)
 451                                 handle Unify ue =>
 452                                        dte (WrongType ("Retrieved environment variable",
 453                                                        (EVar x, loc),
 454                                                        xt',
 455                                                        xt,
 456                                                        SOME ue));
 457                           rt))
 458                   | (TError, _) => rt
 459                   | _ => (dte (WrongForm ("Body of environment variable read",
 460                                           "action",
 461                                           rest,
 462                                           rt,
 463                                           NONE));
 464                           (TError, loc))
 465             end
 466
 467           | ESeq [] => raise Fail "Empty ESeq"
 468           | ESeq [e1] => checkExp G e1
 469           | ESeq (e1 :: rest) =>
 470             let
 471                 val e2 = (ESeq rest, loc)
 472
 473                 val t1 = whnorm (checkExp G e1)
 474                 val t2 = whnorm (checkExp G e2)
 475             in
 476                 case t1 of
 477                     (TAction (p1, d1, r1), _) =>
 478                     (case t2 of
 479                          (TAction (p2, d2, r2), _) =>
 480                          let
 481                              val p' = predSimpl (CAnd (p1, p2), loc)
 482
 483                              val d' = SM.foldli (fn (name, t, d') =>
 484                                                     case SM.find (r1, name) of
 485                                                         NONE =>
 486                                                         (case SM.find (d', name) of
 487                                                              NONE => SM.insert (d', name, t)
 488                                                            | SOME t' =>
 489                                                              ((case envVarSetFrom name e1 of
 490                                                                    NONE => subTyp (t, t')
 491                                                                  | SOME e => hasTyp (e, t, t'))
 492                                                               handle Unify ue =>
 493                                                                      dte (WrongType ("Shared environment variable",
 494                                                                                      (EVar name, loc),
 495                                                                                      t',
 496                                                                                      t,
 497                                                                                      SOME ue));
 498                                                               d'))
 499                                                       | SOME t' =>
 500                                                         ((case envVarSetFrom name e1 of
 501                                                                    NONE => subTyp (t, t')
 502                                                                  | SOME e => hasTyp (e, t, t'))
 503                                                          handle Unify ue =>
 504                                                                 dte (WrongType ("Shared environment variable",
 505                                                                                 (EVar name, loc),
 506                                                                                 t',
 507                                                                                 t,
 508                                                                                 SOME ue));
 509                                                          d'))
 510                                                 d1 d2
 511
 512                              val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
 513                                                 r1 r2
 514                          in
 515                              (TAction (p', d', r'), loc)
 516                          end
 517                        | (TError, _) => t2
 518                        | _ => (dte (WrongForm ("Action to be sequenced",
 519                                                "action",
 520                                                e2,
 521                                                t2,
 522                                                NONE));
 523                                (TError, loc)))
 524                   | (TError, _) => t1
 525                   | _ => (dte (WrongForm ("Action to be sequenced",
 526                                           "action",
 527                                           e1,
 528                                           t1,
 529                                           NONE));
 530                           (TError, loc))
 531             end
 532
 533           | ELocal (e1, e2) =>
 534             let
 535                 val t1 = whnorm (checkExp G e1)
 536                 val t2 = whnorm (checkExp G e2)
 537             in
 538                 case t1 of
 539                     (TAction (p1, d1, r1), _) =>
 540                     (case t2 of
 541                          (TAction (p2, d2, r2), _) =>
 542                          let
 543                              val p' = predSimpl (CAnd (p1, p2), loc)
 544
 545                              val d' = SM.foldli (fn (name, t, d') =>
 546                                                     case SM.find (r1, name) of
 547                                                         NONE =>
 548                                                         (case SM.find (d', name) of
 549                                                              NONE => SM.insert (d', name, t)
 550                                                            | SOME t' =>
 551                                                              ((case envVarSetFrom name e1 of
 552                                                                    NONE => subTyp (t', t)
 553                                                                  | SOME e => hasTyp (e, t', t))
 554                                                               handle Unify ue =>
 555                                                                      dte (WrongType ("Shared environment variable",
 556                                                                                      (EVar name, loc),
 557                                                                                      t',
 558                                                                                      t,
 559                                                                                      SOME ue));
 560                                                               d'))
 561                                                       | SOME t' =>
 562                                                         ((case envVarSetFrom name e1 of
 563                                                                    NONE => subTyp (t', t)
 564                                                                  | SOME e => hasTyp (e, t', t))
 565                                                          handle Unify ue =>
 566                                                                 dte (WrongType ("Shared environment variable",
 567                                                                                 (EVar name, loc),
 568                                                                                 t',
 569                                                                                 t,
 570                                                                                 SOME ue));
 571                                                          d'))
 572                                                 d1 d2
 573                          in
 574                              (TAction (p', d', r2), loc)
 575                          end
 576                        | (TError, _) => t2
 577                        | _ => (dte (WrongForm ("Action to be sequenced",
 578                                                "action",
 579                                                e2,
 580                                                t2,
 581                                                NONE));
 582                                (TError, loc)))
 583                   | (TError, _) => t1
 584                   | _ => (dte (WrongForm ("Action to be sequenced",
 585                                           "action",
 586                                           e1,
 587                                           t1,
 588                                           NONE));
 589                           (TError, loc))
 590             end
 591
 592
 593           | EWith (e1, e2) =>
 594             let
 595                 val t1 = whnorm (checkExp G e1)
 596                 val t2 = whnorm (checkExp G e2)
 597             in
 598                 case t1 of
 599                     (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
 600                     (case t2 of
 601                          (TAction (p, d, r), _) =>
 602                          if predImplies (pd, p) then
 603                              let
 604                                  val combineRecs =
 605                                      SM.unionWithi (fn (name, t1, t2) =>
 606                                                        (subTyp (t1, t2)
 607                                                         handle Unify ue =>
 608                                                                dte (WrongType ("Environment variable",
 609                                                                                (EVar name, loc),
 610                                                                                t1,
 611                                                                                t2,
 612                                                                                SOME ue));
 613                                                         t2))
 614                              in
 615                                  (TAction (pr, combineRecs (d, d1),
 616                                            combineRecs (r, r1)), loc)
 617                              end
 618                          else
 619                              (dte (WrongPred ("nested action",
 620                                               pd,
 621                                               p));
 622                               (TError, loc))
 623                        | (TError, _) => t2
 624                        | _ =>
 625                          (dte (WrongForm ("Body of nested action",
 626                                           "action",
 627                                           e2,
 628                                           t2,
 629                                           NONE));
 630                           (TError, loc)))
 631                   | (TError, _) => t1
 632                   | _ =>
 633                     (dte (WrongForm ("Container of nested action",
 634                                      "action",
 635                                      e1,
 636                                      t1,
 637                                      NONE));
 638                      (TError, loc))
 639             end
 640
 641           | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
 642                                SM.empty, SM.empty), loc)
 643     end
 644
 645 exception Ununif
 646
 647 fun ununif (tAll as (t, loc)) =
 648     case t of
 649         TBase _ => tAll
 650       | TList t => (TList (ununif t), loc)
 651       | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
 652       | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
 653       | TUnif (_, ref (SOME t)) => ununif t
 654       | TNested _ => tAll
 655       | TError => tAll
 656
 657       | TUnif (_, ref NONE) => raise Ununif
 658
 659 fun hasError (t, _) =
 660     case t of
 661         TBase _ => false
 662       | TList t => hasError t
 663       | TArrow (d, r) => hasError d orelse hasError r
 664       | TAction (p, d, r) => List.exists hasError (SM.listItems d)
 665                              orelse List.exists hasError (SM.listItems r)
 666       | TNested _ => false
 667       | TError => false
 668       | TUnif (_, ref (SOME t)) => hasError t
 669       | TUnif (_, ref NONE) => false
 670
 671
 672 fun checkUnit G (eAll as (_, loc)) =
 673     let
 674         val _ = resetUnif ()
 675         val t = checkExp G eAll
 676     in
 677         if hasError t then
 678             t
 679         else
 680             ununif t
 681             handle Ununif =>
 682                    (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
 683                     printd (p_typ t);
 684                     t)
 685     end
 686
 687 fun checkDecl G (d, _, loc) =
 688     case d of
 689         DExternType name => bindType G name
 690       | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
 691       | DVal (name, to, e) =>
 692         let
 693             val to =
 694                 case to of
 695                     NONE => (newUnif (), loc)
 696                   | SOME to => checkTyp G to
 697
 698             val t = checkExp G e
 699         in
 700             hasTyp (e, t, to)
 701             handle Unify ue =>
 702                    describe_type_error loc
 703                                        (WrongType ("Bound value",
 704                                                    e,
 705                                                    t,
 706                                                    to,
 707                                                    SOME ue));
 708             bindVal G (name, to, SOME e)
 709         end
 710       | DContext name => bindContext G name
 711
 712 fun checkFile G tInit (_, ds, eo) =
 713     let
 714         val G' = foldl (fn (d, G) => checkDecl G d) G ds
 715     in
 716         case eo of
 717             NONE => ()
 718           | SOME (e as (_, loc)) =>
 719             let
 720                 val t = checkExp G' e
 721             in
 722                 hasTyp (e, t, tInit)
 723                 handle Unify ue =>
 724                        (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
 725                         preface ("Actual:", p_typ t);
 726                         preface ("Needed:", p_typ tInit))
 727             end;
 728         G'
 729     end
 730
 731 end