Mercurial > urweb

comparison src/elaborate.sml @ 459:f542bc3133dc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Cookies through elaborate
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 10:29:55 -0500
parents 222cbc1da232
children d34834af4512
comparison
equal deleted inserted replaced
458:8f65b0fa3b29 459:f542bc3133dc
1758 1758
1759 val hnormSgn = E.hnormSgn 1759 val hnormSgn = E.hnormSgn
1760 1760
1761 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan) 1761 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan)
1762 fun sequenceOf () = (L'.CModProj (!basis_r, [], "sql_sequence"), ErrorMsg.dummySpan) 1762 fun sequenceOf () = (L'.CModProj (!basis_r, [], "sql_sequence"), ErrorMsg.dummySpan)
1763 fun cookieOf () = (L'.CModProj (!basis_r, [], "http_cookie"), ErrorMsg.dummySpan)
1763 1764
1764 fun elabSgn_item ((sgi, loc), (env, denv, gs)) = 1765 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
1765 case sgi of 1766 case sgi of
1766 L.SgiConAbs (x, k) => 1767 L.SgiConAbs (x, k) =>
1767 let 1768 let
1963 val (env, n) = E.pushCNamed env x k (SOME c') 1964 val (env, n) = E.pushCNamed env x k (SOME c')
1964 val env = E.pushClass env n 1965 val env = E.pushClass env n
1965 in 1966 in
1966 checkKind env c' ck k; 1967 checkKind env c' ck k;
1967 ([(L'.SgiClass (x, n, c'), loc)], (env, denv, [])) 1968 ([(L'.SgiClass (x, n, c'), loc)], (env, denv, []))
1969 end
1970
1971 | L.SgiCookie (x, c) =>
1972 let
1973 val (c', k, gs) = elabCon (env, denv) c
1974 val (env, n) = E.pushENamed env x (L'.CApp (cookieOf (), c'), loc)
1975 in
1976 checkKind env c' k (L'.KType, loc);
1977 ([(L'.SgiCookie (!basis_r, x, n, c'), loc)], (env, denv, gs))
1968 end 1978 end
1969 1979
1970 and elabSgn (env, denv) (sgn, loc) = 1980 and elabSgn (env, denv) (sgn, loc) =
1971 case sgn of 1981 case sgn of
1972 L.SgnConst sgis => 1982 L.SgnConst sgis =>
2049 | L'.SgiClass (x, _, _) => 2059 | L'.SgiClass (x, _, _) =>
2050 (if SS.member (cons, x) then 2060 (if SS.member (cons, x) then
2051 sgnError env (DuplicateCon (loc, x)) 2061 sgnError env (DuplicateCon (loc, x))
2052 else 2062 else
2053 (); 2063 ();
2054 (SS.add (cons, x), vals, sgns, strs))) 2064 (SS.add (cons, x), vals, sgns, strs))
2065 | L'.SgiCookie (_, x, _, _) =>
2066 (if SS.member (vals, x) then
2067 sgnError env (DuplicateVal (loc, x))
2068 else
2069 ();
2070 (cons, SS.add (vals, x), sgns, strs)))
2055 (SS.empty, SS.empty, SS.empty, SS.empty) sgis' 2071 (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
2056 in 2072 in
2057 ((L'.SgnConst sgis', loc), gs) 2073 ((L'.SgnConst sgis', loc), gs)
2058 end 2074 end
2059 | L.SgnVar x => 2075 | L.SgnVar x =>
2201 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 2217 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
2202 val c = (L'.CModProj (str, strs, x), loc) 2218 val c = (L'.CModProj (str, strs, x), loc)
2203 in 2219 in
2204 (L'.DCon (x, n, k, c), loc) 2220 (L'.DCon (x, n, k, c), loc)
2205 end 2221 end
2222 | L'.SgiCookie (_, x, n, c) =>
2223 (L'.DVal (x, n, (L'.CApp (cookieOf (), c), loc),
2224 (L'.EModProj (str, strs, x), loc)), loc)
2206 in 2225 in
2207 (d, (E.declBinds env' d, denv')) 2226 (d, (E.declBinds env' d, denv'))
2208 end) 2227 end)
2209 (env, denv) sgis 2228 (env, denv) sgis
2210 | _ => (strError env (UnOpenable sgn); 2229 | _ => (strError env (UnOpenable sgn);
2257 | L'.DExport _ => [] 2276 | L'.DExport _ => []
2258 | L'.DTable (tn, x, n, c) => [(L'.SgiTable (tn, x, n, c), loc)] 2277 | L'.DTable (tn, x, n, c) => [(L'.SgiTable (tn, x, n, c), loc)]
2259 | L'.DSequence (tn, x, n) => [(L'.SgiSequence (tn, x, n), loc)] 2278 | L'.DSequence (tn, x, n) => [(L'.SgiSequence (tn, x, n), loc)]
2260 | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)] 2279 | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)]
2261 | L'.DDatabase _ => [] 2280 | L'.DDatabase _ => []
2281 | L'.DCookie (tn, x, n, c) => [(L'.SgiCookie (tn, x, n, c), loc)]
2262 2282
2263 fun sgiBindsD (env, denv) (sgi, _) = 2283 fun sgiBindsD (env, denv) (sgi, _) =
2264 case sgi of 2284 case sgi of
2265 L'.SgiConstraint (c1, c2) => 2285 L'.SgiConstraint (c1, c2) =>
2266 (case D.assert env denv (c1, c2) of 2286 (case D.assert env denv (c1, c2) of
2506 handle CUnify (c1, c2, err) => 2526 handle CUnify (c1, c2, err) =>
2507 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2527 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2508 SOME (env, denv)) 2528 SOME (env, denv))
2509 else 2529 else
2510 NONE 2530 NONE
2531 | L'.SgiCookie (_, x', n1, c1) =>
2532 if x = x' then
2533 (case unifyCons (env, denv) (L'.CApp (cookieOf (), c1), loc) c2 of
2534 [] => SOME (env, denv)
2535 | _ => NONE)
2536 handle CUnify (c1, c2, err) =>
2537 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2538 SOME (env, denv))
2539 else
2540 NONE
2511 | _ => NONE) 2541 | _ => NONE)
2512 2542
2513 | L'.SgiStr (x, n2, sgn2) => 2543 | L'.SgiStr (x, n2, sgn2) =>
2514 seek (fn sgi1All as (sgi1, _) => 2544 seek (fn sgi1All as (sgi1, _) =>
2515 case sgi1 of 2545 case sgi1 of
2649 in 2679 in
2650 case sgi1 of 2680 case sgi1 of
2651 L'.SgiClass (x', n1, c1) => found (x', n1, c1) 2681 L'.SgiClass (x', n1, c1) => found (x', n1, c1)
2652 | _ => NONE 2682 | _ => NONE
2653 end) 2683 end)
2684
2685 | L'.SgiCookie (_, x, n2, c2) =>
2686 seek (fn sgi1All as (sgi1, _) =>
2687 case sgi1 of
2688 L'.SgiCookie (_, x', n1, c1) =>
2689 if x = x' then
2690 (case unifyCons (env, denv) c1 c2 of
2691 [] => SOME (env, denv)
2692 | _ => NONE)
2693 handle CUnify (c1, c2, err) =>
2694 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2695 SOME (env, denv))
2696 else
2697 NONE
2698 | _ => NONE)
2654 end 2699 end
2655 in 2700 in
2656 ignore (foldl folder (env, denv) sgis2) 2701 ignore (foldl folder (env, denv) sgis2)
2657 end 2702 end
2658 2703
3191 checkKind env c' ck k; 3236 checkKind env c' ck k;
3192 ([(L'.DClass (x, n, c'), loc)], (env, denv, enD gs' @ gs)) 3237 ([(L'.DClass (x, n, c'), loc)], (env, denv, enD gs' @ gs))
3193 end 3238 end
3194 3239
3195 | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs)) 3240 | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs))
3241
3242 | L.DCookie (x, c) =>
3243 let
3244 val (c', k, gs') = elabCon (env, denv) c
3245 val (env, n) = E.pushENamed env x (L'.CApp (cookieOf (), c'), loc)
3246 in
3247 checkKind env c' k (L'.KType, loc);
3248 ([(L'.DCookie (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
3249 end
3196 3250
3197 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) 3251 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*)
3198 in 3252 in
3199 (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll), 3253 (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll),
3200 ("|tcs|", PD.string (Int.toString (length tcs)))];*) 3254 ("|tcs|", PD.string (Int.toString (length tcs)))];*)
3334 (cons, "?" ^ x) 3388 (cons, "?" ^ x)
3335 else 3389 else
3336 (SS.add (cons, x), x) 3390 (SS.add (cons, x), x)
3337 in 3391 in
3338 ((L'.SgiClass (x, n, c), loc) :: sgis, cons, vals, sgns, strs) 3392 ((L'.SgiClass (x, n, c), loc) :: sgis, cons, vals, sgns, strs)
3393 end
3394 | L'.SgiCookie (tn, x, n, c) =>
3395 let
3396 val (vals, x) =
3397 if SS.member (vals, x) then
3398 (vals, "?" ^ x)
3399 else
3400 (SS.add (vals, x), x)
3401 in
3402 ((L'.SgiCookie (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs)
3339 end) 3403 end)
3340 3404
3341 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis 3405 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
3342 in 3406 in
3343 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs) 3407 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs)