Mercurial > urweb

comparison src/elaborate.sml @ 838:5154a047c6bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Lexing some more string escape sequences; JS versions of number read; fix problem with signature unification; escape < more often in Jscomp
author Adam Chlipala <adamc@hcoop.net>
date Tue, 02 Jun 2009 19:28:25 -0400
parents ccf22c2c77b2
children b2413e4dd109
comparison
equal deleted inserted replaced
837:ccf22c2c77b2 838:5154a047c6bc
156 str (chr (ord #"A" + n)) 156 str (chr (ord #"A" + n))
157 else 157 else
158 "U" ^ Int.toString (n - 26) 158 "U" ^ Int.toString (n - 26)
159 in 159 in
160 count := n + 1; 160 count := n + 1;
161 (L'.KUnif (loc, s, ref NONE), dummy) 161 (L'.KUnif (loc, s, ref NONE), loc)
162 end 162 end
163 163
164 end 164 end
165 165
166 local 166 local
176 str (chr (ord #"A" + n)) 176 str (chr (ord #"A" + n))
177 else 177 else
178 "U" ^ Int.toString (n - 26) 178 "U" ^ Int.toString (n - 26)
179 in 179 in
180 count := n + 1; 180 count := n + 1;
181 (L'.CUnif (loc, k, s, ref NONE), dummy) 181 (L'.CUnif (loc, k, s, ref NONE), loc)
182 end 182 end
183 183
184 end 184 end
185 185
186 fun elabKind env (k, loc) = 186 fun elabKind env (k, loc) =
774 empties) 774 empties)
775 end 775 end
776 | orig as ([(_, r1 as ref NONE)], _, [], [(_, r2 as ref NONE)], _, []) => 776 | orig as ([(_, r1 as ref NONE)], _, [], [(_, r2 as ref NONE)], _, []) =>
777 if List.all (fn (x1, _) => List.all (fn (x2, _) => consNeq env (x1, x2)) fs2) fs1 then 777 if List.all (fn (x1, _) => List.all (fn (x2, _) => consNeq env (x1, x2)) fs2) fs1 then
778 let 778 let
779 val kr = (L'.KRecord k, dummy) 779 val kr = (L'.KRecord k, loc)
780 val u = cunif (loc, kr) 780 val u = cunif (loc, kr)
781 in 781 in
782 r1 := SOME (L'.CConcat ((L'.CRecord (k, fs2), loc), u), loc); 782 r1 := SOME (L'.CConcat ((L'.CRecord (k, fs2), loc), u), loc);
783 r2 := SOME (L'.CConcat ((L'.CRecord (k, fs1), loc), u), loc); 783 r2 := SOME (L'.CConcat ((L'.CRecord (k, fs1), loc), u), loc);
784 empties 784 empties
815 | _ => (fs1, fs2, others1, others2, unifs1, unifs2) 815 | _ => (fs1, fs2, others1, others2, unifs1, unifs2)
816 816
817 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), 817 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
818 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 818 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
819 819
820 val empty = (L'.CRecord (k, []), dummy) 820 val empty = (L'.CRecord (k, []), loc)
821 fun failure () = raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2)) 821 fun failure () = raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
822 in 822 in
823 (case (unifs1, fs1, others1, unifs2, fs2, others2) of 823 (case (unifs1, fs1, others1, unifs2, fs2, others2) of
824 (_, [], [], [], [], []) => 824 (_, [], [], [], [], []) =>
825 app (fn (_, r) => r := SOME empty) unifs1 825 app (fn (_, r) => r := SOME empty) unifs1
1650 val (e1', t1, gs1) = elabExp (env, denv) e1 1650 val (e1', t1, gs1) = elabExp (env, denv) e1
1651 val (e2', t2, gs2) = elabExp (env, denv) e2 1651 val (e2', t2, gs2) = elabExp (env, denv) e2
1652 1652
1653 val dom = cunif (loc, ktype) 1653 val dom = cunif (loc, ktype)
1654 val ran = cunif (loc, ktype) 1654 val ran = cunif (loc, ktype)
1655 val t = (L'.TFun (dom, ran), dummy) 1655 val t = (L'.TFun (dom, ran), loc)
1656 in 1656 in
1657 checkCon env e1' t1 t; 1657 checkCon env e1' t1 t;
1658 checkCon env e2' t2 dom; 1658 checkCon env e2' t2 dom;
1659 ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2) 1659 ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2)
1660 end 1660 end
2505 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)] 2505 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
2506 | L'.DDatabase _ => [] 2506 | L'.DDatabase _ => []
2507 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] 2507 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
2508 | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)] 2508 | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)]
2509 2509
2510 and subSgn env sgn1 (sgn2 as (_, loc2)) = 2510 and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
2511 ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1), 2511 ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1),
2512 ("sgn2", p_sgn env sgn2)];*) 2512 ("sgn2", p_sgn env sgn2)];*)
2513 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of 2513 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
2514 (L'.SgnError, _) => () 2514 (L'.SgnError, _) => ()
2515 | (_, L'.SgnError) => () 2515 | (_, L'.SgnError) => ()
2518 let 2518 let
2519 (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1), 2519 (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1),
2520 ("sgn2", p_sgn env sgn2), 2520 ("sgn2", p_sgn env sgn2),
2521 ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)), 2521 ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)),
2522 ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*) 2522 ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*)
2523
2524 fun cpart n = IM.find (!counterparts, n)
2525 fun cparts (n2, n1) = counterparts := IM.insert (!counterparts, n2, n1)
2526
2527 val sub2 = U.Con.map {kind = fn k => k,
2528 con = fn c =>
2529 case c of
2530 L'.CNamed n2 =>
2531 (case cpart n2 of
2532 NONE => c
2533 | SOME n1 => L'.CNamed n1)
2534 | _ => c}
2523 2535
2524 fun folder (sgi2All as (sgi, loc), env) = 2536 fun folder (sgi2All as (sgi, loc), env) =
2525 let 2537 let
2526 (*val () = prefaces "folder" [("sgis1", p_sgn env (L'.SgnConst sgis1, loc2))]*) 2538 (*val () = prefaces "folder" [("sgis1", p_sgn env (L'.SgnConst sgis1, loc2))]*)
2527 2539
2570 val env = E.pushCNamedAs env x n1 k1 co1 2582 val env = E.pushCNamedAs env x n1 k1 co1
2571 in 2583 in
2572 SOME (if n1 = n2 then 2584 SOME (if n1 = n2 then
2573 env 2585 env
2574 else 2586 else
2575 E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2))) 2587 (cparts (n2, n1);
2588 E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2))))
2576 end 2589 end
2577 else 2590 else
2578 NONE 2591 NONE
2579 in 2592 in
2580 case sgi1 of 2593 case sgi1 of
2614 seek (fn (env, sgi1All as (sgi1, _)) => 2627 seek (fn (env, sgi1All as (sgi1, _)) =>
2615 let 2628 let
2616 fun found (x', n1, k1, c1) = 2629 fun found (x', n1, k1, c1) =
2617 if x = x' then 2630 if x = x' then
2618 let 2631 let
2632 val c2 = sub2 c2
2633
2619 fun good () = 2634 fun good () =
2620 let 2635 let
2621 val env = E.pushCNamedAs env x n2 k2 (SOME c2) 2636 val env = E.pushCNamedAs env x n2 k2 (SOME c2)
2622 val env = if n1 = n2 then 2637 val env = if n1 = n2 then
2623 env 2638 env
2660 let 2675 let
2661 val env = E.sgiBinds env sgi1All 2676 val env = E.sgiBinds env sgi1All
2662 val env = if n1 = n2 then 2677 val env = if n1 = n2 then
2663 env 2678 env
2664 else 2679 else
2665 E.pushCNamedAs env x1 n2 k' 2680 (cparts (n2, n1);
2666 (SOME (L'.CNamed n1, loc)) 2681 E.pushCNamedAs env x1 n2 k'
2682 (SOME (L'.CNamed n1, loc)))
2667 in 2683 in
2668 SOME env 2684 SOME env
2669 end 2685 end
2670 2686
2671 val env = E.pushCNamedAs env x1 n1 k' NONE 2687 val env = E.pushCNamedAs env x1 n1 k' NONE
2672 val env = if n1 = n2 then 2688 val env = if n1 = n2 then
2673 env 2689 env
2674 else 2690 else
2675 E.pushCNamedAs env x1 n2 k' (SOME (L'.CNamed n1, loc)) 2691 (cparts (n2, n1);
2692 E.pushCNamedAs env x1 n2 k' (SOME (L'.CNamed n1, loc)))
2676 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1 2693 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1
2677 fun xncBad ((x1, _, t1), (x2, _, t2)) = 2694 fun xncBad ((x1, _, t1), (x2, _, t2)) =
2678 String.compare (x1, x2) <> EQUAL 2695 String.compare (x1, x2) <> EQUAL
2679 orelse case (t1, t2) of 2696 orelse case (t1, t2) of
2680 (NONE, NONE) => false 2697 (NONE, NONE) => false
2681 | (SOME t1, SOME t2) => 2698 | (SOME t1, SOME t2) =>
2682 (unifyCons env t1 t2; false) 2699 (unifyCons env t1 (sub2 t2); false)
2683 | _ => true 2700 | _ => true
2684 in 2701 in
2685 (if xs1 <> xs2 2702 (if xs1 <> xs2
2686 orelse length xncs1 <> length xncs2 2703 orelse length xncs1 <> length xncs2
2687 orelse ListPair.exists xncBad (xncs1, xncs2) then 2704 orelse ListPair.exists xncBad (xncs1, xncs2) then
2744 fun good () = 2761 fun good () =
2745 let 2762 let
2746 val env = E.pushCNamedAs env x n1 k' (SOME t1) 2763 val env = E.pushCNamedAs env x n1 k' (SOME t1)
2747 val env = E.pushCNamedAs env x n2 k' (SOME t2) 2764 val env = E.pushCNamedAs env x n2 k' (SOME t2)
2748 in 2765 in
2766 cparts (n2, n1);
2749 SOME env 2767 SOME env
2750 end 2768 end
2751 in 2769 in
2752 (unifyCons env t1 t2; 2770 (unifyCons env t1 t2;
2753 good ()) 2771 good ())
2763 | L'.SgiVal (x, n2, c2) => 2781 | L'.SgiVal (x, n2, c2) =>
2764 seek (fn (env, sgi1All as (sgi1, _)) => 2782 seek (fn (env, sgi1All as (sgi1, _)) =>
2765 case sgi1 of 2783 case sgi1 of
2766 L'.SgiVal (x', n1, c1) => 2784 L'.SgiVal (x', n1, c1) =>
2767 if x = x' then 2785 if x = x' then
2768 (unifyCons env c1 c2; 2786 ((*prefaces "val" [("x", PD.string x),
2787 ("n1", PD.string (Int.toString n1)),
2788 ("c1", p_con env c1),
2789 ("c2", p_con env c2),
2790 ("c2'", p_con env (sub2 c2))];*)
2791 unifyCons env c1 (sub2 c2);
2769 SOME env) 2792 SOME env)
2770 handle CUnify (c1, c2, err) => 2793 handle CUnify (c1, c2, err) =>
2771 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2794 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2772 SOME env) 2795 SOME env)
2773 else 2796 else
2778 seek (fn (env, sgi1All as (sgi1, _)) => 2801 seek (fn (env, sgi1All as (sgi1, _)) =>
2779 case sgi1 of 2802 case sgi1 of
2780 L'.SgiStr (x', n1, sgn1) => 2803 L'.SgiStr (x', n1, sgn1) =>
2781 if x = x' then 2804 if x = x' then
2782 let 2805 let
2783 val () = subSgn env sgn1 sgn2 2806 val () = subSgn' counterparts env sgn1 sgn2
2784 val env = E.pushStrNamedAs env x n1 sgn1 2807 val env = E.pushStrNamedAs env x n1 sgn1
2785 val env = if n1 = n2 then 2808 val env = if n1 = n2 then
2786 env 2809 env
2787 else 2810 else
2788 E.pushStrNamedAs env x n2 2811 E.pushStrNamedAs env x n2
2799 seek (fn (env, sgi1All as (sgi1, _)) => 2822 seek (fn (env, sgi1All as (sgi1, _)) =>
2800 case sgi1 of 2823 case sgi1 of
2801 L'.SgiSgn (x', n1, sgn1) => 2824 L'.SgiSgn (x', n1, sgn1) =>
2802 if x = x' then 2825 if x = x' then
2803 let 2826 let
2804 val () = subSgn env sgn1 sgn2 2827 val () = subSgn' counterparts env sgn1 sgn2
2805 val () = subSgn env sgn2 sgn1 2828 val () = subSgn' counterparts env sgn2 sgn1
2806 2829
2807 val env = E.pushSgnNamedAs env x n2 sgn2 2830 val env = E.pushSgnNamedAs env x n2 sgn2
2808 val env = if n1 = n2 then 2831 val env = if n1 = n2 then
2809 env 2832 env
2810 else 2833 else
2811 E.pushSgnNamedAs env x n1 sgn2 2834 (cparts (n2, n1);
2835 E.pushSgnNamedAs env x n1 sgn2)
2812 in 2836 in
2813 SOME env 2837 SOME env
2814 end 2838 end
2815 else 2839 else
2816 NONE 2840 NONE
2839 val env = E.pushCNamedAs env x n1 k1 co 2863 val env = E.pushCNamedAs env x n1 k1 co
2840 in 2864 in
2841 SOME (if n1 = n2 then 2865 SOME (if n1 = n2 then
2842 env 2866 env
2843 else 2867 else
2844 E.pushCNamedAs env x n2 k1 (SOME (L'.CNamed n1, loc2))) 2868 (cparts (n2, n1);
2869 E.pushCNamedAs env x n2 k1 (SOME (L'.CNamed n1, loc2))))
2845 end 2870 end
2846 else 2871 else
2847 NONE 2872 NONE
2848 in 2873 in
2849 case sgi1 of 2874 case sgi1 of
2858 if x = x' then 2883 if x = x' then
2859 let 2884 let
2860 val () = unifyKinds env k1 k2 2885 val () = unifyKinds env k1 k2
2861 handle KUnify (k1, k2, err) => 2886 handle KUnify (k1, k2, err) =>
2862 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) 2887 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
2888
2889 val c2 = sub2 c2
2863 2890
2864 fun good () = 2891 fun good () =
2865 let 2892 let
2866 val env = E.pushCNamedAs env x n2 k2 (SOME c2) 2893 val env = E.pushCNamedAs env x n2 k2 (SOME c2)
2867 val env = if n1 = n2 then 2894 val env = if n1 = n2 then
2896 if n1 = n2 then 2923 if n1 = n2 then
2897 ran2 2924 ran2
2898 else 2925 else
2899 subStrInSgn (n2, n1) ran2 2926 subStrInSgn (n2, n1) ran2
2900 in 2927 in
2901 subSgn env dom2 dom1; 2928 subSgn' counterparts env dom2 dom1;
2902 subSgn (E.pushStrNamedAs env m1 n1 dom2) ran1 ran2 2929 subSgn' counterparts (E.pushStrNamedAs env m1 n1 dom2) ran1 ran2
2903 end 2930 end
2904 2931
2905 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))) 2932 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)))
2906 2933
2934 and subSgn env = subSgn' (ref IM.empty) env
2907 2935
2908 and positive self = 2936 and positive self =
2909 let 2937 let
2910 open L 2938 open L
2911 2939