Mercurial > urweb

comparison src/elaborate.sml @ 987:6dd122f10c0c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Better location calculation for record unification error messages; infer kind arguments to module-projected variables
author Adam Chlipala <adamc@hcoop.net>
date Mon, 05 Oct 2009 16:36:38 -0400
parents b26823138bf8
children 5d7e05b4a5c0
comparison
equal deleted inserted replaced
986:d1dbb9a3c804 987:6dd122f10c0c
324 324
325 val k = case E.projectCon env {sgn = sgn, str = str, field = s} of 325 val k = case E.projectCon env {sgn = sgn, str = str, field = s} of
326 NONE => (conError env (UnboundCon (loc, s)); 326 NONE => (conError env (UnboundCon (loc, s));
327 kerror) 327 kerror)
328 | SOME (k, _) => k 328 | SOME (k, _) => k
329 val (c, k) = elabConHead (L'.CModProj (n, ms, s), loc) k
329 in 330 in
330 ((L'.CModProj (n, ms, s), loc), k, []) 331 (c, k, [])
331 end) 332 end)
332 333
333 | L.CApp (c1, c2) => 334 | L.CApp (c1, c2) =>
334 let 335 let
335 val (c1', k1, gs1) = elabCon (env, denv) c1 336 val (c1', k1, gs1) = elabCon (env, denv) c1
676 | c' => {fields = [], unifs = [], others = [c']} 677 | c' => {fields = [], unifs = [], others = [c']}
677 in 678 in
678 sum 679 sum
679 end 680 end
680 681
681 and consEq env (c1, c2) = 682 and consEq env loc (c1, c2) =
682 let 683 let
683 val mayDelay' = !mayDelay 684 val mayDelay' = !mayDelay
684 in 685 in
685 (mayDelay := false; 686 (mayDelay := false;
686 unifyCons env c1 c2; 687 unifyCons env loc c1 c2;
687 mayDelay := mayDelay'; 688 mayDelay := mayDelay';
688 true) 689 true)
689 handle CUnify _ => (mayDelay := mayDelay'; false) 690 handle CUnify _ => (mayDelay := mayDelay'; false)
690 end 691 end
691 692
722 em (ls1, ls2, []) 723 em (ls1, ls2, [])
723 end 724 end
724 725
725 val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) => 726 val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) =>
726 not (consNeq env (x1, x2)) 727 not (consNeq env (x1, x2))
727 andalso consEq env (c1, c2) 728 andalso consEq env loc (c1, c2)
728 andalso consEq env (x1, x2)) 729 andalso consEq env loc (x1, x2))
729 (#fields s1, #fields s2) 730 (#fields s1, #fields s2)
730 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}), 731 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
731 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*) 732 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
732 733
733 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2) 734 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
734 735
735 val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2) 736 val (others1, others2) = eatMatching (consEq env loc) (#others s1, #others s2)
736 (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), 737 (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
737 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 738 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
738 739
739 fun unsummarize {fields, unifs, others} = 740 fun unsummarize {fields, unifs, others} =
740 let 741 let
791 fun isGuessable (other, fs, unifs) = 792 fun isGuessable (other, fs, unifs) =
792 let 793 let
793 val c = (L'.CRecord (k, fs), loc) 794 val c = (L'.CRecord (k, fs), loc)
794 val c = foldl (fn ((c', _), c) => (L'.CConcat (c', c), loc)) c unifs 795 val c = foldl (fn ((c', _), c) => (L'.CConcat (c', c), loc)) c unifs
795 in 796 in
796 (guessMap env (other, c, GuessFailure); 797 (guessMap env loc (other, c, GuessFailure);
797 true) 798 true)
798 handle GuessFailure => false 799 handle GuessFailure => false
799 end 800 end
800 801
801 val (fs1, fs2, others1, others2, unifs1, unifs2) = 802 val (fs1, fs2, others1, others2, unifs1, unifs2) =
831 832
832 (*before eprefaces "Summaries'" [("#1", p_summary env (normalizeRecordSummary env s1)), 833 (*before eprefaces "Summaries'" [("#1", p_summary env (normalizeRecordSummary env s1)),
833 ("#2", p_summary env (normalizeRecordSummary env s2))]*) 834 ("#2", p_summary env (normalizeRecordSummary env s2))]*)
834 end 835 end
835 836
836 and guessMap env (c1, c2, ex) = 837 and guessMap env loc (c1, c2, ex) =
837 let 838 let
838 val loc = #2 c1
839
840 fun unfold (dom, ran, f, r, c) = 839 fun unfold (dom, ran, f, r, c) =
841 let 840 let
842 fun unfold (r, c) = 841 fun unfold (r, c) =
843 case #1 (hnormCon env c) of 842 case #1 (hnormCon env c) of
844 L'.CRecord (_, []) => unifyCons env r (L'.CRecord (dom, []), loc) 843 L'.CRecord (_, []) => unifyCons env loc r (L'.CRecord (dom, []), loc)
845 | L'.CRecord (_, [(x, v)]) => 844 | L'.CRecord (_, [(x, v)]) =>
846 let 845 let
847 val v' = case dom of 846 val v' = case dom of
848 (L'.KUnit, _) => (L'.CUnit, loc) 847 (L'.KUnit, _) => (L'.CUnit, loc)
849 | _ => cunif (loc, dom) 848 | _ => cunif (loc, dom)
850 in 849 in
851 unifyCons env v (L'.CApp (f, v'), loc); 850 unifyCons env loc v (L'.CApp (f, v'), loc);
852 unifyCons env r (L'.CRecord (dom, [(x, v')]), loc) 851 unifyCons env loc r (L'.CRecord (dom, [(x, v')]), loc)
853 end 852 end
854 | L'.CRecord (_, (x, v) :: rest) => 853 | L'.CRecord (_, (x, v) :: rest) =>
855 let 854 let
856 val r1 = cunif (loc, (L'.KRecord dom, loc)) 855 val r1 = cunif (loc, (L'.KRecord dom, loc))
857 val r2 = cunif (loc, (L'.KRecord dom, loc)) 856 val r2 = cunif (loc, (L'.KRecord dom, loc))
858 in 857 in
859 unfold (r1, (L'.CRecord (ran, [(x, v)]), loc)); 858 unfold (r1, (L'.CRecord (ran, [(x, v)]), loc));
860 unfold (r2, (L'.CRecord (ran, rest), loc)); 859 unfold (r2, (L'.CRecord (ran, rest), loc));
861 unifyCons env r (L'.CConcat (r1, r2), loc) 860 unifyCons env loc r (L'.CConcat (r1, r2), loc)
862 end 861 end
863 | L'.CConcat (c1', c2') => 862 | L'.CConcat (c1', c2') =>
864 let 863 let
865 val r1 = cunif (loc, (L'.KRecord dom, loc)) 864 val r1 = cunif (loc, (L'.KRecord dom, loc))
866 val r2 = cunif (loc, (L'.KRecord dom, loc)) 865 val r2 = cunif (loc, (L'.KRecord dom, loc))
867 in 866 in
868 unfold (r1, c1'); 867 unfold (r1, c1');
869 unfold (r2, c2'); 868 unfold (r2, c2');
870 unifyCons env r (L'.CConcat (r1, r2), loc) 869 unifyCons env loc r (L'.CConcat (r1, r2), loc)
871 end 870 end
872 | L'.CUnif (_, _, _, ur) => 871 | L'.CUnif (_, _, _, ur) =>
873 ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc) 872 ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc)
874 | _ => raise ex 873 | _ => raise ex
875 in 874 in
883 | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) => 882 | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) =>
884 unfold (dom, ran, f, r, c1) 883 unfold (dom, ran, f, r, c1)
885 | _ => raise ex 884 | _ => raise ex
886 end 885 end
887 886
888 and unifyCons' env c1 c2 = 887 and unifyCons' env loc c1 c2 =
889 if isUnitCon env c1 andalso isUnitCon env c2 then 888 if isUnitCon env c1 andalso isUnitCon env c2 then
890 () 889 ()
891 else 890 else
892 let 891 let
893 (*val befor = Time.now () 892 (*val befor = Time.now ()
894 val old1 = c1 893 val old1 = c1
895 val old2 = c2*) 894 val old2 = c2*)
896 val c1 = hnormCon env c1 895 val c1 = hnormCon env c1
897 val c2 = hnormCon env c2 896 val c2 = hnormCon env c2
898 in 897 in
899 unifyCons'' env c1 c2 898 unifyCons'' env loc c1 c2
900 handle ex => guessMap env (c1, c2, ex) 899 handle ex => guessMap env loc (c1, c2, ex)
901 end 900 end
902 901
903 and unifyCons'' env (c1All as (c1, loc)) (c2All as (c2, _)) = 902 and unifyCons'' env loc (c1All as (c1, _)) (c2All as (c2, _)) =
904 let 903 let
905 fun err f = raise CUnify' (f (c1All, c2All)) 904 fun err f = raise CUnify' (f (c1All, c2All))
906 905
907 fun projSpecial1 (c1, n1, onFail) = 906 fun projSpecial1 (c1, n1, onFail) =
908 let 907 let
910 case #1 (hnormCon env c2All) of 909 case #1 (hnormCon env c2All) of
911 L'.CProj (c2, n2) => 910 L'.CProj (c2, n2) =>
912 let 911 let
913 fun tryNormal () = 912 fun tryNormal () =
914 if n1 = n2 then 913 if n1 = n2 then
915 unifyCons' env c1 c2 914 unifyCons' env loc c1 c2
916 else 915 else
917 onFail () 916 onFail ()
918 in 917 in
919 case #1 (hnormCon env c2) of 918 case #1 (hnormCon env c2) of
920 L'.CUnif (_, k, _, r) => 919 L'.CUnif (_, k, _, r) =>
923 let 922 let
924 val loc = #2 c2 923 val loc = #2 c2
925 val us = map (fn k => cunif (loc, k)) ks 924 val us = map (fn k => cunif (loc, k)) ks
926 in 925 in
927 r := SOME (L'.CTuple us, loc); 926 r := SOME (L'.CTuple us, loc);
928 unifyCons' env c1All (List.nth (us, n2 - 1)) 927 unifyCons' env loc c1All (List.nth (us, n2 - 1))
929 end 928 end
930 | _ => tryNormal ()) 929 | _ => tryNormal ())
931 | _ => tryNormal () 930 | _ => tryNormal ()
932 end 931 end
933 | _ => onFail () 932 | _ => onFail ()
939 let 938 let
940 val loc = #2 c1 939 val loc = #2 c1
941 val us = map (fn k => cunif (loc, k)) ks 940 val us = map (fn k => cunif (loc, k)) ks
942 in 941 in
943 r := SOME (L'.CTuple us, loc); 942 r := SOME (L'.CTuple us, loc);
944 unifyCons' env (List.nth (us, n1 - 1)) c2All 943 unifyCons' env loc (List.nth (us, n1 - 1)) c2All
945 end 944 end
946 | _ => trySnd ()) 945 | _ => trySnd ())
947 | _ => trySnd () 946 | _ => trySnd ()
948 end 947 end
949 948
955 let 954 let
956 val loc = #2 c2 955 val loc = #2 c2
957 val us = map (fn k => cunif (loc, k)) ks 956 val us = map (fn k => cunif (loc, k)) ks
958 in 957 in
959 r := SOME (L'.CTuple us, loc); 958 r := SOME (L'.CTuple us, loc);
960 unifyCons' env c1All (List.nth (us, n2 - 1)) 959 unifyCons' env loc c1All (List.nth (us, n2 - 1))
961 end 960 end
962 | _ => onFail ()) 961 | _ => onFail ())
963 | _ => onFail () 962 | _ => onFail ()
964 963
965 fun isRecord' () = unifyRecordCons env (loc, c1All, c2All) 964 fun isRecord' () = unifyRecordCons env (loc, c1All, c2All)
1001 r := SOME c1All 1000 r := SOME c1All
1002 1001
1003 | (L'.CUnit, L'.CUnit) => () 1002 | (L'.CUnit, L'.CUnit) => ()
1004 1003
1005 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => 1004 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
1006 (unifyCons' env d1 d2; 1005 (unifyCons' env loc d1 d2;
1007 unifyCons' env r1 r2) 1006 unifyCons' env loc r1 r2)
1008 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => 1007 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
1009 if expl1 <> expl2 then 1008 if expl1 <> expl2 then
1010 err CExplicitness 1009 err CExplicitness
1011 else 1010 else
1012 (unifyKinds env d1 d2; 1011 (unifyKinds env d1 d2;
1015 val env' = E.pushCRel env x1 d1 1014 val env' = E.pushCRel env x1 d1
1016 in 1015 in
1017 (*TextIO.print ("E.pushCRel: " 1016 (*TextIO.print ("E.pushCRel: "
1018 ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor))) 1017 ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor)))
1019 ^ "\n");*) 1018 ^ "\n");*)
1020 unifyCons' env' r1 r2 1019 unifyCons' env' loc r1 r2
1021 end) 1020 end)
1022 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env r1 r2 1021 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env loc r1 r2
1023 | (L'.TDisjoint (c1, d1, e1), L'.TDisjoint (c2, d2, e2)) => 1022 | (L'.TDisjoint (c1, d1, e1), L'.TDisjoint (c2, d2, e2)) =>
1024 (unifyCons' env c1 c2; 1023 (unifyCons' env loc c1 c2;
1025 unifyCons' env d1 d2; 1024 unifyCons' env loc d1 d2;
1026 unifyCons' env e1 e2) 1025 unifyCons' env loc e1 e2)
1027 1026
1028 | (L'.CRel n1, L'.CRel n2) => 1027 | (L'.CRel n1, L'.CRel n2) =>
1029 if n1 = n2 then 1028 if n1 = n2 then
1030 () 1029 ()
1031 else 1030 else
1035 () 1034 ()
1036 else 1035 else
1037 err CIncompatible 1036 err CIncompatible
1038 1037
1039 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) => 1038 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) =>
1040 (unifyCons' env d1 d2; 1039 (unifyCons' env loc d1 d2;
1041 unifyCons' env r1 r2) 1040 unifyCons' env loc r1 r2)
1042 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => 1041 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
1043 (unifyKinds env k1 k2; 1042 (unifyKinds env k1 k2;
1044 unifyCons' (E.pushCRel env x1 k1) c1 c2) 1043 unifyCons' (E.pushCRel env x1 k1) loc c1 c2)
1045 1044
1046 | (L'.CName n1, L'.CName n2) => 1045 | (L'.CName n1, L'.CName n2) =>
1047 if n1 = n2 then 1046 if n1 = n2 then
1048 () 1047 ()
1049 else 1048 else
1054 () 1053 ()
1055 else 1054 else
1056 err CIncompatible 1055 err CIncompatible
1057 1056
1058 | (L'.CTuple cs1, L'.CTuple cs2) => 1057 | (L'.CTuple cs1, L'.CTuple cs2) =>
1059 ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2)) 1058 ((ListPair.appEq (fn (c1, c2) => unifyCons' env loc c1 c2) (cs1, cs2))
1060 handle ListPair.UnequalLengths => err CIncompatible) 1059 handle ListPair.UnequalLengths => err CIncompatible)
1061 1060
1062 | (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, fn () => err CIncompatible) 1061 | (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, fn () => err CIncompatible)
1063 | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, fn () => err CIncompatible) 1062 | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, fn () => err CIncompatible)
1064 1063
1065 | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) => 1064 | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
1066 (unifyKinds env dom1 dom2; 1065 (unifyKinds env dom1 dom2;
1067 unifyKinds env ran1 ran2) 1066 unifyKinds env ran1 ran2)
1068 1067
1069 | (L'.CKAbs (x, c1), L'.CKAbs (_, c2)) => 1068 | (L'.CKAbs (x, c1), L'.CKAbs (_, c2)) =>
1070 unifyCons' (E.pushKRel env x) c1 c2 1069 unifyCons' (E.pushKRel env x) loc c1 c2
1071 | (L'.CKApp (c1, k1), L'.CKApp (c2, k2)) => 1070 | (L'.CKApp (c1, k1), L'.CKApp (c2, k2)) =>
1072 (unifyKinds env k1 k2; 1071 (unifyKinds env k1 k2;
1073 unifyCons' env c1 c2) 1072 unifyCons' env loc c1 c2)
1074 | (L'.TKFun (x, c1), L'.TKFun (_, c2)) => 1073 | (L'.TKFun (x, c1), L'.TKFun (_, c2)) =>
1075 unifyCons' (E.pushKRel env x) c1 c2 1074 unifyCons' (E.pushKRel env x) loc c1 c2
1076 1075
1077 | _ => err CIncompatible 1076 | _ => err CIncompatible
1078 end 1077 end
1079 1078
1080 and unifyCons env c1 c2 = 1079 and unifyCons env loc c1 c2 =
1081 unifyCons' env c1 c2 1080 unifyCons' env loc c1 c2
1082 handle CUnify' err => raise CUnify (c1, c2, err) 1081 handle CUnify' err => raise CUnify (c1, c2, err)
1083 | KUnify args => raise CUnify (c1, c2, CKind args) 1082 | KUnify args => raise CUnify (c1, c2, CKind args)
1084 1083
1085 fun checkCon env e c1 c2 = 1084 fun checkCon env e c1 c2 =
1086 unifyCons env c1 c2 1085 unifyCons env (#2 e) c1 c2
1087 handle CUnify (c1, c2, err) => 1086 handle CUnify (c1, c2, err) =>
1088 expError env (Unify (e, c1, c2, err)) 1087 expError env (Unify (e, c1, c2, err))
1089 1088
1090 fun checkPatCon env p c1 c2 = 1089 fun checkPatCon env p c1 c2 =
1091 unifyCons env c1 c2 1090 unifyCons env (#2 p) c1 c2
1092 handle CUnify (c1, c2, err) => 1091 handle CUnify (c1, c2, err) =>
1093 expError env (PatUnify (p, c1, c2, err)) 1092 expError env (PatUnify (p, c1, c2, err))
1094 1093
1095 fun primType env p = 1094 fun primType env p =
1096 case p of 1095 case p of
2651 E.pushCNamedAs env x n1 k1 (SOME c1)) 2650 E.pushCNamedAs env x n1 k1 (SOME c1))
2652 in 2651 in
2653 SOME env 2652 SOME env
2654 end 2653 end
2655 in 2654 in
2656 (unifyCons env c1 c2; 2655 (unifyCons env loc c1 c2;
2657 good ()) 2656 good ())
2658 handle CUnify (c1, c2, err) => 2657 handle CUnify (c1, c2, err) =>
2659 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2658 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2660 good ()) 2659 good ())
2661 end 2660 end
2705 fun xncBad ((x1, _, t1), (x2, _, t2)) = 2704 fun xncBad ((x1, _, t1), (x2, _, t2)) =
2706 String.compare (x1, x2) <> EQUAL 2705 String.compare (x1, x2) <> EQUAL
2707 orelse case (t1, t2) of 2706 orelse case (t1, t2) of
2708 (NONE, NONE) => false 2707 (NONE, NONE) => false
2709 | (SOME t1, SOME t2) => 2708 | (SOME t1, SOME t2) =>
2710 (unifyCons env t1 (sub2 t2); false) 2709 (unifyCons env loc t1 (sub2 t2); false)
2711 | _ => true 2710 | _ => true
2712 in 2711 in
2713 (if xs1 <> xs2 2712 (if xs1 <> xs2
2714 orelse length xncs1 <> length xncs2 2713 orelse length xncs1 <> length xncs2
2715 orelse ListPair.exists xncBad (xncs1, xncs2) then 2714 orelse ListPair.exists xncBad (xncs1, xncs2) then
2776 in 2775 in
2777 cparts (n2, n1); 2776 cparts (n2, n1);
2778 SOME env 2777 SOME env
2779 end 2778 end
2780 in 2779 in
2781 (unifyCons env t1 t2; 2780 (unifyCons env loc t1 t2;
2782 good ()) 2781 good ())
2783 handle CUnify (c1, c2, err) => 2782 handle CUnify (c1, c2, err) =>
2784 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2783 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2785 good ()) 2784 good ())
2786 end 2785 end
2797 ((*prefaces "val" [("x", PD.string x), 2796 ((*prefaces "val" [("x", PD.string x),
2798 ("n1", PD.string (Int.toString n1)), 2797 ("n1", PD.string (Int.toString n1)),
2799 ("c1", p_con env c1), 2798 ("c1", p_con env c1),
2800 ("c2", p_con env c2), 2799 ("c2", p_con env c2),
2801 ("c2'", p_con env (sub2 c2))];*) 2800 ("c2'", p_con env (sub2 c2))];*)
2802 unifyCons env c1 (sub2 c2); 2801 unifyCons env loc c1 (sub2 c2);
2803 SOME env) 2802 SOME env)
2804 handle CUnify (c1, c2, err) => 2803 handle CUnify (c1, c2, err) =>
2805 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2804 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2806 SOME env) 2805 SOME env)
2807 else 2806 else
2853 2852
2854 | L'.SgiConstraint (c2, d2) => 2853 | L'.SgiConstraint (c2, d2) =>
2855 seek (fn (env, sgi1All as (sgi1, _)) => 2854 seek (fn (env, sgi1All as (sgi1, _)) =>
2856 case sgi1 of 2855 case sgi1 of
2857 L'.SgiConstraint (c1, d1) => 2856 L'.SgiConstraint (c1, d1) =>
2858 if consEq env (c1, c2) andalso consEq env (d1, d2) then 2857 if consEq env loc (c1, c2)
2858 andalso consEq env loc (d1, d2) then
2859 SOME env 2859 SOME env
2860 else 2860 else
2861 NONE 2861 NONE
2862 | _ => NONE) 2862 | _ => NONE)
2863 2863
2909 E.pushCNamedAs env x n1 k2 (SOME c1)) 2909 E.pushCNamedAs env x n1 k2 (SOME c1))
2910 in 2910 in
2911 SOME env 2911 SOME env
2912 end 2912 end
2913 in 2913 in
2914 (unifyCons env c1 c2; 2914 (unifyCons env loc c1 c2;
2915 good ()) 2915 good ())
2916 handle CUnify (c1, c2, err) => 2916 handle CUnify (c1, c2, err) =>
2917 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2917 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2918 good ()) 2918 good ())
2919 end 2919 end
3817 | _ => raise Fail "Unable to hnormSgn in functor application") 3817 | _ => raise Fail "Unable to hnormSgn in functor application")
3818 | _ => (strError env (NotFunctor sgn1); 3818 | _ => (strError env (NotFunctor sgn1);
3819 (strerror, sgnerror, [])) 3819 (strerror, sgnerror, []))
3820 end 3820 end
3821 3821
3822 fun resolveClass env = E.resolveClass (hnormCon env) (consEq env) env 3822 fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env
3823 3823
3824 fun elabFile basis topStr topSgn env file = 3824 fun elabFile basis topStr topSgn env file =
3825 let 3825 let
3826 val () = mayDelay := true 3826 val () = mayDelay := true
3827 val () = delayedUnifs := [] 3827 val () = delayedUnifs := []