Mercurial > urweb

comparison src/elaborate.sml @ 493:ae03d09043c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add CutMulti
author Adam Chlipala <adamc@hcoop.net>
date Tue, 11 Nov 2008 19:20:37 -0500
parents 40c737913075
children 5fc269f744ee
comparison
equal deleted inserted replaced
492:4a241d108a2c 493:ae03d09043c1
1660 checkCon (env, denv) e' et 1660 checkCon (env, denv) e' et
1661 (L'.TRecord (L'.CConcat (first, rest), loc), loc) 1661 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
1662 val gs4 = D.prove env denv (first, rest, loc) 1662 val gs4 = D.prove env denv (first, rest, loc)
1663 in 1663 in
1664 ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), 1664 ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc),
1665 gs1 @ enD gs2 @ enD gs3 @ enD gs4)
1666 end
1667 | L.ECutMulti (e, c) =>
1668 let
1669 val (e', et, gs1) = elabExp (env, denv) e
1670 val (c', ck, gs2) = elabCon (env, denv) c
1671
1672 val rest = cunif (loc, ktype_record)
1673
1674 val gs3 =
1675 checkCon (env, denv) e' et
1676 (L'.TRecord (L'.CConcat (c', rest), loc), loc)
1677 val gs4 = D.prove env denv (c', rest, loc)
1678 in
1679 ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc),
1665 gs1 @ enD gs2 @ enD gs3 @ enD gs4) 1680 gs1 @ enD gs2 @ enD gs3 @ enD gs4)
1666 end 1681 end
1667 1682
1668 | L.EFold => 1683 | L.EFold =>
1669 let 1684 let
2692 case #1 (hnormSgn env sgn) of 2707 case #1 (hnormSgn env sgn) of
2693 L'.SgnConst sgis => 2708 L'.SgnConst sgis =>
2694 (case #1 str of 2709 (case #1 str of
2695 L.StrConst ds => 2710 L.StrConst ds =>
2696 let 2711 let
2712 fun decompileKind (k, loc) =
2713 case k of
2714 L'.KType => SOME (L.KType, loc)
2715 | L'.KArrow (k1, k2) =>
2716 (case (decompileKind k1, decompileKind k2) of
2717 (SOME k1, SOME k2) => SOME (L.KArrow (k1, k2), loc)
2718 | _ => NONE)
2719 | L'.KName => SOME (L.KName, loc)
2720 | L'.KRecord k =>
2721 (case decompileKind k of
2722 SOME k => SOME (L.KRecord k, loc)
2723 | _ => NONE)
2724 | L'.KUnit => SOME (L.KUnit, loc)
2725 | L'.KTuple ks =>
2726 let
2727 val ks' = List.mapPartial decompileKind ks
2728 in
2729 if length ks' = length ks then
2730 SOME (L.KTuple ks', loc)
2731 else
2732 NONE
2733 end
2734
2735 | L'.KError => NONE
2736 | L'.KUnif (_, _, ref (SOME k)) => decompileKind k
2737 | L'.KUnif _ => NONE
2738
2697 fun decompileCon env (c, loc) = 2739 fun decompileCon env (c, loc) =
2698 case c of 2740 case c of
2699 L'.CRel i => 2741 L'.CRel i =>
2700 let 2742 let
2701 val (s, _) = E.lookupCRel env i 2743 val (s, _) = E.lookupCRel env i
2739 val (neededC, constraints, neededV, _) = 2781 val (neededC, constraints, neededV, _) =
2740 foldl (fn ((sgi, loc), (neededC, constraints, neededV, env')) => 2782 foldl (fn ((sgi, loc), (neededC, constraints, neededV, env')) =>
2741 let 2783 let
2742 val (needed, constraints, neededV) = 2784 val (needed, constraints, neededV) =
2743 case sgi of 2785 case sgi of
2744 L'.SgiConAbs (x, _, _) => (SS.add (neededC, x), constraints, neededV) 2786 L'.SgiConAbs (x, _, k) => (SM.insert (neededC, x, k), constraints, neededV)
2745 | L'.SgiConstraint cs => (neededC, (env', cs, loc) :: constraints, neededV) 2787 | L'.SgiConstraint cs => (neededC, (env', cs, loc) :: constraints, neededV)
2746 2788
2747 | L'.SgiVal (x, _, t) => 2789 | L'.SgiVal (x, _, t) =>
2748 let 2790 let
2749 fun default () = (neededC, constraints, neededV) 2791 fun default () = (neededC, constraints, neededV)
2762 2804
2763 | _ => (neededC, constraints, neededV) 2805 | _ => (neededC, constraints, neededV)
2764 in 2806 in
2765 (needed, constraints, neededV, E.sgiBinds env' (sgi, loc)) 2807 (needed, constraints, neededV, E.sgiBinds env' (sgi, loc))
2766 end) 2808 end)
2767 (SS.empty, [], SS.empty, env) sgis 2809 (SM.empty, [], SS.empty, env) sgis
2768 2810
2769 val (neededC, neededV) = foldl (fn ((d, _), needed as (neededC, neededV)) => 2811 val (neededC, neededV) = foldl (fn ((d, _), needed as (neededC, neededV)) =>
2770 case d of 2812 case d of
2771 L.DCon (x, _, _) => ((SS.delete (neededC, x), neededV) 2813 L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
2772 handle NotFound => 2814 handle NotFound =>
2773 needed) 2815 needed)
2774 | L.DClass (x, _) => ((SS.delete (neededC, x), neededV) 2816 | L.DClass (x, _) => ((#1 (SM.remove (neededC, x)), neededV)
2775 handle NotFound => needed) 2817 handle NotFound => needed)
2776 | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x)) 2818 | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x))
2777 handle NotFound => needed) 2819 handle NotFound => needed)
2778 | L.DOpen _ => (SS.empty, SS.empty) 2820 | L.DOpen _ => (SM.empty, SS.empty)
2779 | _ => needed) 2821 | _ => needed)
2780 (neededC, neededV) ds 2822 (neededC, neededV) ds
2781 2823
2782 val ds' = List.mapPartial (fn (env', (c1, c2), loc) => 2824 val ds' = List.mapPartial (fn (env', (c1, c2), loc) =>
2783 case (decompileCon env' c1, decompileCon env' c2) of 2825 case (decompileCon env' c1, decompileCon env' c2) of
2795 in 2837 in
2796 ds'' @ ds' 2838 ds'' @ ds'
2797 end 2839 end
2798 2840
2799 val ds' = 2841 val ds' =
2800 case SS.listItems neededC of 2842 case SM.listItemsi neededC of
2801 [] => ds' 2843 [] => ds'
2802 | xs => 2844 | xs =>
2803 let 2845 let
2804 val kwild = (L.KWild, #2 str) 2846 val ds'' = map (fn (x, k) =>
2805 val cwild = (L.CWild kwild, #2 str) 2847 let
2806 val ds'' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs 2848 val k =
2849 case decompileKind k of
2850 NONE => (L.KWild, #2 str)
2851 | SOME k => k
2852 val cwild = (L.CWild k, #2 str)
2853 in
2854 (L.DCon (x, NONE, cwild), #2 str)
2855 end) xs
2807 in 2856 in
2808 ds'' @ ds' 2857 ds'' @ ds'
2809 end 2858 end
2810 in 2859 in
2811 (L.StrConst (ds @ ds'), #2 str) 2860 (L.StrConst (ds @ ds'), #2 str)