Mercurial > urweb

comparison src/elab_env.sml @ 1325:fdf48f6ba418

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More hnorm during type class resolution
author Adam Chlipala <adam@chlipala.net>
date Thu, 02 Dec 2010 12:24:09 -0500
parents c7b9a33c26c8
children 03642b83b57b
comparison
equal deleted inserted replaced
1324:d596c7002ad8 1325:fdf48f6ba418
557 | (CProj (c1, n1), CProj (c2, n2)) => (eqCons (c1, c2); 557 | (CProj (c1, n1), CProj (c2, n2)) => (eqCons (c1, c2);
558 if n1 = n2 then () else raise Unify) 558 if n1 = n2 then () else raise Unify)
559 559
560 | _ => raise Unify 560 | _ => raise Unify
561 561
562 fun unifyCons rs = 562 fun unifyCons (hnorm : con -> con) rs =
563 let 563 let
564 fun unify d (c1, c2) = 564 fun unify d (c1, c2) =
565 case (#1 c1, #1 c2) of 565 case (#1 (hnorm c1), #1 (hnorm c2)) of
566 (CUnif (nl, _, _, _, ref (SOME c1)), _) => unify d (mliftConInCon nl c1, c2) 566 (CUnif (nl, _, _, _, ref (SOME c1)), _) => unify d (mliftConInCon nl c1, c2)
567 | (_, CUnif (nl, _, _, _, ref (SOME c2))) => unify d (c1, mliftConInCon nl c2) 567 | (_, CUnif (nl, _, _, _, ref (SOME c2))) => unify d (c1, mliftConInCon nl c2)
568 568
569 | (CUnif _, _) => () 569 | (CUnif _, _) => ()
570 570
621 | _ => raise Unify 621 | _ => raise Unify
622 in 622 in
623 unify 623 unify
624 end 624 end
625 625
626 fun tryUnify nRs (c1, c2) = 626 fun tryUnify hnorm nRs (c1, c2) =
627 let 627 let
628 val rs = List.tabulate (nRs, fn _ => ref NONE) 628 val rs = List.tabulate (nRs, fn _ => ref NONE)
629 in 629 in
630 (unifyCons rs 0 (c1, c2); 630 (unifyCons hnorm rs 0 (c1, c2);
631 SOME (map (fn r => case !r of 631 SOME (map (fn r => case !r of
632 NONE => raise Unify 632 NONE => raise Unify
633 | SOME c => c) rs)) 633 | SOME c => c) rs))
634 handle Unify => NONE 634 handle Unify => NONE
635 end 635 end
710 710
711 fun tryRules rules = 711 fun tryRules rules =
712 case rules of 712 case rules of
713 [] => NONE 713 [] => NONE
714 | (nRs, cs, c', e) :: rules' => 714 | (nRs, cs, c', e) :: rules' =>
715 case tryUnify nRs (c, c') of 715 case tryUnify hnorm nRs (c, c') of
716 NONE => tryRules rules' 716 NONE => tryRules rules'
717 | SOME rs => 717 | SOME rs =>
718 let 718 let
719 val eos = map (resolve o unifySubst rs) cs 719 val eos = map (resolve o unifySubst rs) cs
720 in 720 in
737 737
738 fun tryGrounds ces = 738 fun tryGrounds ces =
739 case ces of 739 case ces of
740 [] => rules () 740 [] => rules ()
741 | (c', e) :: ces' => 741 | (c', e) :: ces' =>
742 case tryUnify 0 (c, c') of 742 case tryUnify hnorm 0 (c, c') of
743 NONE => tryGrounds ces' 743 NONE => tryGrounds ces'
744 | SOME _ => SOME e 744 | SOME _ => SOME e
745 in 745 in
746 tryGrounds (#ground class) 746 tryGrounds (#ground class)
747 end 747 end