Mercurial > urweb

comparison src/elab_env.sml @ 1639:6c00d8af6239

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add a new scoping check for unification variables, to fix a type inference bug
author Adam Chlipala <adam@chlipala.net>
date Sun, 18 Dec 2011 11:29:13 -0500
parents 287604b4a08d
children fca4a6d05ac1
comparison
equal deleted inserted replaced
1638:3bf727a08db8 1639:6c00d8af6239
482 482
483 fun class_name_in (c, _) = 483 fun class_name_in (c, _) =
484 case c of 484 case c of
485 CNamed n => SOME (ClNamed n) 485 CNamed n => SOME (ClNamed n)
486 | CModProj x => SOME (ClProj x) 486 | CModProj x => SOME (ClProj x)
487 | CUnif (_, _, _, _, ref (SOME c)) => class_name_in c 487 | CUnif (_, _, _, _, ref (Known c)) => class_name_in c
488 | _ => NONE 488 | _ => NONE
489 489
490 fun isClass (env : env) c = 490 fun isClass (env : env) c =
491 let 491 let
492 fun find NONE = false 492 fun find NONE = false
496 end 496 end
497 497
498 fun class_head_in c = 498 fun class_head_in c =
499 case #1 c of 499 case #1 c of
500 CApp (f, _) => class_head_in f 500 CApp (f, _) => class_head_in f
501 | CUnif (_, _, _, _, ref (SOME c)) => class_head_in c 501 | CUnif (_, _, _, _, ref (Known c)) => class_head_in c
502 | _ => class_name_in c 502 | _ => class_name_in c
503 503
504 exception Unify 504 exception Unify
505 505
506 fun unifyKinds (k1, k2) = 506 fun unifyKinds (k1, k2) =
510 | (KName, KName) => () 510 | (KName, KName) => ()
511 | (KRecord k1, KRecord k2) => unifyKinds (k1, k2) 511 | (KRecord k1, KRecord k2) => unifyKinds (k1, k2)
512 | (KUnit, KUnit) => () 512 | (KUnit, KUnit) => ()
513 | (KTuple ks1, KTuple ks2) => (ListPair.appEq unifyKinds (ks1, ks2) 513 | (KTuple ks1, KTuple ks2) => (ListPair.appEq unifyKinds (ks1, ks2)
514 handle ListPair.UnequalLengths => raise Unify) 514 handle ListPair.UnequalLengths => raise Unify)
515 | (KUnif (_, _, ref (SOME k1)), _) => unifyKinds (k1, k2) 515 | (KUnif (_, _, ref (KKnown k1)), _) => unifyKinds (k1, k2)
516 | (_, KUnif (_, _, ref (SOME k2))) => unifyKinds (k1, k2) 516 | (_, KUnif (_, _, ref (KKnown k2))) => unifyKinds (k1, k2)
517 | (KRel n1, KRel n2) => if n1 = n2 then () else raise Unify 517 | (KRel n1, KRel n2) => if n1 = n2 then () else raise Unify
518 | (KFun (_, k1), KFun (_, k2)) => unifyKinds (k1, k2) 518 | (KFun (_, k1), KFun (_, k2)) => unifyKinds (k1, k2)
519 | _ => raise Unify 519 | _ => raise Unify
520 520
521 fun eqCons (c1, c2) = 521 fun eqCons (c1, c2) =
522 case (#1 c1, #1 c2) of 522 case (#1 c1, #1 c2) of
523 (CUnif (nl, _, _, _, ref (SOME c1)), _) => eqCons (mliftConInCon nl c1, c2) 523 (CUnif (nl, _, _, _, ref (Known c1)), _) => eqCons (mliftConInCon nl c1, c2)
524 | (_, CUnif (nl, _, _, _, ref (SOME c2))) => eqCons (c1, mliftConInCon nl c2) 524 | (_, CUnif (nl, _, _, _, ref (Known c2))) => eqCons (c1, mliftConInCon nl c2)
525 525
526 | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify 526 | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify
527 527
528 | (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))
529 | (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))
567 567
568 fun unifyCons (hnorm : con -> con) rs = 568 fun unifyCons (hnorm : con -> con) rs =
569 let 569 let
570 fun unify d (c1, c2) = 570 fun unify d (c1, c2) =
571 case (#1 (hnorm c1), #1 (hnorm c2)) of 571 case (#1 (hnorm c1), #1 (hnorm c2)) of
572 (CUnif (nl, _, _, _, ref (SOME c1)), _) => unify d (mliftConInCon nl c1, c2) 572 (CUnif (nl, _, _, _, ref (Known c1)), _) => unify d (mliftConInCon nl c1, c2)
573 | (_, CUnif (nl, _, _, _, ref (SOME c2))) => unify d (c1, mliftConInCon nl c2) 573 | (_, CUnif (nl, _, _, _, ref (Known c2))) => unify d (c1, mliftConInCon nl c2)
574 574
575 | (CUnif _, _) => () 575 | (CUnif _, _) => ()
576 576
577 | (c1', CRel n2) => 577 | (c1', CRel n2) =>
578 if n2 < d then 578 if n2 < d then
661 0 661 0
662 662
663 exception Bad of con * con 663 exception Bad of con * con
664 664
665 val hasUnif = U.Con.exists {kind = fn _ => false, 665 val hasUnif = U.Con.exists {kind = fn _ => false,
666 con = fn CUnif (_, _, _, _, ref NONE) => true 666 con = fn CUnif (_, _, _, _, ref (Unknown _)) => true
667 | _ => false} 667 | _ => false}
668 668
669 fun startsWithUnif c = 669 fun startsWithUnif c =
670 let 670 let
671 fun firstArg (c, acc) = 671 fun firstArg (c, acc) =
695 let 695 let
696 val (f, equate) = generalize f 696 val (f, equate) = generalize f
697 697
698 fun isRecord () = 698 fun isRecord () =
699 let 699 let
700 val rk = ref NONE 700 val rk = ref (KUnknown (fn _ => true))
701 val k = (KUnif (loc, "k", rk), loc) 701 val k = (KUnif (loc, "k", rk), loc)
702 val r = ref NONE 702 val r = ref (Unknown (fn _ => true))
703 val rc = (CUnif (0, loc, k, "x", r), loc) 703 val rc = (CUnif (0, loc, k, "x", r), loc)
704 in 704 in
705 ((CApp (f, rc), loc), 705 ((CApp (f, rc), loc),
706 fn () => (if consEq (rc, x) then 706 fn () => (if consEq (rc, x) then
707 true 707 true