Mercurial > urweb

comparison src/elaborate.sml @ 325:e457d8972ff1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Crud listing IDs
author Adam Chlipala <adamc@hcoop.net>
date Thu, 11 Sep 2008 17:41:52 -0400
parents f387d12193ba
children 950320f33232
comparison
equal deleted inserted replaced
324:b91480c9a729 325:e457d8972ff1
2803 | CWild _ => false 2803 | CWild _ => false
2804 in 2804 in
2805 pos 2805 pos
2806 end 2806 end
2807 2807
2808 fun wildifyStr env (str, sgn) =
2809 case #1 (hnormSgn env sgn) of
2810 L'.SgnConst sgis =>
2811 (case #1 str of
2812 L.StrConst ds =>
2813 let
2814 fun decompileCon env (c, loc) =
2815 case c of
2816 L'.CRel i =>
2817 let
2818 val (s, _) = E.lookupCRel env i
2819 in
2820 SOME (L.CVar ([], s), loc)
2821 end
2822 | L'.CNamed i =>
2823 let
2824 val (s, _, _) = E.lookupCNamed env i
2825 in
2826 SOME (L.CVar ([], s), loc)
2827 end
2828 | L'.CModProj (m1, ms, x) =>
2829 let
2830 val (s, _) = E.lookupStrNamed env m1
2831 in
2832 SOME (L.CVar (s :: ms, x), loc)
2833 end
2834 | L'.CName s => SOME (L.CName s, loc)
2835 | L'.CRecord (_, xcs) =>
2836 let
2837 fun fields xcs =
2838 case xcs of
2839 [] => SOME []
2840 | (x, t) :: xcs =>
2841 case (decompileCon env x, decompileCon env t, fields xcs) of
2842 (SOME x, SOME t, SOME xcs) => SOME ((x, t) :: xcs)
2843 | _ => NONE
2844 in
2845 Option.map (fn xcs => (L.CRecord xcs, loc))
2846 (fields xcs)
2847 end
2848 | L'.CConcat (c1, c2) =>
2849 (case (decompileCon env c1, decompileCon env c2) of
2850 (SOME c1, SOME c2) => SOME (L.CConcat (c1, c2), loc)
2851 | _ => NONE)
2852 | L'.CUnit => SOME (L.CUnit, loc)
2853
2854 | _ => NONE
2855
2856 val (needed, constraints, _) =
2857 foldl (fn ((sgi, loc), (needed, constraints, env')) =>
2858 let
2859 val (needed, constraints) =
2860 case sgi of
2861 L'.SgiConAbs (x, _, _) => (SS.add (needed, x), constraints)
2862 | L'.SgiConstraint cs => (needed, (env', cs, loc) :: constraints)
2863 | _ => (needed, constraints)
2864 in
2865 (needed, constraints, E.sgiBinds env' (sgi, loc))
2866 end)
2867 (SS.empty, [], env) sgis
2868
2869 val needed = foldl (fn ((d, _), needed) =>
2870 case d of
2871 L.DCon (x, _, _) => (SS.delete (needed, x)
2872 handle NotFound =>
2873 needed)
2874 | L.DClass (x, _) => (SS.delete (needed, x)
2875 handle NotFound => needed)
2876 | L.DOpen _ => SS.empty
2877 | _ => needed)
2878 needed ds
2879
2880 val cds = List.mapPartial (fn (env', (c1, c2), loc) =>
2881 case (decompileCon env' c1, decompileCon env' c2) of
2882 (SOME c1, SOME c2) =>
2883 SOME (L.DConstraint (c1, c2), loc)
2884 | _ => NONE) constraints
2885 in
2886 case SS.listItems needed of
2887 [] => (L.StrConst (ds @ cds), #2 str)
2888 | xs =>
2889 let
2890 val kwild = (L.KWild, #2 str)
2891 val cwild = (L.CWild kwild, #2 str)
2892 val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
2893 in
2894 (L.StrConst (ds @ ds' @ cds), #2 str)
2895 end
2896 end
2897 | _ => str)
2898 | _ => str
2899
2808 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = 2900 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
2809 let 2901 let
2810 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*) 2902 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
2811 2903
2812 val r = 2904 val r =
3008 in 3100 in
3009 (str', selfifyAt env {str = str', sgn = actual}, gs') 3101 (str', selfifyAt env {str = str', sgn = actual}, gs')
3010 end 3102 end
3011 | SOME (formal, gs1) => 3103 | SOME (formal, gs1) =>
3012 let 3104 let
3013 val str = 3105 val str = wildifyStr env (str, formal)
3014 case #1 (hnormSgn env formal) of
3015 L'.SgnConst sgis =>
3016 (case #1 str of
3017 L.StrConst ds =>
3018 let
3019 val needed = foldl (fn ((sgi, _), needed) =>
3020 case sgi of
3021 L'.SgiConAbs (x, _, _) => SS.add (needed, x)
3022 | _ => needed)
3023 SS.empty sgis
3024
3025 val needed = foldl (fn ((d, _), needed) =>
3026 case d of
3027 L.DCon (x, _, _) => (SS.delete (needed, x)
3028 handle NotFound =>
3029 needed)
3030 | L.DClass (x, _) => (SS.delete (needed, x)
3031 handle NotFound => needed)
3032 | L.DOpen _ => SS.empty
3033 | _ => needed)
3034 needed ds
3035 in
3036 case SS.listItems needed of
3037 [] => str
3038 | xs =>
3039 let
3040 val kwild = (L.KWild, #2 str)
3041 val cwild = (L.CWild kwild, #2 str)
3042 val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
3043 in
3044 (L.StrConst (ds @ ds'), #2 str)
3045 end
3046 end
3047 | _ => str)
3048 | _ => str
3049
3050 val (str', actual, gs2) = elabStr (env, denv) str 3106 val (str', actual, gs2) = elabStr (env, denv) str
3051 in 3107 in
3052 subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal; 3108 subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal;
3053 (str', formal, enD gs1 @ gs2) 3109 (str', formal, enD gs1 @ gs2)
3054 end 3110 end
3123 L'.SgnConst sgis => 3179 L'.SgnConst sgis =>
3124 let 3180 let
3125 fun doOne (all as (sgi, _), env) = 3181 fun doOne (all as (sgi, _), env) =
3126 (case sgi of 3182 (case sgi of
3127 L'.SgiVal (x, n, t) => 3183 L'.SgiVal (x, n, t) =>
3128 (case hnormCon (env, denv) t of 3184 let
3129 ((L'.TFun (dom, ran), _), []) => 3185 fun doPage (makeRes, ran) =
3130 (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of 3186 case hnormCon (env, denv) ran of
3131 (((L'.TRecord domR, _), []), 3187 ((L'.CApp (tf, arg), _), []) =>
3132 ((L'.CApp (tf, arg), _), [])) => 3188 (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of
3133 (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of 3189 (((L'.CModProj (basis, [], "transaction"), _), []),
3134 (((L'.CModProj (basis, [], "transaction"), _), []), 3190 ((L'.CApp (tf, arg3), _), [])) =>
3135 ((L'.CApp (tf, arg3), _), [])) => 3191 (case (basis = !basis_r,
3136 (case (basis = !basis_r, 3192 hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of
3137 hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of 3193 (true,
3138 (true, 3194 ((L'.CApp (tf, arg2), _), []),
3139 ((L'.CApp (tf, arg2), _), []), 3195 (((L'.CRecord (_, []), _), []))) =>
3140 (((L'.CRecord (_, []), _), []))) => 3196 (case (hnormCon (env, denv) tf) of
3141 (case (hnormCon (env, denv) tf) of 3197 ((L'.CApp (tf, arg1), _), []) =>
3142 ((L'.CApp (tf, arg1), _), []) => 3198 (case (hnormCon (env, denv) tf,
3143 (case (hnormCon (env, denv) tf, 3199 hnormCon (env, denv) arg1,
3144 hnormCon (env, denv) domR, 3200 hnormCon (env, denv) arg2) of
3145 hnormCon (env, denv) arg1, 3201 ((tf, []), (arg1, []),
3146 hnormCon (env, denv) arg2) of 3202 ((L'.CRecord (_, []), _), [])) =>
3147 ((tf, []), (domR, []), (arg1, []), 3203 let
3148 ((L'.CRecord (_, []), _), [])) => 3204 val t = (L'.CApp (tf, arg1), loc)
3149 let 3205 val t = (L'.CApp (t, arg2), loc)
3150 val t = (L'.CApp (tf, arg1), loc) 3206 val t = (L'.CApp (t, arg3), loc)
3151 val t = (L'.CApp (t, arg2), loc) 3207 val t = (L'.CApp (
3152 val t = (L'.CApp (t, arg3), loc) 3208 (L'.CModProj
3153 val t = (L'.CApp ( 3209 (basis, [], "transaction"), loc),
3154 (L'.CModProj 3210 t), loc)
3155 (basis, [], "transaction"), loc), 3211 in
3156 t), loc) 3212 (L'.SgiVal (x, n, makeRes t), loc)
3157 in 3213 end
3158 (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, 3214 | _ => all)
3159 loc), 3215 | _ => all)
3160 t), 3216 | _ => all)
3161 loc)), loc) 3217 | _ => all)
3162 end 3218 | _ => all
3163 | _ => all) 3219 in
3164 | _ => all) 3220 case hnormCon (env, denv) t of
3165 | _ => all) 3221 ((L'.TFun (dom, ran), _), []) =>
3166 | _ => all) 3222 (case hnormCon (env, denv) dom of
3167 | _ => all) 3223 ((L'.TRecord domR, _), []) =>
3168 | _ => all) 3224 doPage (fn t => (L'.TFun ((L'.TRecord domR,
3225 loc),
3226 t), loc), ran)
3227 | _ => all)
3228 | _ => doPage (fn t => t, t)
3229 end
3169 | _ => all, 3230 | _ => all,
3170 E.sgiBinds env all) 3231 E.sgiBinds env all)
3171 in 3232 in
3172 (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc) 3233 (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc)
3173 end 3234 end
3373 enD gs1 @ gs2 @ enD gs3) 3434 enD gs1 @ gs2 @ enD gs3)
3374 end 3435 end
3375 | L.StrApp (str1, str2) => 3436 | L.StrApp (str1, str2) =>
3376 let 3437 let
3377 val (str1', sgn1, gs1) = elabStr (env, denv) str1 3438 val (str1', sgn1, gs1) = elabStr (env, denv) str1
3439 val str2 =
3440 case sgn1 of
3441 (L'.SgnFun (_, _, dom, _), _) =>
3442 wildifyStr env (str2, dom)
3443 | _ => str2
3378 val (str2', sgn2, gs2) = elabStr (env, denv) str2 3444 val (str2', sgn2, gs2) = elabStr (env, denv) str2
3379 in 3445 in
3380 case #1 (hnormSgn env sgn1) of 3446 case #1 (hnormSgn env sgn1) of
3381 L'.SgnError => (strerror, sgnerror, []) 3447 L'.SgnError => (strerror, sgnerror, [])
3382 | L'.SgnFun (m, n, dom, ran) => 3448 | L'.SgnFun (m, n, dom, ran) =>
3390 | _ => raise Fail "Unable to hnormSgn in functor application") 3456 | _ => raise Fail "Unable to hnormSgn in functor application")
3391 | _ => (strError env (NotFunctor sgn1); 3457 | _ => (strError env (NotFunctor sgn1);
3392 (strerror, sgnerror, [])) 3458 (strerror, sgnerror, []))
3393 end 3459 end
3394 3460
3395 fun elabFile basis env file = 3461 fun elabFile basis topStr topSgn env file =
3396 let 3462 let
3397 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan) 3463 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan)
3398 val () = case gs of 3464 val () = case gs of
3399 [] => () 3465 [] => ()
3400 | _ => (app (fn (_, env, _, c1, c2) => 3466 | _ => (app (fn (_, env, _, c1, c2) =>
3416 3482
3417 val () = discoverC int "int" 3483 val () = discoverC int "int"
3418 val () = discoverC float "float" 3484 val () = discoverC float "float"
3419 val () = discoverC string "string" 3485 val () = discoverC string "string"
3420 val () = discoverC table "sql_table" 3486 val () = discoverC table "sql_table"
3487
3488 val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan)
3489 val () = case gs of
3490 [] => ()
3491 | _ => raise Fail "Unresolved disjointness constraints in top.urs"
3492 val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan)
3493 val () = case gs of
3494 [] => ()
3495 | _ => (app (fn Disjoint (_, env, _, c1, c2) =>
3496 prefaces "Unresolved"
3497 [("c1", p_con env c1),
3498 ("c2", p_con env c2)]
3499 | TypeClass _ => TextIO.print "Type class\n") gs;
3500 raise Fail "Unresolved constraints in top.ur")
3501 val () = subSgn (env', D.empty) topSgn' topSgn
3502
3503 val (env', top_n) = E.pushStrNamed env' "Top" topSgn
3504
3505 val (ds', (env', _)) = dopen (env', D.empty) {str = top_n, strs = [], sgn = topSgn}
3421 3506
3422 fun elabDecl' (d, (env, gs)) = 3507 fun elabDecl' (d, (env, gs)) =
3423 let 3508 let
3424 val () = resetKunif () 3509 val () = resetKunif ()
3425 val () = resetCunif () 3510 val () = resetCunif ()
3459 | TypeClass (env, c, r, loc) => 3544 | TypeClass (env, c, r, loc) =>
3460 case E.resolveClass env c of 3545 case E.resolveClass env c of
3461 SOME e => r := SOME e 3546 SOME e => r := SOME e
3462 | NONE => expError env (Unresolvable (loc, c))) gs; 3547 | NONE => expError env (Unresolvable (loc, c))) gs;
3463 3548
3464 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file 3549 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
3550 :: ds
3551 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)
3552 :: ds' @ file
3465 end 3553 end
3466 3554
3467 end 3555 end