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