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