Mercurial > urweb

comparison src/elaborate.sml @ 460:d34834af4512

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Cookies through explify
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 10:43:48 -0500
parents f542bc3133dc
children 3f1b9231a37b
comparison
equal deleted inserted replaced
459:f542bc3133dc 460:d34834af4512
1930 checkKind env c2' k2 (L'.KRecord (kunif loc), loc); 1930 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
1931 1931
1932 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3)) 1932 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3))
1933 end 1933 end
1934 1934
1935 | L.SgiTable (x, c) =>
1936 let
1937 val (c', k, gs) = elabCon (env, denv) c
1938 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
1939 in
1940 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
1941 ([(L'.SgiTable (!basis_r, x, n, c'), loc)], (env, denv, gs))
1942 end
1943
1944 | L.SgiSequence x =>
1945 let
1946 val (env, n) = E.pushENamed env x (sequenceOf ())
1947 in
1948 ([(L'.SgiSequence (!basis_r, x, n), loc)], (env, denv, gs))
1949 end
1950
1951 | L.SgiClassAbs x => 1935 | L.SgiClassAbs x =>
1952 let 1936 let
1953 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 1937 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
1954 val (env, n) = E.pushCNamed env x k NONE 1938 val (env, n) = E.pushCNamed env x k NONE
1955 val env = E.pushClass env n 1939 val env = E.pushClass env n
1964 val (env, n) = E.pushCNamed env x k (SOME c') 1948 val (env, n) = E.pushCNamed env x k (SOME c')
1965 val env = E.pushClass env n 1949 val env = E.pushClass env n
1966 in 1950 in
1967 checkKind env c' ck k; 1951 checkKind env c' ck k;
1968 ([(L'.SgiClass (x, n, c'), loc)], (env, denv, [])) 1952 ([(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))
1978 end 1953 end
1979 1954
1980 and elabSgn (env, denv) (sgn, loc) = 1955 and elabSgn (env, denv) (sgn, loc) =
1981 case sgn of 1956 case sgn of
1982 L.SgnConst sgis => 1957 L.SgnConst sgis =>
2036 sgnError env (DuplicateStr (loc, x)) 2011 sgnError env (DuplicateStr (loc, x))
2037 else 2012 else
2038 (); 2013 ();
2039 (cons, vals, sgns, SS.add (strs, x))) 2014 (cons, vals, sgns, SS.add (strs, x)))
2040 | L'.SgiConstraint _ => (cons, vals, sgns, strs) 2015 | L'.SgiConstraint _ => (cons, vals, sgns, strs)
2041 | L'.SgiTable (_, x, _, _) =>
2042 (if SS.member (vals, x) then
2043 sgnError env (DuplicateVal (loc, x))
2044 else
2045 ();
2046 (cons, SS.add (vals, x), sgns, strs))
2047 | L'.SgiSequence (_, x, _) =>
2048 (if SS.member (vals, x) then
2049 sgnError env (DuplicateVal (loc, x))
2050 else
2051 ();
2052 (cons, SS.add (vals, x), sgns, strs))
2053 | L'.SgiClassAbs (x, _) => 2016 | L'.SgiClassAbs (x, _) =>
2054 (if SS.member (cons, x) then 2017 (if SS.member (cons, x) then
2055 sgnError env (DuplicateCon (loc, x)) 2018 sgnError env (DuplicateCon (loc, x))
2056 else 2019 else
2057 (); 2020 ();
2059 | L'.SgiClass (x, _, _) => 2022 | L'.SgiClass (x, _, _) =>
2060 (if SS.member (cons, x) then 2023 (if SS.member (cons, x) then
2061 sgnError env (DuplicateCon (loc, x)) 2024 sgnError env (DuplicateCon (loc, x))
2062 else 2025 else
2063 (); 2026 ();
2064 (SS.add (cons, x), vals, sgns, strs)) 2027 (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)))
2071 (SS.empty, SS.empty, SS.empty, SS.empty) sgis' 2028 (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
2072 in 2029 in
2073 ((L'.SgnConst sgis', loc), gs) 2030 ((L'.SgnConst sgis', loc), gs)
2074 end 2031 end
2075 | L.SgnVar x => 2032 | L.SgnVar x =>
2197 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc) 2154 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)
2198 | L'.SgiSgn (x, n, sgn) => 2155 | L'.SgiSgn (x, n, sgn) =>
2199 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc) 2156 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
2200 | L'.SgiConstraint (c1, c2) => 2157 | L'.SgiConstraint (c1, c2) =>
2201 (L'.DConstraint (c1, c2), loc) 2158 (L'.DConstraint (c1, c2), loc)
2202 | L'.SgiTable (_, x, n, c) =>
2203 (L'.DVal (x, n, (L'.CApp (tableOf (), c), loc),
2204 (L'.EModProj (str, strs, x), loc)), loc)
2205 | L'.SgiSequence (_, x, n) =>
2206 (L'.DVal (x, n, sequenceOf (),
2207 (L'.EModProj (str, strs, x), loc)), loc)
2208 | L'.SgiClassAbs (x, n) => 2159 | L'.SgiClassAbs (x, n) =>
2209 let 2160 let
2210 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 2161 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
2211 val c = (L'.CModProj (str, strs, x), loc) 2162 val c = (L'.CModProj (str, strs, x), loc)
2212 in 2163 in
2217 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 2168 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
2218 val c = (L'.CModProj (str, strs, x), loc) 2169 val c = (L'.CModProj (str, strs, x), loc)
2219 in 2170 in
2220 (L'.DCon (x, n, k, c), loc) 2171 (L'.DCon (x, n, k, c), loc)
2221 end 2172 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)
2225 in 2173 in
2226 (d, (E.declBinds env' d, denv')) 2174 (d, (E.declBinds env' d, denv'))
2227 end) 2175 end)
2228 (env, denv) sgis 2176 (env, denv) sgis
2229 | _ => (strError env (UnOpenable sgn); 2177 | _ => (strError env (UnOpenable sgn);
2272 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)] 2220 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
2273 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)] 2221 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)]
2274 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] 2222 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
2275 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] 2223 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
2276 | L'.DExport _ => [] 2224 | L'.DExport _ => []
2277 | L'.DTable (tn, x, n, c) => [(L'.SgiTable (tn, x, n, c), loc)] 2225 | L'.DTable (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), loc)), loc)]
2278 | L'.DSequence (tn, x, n) => [(L'.SgiSequence (tn, x, n), loc)] 2226 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
2279 | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)] 2227 | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)]
2280 | L'.DDatabase _ => [] 2228 | L'.DDatabase _ => []
2281 | L'.DCookie (tn, x, n, c) => [(L'.SgiCookie (tn, x, n, c), loc)] 2229 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
2282 2230
2283 fun sgiBindsD (env, denv) (sgi, _) = 2231 fun sgiBindsD (env, denv) (sgi, _) =
2284 case sgi of 2232 case sgi of
2285 L'.SgiConstraint (c1, c2) => 2233 L'.SgiConstraint (c1, c2) =>
2286 (case D.assert env denv (c1, c2) of 2234 (case D.assert env denv (c1, c2) of
2506 handle CUnify (c1, c2, err) => 2454 handle CUnify (c1, c2, err) =>
2507 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2455 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2508 SOME (env, denv)) 2456 SOME (env, denv))
2509 else 2457 else
2510 NONE 2458 NONE
2511 | L'.SgiTable (_, x', n1, c1) =>
2512 if x = x' then
2513 (case unifyCons (env, denv) (L'.CApp (tableOf (), c1), loc) c2 of
2514 [] => SOME (env, denv)
2515 | _ => NONE)
2516 handle CUnify (c1, c2, err) =>
2517 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2518 SOME (env, denv))
2519 else
2520 NONE
2521 | L'.SgiSequence (_, x', n1) =>
2522 if x = x' then
2523 (case unifyCons (env, denv) (sequenceOf ()) c2 of
2524 [] => SOME (env, denv)
2525 | _ => NONE)
2526 handle CUnify (c1, c2, err) =>
2527 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2528 SOME (env, denv))
2529 else
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
2541 | _ => NONE) 2459 | _ => NONE)
2542 2460
2543 | L'.SgiStr (x, n2, sgn2) => 2461 | L'.SgiStr (x, n2, sgn2) =>
2544 seek (fn sgi1All as (sgi1, _) => 2462 seek (fn sgi1All as (sgi1, _) =>
2545 case sgi1 of 2463 case sgi1 of
2594 [] => () 2512 [] => ()
2595 | _ => raise Fail "subSgn: Sub-constraints remain"; 2513 | _ => raise Fail "subSgn: Sub-constraints remain";
2596 2514
2597 SOME (env, denv) 2515 SOME (env, denv)
2598 end 2516 end
2599 else
2600 NONE
2601 | _ => NONE)
2602
2603 | L'.SgiTable (_, x, n2, c2) =>
2604 seek (fn sgi1All as (sgi1, _) =>
2605 case sgi1 of
2606 L'.SgiTable (_, x', n1, c1) =>
2607 if x = x' then
2608 (case unifyCons (env, denv) c1 c2 of
2609 [] => SOME (env, denv)
2610 | _ => NONE)
2611 handle CUnify (c1, c2, err) =>
2612 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2613 SOME (env, denv))
2614 else
2615 NONE
2616 | _ => NONE)
2617
2618 | L'.SgiSequence (_, x, n2) =>
2619 seek (fn sgi1All as (sgi1, _) =>
2620 case sgi1 of
2621 L'.SgiSequence (_, x', n1) =>
2622 if x = x' then
2623 SOME (env, denv)
2624 else 2517 else
2625 NONE 2518 NONE
2626 | _ => NONE) 2519 | _ => NONE)
2627 2520
2628 | L'.SgiClassAbs (x, n2) => 2521 | L'.SgiClassAbs (x, n2) =>
2679 in 2572 in
2680 case sgi1 of 2573 case sgi1 of
2681 L'.SgiClass (x', n1, c1) => found (x', n1, c1) 2574 L'.SgiClass (x', n1, c1) => found (x', n1, c1)
2682 | _ => NONE 2575 | _ => NONE
2683 end) 2576 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)
2699 end 2577 end
2700 in 2578 in
2701 ignore (foldl folder (env, denv) sgis2) 2579 ignore (foldl folder (env, denv) sgis2)
2702 end 2580 end
2703 2581
3345 (SS.add (strs, x), x) 3223 (SS.add (strs, x), x)
3346 in 3224 in
3347 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) 3225 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
3348 end 3226 end
3349 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs) 3227 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)
3350 | L'.SgiTable (tn, x, n, c) =>
3351 let
3352 val (vals, x) =
3353 if SS.member (vals, x) then
3354 (vals, "?" ^ x)
3355 else
3356 (SS.add (vals, x), x)
3357 in
3358 ((L'.SgiTable (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs)
3359 end
3360 | L'.SgiSequence (tn, x, n) =>
3361 let
3362 val (vals, x) =
3363 if SS.member (vals, x) then
3364 (vals, "?" ^ x)
3365 else
3366 (SS.add (vals, x), x)
3367 in
3368 ((L'.SgiSequence (tn, x, n), loc) :: sgis, cons, vals, sgns, strs)
3369 end
3370 | L'.SgiClassAbs (x, n) => 3228 | L'.SgiClassAbs (x, n) =>
3371 let 3229 let
3372 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 3230 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
3373 3231
3374 val (cons, x) = 3232 val (cons, x) =
3388 (cons, "?" ^ x) 3246 (cons, "?" ^ x)
3389 else 3247 else
3390 (SS.add (cons, x), x) 3248 (SS.add (cons, x), x)
3391 in 3249 in
3392 ((L'.SgiClass (x, n, c), loc) :: sgis, cons, vals, sgns, strs) 3250 ((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)
3403 end) 3251 end)
3404 3252
3405 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis 3253 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
3406 in 3254 in
3407 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs) 3255 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs)