src/tycheck.sml

   1 (* HCoop Domtool (http://hcoop.sourceforge.net/)
   2  * Copyright (c) 2006, 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 local
  28     val unifCount = ref 0
  29 in
  30 fun resetUnif () = unifCount := 0
  31
  32 fun newUnif () =
  33     let
  34         val c = !unifCount
  35         val name =
  36             if c < 26 then
  37                 str (chr (ord #"A" + c))
  38             else
  39                 "UNIF" ^ Int.toString (c - 26)
  40     in
  41         unifCount := c + 1;
  42         TUnif (name, ref NONE)
  43     end
  44 end
  45
  46 exception UnequalDomains
  47
  48 fun eqRecord f (r1, r2) =
  49     (SM.appi (fn (k, v1) =>
  50                  case SM.find (r2, k) of
  51                      NONE => raise UnequalDomains
  52                    | SOME v2 =>
  53                      if f (v1, v2) then
  54                          ()
  55                      else
  56                          raise UnequalDomains) r1;
  57      SM.appi (fn (k, v2) =>
  58                  case SM.find (r1, k) of
  59                      NONE => raise UnequalDomains
  60                    | SOME v1 =>
  61                      if f (v1, v2) then
  62                          ()
  63                      else
  64                          raise UnequalDomains) r2;
  65      true)
  66     handle UnequalDomains => false
  67
  68 fun eqPred ((p1, _), (p2, _)) =
  69     case (p1, p2) of
  70         (CRoot, CRoot) => true
  71       | (CConst s1, CConst s2) => s1 = s2
  72       | (CPrefix p1, CPrefix p2) => eqPred (p1, p2)
  73       | (CNot p1, CNot p2) => eqPred (p1, p2)
  74       | (CAnd (p1, q1), CAnd (p2, q2)) =>
  75         eqPred (p1, p2) andalso eqPred (q1, q2)
  76
  77       | _ => false
  78
  79 fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
  80     case (t1, t2) of
  81         (TBase s1, TBase s2) => s1 = s2
  82       | (TList t1, TList t2) => eqTy (t1, t2)
  83       | (TArrow (d1, r1), TArrow (d2, r2)) =>
  84         eqTy (d1, d2) andalso eqTy (r1, r2)
  85
  86       | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
  87         eqPred (p1, p2) andalso eqRecord eqTy (d1, d2)
  88         andalso eqRecord eqTy (r1, r2)
  89
  90       | (TNested (p1, q1), TNested (p2, q2)) =>
  91         eqPred (p1, p2) andalso eqTy (q1, q2)
  92
  93       | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
  94       | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)
  95
  96       | (TUnif (_, r1), TUnif (_, r2)) => r1 = r2
  97
  98       | (TError, TError) => true
  99
 100       | _ => false
 101
 102 datatype unification_error =
 103          UnifyPred of pred * pred
 104        | UnifyTyp of typ * typ
 105        | UnifyOccurs of string * typ
 106
 107 exception Unify of unification_error
 108
 109 datatype type_error =
 110          WrongType of string * exp * typ * typ * unification_error option
 111        | WrongForm of string * string * exp * typ * unification_error option
 112        | UnboundVariable of string
 113        | WrongPred of string * pred * pred
 114
 115 fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
 116                                         [PD.string s, PD.space 1, d]))
 117
 118 fun describe_unification_error t ue =
 119     case ue of
 120         UnifyPred (p1, p2) =>
 121         (print "Reason: Incompatible contexts.\n";
 122          preface ("Have:", p_pred p1);
 123          preface ("Need:", p_pred p2))
 124       | UnifyTyp (t1, t2) =>
 125         if eqTy (t, t1) then
 126             ()
 127         else
 128             (print "Reason: Incompatible types.\n";
 129              preface ("Have:", p_typ t1);
 130              preface ("Need:", p_typ t2))
 131       | UnifyOccurs (name, t') =>
 132         if eqTy (t, t') then
 133             ()
 134         else
 135             (print "Reason: Occurs check failed for ";
 136              print name;
 137              print " in:\n";
 138              printd (p_typ t))
 139
 140 fun describe_type_error loc te =
 141     case te of
 142         WrongType (place, e, t1, t2, ueo) =>
 143         (ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
 144          preface (" Expression:", p_exp e);
 145          preface ("Actual type:", p_typ t1);
 146          preface ("Needed type:", p_typ t2);
 147          Option.app (describe_unification_error t1) ueo)
 148       | WrongForm (place, form, e, t, ueo) =>
 149         (ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
 150          preface ("Expression:", p_exp e);
 151          preface ("      Type:", p_typ t);
 152          Option.app (describe_unification_error t) ueo)
 153       | UnboundVariable name =>
 154         ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
 155       | WrongPred (place, p1, p2) =>
 156         (ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
 157          preface ("Have:", p_pred p1);
 158          preface ("Need:", p_pred p2))
 159
 160 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
 161     case (p1, p2) of
 162         (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
 163       | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
 164
 165       | (_, CPrefix (CRoot, _)) => true
 166       | (CNot (CPrefix (CRoot, _), _), _) => true
 167
 168       | (CRoot, CRoot) => true
 169
 170       | (CConst s1, CConst s2) => s1 = s2
 171
 172       | (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
 173       | (_, CPrefix p2) => predImplies (p1All, p2)
 174
 175       | (CNot p1, CNot p2) => predImplies (p2, p1)
 176
 177       | _ => false
 178
 179 fun predSimpl (pAll as (p, loc)) =
 180     case p of
 181         CRoot => pAll
 182       | CConst _ => pAll
 183       | CPrefix p => (CPrefix (predSimpl p), loc)
 184       | CNot p => (CNot (predSimpl p), loc)
 185       | CAnd (p1, p2) =>
 186         let
 187             val p1' = predSimpl p1
 188             val p2' = predSimpl p2
 189         in
 190             case p1' of
 191                 (CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
 192               | _ => if predImplies (p2', p1') then
 193                          p2'
 194                      else if predImplies (p1', p2') then
 195                          p1'
 196                      else
 197                          (CAnd (p1', p2'), loc)
 198         end
 199
 200 fun subPred (p1, p2) =
 201     if predImplies (p1, p2) then
 202         ()
 203     else
 204         raise (Unify (UnifyPred (p1, p2)))
 205
 206 fun subRecord f (r1, r2) =
 207     SM.appi (fn (k, v2) =>
 208                 case SM.find (r1, k) of
 209                     NONE => raise UnequalDomains
 210                   | SOME v1 => f (v1, v2)) r2
 211
 212 fun occurs u (t, _) =
 213     case t of
 214         TBase _ => false
 215       | TList t => occurs u t
 216       | TArrow (d, r) => occurs u d orelse occurs u r
 217       | TAction (_, d, r) =>
 218         List.exists (occurs u) (SM.listItems d)
 219         orelse List.exists (occurs u) (SM.listItems r)
 220       | TNested (_, t) => occurs u t
 221       | TError => false
 222       | TUnif (_, ref (SOME t)) => occurs u t
 223       | TUnif (_, u') => u = u'
 224
 225 fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
 226     case (t1, t2) of
 227         (TBase s1, TBase s2) =>
 228         if s1 = s2 then
 229             ()
 230         else
 231             raise Unify (UnifyTyp (t1All, t2All))
 232       | (TList t1, TList t2) => subTyp (t1, t2)
 233       | (TArrow (d1, r1), TArrow (d2, r2)) =>
 234         (subTyp (d2, d1);
 235          subTyp (r1, r2))
 236
 237       | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
 238         ((subPred (p2, p1);
 239           subRecord subTyp (d2, d1);
 240           subRecord subTyp (r1, r2);
 241           subRecord subTyp (r2, r1))
 242          handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
 243
 244       | (TNested (d1, r1), TNested (d2, r2)) =>
 245         (subPred (d2, d1);
 246          subTyp (r1, r2))
 247
 248       | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
 249       | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
 250
 251       | (TUnif (_, r1), TUnif (_, r2)) =>
 252         if r1 = r2 then
 253             ()
 254         else
 255             r1 := SOME t2All
 256
 257       | (TUnif (name, r), _) =>
 258         if occurs r t2All then
 259             raise (Unify (UnifyOccurs (name, t2All)))
 260         else
 261             r := SOME t2All
 262
 263       | (_, TUnif (name, r)) =>
 264         if occurs r t1All then
 265             raise (Unify (UnifyOccurs (name, t1All)))
 266         else
 267             r := SOME t1All
 268
 269       | (TError, _) => ()
 270       | (_, TError) => ()
 271
 272       | _ => raise Unify (UnifyTyp (t1All, t2All))
 273
 274 fun isError t =
 275     case t of
 276         (TError, _) => true
 277       | _ => false
 278
 279 fun whnorm (tAll as (t, loc)) =
 280     case t of
 281         TUnif (_, ref (SOME tAll)) => whnorm tAll
 282       | _ => tAll
 283
 284 fun checkTyp G (tAll as (t, loc)) =
 285     let
 286         val err = ErrorMsg.error (SOME loc)
 287     in
 288         case t of
 289             TBase name =>
 290             if lookupType G name then
 291                 tAll
 292             else
 293                 (err ("Unbound type name " ^ name);
 294                  (TError, loc))
 295           | TList t => (TList (checkTyp G t), loc)
 296           | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
 297           | TAction (p, d, r) => (TAction (p, SM.map (checkTyp G) d,
 298                                            SM.map (checkTyp G) r), loc)
 299           | TNested (p, t) => (TNested (p, checkTyp G t), loc)
 300           | TError => raise Fail "TError in parser-generated type"
 301           | TUnif _ => raise Fail "TUnif in parser-generated type"
 302     end
 303
 304 fun checkExp G (eAll as (e, loc)) =
 305     let
 306         val dte = describe_type_error loc
 307     in
 308         case e of
 309             EInt _ => (TBase "int", loc)
 310           | EString _ => (TBase "string", loc)
 311           | EList es =>
 312             let
 313                 val t = (newUnif (), loc)
 314             in
 315                 foldl (fn (e', ret) =>
 316                           let
 317                               val t' = checkExp G e'
 318                           in
 319                               (subTyp (t', t);
 320                                if isError t' then
 321                                    (TList (TError, loc), loc)
 322                                else
 323                                    ret)
 324                               handle Unify ue =>
 325                                      (dte (WrongType ("List element",
 326                                                       e',
 327                                                       t',
 328                                                       t,
 329                                                       SOME ue));
 330                                       (TError, loc))
 331                           end) (TList t, loc) es
 332             end
 333
 334           | ELam (x, to, e) =>
 335             let
 336                 val t =
 337                     case to of
 338                         NONE => (newUnif (), loc)
 339                       | SOME t => checkTyp G t
 340
 341                 val G' = bindVal G (x, t, NONE)
 342                 val t' = checkExp G' e
 343             in
 344                 (TArrow (t, t'), loc)
 345             end
 346           | EVar x =>
 347             (case lookupVal G x of
 348                  NONE => (dte (UnboundVariable x);
 349                           (TError, loc))
 350                | SOME t => t)
 351           | EApp (func, arg) =>
 352             let
 353                 val dom = (newUnif (), loc)
 354                 val ran = (newUnif (), loc)
 355
 356                 val tf = checkExp G func
 357                 val ta = checkExp G arg
 358             in
 359                 (subTyp (tf, (TArrow (dom, ran), loc));
 360                  subTyp (ta, dom)
 361                  handle Unify ue =>
 362                         dte (WrongType ("Function argument",
 363                                         arg,
 364                                         ta,
 365                                         dom,
 366                                         SOME ue));
 367                  ran)
 368                 handle Unify ue =>
 369                        (dte (WrongForm ("Function to be applied",
 370                                         "function",
 371                                         func,
 372                                         tf,
 373                                         SOME ue));
 374                         (TError, loc))
 375             end
 376
 377           | ESet (evar, e) =>
 378             let
 379                 val t = checkExp G e
 380             in
 381                 (TAction ((CPrefix (CRoot, loc), loc),
 382                           SM.empty,
 383                           SM.insert (SM.empty, evar, t)),
 384                  loc)
 385             end
 386           | EGet (x, evar, rest) =>
 387             let
 388                 val xt = (newUnif (), loc)
 389                 val G' = bindVal G (x, xt, NONE)
 390
 391                 val rt = whnorm (checkExp G' rest)
 392             in
 393                 case rt of
 394                     (TAction (p, d, r), _) =>
 395                     (case SM.find (d, evar) of
 396                          NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
 397                        | SOME xt' =>
 398                          (subTyp (xt', xt)
 399                                 handle Unify ue =>
 400                                        dte (WrongType ("Retrieved environment variable",
 401                                                        (EVar x, loc),
 402                                                        xt',
 403                                                        xt,
 404                                                        SOME ue));
 405                           rt))
 406                   | (TError, _) => rt
 407                   | _ => (dte (WrongForm ("Body of environment variable read",
 408                                           "action",
 409                                           rest,
 410                                           rt,
 411                                           NONE));
 412                           (TError, loc))
 413             end
 414
 415           | ESeq [] => raise Fail "Empty ESeq"
 416           | ESeq [e1] => checkExp G e1
 417           | ESeq (e1 :: rest) =>
 418             let
 419                 val e2 = (ESeq rest, loc)
 420
 421                 val t1 = whnorm (checkExp G e1)
 422                 val t2 = whnorm (checkExp G e2)
 423             in
 424                 case t1 of
 425                     (TAction (p1, d1, r1), _) =>
 426                     (case t2 of
 427                          (TAction (p2, d2, r2), _) =>
 428                          let
 429                              val p' = predSimpl (CAnd (p1, p2), loc)
 430
 431                              val d' = SM.foldli (fn (name, t, d') =>
 432                                                     case SM.find (r1, name) of
 433                                                         NONE =>
 434                                                         (case SM.find (d', name) of
 435                                                              NONE => SM.insert (d', name, t)
 436                                                            | SOME t' =>
 437                                                              (subTyp (t, t')
 438                                                               handle Unify ue =>
 439                                                                      dte (WrongType ("Shared environment variable",
 440                                                                                      (EVar name, loc),
 441                                                                                      t,
 442                                                                                      t',
 443                                                                                      SOME ue));
 444                                                               d'))
 445                                                       | SOME t' =>
 446                                                         (subTyp (t, t')
 447                                                          handle Unify ue =>
 448                                                                 dte (WrongType ("Shared environment variable",
 449                                                                                 (EVar name, loc),
 450                                                                                 t,
 451                                                                                 t',
 452                                                                                 SOME ue));
 453                                                          d'))
 454                                                 d1 d2
 455
 456                              val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
 457                                                 r1 r2
 458                          in
 459                              (TAction (p', d', r'), loc)
 460                          end
 461                        | (TError, _) => t2
 462                        | _ => (dte (WrongForm ("Action to be sequenced",
 463                                                "action",
 464                                                e2,
 465                                                t2,
 466                                                NONE));
 467                                (TError, loc)))
 468                   | (TError, _) => t1
 469                   | _ => (dte (WrongForm ("Action to be sequenced",
 470                                           "action",
 471                                           e1,
 472                                           t1,
 473                                           NONE));
 474                           (TError, loc))
 475             end
 476
 477           | ELocal (e1, e2) =>
 478             let
 479                 val t1 = whnorm (checkExp G e1)
 480                 val t2 = whnorm (checkExp G e2)
 481             in
 482                 case t1 of
 483                     (TAction (p1, d1, r1), _) =>
 484                     (case t2 of
 485                          (TAction (p2, d2, r2), _) =>
 486                          let
 487                              val p' = predSimpl (CAnd (p1, p2), loc)
 488
 489                              val d' = SM.foldli (fn (name, t, d') =>
 490                                                     case SM.find (r1, name) of
 491                                                         NONE =>
 492                                                         (case SM.find (d', name) of
 493                                                              NONE => SM.insert (d', name, t)
 494                                                            | SOME t' =>
 495                                                              (subTyp (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                                                       | SOME t' =>
 504                                                         (subTyp (t, t')
 505                                                          handle Unify ue =>
 506                                                                 dte (WrongType ("Shared environment variable",
 507                                                                                 (EVar name, loc),
 508                                                                                 t,
 509                                                                                 t',
 510                                                                                 SOME ue));
 511                                                          d'))
 512                                                 d1 d2
 513                          in
 514                              (TAction (p', d', r2), loc)
 515                          end
 516                        | (TError, _) => t2
 517                        | _ => (dte (WrongForm ("Action to be sequenced",
 518                                                "action",
 519                                                e2,
 520                                                t2,
 521                                                NONE));
 522                                (TError, loc)))
 523                   | (TError, _) => t1
 524                   | _ => (dte (WrongForm ("Action to be sequenced",
 525                                           "action",
 526                                           e1,
 527                                           t1,
 528                                           NONE));
 529                           (TError, loc))
 530             end
 531
 532
 533           | EWith (e1, e2) =>
 534             let
 535                 val t1 = whnorm (checkExp G e1)
 536                 val t2 = whnorm (checkExp G e2)
 537             in
 538                 case t1 of
 539                     (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
 540                     (case t2 of
 541                          (TAction (p, d, r), _) =>
 542                          if predImplies (pd, p) then
 543                              let
 544                                  val combineRecs =
 545                                      SM.unionWithi (fn (name, t1, t2) =>
 546                                                        (subTyp (t1, t2)
 547                                                         handle Unify ue =>
 548                                                                dte (WrongType ("Environment variable",
 549                                                                                (EVar name, loc),
 550                                                                                t1,
 551                                                                                t2,
 552                                                                                SOME ue));
 553                                                         t2))
 554                              in
 555                                  (TAction (pr, combineRecs (d, d1),
 556                                            combineRecs (r, r1)), loc)
 557                              end
 558                          else
 559                              (dte (WrongPred ("nested action",
 560                                               pd,
 561                                               p));
 562                               (TError, loc))
 563                        | (TError, _) => t2
 564                        | _ =>
 565                          (dte (WrongForm ("Body of nested action",
 566                                           "action",
 567                                           e2,
 568                                           t2,
 569                                           NONE));
 570                           (TError, loc)))
 571                   | (TError, _) => t1
 572                   | _ =>
 573                     (dte (WrongForm ("Container of nested action",
 574                                      "action",
 575                                      e1,
 576                                      t1,
 577                                      NONE));
 578                      (TError, loc))
 579             end
 580
 581           | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
 582                                SM.empty, SM.empty), loc)
 583     end
 584
 585 exception Ununif
 586
 587 fun ununif (tAll as (t, loc)) =
 588     case t of
 589         TBase _ => tAll
 590       | TList t => (TList (ununif t), loc)
 591       | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
 592       | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
 593       | TUnif (_, ref (SOME t)) => ununif t
 594       | TNested _ => tAll
 595       | TError => tAll
 596
 597       | TUnif (_, ref NONE) => raise Ununif
 598
 599 fun hasError (t, _) =
 600     case t of
 601         TBase _ => false
 602       | TList t => hasError t
 603       | TArrow (d, r) => hasError d orelse hasError r
 604       | TAction (p, d, r) => List.exists hasError (SM.listItems d)
 605                              orelse List.exists hasError (SM.listItems r)
 606       | TNested _ => false
 607       | TError => false
 608       | TUnif (_, ref (SOME t)) => hasError t
 609       | TUnif (_, ref NONE) => false
 610
 611
 612 fun checkUnit G (eAll as (_, loc)) =
 613     let
 614         val _ = resetUnif ()
 615         val t = checkExp G eAll
 616     in
 617         if hasError t then
 618             t
 619         else
 620             ununif t
 621             handle Ununif =>
 622                    (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
 623                     printd (p_typ t);
 624                     t)
 625     end
 626
 627 fun checkDecl G (d, _, loc) =
 628     case d of
 629         DExternType name => bindType G name
 630       | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
 631       | DVal (name, to, e) =>
 632         let
 633             val to =
 634                 case to of
 635                     NONE => (newUnif (), loc)
 636                   | SOME to => checkTyp G to
 637
 638             val t = checkExp G e
 639         in
 640             subTyp (t, to)
 641             handle Unify ue =>
 642                    describe_type_error loc
 643                                        (WrongType ("Bound value",
 644                                                    e,
 645                                                    t,
 646                                                    to,
 647                                                    SOME ue));
 648             bindVal G (name, to, SOME e)
 649         end
 650
 651 fun checkFile G tInit (ds, eo) =
 652     let
 653         val G' = foldl (fn (d, G) => checkDecl G d) G ds
 654     in
 655         case eo of
 656             NONE => ()
 657           | SOME (e as (_, loc)) =>
 658             let
 659                 val t = checkExp G' e
 660             in
 661                 subTyp (t, tInit)
 662                 handle Unify ue =>
 663                        (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
 664                         preface ("Actual:", p_typ t);
 665                         preface ("Needed:", p_typ tInit))
 666             end;
 667         G'
 668     end
 669
 670 end