Mercurial > urweb

comparison src/elaborate.sml @ 469:b393c2fc80f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
About to begin optimization of recursive transaction functions
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 17:09:53 -0500
parents 3f1b9231a37b
children 20fab0e96217
comparison
equal deleted inserted replaced
468:4efab85405be 469:b393c2fc80f8
1774 val hnormSgn = E.hnormSgn 1774 val hnormSgn = E.hnormSgn
1775 1775
1776 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan) 1776 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan)
1777 fun sequenceOf () = (L'.CModProj (!basis_r, [], "sql_sequence"), ErrorMsg.dummySpan) 1777 fun sequenceOf () = (L'.CModProj (!basis_r, [], "sql_sequence"), ErrorMsg.dummySpan)
1778 fun cookieOf () = (L'.CModProj (!basis_r, [], "http_cookie"), ErrorMsg.dummySpan) 1778 fun cookieOf () = (L'.CModProj (!basis_r, [], "http_cookie"), ErrorMsg.dummySpan)
1779
1780 fun dopenConstraints (loc, env, denv) {str, strs} =
1781 case E.lookupStr env str of
1782 NONE => (strError env (UnboundStr (loc, str));
1783 denv)
1784 | SOME (n, sgn) =>
1785 let
1786 val (st, sgn) = foldl (fn (m, (str, sgn)) =>
1787 case E.projectStr env {str = str, sgn = sgn, field = m} of
1788 NONE => (strError env (UnboundStr (loc, m));
1789 (strerror, sgnerror))
1790 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1791 ((L'.StrVar n, loc), sgn) strs
1792
1793 val cso = E.projectConstraints env {sgn = sgn, str = st}
1794
1795 val denv = case cso of
1796 NONE => (strError env (UnboundStr (loc, str));
1797 denv)
1798 | SOME cs => foldl (fn ((c1, c2), denv) =>
1799 let
1800 val (denv, gs) = D.assert env denv (c1, c2)
1801 in
1802 case gs of
1803 [] => ()
1804 | _ => raise Fail "dopenConstraints: Sub-constraints remain";
1805
1806 denv
1807 end) denv cs
1808 in
1809 denv
1810 end
1779 1811
1780 fun elabSgn_item ((sgi, loc), (env, denv, gs)) = 1812 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
1781 case sgi of 1813 case sgi of
1782 L.SgiConAbs (x, k) => 1814 L.SgiConAbs (x, k) =>
1783 let 1815 let
2052 | SOME (n, sgis) => ((L'.SgnVar n, loc), [])) 2084 | SOME (n, sgis) => ((L'.SgnVar n, loc), []))
2053 | L.SgnFun (m, dom, ran) => 2085 | L.SgnFun (m, dom, ran) =>
2054 let 2086 let
2055 val (dom', gs1) = elabSgn (env, denv) dom 2087 val (dom', gs1) = elabSgn (env, denv) dom
2056 val (env', n) = E.pushStrNamed env m dom' 2088 val (env', n) = E.pushStrNamed env m dom'
2057 val (ran', gs2) = elabSgn (env', denv) ran 2089 val denv' = dopenConstraints (loc, env', denv) {str = m, strs = []}
2090 val (ran', gs2) = elabSgn (env', denv') ran
2058 in 2091 in
2059 ((L'.SgnFun (m, n, dom', ran'), loc), gs1 @ gs2) 2092 ((L'.SgnFun (m, n, dom', ran'), loc), gs1 @ gs2)
2060 end 2093 end
2061 | L.SgnWhere (sgn, x, c) => 2094 | L.SgnWhere (sgn, x, c) =>
2062 let 2095 let
2191 (env, denv) sgis 2224 (env, denv) sgis
2192 | _ => (strError env (UnOpenable sgn); 2225 | _ => (strError env (UnOpenable sgn);
2193 ([], (env, denv))) 2226 ([], (env, denv)))
2194 end 2227 end
2195 2228
2196 fun dopenConstraints (loc, env, denv) {str, strs} =
2197 case E.lookupStr env str of
2198 NONE => (strError env (UnboundStr (loc, str));
2199 denv)
2200 | SOME (n, sgn) =>
2201 let
2202 val (st, sgn) = foldl (fn (m, (str, sgn)) =>
2203 case E.projectStr env {str = str, sgn = sgn, field = m} of
2204 NONE => (strError env (UnboundStr (loc, m));
2205 (strerror, sgnerror))
2206 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
2207 ((L'.StrVar n, loc), sgn) strs
2208
2209 val cso = E.projectConstraints env {sgn = sgn, str = st}
2210
2211 val denv = case cso of
2212 NONE => (strError env (UnboundStr (loc, str));
2213 denv)
2214 | SOME cs => foldl (fn ((c1, c2), denv) =>
2215 let
2216 val (denv, gs) = D.assert env denv (c1, c2)
2217 in
2218 case gs of
2219 [] => ()
2220 | _ => raise Fail "dopenConstraints: Sub-constraints remain";
2221
2222 denv
2223 end) denv cs
2224 in
2225 denv
2226 end
2227
2228 fun sgiOfDecl (d, loc) = 2229 fun sgiOfDecl (d, loc) =
2229 case d of 2230 case d of
2230 L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)] 2231 L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)]
2231 | L'.DDatatype x => [(L'.SgiDatatype x, loc)] 2232 | L'.DDatatype x => [(L'.SgiDatatype x, loc)]
2232 | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)] 2233 | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)]
2250 (denv, []) => denv 2251 (denv, []) => denv
2251 | _ => raise Fail "sgiBindsD: Sub-constraints remain") 2252 | _ => raise Fail "sgiBindsD: Sub-constraints remain")
2252 | _ => denv 2253 | _ => denv
2253 2254
2254 fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = 2255 fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
2256 ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1),
2257 ("sgn2", p_sgn env sgn2)];*)
2255 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of 2258 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
2256 (L'.SgnError, _) => () 2259 (L'.SgnError, _) => ()
2257 | (_, L'.SgnError) => () 2260 | (_, L'.SgnError) => ()
2258 2261
2259 | (L'.SgnConst sgis1, L'.SgnConst sgis2) => 2262 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
2272 fun seek (env, denv) ls = 2275 fun seek (env, denv) ls =
2273 case ls of 2276 case ls of
2274 [] => (sgnError env (UnmatchedSgi sgi2All); 2277 [] => (sgnError env (UnmatchedSgi sgi2All);
2275 (env, denv)) 2278 (env, denv))
2276 | h :: t => 2279 | h :: t =>
2277 case p h of 2280 case p (env, h) of
2278 NONE => seek (E.sgiBinds env h, sgiBindsD (env, denv) h) t 2281 NONE =>
2282 let
2283 val env = case #1 h of
2284 L'.SgiCon (x, n, k, c) =>
2285 E.pushCNamedAs env x n k (SOME c)
2286 | L'.SgiConAbs (x, n, k) =>
2287 E.pushCNamedAs env x n k NONE
2288 | _ => env
2289 in
2290 seek (E.sgiBinds env h, sgiBindsD (env, denv) h) t
2291 end
2279 | SOME envs => envs 2292 | SOME envs => envs
2280 in 2293 in
2281 seek (env, denv) sgis1 2294 seek (env, denv) sgis1
2282 end 2295 end
2283 in 2296 in
2284 case sgi of 2297 case sgi of
2285 L'.SgiConAbs (x, n2, k2) => 2298 L'.SgiConAbs (x, n2, k2) =>
2286 seek (fn sgi1All as (sgi1, _) => 2299 seek (fn (env, sgi1All as (sgi1, _)) =>
2287 let 2300 let
2288 fun found (x', n1, k1, co1) = 2301 fun found (x', n1, k1, co1) =
2289 if x = x' then 2302 if x = x' then
2290 let 2303 let
2291 val () = unifyKinds k1 k2 2304 val () = unifyKinds k1 k2
2329 SOME c) 2342 SOME c)
2330 | _ => NONE 2343 | _ => NONE
2331 end) 2344 end)
2332 2345
2333 | L'.SgiCon (x, n2, k2, c2) => 2346 | L'.SgiCon (x, n2, k2, c2) =>
2334 seek (fn sgi1All as (sgi1, _) => 2347 seek (fn (env, sgi1All as (sgi1, _)) =>
2335 let 2348 let
2336 fun found (x', n1, k1, c1) = 2349 fun found (x', n1, k1, c1) =
2337 if x = x' then 2350 if x = x' then
2338 let 2351 let
2339 fun good () = 2352 fun good () =
2363 found (x', n1, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), c1) 2376 found (x', n1, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), c1)
2364 | _ => NONE 2377 | _ => NONE
2365 end) 2378 end)
2366 2379
2367 | L'.SgiDatatype (x, n2, xs2, xncs2) => 2380 | L'.SgiDatatype (x, n2, xs2, xncs2) =>
2368 seek (fn sgi1All as (sgi1, _) => 2381 seek (fn (env, sgi1All as (sgi1, _)) =>
2369 let 2382 let
2370 fun found (n1, xs1, xncs1) = 2383 fun found (n1, xs1, xncs1) =
2371 let 2384 let
2372 fun mismatched ue = 2385 fun mismatched ue =
2373 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue)); 2386 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
2424 NONE 2437 NONE
2425 | _ => NONE 2438 | _ => NONE
2426 end) 2439 end)
2427 2440
2428 | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) => 2441 | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) =>
2429 seek (fn sgi1All as (sgi1, _) => 2442 seek (fn (env, sgi1All as (sgi1, _)) =>
2430 case sgi1 of 2443 case sgi1 of
2431 L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) => 2444 L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) =>
2432 if x = x' then 2445 if x = x' then
2433 let 2446 let
2434 val k = (L'.KType, loc) 2447 val k = (L'.KType, loc)
2455 NONE 2468 NONE
2456 2469
2457 | _ => NONE) 2470 | _ => NONE)
2458 2471
2459 | L'.SgiVal (x, n2, c2) => 2472 | L'.SgiVal (x, n2, c2) =>
2460 seek (fn sgi1All as (sgi1, _) => 2473 seek (fn (env, sgi1All as (sgi1, _)) =>
2461 case sgi1 of 2474 case sgi1 of
2462 L'.SgiVal (x', n1, c1) => 2475 L'.SgiVal (x', n1, c1) =>
2463 if x = x' then 2476 if x = x' then
2464 ((*prefaces "Pre" [("c1", p_con env c1), 2477 ((*prefaces "Pre" [("c1", p_con env c1),
2465 ("c2", p_con env c2)];*) 2478 ("c2", p_con env c2)];*)
2472 else 2485 else
2473 NONE 2486 NONE
2474 | _ => NONE) 2487 | _ => NONE)
2475 2488
2476 | L'.SgiStr (x, n2, sgn2) => 2489 | L'.SgiStr (x, n2, sgn2) =>
2477 seek (fn sgi1All as (sgi1, _) => 2490 seek (fn (env, sgi1All as (sgi1, _)) =>
2478 case sgi1 of 2491 case sgi1 of
2479 L'.SgiStr (x', n1, sgn1) => 2492 L'.SgiStr (x', n1, sgn1) =>
2480 if x = x' then 2493 if x = x' then
2481 let 2494 let
2482 val () = subSgn (env, denv) sgn1 sgn2 2495 val () = subSgn (env, denv) sgn1 sgn2
2493 else 2506 else
2494 NONE 2507 NONE
2495 | _ => NONE) 2508 | _ => NONE)
2496 2509
2497 | L'.SgiSgn (x, n2, sgn2) => 2510 | L'.SgiSgn (x, n2, sgn2) =>
2498 seek (fn sgi1All as (sgi1, _) => 2511 seek (fn (env, sgi1All as (sgi1, _)) =>
2499 case sgi1 of 2512 case sgi1 of
2500 L'.SgiSgn (x', n1, sgn1) => 2513 L'.SgiSgn (x', n1, sgn1) =>
2501 if x = x' then 2514 if x = x' then
2502 let 2515 let
2503 val () = subSgn (env, denv) sgn1 sgn2 2516 val () = subSgn (env, denv) sgn1 sgn2
2514 else 2527 else
2515 NONE 2528 NONE
2516 | _ => NONE) 2529 | _ => NONE)
2517 2530
2518 | L'.SgiConstraint (c2, d2) => 2531 | L'.SgiConstraint (c2, d2) =>
2519 seek (fn sgi1All as (sgi1, _) => 2532 seek (fn (env, sgi1All as (sgi1, _)) =>
2520 case sgi1 of 2533 case sgi1 of
2521 L'.SgiConstraint (c1, d1) => 2534 L'.SgiConstraint (c1, d1) =>
2522 if consEq (env, denv) (c1, c2) andalso consEq (env, denv) (d1, d2) then 2535 if consEq (env, denv) (c1, c2) andalso consEq (env, denv) (d1, d2) then
2523 let 2536 let
2524 val (denv, gs) = D.assert env denv (c2, d2) 2537 val (denv, gs) = D.assert env denv (c2, d2)
2532 else 2545 else
2533 NONE 2546 NONE
2534 | _ => NONE) 2547 | _ => NONE)
2535 2548
2536 | L'.SgiClassAbs (x, n2) => 2549 | L'.SgiClassAbs (x, n2) =>
2537 seek (fn sgi1All as (sgi1, _) => 2550 seek (fn (env, sgi1All as (sgi1, _)) =>
2538 let 2551 let
2539 fun found (x', n1, co) = 2552 fun found (x', n1, co) =
2540 if x = x' then 2553 if x = x' then
2541 let 2554 let
2542 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 2555 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
2555 L'.SgiClassAbs (x', n1) => found (x', n1, NONE) 2568 L'.SgiClassAbs (x', n1) => found (x', n1, NONE)
2556 | L'.SgiClass (x', n1, c) => found (x', n1, SOME c) 2569 | L'.SgiClass (x', n1, c) => found (x', n1, SOME c)
2557 | _ => NONE 2570 | _ => NONE
2558 end) 2571 end)
2559 | L'.SgiClass (x, n2, c2) => 2572 | L'.SgiClass (x, n2, c2) =>
2560 seek (fn sgi1All as (sgi1, _) => 2573 seek (fn (env, sgi1All as (sgi1, _)) =>
2561 let 2574 let
2562 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 2575 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
2563 2576
2564 fun found (x', n1, c1) = 2577 fun found (x', n1, c1) =
2565 if x = x' then 2578 if x = x' then
2604 in 2617 in
2605 subSgn (env, denv) dom2 dom1; 2618 subSgn (env, denv) dom2 dom1;
2606 subSgn (E.pushStrNamedAs env m2 n2 dom2, denv) ran1 ran2 2619 subSgn (E.pushStrNamedAs env m2 n2 dom2, denv) ran1 ran2
2607 end 2620 end
2608 2621
2609 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)) 2622 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)))
2610 2623
2611 2624
2612 fun positive self = 2625 fun positive self =
2613 let 2626 let
2614 open L 2627 open L
2715 | _ => NONE) 2728 | _ => NONE)
2716 | L'.CUnit => SOME (L.CUnit, loc) 2729 | L'.CUnit => SOME (L.CUnit, loc)
2717 2730
2718 | _ => NONE 2731 | _ => NONE
2719 2732
2720 val (needed, constraints, _) = 2733 val (neededC, constraints, neededV, _) =
2721 foldl (fn ((sgi, loc), (needed, constraints, env')) => 2734 foldl (fn ((sgi, loc), (neededC, constraints, neededV, env')) =>
2722 let 2735 let
2723 val (needed, constraints) = 2736 val (needed, constraints, neededV) =
2724 case sgi of 2737 case sgi of
2725 L'.SgiConAbs (x, _, _) => (SS.add (needed, x), constraints) 2738 L'.SgiConAbs (x, _, _) => (SS.add (neededC, x), constraints, neededV)
2726 | L'.SgiConstraint cs => (needed, (env', cs, loc) :: constraints) 2739 | L'.SgiConstraint cs => (neededC, (env', cs, loc) :: constraints, neededV)
2727 | _ => (needed, constraints) 2740
2741 | L'.SgiVal (x, _, t) =>
2742 let
2743 fun default () = (neededC, constraints, neededV)
2744
2745 val t = normClassConstraint env' t
2746 in
2747 case #1 t of
2748 L'.CApp (f, _) =>
2749 if E.isClass env' f then
2750 (neededC, constraints, SS.add (neededV, x))
2751 else
2752 default ()
2753
2754 | _ => default ()
2755 end
2756
2757 | _ => (neededC, constraints, neededV)
2728 in 2758 in
2729 (needed, constraints, E.sgiBinds env' (sgi, loc)) 2759 (needed, constraints, neededV, E.sgiBinds env' (sgi, loc))
2730 end) 2760 end)
2731 (SS.empty, [], env) sgis 2761 (SS.empty, [], SS.empty, env) sgis
2732 2762
2733 val needed = foldl (fn ((d, _), needed) => 2763 val (neededC, neededV) = foldl (fn ((d, _), needed as (neededC, neededV)) =>
2734 case d of 2764 case d of
2735 L.DCon (x, _, _) => (SS.delete (needed, x) 2765 L.DCon (x, _, _) => ((SS.delete (neededC, x), neededV)
2736 handle NotFound => 2766 handle NotFound =>
2737 needed) 2767 needed)
2738 | L.DClass (x, _) => (SS.delete (needed, x) 2768 | L.DClass (x, _) => ((SS.delete (neededC, x), neededV)
2739 handle NotFound => needed) 2769 handle NotFound => needed)
2740 | L.DOpen _ => SS.empty 2770 | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x))
2741 | _ => needed) 2771 handle NotFound => needed)
2742 needed ds 2772 | L.DOpen _ => (SS.empty, SS.empty)
2743 2773 | _ => needed)
2744 val cds = List.mapPartial (fn (env', (c1, c2), loc) => 2774 (neededC, neededV) ds
2775
2776 val ds' = List.mapPartial (fn (env', (c1, c2), loc) =>
2745 case (decompileCon env' c1, decompileCon env' c2) of 2777 case (decompileCon env' c1, decompileCon env' c2) of
2746 (SOME c1, SOME c2) => 2778 (SOME c1, SOME c2) =>
2747 SOME (L.DConstraint (c1, c2), loc) 2779 SOME (L.DConstraint (c1, c2), loc)
2748 | _ => NONE) constraints 2780 | _ => NONE) constraints
2781
2782 val ds' =
2783 case SS.listItems neededV of
2784 [] => ds'
2785 | xs =>
2786 let
2787 val ewild = (L.EWild, #2 str)
2788 val ds'' = map (fn x => (L.DVal (x, NONE, ewild), #2 str)) xs
2789 in
2790 ds'' @ ds'
2791 end
2792
2793 val ds' =
2794 case SS.listItems neededC of
2795 [] => ds'
2796 | xs =>
2797 let
2798 val kwild = (L.KWild, #2 str)
2799 val cwild = (L.CWild kwild, #2 str)
2800 val ds'' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
2801 in
2802 ds'' @ ds'
2803 end
2749 in 2804 in
2750 case SS.listItems needed of 2805 (L.StrConst (ds @ ds'), #2 str)
2751 [] => (L.StrConst (ds @ cds), #2 str)
2752 | xs =>
2753 let
2754 val kwild = (L.KWild, #2 str)
2755 val cwild = (L.CWild kwild, #2 str)
2756 val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
2757 in
2758 (L.StrConst (ds @ ds' @ cds), #2 str)
2759 end
2760 end 2806 end
2761 | _ => str) 2807 | _ => str)
2762 | _ => str 2808 | _ => str
2763 2809
2764 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = 2810 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =