src/tycheck.sml

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