Mercurial > urweb

comparison src/elaborate.sml @ 255:69d337f186eb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Monoized GROUP BY
author Adam Chlipala <adamc@hcoop.net>
date Sun, 31 Aug 2008 15:04:10 -0400
parents b6b75e6e0898
children e52243e20858
comparison
equal deleted inserted replaced
254:f8d9395575ec 255:69d337f186eb
1679 end 1679 end
1680 1680
1681 val gsD = List.mapPartial (fn Disjoint d => SOME d | _ => NONE) gs 1681 val gsD = List.mapPartial (fn Disjoint d => SOME d | _ => NONE) gs
1682 val gsO = List.filter (fn Disjoint _ => false | _ => true) gs 1682 val gsO = List.filter (fn Disjoint _ => false | _ => true) gs
1683 in 1683 in
1684 (*TextIO.print ("|gsO| = " ^ Int.toString (length gsO) ^ "\n");*)
1684 ((L'.ERecord xes', loc), 1685 ((L'.ERecord xes', loc),
1685 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc), 1686 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
1686 enD (prove (xes', gsD)) @ gsO) 1687 enD (prove (xes', gsD)) @ gsO)
1687 end 1688 end
1688 1689
2727 2728
2728 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)) 2729 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
2729 2730
2730 2731
2731 fun elabDecl ((d, loc), (env, denv, gs : constraint list)) = 2732 fun elabDecl ((d, loc), (env, denv, gs : constraint list)) =
2732 case d of 2733 let
2733 L.DCon (x, ko, c) => 2734 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
2734 let 2735
2735 val k' = case ko of 2736 val r =
2736 NONE => kunif loc 2737 case d of
2737 | SOME k => elabKind k 2738 L.DCon (x, ko, c) =>
2738 2739 let
2739 val (c', ck, gs') = elabCon (env, denv) c 2740 val k' = case ko of
2740 val (env', n) = E.pushCNamed env x k' (SOME c') 2741 NONE => kunif loc
2741 in 2742 | SOME k => elabKind k
2742 checkKind env c' ck k'; 2743
2743 2744 val (c', ck, gs') = elabCon (env, denv) c
2744 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs)) 2745 val (env', n) = E.pushCNamed env x k' (SOME c')
2745 end 2746 in
2746 | L.DDatatype (x, xs, xcs) => 2747 checkKind env c' ck k';
2747 let 2748
2748 val k = (L'.KType, loc) 2749 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs))
2749 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs 2750 end
2750 val (env, n) = E.pushCNamed env x k' NONE 2751 | L.DDatatype (x, xs, xcs) =>
2751 val t = (L'.CNamed n, loc) 2752 let
2752 val nxs = length xs - 1 2753 val k = (L'.KType, loc)
2753 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs 2754 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
2754 2755 val (env, n) = E.pushCNamed env x k' NONE
2755 val (env', denv') = foldl (fn (x, (env', denv')) => 2756 val t = (L'.CNamed n, loc)
2756 (E.pushCRel env' x k, 2757 val nxs = length xs - 1
2757 D.enter denv')) (env, denv) xs 2758 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
2758 2759
2759 val (xcs, (used, env, gs)) = 2760 val (env', denv') = foldl (fn (x, (env', denv')) =>
2760 ListUtil.foldlMap 2761 (E.pushCRel env' x k,
2761 (fn ((x, to), (used, env, gs)) => 2762 D.enter denv')) (env, denv) xs
2762 let 2763
2763 val (to, t, gs') = case to of 2764 val (xcs, (used, env, gs')) =
2764 NONE => (NONE, t, gs) 2765 ListUtil.foldlMap
2765 | SOME t' => 2766 (fn ((x, to), (used, env, gs)) =>
2766 let 2767 let
2767 val (t', tk, gs') = elabCon (env', denv') t' 2768 val (to, t, gs') = case to of
2768 in 2769 NONE => (NONE, t, gs)
2769 checkKind env' t' tk k; 2770 | SOME t' =>
2770 (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs) 2771 let
2771 end 2772 val (t', tk, gs') = elabCon (env', denv') t'
2772 val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs 2773 in
2773 2774 checkKind env' t' tk k;
2774 val (env, n') = E.pushENamed env x t 2775 (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs)
2775 in 2776 end
2776 if SS.member (used, x) then 2777 val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
2777 strError env (DuplicateConstructor (x, loc)) 2778
2778 else 2779 val (env, n') = E.pushENamed env x t
2779 (); 2780 in
2780 ((x, n', to), (SS.add (used, x), env, gs')) 2781 if SS.member (used, x) then
2781 end) 2782 strError env (DuplicateConstructor (x, loc))
2782 (SS.empty, env, []) xcs 2783 else
2783 2784 ();
2784 val env = E.pushDatatype env n xs xcs 2785 ((x, n', to), (SS.add (used, x), env, gs'))
2785 in 2786 end)
2786 ([(L'.DDatatype (x, n, xs, xcs), loc)], (env, denv, gs)) 2787 (SS.empty, env, []) xcs
2787 end 2788
2788 2789 val env = E.pushDatatype env n xs xcs
2789 | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp" 2790 in
2790 2791 ([(L'.DDatatype (x, n, xs, xcs), loc)], (env, denv, gs' @ gs))
2791 | L.DDatatypeImp (x, m1 :: ms, s) => 2792 end
2792 (case E.lookupStr env m1 of 2793
2793 NONE => (expError env (UnboundStrInExp (loc, m1)); 2794 | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
2794 ([], (env, denv, gs))) 2795
2795 | SOME (n, sgn) => 2796 | L.DDatatypeImp (x, m1 :: ms, s) =>
2796 let 2797 (case E.lookupStr env m1 of
2797 val (str, sgn) = foldl (fn (m, (str, sgn)) => 2798 NONE => (expError env (UnboundStrInExp (loc, m1));
2798 case E.projectStr env {sgn = sgn, str = str, field = m} of 2799 ([], (env, denv, gs)))
2799 NONE => (conError env (UnboundStrInCon (loc, m)); 2800 | SOME (n, sgn) =>
2800 (strerror, sgnerror)) 2801 let
2801 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) 2802 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
2802 ((L'.StrVar n, loc), sgn) ms 2803 case E.projectStr env {sgn = sgn, str = str, field = m} of
2803 in 2804 NONE => (conError env (UnboundStrInCon (loc, m));
2804 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of 2805 (strerror, sgnerror))
2805 ((L'.CModProj (n, ms, s), _), gs') => 2806 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
2806 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of 2807 ((L'.StrVar n, loc), sgn) ms
2807 NONE => (conError env (UnboundDatatype (loc, s)); 2808 in
2808 ([], (env, denv, gs))) 2809 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
2809 | SOME (xs, xncs) => 2810 ((L'.CModProj (n, ms, s), _), gs') =>
2810 let 2811 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
2811 val k = (L'.KType, loc) 2812 NONE => (conError env (UnboundDatatype (loc, s));
2812 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs 2813 ([], (env, denv, gs)))
2813 val t = (L'.CModProj (n, ms, s), loc) 2814 | SOME (xs, xncs) =>
2814 val (env, n') = E.pushCNamed env x k' (SOME t) 2815 let
2815 val env = E.pushDatatype env n' xs xncs 2816 val k = (L'.KType, loc)
2816 2817 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
2817 val t = (L'.CNamed n', loc) 2818 val t = (L'.CModProj (n, ms, s), loc)
2818 val env = foldl (fn ((x, n, to), env) => 2819 val (env, n') = E.pushCNamed env x k' (SOME t)
2819 let 2820 val env = E.pushDatatype env n' xs xncs
2820 val t = case to of 2821
2821 NONE => t 2822 val t = (L'.CNamed n', loc)
2822 | SOME t' => (L'.TFun (t', t), loc) 2823 val env = foldl (fn ((x, n, to), env) =>
2823 2824 let
2824 val t = foldr (fn (x, t) => 2825 val t = case to of
2825 (L'.TCFun (L'.Implicit, x, k, t), loc)) 2826 NONE => t
2826 t xs 2827 | SOME t' => (L'.TFun (t', t), loc)
2827 in 2828
2828 E.pushENamedAs env x n t 2829 val t = foldr (fn (x, t) =>
2829 end) env xncs 2830 (L'.TCFun (L'.Implicit, x, k, t), loc))
2830 in 2831 t xs
2831 ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, enD gs' @ gs)) 2832 in
2832 end) 2833 E.pushENamedAs env x n t
2833 | _ => (strError env (NotDatatype loc); 2834 end) env xncs
2834 ([], (env, denv, []))) 2835 in
2835 end) 2836 ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, enD gs' @ gs))
2836 2837 end)
2837 | L.DVal (x, co, e) => 2838 | _ => (strError env (NotDatatype loc);
2838 let 2839 ([], (env, denv, [])))
2839 val (c', _, gs1) = case co of 2840 end)
2840 NONE => (cunif (loc, ktype), ktype, []) 2841
2841 | SOME c => elabCon (env, denv) c 2842 | L.DVal (x, co, e) =>
2842 2843 let
2843 val (e', et, gs2) = elabExp (env, denv) e 2844 val (c', _, gs1) = case co of
2844 val gs3 = checkCon (env, denv) e' et c' 2845 NONE => (cunif (loc, ktype), ktype, [])
2845 val (c', gs4) = normClassConstraint (env, denv) c' 2846 | SOME c => elabCon (env, denv) c
2846 val (env', n) = E.pushENamed env x c' 2847
2847 in 2848 val (e', et, gs2) = elabExp (env, denv) e
2848 (*prefaces "DVal" [("x", Print.PD.string x), 2849 val gs3 = checkCon (env, denv) e' et c'
2849 ("c'", p_con env c')];*) 2850 val (c', gs4) = normClassConstraint (env, denv) c'
2850 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs)) 2851 val (env', n) = E.pushENamed env x c'
2851 end 2852 in
2852 | L.DValRec vis => 2853 (*prefaces "DVal" [("x", Print.PD.string x),
2853 let 2854 ("c'", p_con env c')];*)
2854 fun allowable (e, _) = 2855 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs))
2855 case e of 2856 end
2856 L.EAbs _ => true 2857 | L.DValRec vis =>
2857 | L.ECAbs (_, _, _, e) => allowable e 2858 let
2858 | L.EDisjoint (_, _, e) => allowable e 2859 fun allowable (e, _) =
2859 | _ => false 2860 case e of
2860 2861 L.EAbs _ => true
2861 val (vis, gs) = ListUtil.foldlMap 2862 | L.ECAbs (_, _, _, e) => allowable e
2862 (fn ((x, co, e), gs) => 2863 | L.EDisjoint (_, _, e) => allowable e
2863 let 2864 | _ => false
2864 val (c', _, gs1) = case co of 2865
2865 NONE => (cunif (loc, ktype), ktype, []) 2866 val (vis, gs) = ListUtil.foldlMap
2866 | SOME c => elabCon (env, denv) c 2867 (fn ((x, co, e), gs) =>
2867 in 2868 let
2868 ((x, c', e), enD gs1 @ gs) 2869 val (c', _, gs1) = case co of
2869 end) [] vis 2870 NONE => (cunif (loc, ktype), ktype, [])
2870 2871 | SOME c => elabCon (env, denv) c
2871 val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) => 2872 in
2872 let 2873 ((x, c', e), enD gs1 @ gs)
2873 val (env, n) = E.pushENamed env x c' 2874 end) [] vis
2874 in 2875
2875 ((x, n, c', e), env) 2876 val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>
2876 end) env vis 2877 let
2877 2878 val (env, n) = E.pushENamed env x c'
2878 val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) => 2879 in
2879 let 2880 ((x, n, c', e), env)
2880 val (e', et, gs1) = elabExp (env, denv) e 2881 end) env vis
2881 2882
2882 val gs2 = checkCon (env, denv) e' et c' 2883 val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) =>
2883 in 2884 let
2884 if allowable e then 2885 val (e', et, gs1) = elabExp (env, denv) e
2885 () 2886
2886 else 2887 val gs2 = checkCon (env, denv) e' et c'
2887 expError env (IllegalRec (x, e')); 2888 in
2888 ((x, n, c', e'), gs1 @ enD gs2 @ gs) 2889 if allowable e then
2889 end) gs vis 2890 ()
2890 in 2891 else
2891 ([(L'.DValRec vis, loc)], (env, denv, gs)) 2892 expError env (IllegalRec (x, e'));
2892 end 2893 ((x, n, c', e'), gs1 @ enD gs2 @ gs)
2893 2894 end) gs vis
2894 | L.DSgn (x, sgn) => 2895 in
2895 let 2896 ([(L'.DValRec vis, loc)], (env, denv, gs))
2896 val (sgn', gs') = elabSgn (env, denv) sgn 2897 end
2897 val (env', n) = E.pushSgnNamed env x sgn' 2898
2898 in 2899 | L.DSgn (x, sgn) =>
2899 ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs)) 2900 let
2900 end 2901 val (sgn', gs') = elabSgn (env, denv) sgn
2901 2902 val (env', n) = E.pushSgnNamed env x sgn'
2902 | L.DStr (x, sgno, str) => 2903 in
2903 let 2904 ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
2904 val () = if x = "Basis" then 2905 end
2905 raise Fail "Not allowed to redefine structure 'Basis'" 2906
2906 else 2907 | L.DStr (x, sgno, str) =>
2907 () 2908 let
2908 2909 val () = if x = "Basis" then
2909 val formal = Option.map (elabSgn (env, denv)) sgno 2910 raise Fail "Not allowed to redefine structure 'Basis'"
2910 2911 else
2911 val (str', sgn', gs') = 2912 ()
2912 case formal of 2913
2913 NONE => 2914 val formal = Option.map (elabSgn (env, denv)) sgno
2914 let 2915
2915 val (str', actual, ds) = elabStr (env, denv) str 2916 val (str', sgn', gs') =
2916 in 2917 case formal of
2917 (str', selfifyAt env {str = str', sgn = actual}, ds) 2918 NONE =>
2918 end 2919 let
2919 | SOME (formal, gs1) => 2920 val (str', actual, gs') = elabStr (env, denv) str
2920 let 2921 in
2921 val str = 2922 (str', selfifyAt env {str = str', sgn = actual}, gs')
2922 case #1 (hnormSgn env formal) of 2923 end
2923 L'.SgnConst sgis => 2924 | SOME (formal, gs1) =>
2924 (case #1 str of 2925 let
2925 L.StrConst ds => 2926 val str =
2926 let 2927 case #1 (hnormSgn env formal) of
2927 val needed = foldl (fn ((sgi, _), needed) => 2928 L'.SgnConst sgis =>
2928 case sgi of 2929 (case #1 str of
2929 L'.SgiConAbs (x, _, _) => SS.add (needed, x) 2930 L.StrConst ds =>
2930 | _ => needed)
2931 SS.empty sgis
2932
2933 val needed = foldl (fn ((d, _), needed) =>
2934 case d of
2935 L.DCon (x, _, _) => (SS.delete (needed, x)
2936 handle NotFound => needed)
2937 | L.DClass (x, _) => (SS.delete (needed, x)
2938 handle NotFound => needed)
2939 | L.DOpen _ => SS.empty
2940 | _ => needed)
2941 needed ds
2942 in
2943 case SS.listItems needed of
2944 [] => str
2945 | xs =>
2946 let 2931 let
2947 val kwild = (L.KWild, #2 str) 2932 val needed = foldl (fn ((sgi, _), needed) =>
2948 val cwild = (L.CWild kwild, #2 str) 2933 case sgi of
2949 val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs 2934 L'.SgiConAbs (x, _, _) => SS.add (needed, x)
2935 | _ => needed)
2936 SS.empty sgis
2937
2938 val needed = foldl (fn ((d, _), needed) =>
2939 case d of
2940 L.DCon (x, _, _) => (SS.delete (needed, x)
2941 handle NotFound =>
2942 needed)
2943 | L.DClass (x, _) => (SS.delete (needed, x)
2944 handle NotFound => needed)
2945 | L.DOpen _ => SS.empty
2946 | _ => needed)
2947 needed ds
2950 in 2948 in
2951 (L.StrConst (ds @ ds'), #2 str) 2949 case SS.listItems needed of
2950 [] => str
2951 | xs =>
2952 let
2953 val kwild = (L.KWild, #2 str)
2954 val cwild = (L.CWild kwild, #2 str)
2955 val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
2956 in
2957 (L.StrConst (ds @ ds'), #2 str)
2958 end
2952 end 2959 end
2953 end 2960 | _ => str)
2954 | _ => str) 2961 | _ => str
2955 | _ => str 2962
2956 2963 val (str', actual, gs2) = elabStr (env, denv) str
2957 val (str', actual, gs2) = elabStr (env, denv) str 2964 in
2958 in 2965 subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal;
2959 subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal; 2966 (str', formal, enD gs1 @ gs2)
2960 (str', formal, enD gs1 @ gs2) 2967 end
2961 end 2968
2962 2969 val (env', n) = E.pushStrNamed env x sgn'
2963 val (env', n) = E.pushStrNamed env x sgn' 2970 in
2964 in 2971 case #1 (hnormSgn env sgn') of
2965 case #1 (hnormSgn env sgn') of 2972 L'.SgnFun _ =>
2966 L'.SgnFun _ => 2973 (case #1 str' of
2967 (case #1 str' of 2974 L'.StrFun _ => ()
2968 L'.StrFun _ => () 2975 | _ => strError env (FunctorRebind loc))
2969 | _ => strError env (FunctorRebind loc)) 2976 | _ => ();
2970 | _ => (); 2977
2971 2978 ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs))
2972 ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs)) 2979 end
2973 end 2980
2974 2981 | L.DFfiStr (x, sgn) =>
2975 | L.DFfiStr (x, sgn) => 2982 let
2976 let 2983 val (sgn', gs') = elabSgn (env, denv) sgn
2977 val (sgn', gs') = elabSgn (env, denv) sgn 2984
2978 2985 val (env', n) = E.pushStrNamed env x sgn'
2979 val (env', n) = E.pushStrNamed env x sgn' 2986 in
2980 in 2987 ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
2981 ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs)) 2988 end
2982 end 2989
2983 2990 | L.DOpen (m, ms) =>
2984 | L.DOpen (m, ms) => 2991 (case E.lookupStr env m of
2985 (case E.lookupStr env m of 2992 NONE => (strError env (UnboundStr (loc, m));
2986 NONE => (strError env (UnboundStr (loc, m)); 2993 ([], (env, denv, gs)))
2987 ([], (env, denv, gs))) 2994 | SOME (n, sgn) =>
2988 | SOME (n, sgn) => 2995 let
2989 let 2996 val (_, sgn) = foldl (fn (m, (str, sgn)) =>
2990 val (_, sgn) = foldl (fn (m, (str, sgn)) => 2997 case E.projectStr env {str = str, sgn = sgn, field = m} of
2991 case E.projectStr env {str = str, sgn = sgn, field = m} of 2998 NONE => (strError env (UnboundStr (loc, m));
2992 NONE => (strError env (UnboundStr (loc, m)); 2999 (strerror, sgnerror))
2993 (strerror, sgnerror)) 3000 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
2994 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) 3001 ((L'.StrVar n, loc), sgn) ms
2995 ((L'.StrVar n, loc), sgn) ms 3002
2996 3003 val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn}
2997 val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn} 3004 val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms}
2998 val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms} 3005 in
2999 in 3006 (ds, (env', denv', gs))
3000 (ds, (env', denv', gs)) 3007 end)
3001 end) 3008
3002 3009 | L.DConstraint (c1, c2) =>
3003 | L.DConstraint (c1, c2) => 3010 let
3004 let 3011 val (c1', k1, gs1) = elabCon (env, denv) c1
3005 val (c1', k1, gs1) = elabCon (env, denv) c1 3012 val (c2', k2, gs2) = elabCon (env, denv) c2
3006 val (c2', k2, gs2) = elabCon (env, denv) c2 3013 val gs3 = D.prove env denv (c1', c2', loc)
3007 val gs3 = D.prove env denv (c1', c2', loc) 3014
3008 3015 val (denv', gs4) = D.assert env denv (c1', c2')
3009 val (denv', gs4) = D.assert env denv (c1', c2') 3016 in
3010 in 3017 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
3011 checkKind env c1' k1 (L'.KRecord (kunif loc), loc); 3018 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
3012 checkKind env c2' k2 (L'.KRecord (kunif loc), loc); 3019
3013 3020 ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ enD gs4 @ gs))
3014 ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ enD gs4 @ gs)) 3021 end
3015 end 3022
3016 3023 | L.DOpenConstraints (m, ms) =>
3017 | L.DOpenConstraints (m, ms) => 3024 let
3018 let 3025 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
3019 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms} 3026 in
3020 in 3027 ([], (env, denv, gs))
3021 ([], (env, denv, gs)) 3028 end
3022 end 3029
3023 3030 | L.DExport str =>
3024 | L.DExport str => 3031 let
3025 let 3032 val (str', sgn, gs') = elabStr (env, denv) str
3026 val (str', sgn, gs') = elabStr (env, denv) str 3033
3027 3034 val sgn =
3028 val sgn = 3035 case #1 (hnormSgn env sgn) of
3029 case #1 (hnormSgn env sgn) of 3036 L'.SgnConst sgis =>
3030 L'.SgnConst sgis => 3037 let
3031 let 3038 fun doOne (all as (sgi, _), env) =
3032 fun doOne (all as (sgi, _), env) = 3039 (case sgi of
3033 (case sgi of 3040 L'.SgiVal (x, n, t) =>
3034 L'.SgiVal (x, n, t) => 3041 (case hnormCon (env, denv) t of
3035 (case hnormCon (env, denv) t of 3042 ((L'.TFun (dom, ran), _), []) =>
3036 ((L'.TFun (dom, ran), _), []) => 3043 (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of
3037 (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of 3044 (((L'.TRecord domR, _), []),
3038 (((L'.TRecord domR, _), []), 3045 ((L'.CApp (tf, arg), _), [])) =>
3039 ((L'.CApp (tf, arg), _), [])) => 3046 (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of
3040 (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of 3047 (((L'.CModProj (basis, [], "transaction"), _), []),
3041 (((L'.CModProj (basis, [], "transaction"), _), []), 3048 ((L'.CApp (tf, arg3), _), [])) =>
3042 ((L'.CApp (tf, arg3), _), [])) => 3049 (case (basis = !basis_r,
3043 (case (basis = !basis_r, 3050 hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of
3044 hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of 3051 (true,
3045 (true, 3052 ((L'.CApp (tf, arg2), _), []),
3046 ((L'.CApp (tf, arg2), _), []), 3053 (((L'.CRecord (_, []), _), []))) =>
3047 (((L'.CRecord (_, []), _), []))) => 3054 (case (hnormCon (env, denv) tf) of
3048 (case (hnormCon (env, denv) tf) of 3055 ((L'.CApp (tf, arg1), _), []) =>
3049 ((L'.CApp (tf, arg1), _), []) => 3056 (case (hnormCon (env, denv) tf,
3050 (case (hnormCon (env, denv) tf, 3057 hnormCon (env, denv) domR,
3051 hnormCon (env, denv) domR, 3058 hnormCon (env, denv) arg1,
3052 hnormCon (env, denv) arg1, 3059 hnormCon (env, denv) arg2) of
3053 hnormCon (env, denv) arg2) of 3060 ((tf, []), (domR, []), (arg1, []),
3054 ((tf, []), (domR, []), (arg1, []), 3061 ((L'.CRecord (_, []), _), [])) =>
3055 ((L'.CRecord (_, []), _), [])) => 3062 let
3056 let 3063 val t = (L'.CApp (tf, arg1), loc)
3057 val t = (L'.CApp (tf, arg1), loc) 3064 val t = (L'.CApp (t, arg2), loc)
3058 val t = (L'.CApp (t, arg2), loc) 3065 val t = (L'.CApp (t, arg3), loc)
3059 val t = (L'.CApp (t, arg3), loc) 3066 val t = (L'.CApp (
3060 val t = (L'.CApp ( 3067 (L'.CModProj
3061 (L'.CModProj (basis, [], "transaction"), loc), 3068 (basis, [], "transaction"), loc),
3062 t), loc) 3069 t), loc)
3063 in 3070 in
3064 (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc), 3071 (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR,
3065 t), 3072 loc),
3066 loc)), loc) 3073 t),
3067 end 3074 loc)), loc)
3068 | _ => all) 3075 end
3069 | _ => all) 3076 | _ => all)
3070 | _ => all) 3077 | _ => all)
3071 | _ => all) 3078 | _ => all)
3072 | _ => all) 3079 | _ => all)
3073 | _ => all) 3080 | _ => all)
3074 | _ => all, 3081 | _ => all)
3075 E.sgiBinds env all) 3082 | _ => all,
3076 in 3083 E.sgiBinds env all)
3077 (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc) 3084 in
3078 end 3085 (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc)
3079 | _ => sgn 3086 end
3080 in 3087 | _ => sgn
3081 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs)) 3088 in
3082 end 3089 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs))
3083 3090 end
3084 | L.DTable (x, c) => 3091
3085 let 3092 | L.DTable (x, c) =>
3086 val (c', k, gs') = elabCon (env, denv) c 3093 let
3087 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc) 3094 val (c', k, gs') = elabCon (env, denv) c
3088 in 3095 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
3089 checkKind env c' k (L'.KRecord (L'.KType, loc), loc); 3096 in
3090 ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs)) 3097 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
3091 end 3098 ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
3092 3099 end
3093 | L.DClass (x, c) => 3100
3094 let 3101 | L.DClass (x, c) =>
3095 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 3102 let
3096 val (c', ck, gs) = elabCon (env, denv) c 3103 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
3097 val (env, n) = E.pushCNamed env x k (SOME c') 3104 val (c', ck, gs) = elabCon (env, denv) c
3098 val env = E.pushClass env n 3105 val (env, n) = E.pushCNamed env x k (SOME c')
3099 in 3106 val env = E.pushClass env n
3100 checkKind env c' ck k; 3107 in
3101 ([(L'.DClass (x, n, c'), loc)], (env, denv, [])) 3108 checkKind env c' ck k;
3102 end 3109 ([(L'.DClass (x, n, c'), loc)], (env, denv, []))
3110 end
3111 in
3112 r
3113 end
3103 3114
3104 and elabStr (env, denv) (str, loc) = 3115 and elabStr (env, denv) (str, loc) =
3105 case str of 3116 case str of
3106 L.StrConst ds => 3117 L.StrConst ds =>
3107 let 3118 let