Mercurial > urweb

comparison src/elaborate.sml @ 1000:5d7e05b4a5c0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Better subSgn error locations
author Adam Chlipala <adamc@hcoop.net>
date Thu, 15 Oct 2009 14:27:38 -0400
parents 6dd122f10c0c
children 4de35df3d545
comparison
equal deleted inserted replaced
999:8d821baac99e 1000:5d7e05b4a5c0
2514 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)] 2514 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
2515 | L'.DDatabase _ => [] 2515 | L'.DDatabase _ => []
2516 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] 2516 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
2517 | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)] 2517 | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)]
2518 2518
2519 and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) = 2519 and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
2520 ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1), 2520 ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1),
2521 ("sgn2", p_sgn env sgn2)];*) 2521 ("sgn2", p_sgn env sgn2)];*)
2522 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of 2522 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
2523 (L'.SgnError, _) => () 2523 (L'.SgnError, _) => ()
2524 | (_, L'.SgnError) => () 2524 | (_, L'.SgnError) => ()
2573 | SOME envs => envs 2573 | SOME envs => envs
2574 in 2574 in
2575 seek env sgis1 2575 seek env sgis1
2576 end 2576 end
2577 2577
2578 val seek = seek' (fn env => (sgnError env (UnmatchedSgi sgi2All); 2578 val seek = seek' (fn env => (sgnError env (UnmatchedSgi (strLoc, sgi2All));
2579 env)) 2579 env))
2580 in 2580 in
2581 case sgi of 2581 case sgi of
2582 L'.SgiConAbs (x, n2, k2) => 2582 L'.SgiConAbs (x, n2, k2) =>
2583 seek (fn (env, sgi1All as (sgi1, _)) => 2583 seek (fn (env, sgi1All as (sgi1, _)) =>
2585 fun found (x', n1, k1, co1) = 2585 fun found (x', n1, k1, co1) =
2586 if x = x' then 2586 if x = x' then
2587 let 2587 let
2588 val () = unifyKinds env k1 k2 2588 val () = unifyKinds env k1 k2
2589 handle KUnify (k1, k2, err) => 2589 handle KUnify (k1, k2, err) =>
2590 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) 2590 sgnError env (SgiWrongKind (strLoc, sgi1All, k1,
2591 sgi2All, k2, err))
2591 val env = E.pushCNamedAs env x n1 k1 co1 2592 val env = E.pushCNamedAs env x n1 k1 co1
2592 in 2593 in
2593 SOME (if n1 = n2 then 2594 SOME (if n1 = n2 then
2594 env 2595 env
2595 else 2596 else
2653 end 2654 end
2654 in 2655 in
2655 (unifyCons env loc c1 c2; 2656 (unifyCons env loc c1 c2;
2656 good ()) 2657 good ())
2657 handle CUnify (c1, c2, err) => 2658 handle CUnify (c1, c2, err) =>
2658 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2659 (sgnError env (SgiWrongCon (strLoc, sgi1All, c1,
2660 sgi2All, c2, err));
2659 good ()) 2661 good ())
2660 end 2662 end
2661 else 2663 else
2662 NONE 2664 NONE
2663 in 2665 in
2673 if x1 <> x2 then 2675 if x1 <> x2 then
2674 NONE 2676 NONE
2675 else 2677 else
2676 let 2678 let
2677 fun mismatched ue = 2679 fun mismatched ue =
2678 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue)); 2680 (sgnError env (SgiMismatchedDatatypes (strLoc, sgi1All, sgi2All, ue));
2679 SOME env) 2681 SOME env)
2680 2682
2681 val k = (L'.KType, loc) 2683 val k = (L'.KType, loc)
2682 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1 2684 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1
2683 2685
2778 end 2780 end
2779 in 2781 in
2780 (unifyCons env loc t1 t2; 2782 (unifyCons env loc t1 t2;
2781 good ()) 2783 good ())
2782 handle CUnify (c1, c2, err) => 2784 handle CUnify (c1, c2, err) =>
2783 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2785 (sgnError env (SgiWrongCon (strLoc, sgi1All, c1, sgi2All, c2, err));
2784 good ()) 2786 good ())
2785 end 2787 end
2786 else 2788 else
2787 NONE 2789 NONE
2788 2790
2799 ("c2", p_con env c2), 2801 ("c2", p_con env c2),
2800 ("c2'", p_con env (sub2 c2))];*) 2802 ("c2'", p_con env (sub2 c2))];*)
2801 unifyCons env loc c1 (sub2 c2); 2803 unifyCons env loc c1 (sub2 c2);
2802 SOME env) 2804 SOME env)
2803 handle CUnify (c1, c2, err) => 2805 handle CUnify (c1, c2, err) =>
2804 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2806 (sgnError env (SgiWrongCon (strLoc, sgi1All, c1, sgi2All, c2, err));
2805 SOME env) 2807 SOME env)
2806 else 2808 else
2807 NONE 2809 NONE
2808 | _ => NONE) 2810 | _ => NONE)
2809 2811
2811 seek (fn (env, sgi1All as (sgi1, _)) => 2813 seek (fn (env, sgi1All as (sgi1, _)) =>
2812 case sgi1 of 2814 case sgi1 of
2813 L'.SgiStr (x', n1, sgn1) => 2815 L'.SgiStr (x', n1, sgn1) =>
2814 if x = x' then 2816 if x = x' then
2815 let 2817 let
2816 val () = subSgn' counterparts env sgn1 sgn2 2818 val () = subSgn' counterparts env strLoc sgn1 sgn2
2817 val env = E.pushStrNamedAs env x n1 sgn1 2819 val env = E.pushStrNamedAs env x n1 sgn1
2818 val env = if n1 = n2 then 2820 val env = if n1 = n2 then
2819 env 2821 env
2820 else 2822 else
2821 E.pushStrNamedAs env x n2 2823 E.pushStrNamedAs env x n2
2832 seek (fn (env, sgi1All as (sgi1, _)) => 2834 seek (fn (env, sgi1All as (sgi1, _)) =>
2833 case sgi1 of 2835 case sgi1 of
2834 L'.SgiSgn (x', n1, sgn1) => 2836 L'.SgiSgn (x', n1, sgn1) =>
2835 if x = x' then 2837 if x = x' then
2836 let 2838 let
2837 val () = subSgn' counterparts env sgn1 sgn2 2839 val () = subSgn' counterparts env strLoc sgn1 sgn2
2838 val () = subSgn' counterparts env sgn2 sgn1 2840 val () = subSgn' counterparts env strLoc sgn2 sgn1
2839 2841
2840 val env = E.pushSgnNamedAs env x n2 sgn2 2842 val env = E.pushSgnNamedAs env x n2 sgn2
2841 val env = if n1 = n2 then 2843 val env = if n1 = n2 then
2842 env 2844 env
2843 else 2845 else
2867 fun found (x', n1, k1, co) = 2869 fun found (x', n1, k1, co) =
2868 if x = x' then 2870 if x = x' then
2869 let 2871 let
2870 val () = unifyKinds env k1 k2 2872 val () = unifyKinds env k1 k2
2871 handle KUnify (k1, k2, err) => 2873 handle KUnify (k1, k2, err) =>
2872 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) 2874 sgnError env (SgiWrongKind (strLoc, sgi1All, k1,
2875 sgi2All, k2, err))
2873 2876
2874 val env = E.pushCNamedAs env x n1 k1 co 2877 val env = E.pushCNamedAs env x n1 k1 co
2875 in 2878 in
2876 SOME (if n1 = n2 then 2879 SOME (if n1 = n2 then
2877 env 2880 env
2893 fun found (x', n1, k1, c1) = 2896 fun found (x', n1, k1, c1) =
2894 if x = x' then 2897 if x = x' then
2895 let 2898 let
2896 val () = unifyKinds env k1 k2 2899 val () = unifyKinds env k1 k2
2897 handle KUnify (k1, k2, err) => 2900 handle KUnify (k1, k2, err) =>
2898 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) 2901 sgnError env (SgiWrongKind (strLoc, sgi1All, k1,
2902 sgi2All, k2, err))
2899 2903
2900 val c2 = sub2 c2 2904 val c2 = sub2 c2
2901 2905
2902 fun good () = 2906 fun good () =
2903 let 2907 let
2912 end 2916 end
2913 in 2917 in
2914 (unifyCons env loc c1 c2; 2918 (unifyCons env loc c1 c2;
2915 good ()) 2919 good ())
2916 handle CUnify (c1, c2, err) => 2920 handle CUnify (c1, c2, err) =>
2917 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2921 (sgnError env (SgiWrongCon (strLoc, sgi1All, c1,
2922 sgi2All, c2, err));
2918 good ()) 2923 good ())
2919 end 2924 end
2920 else 2925 else
2921 NONE 2926 NONE
2922 in 2927 in
2935 if n1 = n2 then 2940 if n1 = n2 then
2936 ran2 2941 ran2
2937 else 2942 else
2938 subStrInSgn (n2, n1) ran2 2943 subStrInSgn (n2, n1) ran2
2939 in 2944 in
2940 subSgn' counterparts env dom2 dom1; 2945 subSgn' counterparts env strLoc dom2 dom1;
2941 subSgn' counterparts (E.pushStrNamedAs env m1 n1 dom2) ran1 ran2 2946 subSgn' counterparts (E.pushStrNamedAs env m1 n1 dom2) strLoc ran1 ran2
2942 end 2947 end
2943 2948
2944 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))) 2949 | _ => sgnError env (SgnWrongForm (strLoc, sgn1, sgn2)))
2945 2950
2946 and subSgn env = subSgn' (ref IM.empty) env 2951 and subSgn env = subSgn' (ref IM.empty) env
2947 2952
2948 and positive self = 2953 and positive self =
2949 let 2954 let
3403 | SOME (formal, gs1) => 3408 | SOME (formal, gs1) =>
3404 let 3409 let
3405 val str = wildifyStr env (str, formal) 3410 val str = wildifyStr env (str, formal)
3406 val (str', actual, gs2) = elabStr (env, denv) str 3411 val (str', actual, gs2) = elabStr (env, denv) str
3407 in 3412 in
3408 subSgn env (selfifyAt env {str = str', sgn = actual}) formal; 3413 subSgn env loc (selfifyAt env {str = str', sgn = actual}) formal;
3409 (str', formal, enD gs1 @ gs2) 3414 (str', formal, enD gs1 @ gs2)
3410 end 3415 end
3411 3416
3412 val (env', n) = E.pushStrNamed env x sgn' 3417 val (env', n) = E.pushStrNamed env x sgn'
3413 val denv' = 3418 val denv' =
3784 NONE => (actual, []) 3789 NONE => (actual, [])
3785 | SOME ran => 3790 | SOME ran =>
3786 let 3791 let
3787 val (ran', gs) = elabSgn (env', denv') ran 3792 val (ran', gs) = elabSgn (env', denv') ran
3788 in 3793 in
3789 subSgn env' actual ran'; 3794 subSgn env' loc actual ran';
3790 (ran', gs) 3795 (ran', gs)
3791 end 3796 end
3792 in 3797 in
3793 ((L'.StrFun (m, n, dom', formal, str'), loc), 3798 ((L'.StrFun (m, n, dom', formal, str'), loc),
3794 (L'.SgnFun (m, n, dom', formal), loc), 3799 (L'.SgnFun (m, n, dom', formal), loc),
3805 val (str2', sgn2, gs2) = elabStr (env, denv) str2 3810 val (str2', sgn2, gs2) = elabStr (env, denv) str2
3806 in 3811 in
3807 case #1 (hnormSgn env sgn1) of 3812 case #1 (hnormSgn env sgn1) of
3808 L'.SgnError => (strerror, sgnerror, []) 3813 L'.SgnError => (strerror, sgnerror, [])
3809 | L'.SgnFun (m, n, dom, ran) => 3814 | L'.SgnFun (m, n, dom, ran) =>
3810 (subSgn env sgn2 dom; 3815 (subSgn env loc sgn2 dom;
3811 case #1 (hnormSgn env ran) of 3816 case #1 (hnormSgn env ran) of
3812 L'.SgnError => (strerror, sgnerror, []) 3817 L'.SgnError => (strerror, sgnerror, [])
3813 | L'.SgnConst sgis => 3818 | L'.SgnConst sgis =>
3814 ((L'.StrApp (str1', str2'), loc), 3819 ((L'.StrApp (str1', str2'), loc),
3815 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc), 3820 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc),
3876 case resolveClass env c of 3881 case resolveClass env c of
3877 SOME e => r := SOME e 3882 SOME e => r := SOME e
3878 | NONE => expError env (Unresolvable (loc, c)) 3883 | NONE => expError env (Unresolvable (loc, c))
3879 end) gs 3884 end) gs
3880 3885
3881 val () = subSgn env' topSgn' topSgn 3886 val () = subSgn env' ErrorMsg.dummySpan topSgn' topSgn
3882 3887
3883 val (env', top_n) = E.pushStrNamed env' "Top" topSgn 3888 val (env', top_n) = E.pushStrNamed env' "Top" topSgn
3884 val () = top_r := top_n 3889 val () = top_r := top_n
3885 3890
3886 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} 3891 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}