Mercurial > urweb

comparison src/elab_env.sml @ 1742:fca4a6d05ac1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More diagnostic information about some type class resolution failures
author Adam Chlipala <adam@chlipala.net>
date Fri, 04 May 2012 10:33:04 -0400
parents 6c00d8af6239
children d28adceef22a
comparison
equal deleted inserted replaced
1741:d6e233db97c8 1742:fca4a6d05ac1
676 case firstArg (c, NONE) of 676 case firstArg (c, NONE) of
677 NONE => false 677 NONE => false
678 | SOME x => hasUnif x 678 | SOME x => hasUnif x
679 end 679 end
680 680
681 val cause = ref (NONE : con option)
682 fun resolveFailureCause () = !cause
683
681 fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) = 684 fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) =
682 let 685 let
683 fun resolve c = 686 fun resolve firstLevel c =
684 let 687 let
688 fun notFound () = (if firstLevel then () else cause := SOME c; NONE)
689
685 fun doHead f = 690 fun doHead f =
686 case CM.find (#classes env, f) of 691 case CM.find (#classes env, f) of
687 NONE => NONE 692 NONE => notFound ()
688 | SOME class => 693 | SOME class =>
689 let 694 let
690 val loc = #2 c 695 val loc = #2 c
691 696
692 fun generalize (c as (_, loc)) = 697 fun generalize (c as (_, loc)) =
720 725
721 val (c, equate) = generalize c 726 val (c, equate) = generalize c
722 727
723 fun tryRules rules = 728 fun tryRules rules =
724 case rules of 729 case rules of
725 [] => NONE 730 [] => notFound ()
726 | (nRs, cs, c', e) :: rules' => 731 | (nRs, cs, c', e) :: rules' =>
727 case tryUnify hnorm nRs (c, c') of 732 case tryUnify hnorm nRs (c, c') of
728 NONE => tryRules rules' 733 NONE => tryRules rules'
729 | SOME rs => 734 | SOME rs =>
730 let 735 let
731 val eos = map (resolve o unifySubst rs) cs 736 val eos = map (resolve false o unifySubst rs) cs
732 in 737 in
733 if List.exists (not o Option.isSome) eos 738 if List.exists (not o Option.isSome) eos
734 orelse not (equate ()) 739 orelse not (equate ())
735 orelse not (consEq (c, unifySubst rs c')) then 740 orelse not (consEq (c, unifySubst rs c')) then
736 tryRules rules' 741 tryRules rules'
757 in 762 in
758 tryGrounds (#ground class) 763 tryGrounds (#ground class)
759 end 764 end
760 in 765 in
761 if startsWithUnif c then 766 if startsWithUnif c then
762 NONE 767 notFound ()
763 else 768 else
764 case #1 c of 769 case #1 c of
765 TRecord c => 770 TRecord c =>
766 (case #1 (hnorm c) of 771 (case #1 (hnorm c) of
767 CRecord (_, xts) => 772 CRecord (_, xts) =>
775 780
776 val t = case t of 781 val t = case t of
777 (CApp (f, x), loc) => (CApp (hnorm f, hnorm x), loc) 782 (CApp (f, x), loc) => (CApp (hnorm f, hnorm x), loc)
778 | _ => t 783 | _ => t
779 in 784 in
780 case resolve t of 785 case resolve false t of
781 NONE => NONE 786 NONE => notFound ()
782 | SOME e => resolver (xts, (x, e, t) :: acc) 787 | SOME e => resolver (xts, (x, e, t) :: acc)
783 end 788 end
784 in 789 in
785 resolver (xts, []) 790 resolver (xts, [])
786 end 791 end
787 | _ => NONE) 792 | _ => notFound ())
788 | _ => 793 | _ =>
789 case class_head_in c of 794 case class_head_in c of
790 SOME f => doHead f 795 SOME f => doHead f
791 | _ => NONE 796 | _ => notFound ()
792 end 797 end
793 in 798 in
794 resolve 799 cause := NONE;
800 resolve true
795 end 801 end
796 802
797 fun pushERel (env : env) x t = 803 fun pushERel (env : env) x t =
798 let 804 let
799 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) 805 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)