src/tycheck.sml

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