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