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 fun ununify (tAll as (t, _)) =
 262     case t of
 263         TUnif (_, ref (SOME t)) => ununify t
 264       | _ => tAll
 265
 266 fun checkExp G (eAll as (e, loc)) =
 267     let
 268         val dte = Describe.describe_type_error loc
 269     in
 270         case e of
 271             EInt _ => (TBase "int", loc)
 272           | EString _ => (TBase "string", loc)
 273           | EList es =>
 274             let
 275                 val t = (newUnif (), loc)
 276             in
 277                 foldl (fn (e', ret) =>
 278                           let
 279                               val t' = checkExp G e'
 280                           in
 281                               (hasTyp (eAll, t', t);
 282                                if isError t' then
 283                                    (TList (TError, loc), loc)
 284                                else
 285                                    ret)
 286                               handle Unify ue =>
 287                                      (dte (WrongType ("List element",
 288                                                       e',
 289                                                       t',
 290                                                       t,
 291                                                       SOME ue));
 292                                       (TError, loc))
 293                           end) (TList t, loc) es
 294             end
 295
 296           | ELam (x, to, e) =>
 297             let
 298                 val t =
 299                     case to of
 300                         NONE => (newUnif (), loc)
 301                       | SOME t => checkTyp G t
 302
 303                 val G' = bindVal G (x, t, NONE)
 304                 val t' = checkExp G' e
 305             in
 306                 (TArrow (t, t'), loc)
 307             end
 308           | EVar x =>
 309             (case lookupVal G x of
 310                  NONE => (dte (UnboundVariable x);
 311                           (TError, loc))
 312                | SOME t => t)
 313           | EApp (func, arg) =>
 314             let
 315                 val dom = (newUnif (), loc)
 316                 val ran = (newUnif (), loc)
 317
 318                 val tf = checkExp G func
 319                 val ta = checkExp G arg
 320             in
 321                 (hasTyp (func, tf, (TArrow (dom, ran), loc));
 322                  hasTyp (arg, ta, dom)
 323                  handle Unify ue =>
 324                         dte (WrongType ("Function argument",
 325                                         arg,
 326                                         ta,
 327                                         dom,
 328                                         SOME ue));
 329                  ran)
 330                 handle Unify ue =>
 331                        (dte (WrongForm ("Function to be applied",
 332                                         "function",
 333                                         func,
 334                                         tf,
 335                                         SOME ue));
 336                         (TError, loc))
 337             end
 338
 339           | EALam (x, p, e) =>
 340             let
 341                 val p' = checkPred G p
 342
 343                 val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
 344                 val t' = whnorm (checkExp G' e)
 345             in
 346                 case t' of
 347                     (TAction _, _) => (TNested (p, t'), loc)
 348                   | _ => (dte (WrongForm ("Body of nested configuration 'fn'",
 349                                           "action",
 350                                           e,
 351                                           t',
 352                                           NONE));
 353                           (TError, loc))
 354             end
 355
 356           | ESet (evar, e) =>
 357             let
 358                 val t = checkExp G e
 359             in
 360                 (TAction ((CPrefix (CRoot, loc), loc),
 361                           SM.empty,
 362                           SM.insert (SM.empty, evar, t)),
 363                  loc)
 364             end
 365           | EGet (x, topt, evar, rest) =>
 366             let
 367                 val xt = (newUnif (), loc)
 368                 val G' = bindVal G (x, xt, NONE)
 369
 370                 val rt = whnorm (checkExp G' rest)
 371             in
 372                 case topt of
 373                     NONE => ()
 374                   | SOME t => subTyp (xt, checkTyp G t);
 375
 376                 case ununify rt of
 377                     (TAction (p, d, r), _) =>
 378                     (case SM.find (d, evar) of
 379                          NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
 380                        | SOME xt' =>
 381                          (subTyp (xt', xt)
 382                                 handle Unify ue =>
 383                                        dte (WrongType ("Retrieved environment variable",
 384                                                        (EVar x, loc),
 385                                                        xt',
 386                                                        xt,
 387                                                        SOME ue));
 388                           rt))
 389                   | (TError, _) => rt
 390                   | _ => (dte (WrongForm ("Body of environment variable read",
 391                                           "action",
 392                                           rest,
 393                                           rt,
 394                                           NONE));
 395                           (TError, loc))
 396             end
 397
 398           | ESeq [] => raise Fail "Empty ESeq"
 399           | ESeq [e1] => checkExp G e1
 400           | ESeq (e1 :: rest) =>
 401             let
 402                 val e2 = (ESeq rest, loc)
 403
 404                 val t1 = whnorm (checkExp G e1)
 405                 val t2 = whnorm (checkExp G e2)
 406             in
 407                 case t1 of
 408                     (TAction (p1, d1, r1), _) =>
 409                     (case t2 of
 410                          (TAction (p2, d2, r2), _) =>
 411                          let
 412                              val p' = predSimpl (CAnd (p1, p2), loc)
 413
 414                              val d' = SM.foldli (fn (name, t, d') =>
 415                                                     case SM.find (r1, name) of
 416                                                         NONE =>
 417                                                         (case SM.find (d', name) of
 418                                                              NONE => SM.insert (d', name, t)
 419                                                            | SOME t' =>
 420                                                              ((case envVarSetFrom name e1 of
 421                                                                    NONE => subTyp (t, t')
 422                                                                  | SOME e => hasTyp (e, t, t'))
 423                                                               handle Unify ue =>
 424                                                                      dte (WrongType ("Shared environment variable",
 425                                                                                      (EVar name, loc),
 426                                                                                      t',
 427                                                                                      t,
 428                                                                                      SOME ue));
 429                                                               d'))
 430                                                       | SOME t' =>
 431                                                         ((case envVarSetFrom name e1 of
 432                                                                    NONE => subTyp (t, t')
 433                                                                  | SOME e => hasTyp (e, t, t'))
 434                                                          handle Unify ue =>
 435                                                                 dte (WrongType ("Shared environment variable",
 436                                                                                 (EVar name, loc),
 437                                                                                 t',
 438                                                                                 t,
 439                                                                                 SOME ue));
 440                                                          d'))
 441                                                 d1 d2
 442
 443                              val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
 444                                                 r1 r2
 445                          in
 446                              (TAction (p', d', r'), loc)
 447                          end
 448                        | (TError, _) => t2
 449                        | _ => (dte (WrongForm ("Action to be sequenced",
 450                                                "action",
 451                                                e2,
 452                                                t2,
 453                                                NONE));
 454                                (TError, loc)))
 455                   | (TError, _) => t1
 456                   | _ => (dte (WrongForm ("Action to be sequenced",
 457                                           "action",
 458                                           e1,
 459                                           t1,
 460                                           NONE));
 461                           (TError, loc))
 462             end
 463
 464           | ELocal (e1, e2) =>
 465             let
 466                 val t1 = whnorm (checkExp G e1)
 467                 val t2 = whnorm (checkExp G e2)
 468             in
 469                 case t1 of
 470                     (TAction (p1, d1, r1), _) =>
 471                     (case t2 of
 472                          (TAction (p2, d2, r2), _) =>
 473                          let
 474                              val p' = predSimpl (CAnd (p1, p2), loc)
 475
 476                              val d' = SM.foldli (fn (name, t, d') =>
 477                                                     case SM.find (r1, name) of
 478                                                         NONE =>
 479                                                         (case SM.find (d', name) of
 480                                                              NONE => SM.insert (d', name, t)
 481                                                            | SOME t' =>
 482                                                              ((case envVarSetFrom name e1 of
 483                                                                    NONE => subTyp (t', t)
 484                                                                  | SOME e => hasTyp (e, t', t))
 485                                                               handle Unify ue =>
 486                                                                      dte (WrongType ("Shared environment variable",
 487                                                                                      (EVar name, loc),
 488                                                                                      t',
 489                                                                                      t,
 490                                                                                      SOME ue));
 491                                                               d'))
 492                                                       | SOME t' =>
 493                                                         ((case envVarSetFrom name e1 of
 494                                                                    NONE => subTyp (t', t)
 495                                                                  | SOME e => hasTyp (e, t', t))
 496                                                          handle Unify ue =>
 497                                                                 dte (WrongType ("Shared environment variable",
 498                                                                                 (EVar name, loc),
 499                                                                                 t',
 500                                                                                 t,
 501                                                                                 SOME ue));
 502                                                          d'))
 503                                                 d1 d2
 504                          in
 505                              (TAction (p', d', r2), loc)
 506                          end
 507                        | (TError, _) => t2
 508                        | _ => (dte (WrongForm ("Action to be sequenced",
 509                                                "action",
 510                                                e2,
 511                                                t2,
 512                                                NONE));
 513                                (TError, loc)))
 514                   | (TError, _) => t1
 515                   | _ => (dte (WrongForm ("Action to be sequenced",
 516                                           "action",
 517                                           e1,
 518                                           t1,
 519                                           NONE));
 520                           (TError, loc))
 521             end
 522
 523
 524           | EWith (e1, e2) =>
 525             let
 526                 val t1 = whnorm (checkExp G e1)
 527                 val t2 = whnorm (checkExp G e2)
 528             in
 529                 case t1 of
 530                     (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
 531                     (case t2 of
 532                          (TAction (p, d, r), _) =>
 533                          if predImplies (pd, p) then
 534                              let
 535                                  val combineRecs =
 536                                      SM.unionWithi (fn (name, t1, t2) =>
 537                                                        (subTyp (t1, t2)
 538                                                         handle Unify ue =>
 539                                                                dte (WrongType ("Environment variable",
 540                                                                                (EVar name, loc),
 541                                                                                t1,
 542                                                                                t2,
 543                                                                                SOME ue));
 544                                                         t2))
 545                              in
 546                                  (TAction (pr, combineRecs (d, d1),
 547                                            combineRecs (r, r1)), loc)
 548                              end
 549                          else
 550                              (dte (WrongPred ("nested action",
 551                                               pd,
 552                                               p));
 553                               (TError, loc))
 554                        | (TError, _) => t2
 555                        | _ =>
 556                          (dte (WrongForm ("Body of nested action",
 557                                           "action",
 558                                           e2,
 559                                           t2,
 560                                           NONE));
 561                           (TError, loc)))
 562                   | (TError, _) => t1
 563                   | _ =>
 564                     (dte (WrongForm ("Container of nested action",
 565                                      "action",
 566                                      e1,
 567                                      t1,
 568                                      NONE));
 569                      (TError, loc))
 570             end
 571
 572           | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
 573                                SM.empty, SM.empty), loc)
 574     end
 575
 576 exception Ununif
 577
 578 fun ununif (tAll as (t, loc)) =
 579     case t of
 580         TBase _ => tAll
 581       | TList t => (TList (ununif t), loc)
 582       | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
 583       | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
 584       | TUnif (_, ref (SOME t)) => ununif t
 585       | TNested _ => tAll
 586       | TError => tAll
 587
 588       | TUnif (_, ref NONE) => raise Ununif
 589
 590 fun hasError (t, _) =
 591     case t of
 592         TBase _ => false
 593       | TList t => hasError t
 594       | TArrow (d, r) => hasError d orelse hasError r
 595       | TAction (p, d, r) => List.exists hasError (SM.listItems d)
 596                              orelse List.exists hasError (SM.listItems r)
 597       | TNested _ => false
 598       | TError => false
 599       | TUnif (_, ref (SOME t)) => hasError t
 600       | TUnif (_, ref NONE) => false
 601
 602
 603 fun checkUnit G (eAll as (_, loc)) =
 604     let
 605         val _ = resetUnif ()
 606         val t = checkExp G eAll
 607     in
 608         if hasError t then
 609             t
 610         else
 611             ununif t
 612             handle Ununif =>
 613                    (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
 614                     output (p_typ t);
 615                     t)
 616     end
 617
 618 fun checkDecl G (d, _, loc) =
 619     case d of
 620         DExternType name =>
 621         if !externFlag then
 622             bindType G name
 623         else
 624             (ErrorMsg.error (SOME loc) "'extern type' not allowed in untrusted code";
 625              G)
 626       | DExternVal (name, t) =>
 627         if !externFlag then
 628             bindVal G (name, checkTyp G t, NONE)
 629         else
 630             (ErrorMsg.error (SOME loc) "'extern val' not allowed in untrusted code";
 631              G)
 632       | DVal (name, to, e) =>
 633         let
 634             val to =
 635                 case to of
 636                     NONE => (newUnif (), loc)
 637                   | SOME to => checkTyp G to
 638
 639             val t = checkExp G e
 640         in
 641             hasTyp (e, t, to)
 642             handle Unify ue =>
 643                    Describe.describe_type_error loc
 644                                                 (WrongType ("Bound value",
 645                                                             e,
 646                                                             t,
 647                                                             to,
 648                                                             SOME ue));
 649             bindVal G (name, to, SOME e)
 650         end
 651       | DContext name => bindContext G name
 652
 653 fun checkFile G tInit (_, ds, eo) =
 654     let
 655         val G' = foldl (fn (d, G) => checkDecl G d) G ds
 656     in
 657         case eo of
 658             NONE => ()
 659           | SOME (e as (_, loc)) =>
 660             let
 661                 val t = checkExp G' e
 662             in
 663                 hasTyp (e, t, tInit)
 664                 handle Unify ue =>
 665                        (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
 666                         preface ("Actual:", p_typ t);
 667                         preface ("Needed:", p_typ tInit))
 668             end;
 669         G'
 670     end
 671
 672 end