Mercurial > urweb

comparison src/elab_env.sml @ 1303:c7b9a33c26c8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hopeful fix for the Great Unification Bug
author Adam Chlipala <adam@chlipala.net>
date Sun, 10 Oct 2010 14:41:03 -0400
parents b4480a56cab7
children fdf48f6ba418
comparison
equal deleted inserted replaced
1302:d008c4c43a0a 1303:c7b9a33c26c8
41 exception UnboundNamed of int 41 exception UnboundNamed of int
42 42
43 43
44 (* AST utility functions *) 44 (* AST utility functions *)
45 45
46 exception SynUnif
47
48 val liftKindInKind = 46 val liftKindInKind =
49 U.Kind.mapB {kind = fn bound => fn k => 47 U.Kind.mapB {kind = fn bound => fn k =>
50 case k of 48 case k of
51 KRel xn => 49 KRel xn =>
52 if xn < bound then 50 if xn < bound then
76 CRel xn => 74 CRel xn =>
77 if xn < bound then 75 if xn < bound then
78 c 76 c
79 else 77 else
80 CRel (xn + 1) 78 CRel (xn + 1)
81 (*| CUnif _ => raise SynUnif*) 79 | CUnif (nl, loc, k, s, r) => CUnif (nl+1, loc, k, s, r)
82 | _ => c, 80 | _ => c,
83 bind = fn (bound, U.Con.RelC _) => bound + 1 81 bind = fn (bound, U.Con.RelC _) => bound + 1
84 | (bound, _) => bound} 82 | (bound, _) => bound}
85 83
86 val lift = liftConInCon 0 84 val lift = liftConInCon 0
85
86 fun mliftConInCon by c =
87 if by = 0 then
88 c
89 else
90 U.Con.mapB {kind = fn _ => fn k => k,
91 con = fn bound => fn c =>
92 case c of
93 CRel xn =>
94 if xn < bound then
95 c
96 else
97 CRel (xn + by)
98 | CUnif (nl, loc, k, s, r) => CUnif (nl+by, loc, k, s, r)
99 | _ => c,
100 bind = fn (bound, U.Con.RelC _) => bound + 1
101 | (bound, _) => bound} 0 c
102
103 val () = U.mliftConInCon := mliftConInCon
87 104
88 val liftKindInExp = 105 val liftKindInExp =
89 U.Exp.mapB {kind = fn bound => fn k => 106 U.Exp.mapB {kind = fn bound => fn k =>
90 case k of 107 case k of
91 KRel xn => 108 KRel xn =>
106 CRel xn => 123 CRel xn =>
107 if xn < bound then 124 if xn < bound then
108 c 125 c
109 else 126 else
110 CRel (xn + 1) 127 CRel (xn + 1)
128 | CUnif (nl, loc, k, s, r) => CUnif (nl+1, loc, k, s, r)
111 | _ => c, 129 | _ => c,
112 exp = fn _ => fn e => e, 130 exp = fn _ => fn e => e,
113 bind = fn (bound, U.Exp.RelC _) => bound + 1 131 bind = fn (bound, U.Exp.RelC _) => bound + 1
114 | (bound, _) => bound} 132 | (bound, _) => bound}
115 133
464 482
465 fun class_name_in (c, _) = 483 fun class_name_in (c, _) =
466 case c of 484 case c of
467 CNamed n => SOME (ClNamed n) 485 CNamed n => SOME (ClNamed n)
468 | CModProj x => SOME (ClProj x) 486 | CModProj x => SOME (ClProj x)
469 | CUnif (_, _, _, ref (SOME c)) => class_name_in c 487 | CUnif (_, _, _, _, ref (SOME c)) => class_name_in c
470 | _ => NONE 488 | _ => NONE
471 489
472 fun isClass (env : env) c = 490 fun isClass (env : env) c =
473 let 491 let
474 fun find NONE = false 492 fun find NONE = false
478 end 496 end
479 497
480 fun class_head_in c = 498 fun class_head_in c =
481 case #1 c of 499 case #1 c of
482 CApp (f, _) => class_head_in f 500 CApp (f, _) => class_head_in f
483 | CUnif (_, _, _, ref (SOME c)) => class_head_in c 501 | CUnif (_, _, _, _, ref (SOME c)) => class_head_in c
484 | _ => class_name_in c 502 | _ => class_name_in c
485 503
486 exception Unify 504 exception Unify
487 505
488 fun unifyKinds (k1, k2) = 506 fun unifyKinds (k1, k2) =
500 | (KFun (_, k1), KFun (_, k2)) => unifyKinds (k1, k2) 518 | (KFun (_, k1), KFun (_, k2)) => unifyKinds (k1, k2)
501 | _ => raise Unify 519 | _ => raise Unify
502 520
503 fun eqCons (c1, c2) = 521 fun eqCons (c1, c2) =
504 case (#1 c1, #1 c2) of 522 case (#1 c1, #1 c2) of
505 (CUnif (_, _, _, ref (SOME c1)), _) => eqCons (c1, c2) 523 (CUnif (nl, _, _, _, ref (SOME c1)), _) => eqCons (mliftConInCon nl c1, c2)
506 | (_, CUnif (_, _, _, ref (SOME c2))) => eqCons (c1, c2) 524 | (_, CUnif (nl, _, _, _, ref (SOME c2))) => eqCons (c1, mliftConInCon nl c2)
507 525
508 | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify 526 | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify
509 527
510 | (TFun (d1, r1), TFun (d2, r2)) => (eqCons (d1, d2); eqCons (r1, r2)) 528 | (TFun (d1, r1), TFun (d2, r2)) => (eqCons (d1, d2); eqCons (r1, r2))
511 | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); eqCons (r1, r2)) 529 | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); eqCons (r1, r2))
543 561
544 fun unifyCons rs = 562 fun unifyCons rs =
545 let 563 let
546 fun unify d (c1, c2) = 564 fun unify d (c1, c2) =
547 case (#1 c1, #1 c2) of 565 case (#1 c1, #1 c2) of
548 (CUnif (_, _, _, ref (SOME c1)), _) => unify d (c1, c2) 566 (CUnif (nl, _, _, _, ref (SOME c1)), _) => unify d (mliftConInCon nl c1, c2)
549 | (_, CUnif (_, _, _, ref (SOME c2))) => unify d (c1, c2) 567 | (_, CUnif (nl, _, _, _, ref (SOME c2))) => unify d (c1, mliftConInCon nl c2)
550 568
551 | (CUnif _, _) => () 569 | (CUnif _, _) => ()
552 570
553 | (c1', CRel n2) => 571 | (c1', CRel n2) =>
554 if n2 < d then 572 if n2 < d then
631 0 649 0
632 650
633 exception Bad of con * con 651 exception Bad of con * con
634 652
635 val hasUnif = U.Con.exists {kind = fn _ => false, 653 val hasUnif = U.Con.exists {kind = fn _ => false,
636 con = fn CUnif (_, _, _, ref NONE) => true 654 con = fn CUnif (_, _, _, _, ref NONE) => true
637 | _ => false} 655 | _ => false}
638 656
639 fun startsWithUnif c = 657 fun startsWithUnif c =
640 let 658 let
641 fun firstArg (c, acc) = 659 fun firstArg (c, acc) =
668 fun isRecord () = 686 fun isRecord () =
669 let 687 let
670 val rk = ref NONE 688 val rk = ref NONE
671 val k = (KUnif (loc, "k", rk), loc) 689 val k = (KUnif (loc, "k", rk), loc)
672 val r = ref NONE 690 val r = ref NONE
673 val rc = (CUnif (loc, k, "x", r), loc) 691 val rc = (CUnif (0, loc, k, "x", r), loc)
674 in 692 in
675 ((CApp (f, rc), loc), 693 ((CApp (f, rc), loc),
676 fn () => (if consEq (rc, x) then 694 fn () => (if consEq (rc, x) then
677 true 695 true
678 else 696 else