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