Mercurial > urweb

comparison src/elaborate.sml @ 338:e976b187d73a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
SQL sequences
author Adam Chlipala <adamc@hcoop.net>
date Sun, 14 Sep 2008 11:02:18 -0400
parents 9601c717d2f3
children 075b36dbb1a4
comparison
equal deleted inserted replaced
337:18d5affa790d 338:e976b187d73a
1646 end 1646 end
1647 1647
1648 val hnormSgn = E.hnormSgn 1648 val hnormSgn = E.hnormSgn
1649 1649
1650 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan) 1650 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan)
1651 fun sequenceOf () = (L'.CModProj (!basis_r, [], "sql_sequence"), ErrorMsg.dummySpan)
1651 1652
1652 fun elabSgn_item ((sgi, loc), (env, denv, gs)) = 1653 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
1653 case sgi of 1654 case sgi of
1654 L.SgiConAbs (x, k) => 1655 L.SgiConAbs (x, k) =>
1655 let 1656 let
1824 val (c', k, gs) = elabCon (env, denv) c 1825 val (c', k, gs) = elabCon (env, denv) c
1825 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc) 1826 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
1826 in 1827 in
1827 checkKind env c' k (L'.KRecord (L'.KType, loc), loc); 1828 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
1828 ([(L'.SgiTable (!basis_r, x, n, c'), loc)], (env, denv, gs)) 1829 ([(L'.SgiTable (!basis_r, x, n, c'), loc)], (env, denv, gs))
1830 end
1831
1832 | L.SgiSequence x =>
1833 let
1834 val (env, n) = E.pushENamed env x (sequenceOf ())
1835 in
1836 ([(L'.SgiSequence (!basis_r, x, n), loc)], (env, denv, gs))
1829 end 1837 end
1830 1838
1831 | L.SgiClassAbs x => 1839 | L.SgiClassAbs x =>
1832 let 1840 let
1833 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 1841 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
1913 (if SS.member (vals, x) then 1921 (if SS.member (vals, x) then
1914 sgnError env (DuplicateVal (loc, x)) 1922 sgnError env (DuplicateVal (loc, x))
1915 else 1923 else
1916 (); 1924 ();
1917 (cons, SS.add (vals, x), sgns, strs)) 1925 (cons, SS.add (vals, x), sgns, strs))
1926 | L'.SgiSequence (_, x, _) =>
1927 (if SS.member (vals, x) then
1928 sgnError env (DuplicateVal (loc, x))
1929 else
1930 ();
1931 (cons, SS.add (vals, x), sgns, strs))
1918 | L'.SgiClassAbs (x, _) => 1932 | L'.SgiClassAbs (x, _) =>
1919 (if SS.member (cons, x) then 1933 (if SS.member (cons, x) then
1920 sgnError env (DuplicateCon (loc, x)) 1934 sgnError env (DuplicateCon (loc, x))
1921 else 1935 else
1922 (); 1936 ();
2059 | L'.SgiConstraint (c1, c2) => 2073 | L'.SgiConstraint (c1, c2) =>
2060 (L'.DConstraint (c1, c2), loc) 2074 (L'.DConstraint (c1, c2), loc)
2061 | L'.SgiTable (_, x, n, c) => 2075 | L'.SgiTable (_, x, n, c) =>
2062 (L'.DVal (x, n, (L'.CApp (tableOf (), c), loc), 2076 (L'.DVal (x, n, (L'.CApp (tableOf (), c), loc),
2063 (L'.EModProj (str, strs, x), loc)), loc) 2077 (L'.EModProj (str, strs, x), loc)), loc)
2078 | L'.SgiSequence (_, x, n) =>
2079 (L'.DVal (x, n, sequenceOf (),
2080 (L'.EModProj (str, strs, x), loc)), loc)
2064 | L'.SgiClassAbs (x, n) => 2081 | L'.SgiClassAbs (x, n) =>
2065 let 2082 let
2066 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 2083 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
2067 val c = (L'.CModProj (str, strs, x), loc) 2084 val c = (L'.CModProj (str, strs, x), loc)
2068 in 2085 in
2126 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)] 2143 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)]
2127 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] 2144 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
2128 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] 2145 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
2129 | L'.DExport _ => [] 2146 | L'.DExport _ => []
2130 | L'.DTable (tn, x, n, c) => [(L'.SgiTable (tn, x, n, c), loc)] 2147 | L'.DTable (tn, x, n, c) => [(L'.SgiTable (tn, x, n, c), loc)]
2148 | L'.DSequence (tn, x, n) => [(L'.SgiSequence (tn, x, n), loc)]
2131 | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)] 2149 | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)]
2132 | L'.DDatabase _ => [] 2150 | L'.DDatabase _ => []
2133 2151
2134 fun sgiBindsD (env, denv) (sgi, _) = 2152 fun sgiBindsD (env, denv) (sgi, _) =
2135 case sgi of 2153 case sgi of
2353 handle CUnify (c1, c2, err) => 2371 handle CUnify (c1, c2, err) =>
2354 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2372 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2355 SOME (env, denv)) 2373 SOME (env, denv))
2356 else 2374 else
2357 NONE 2375 NONE
2376 | L'.SgiSequence (_, x', n1) =>
2377 if x = x' then
2378 (case unifyCons (env, denv) (sequenceOf ()) c2 of
2379 [] => SOME (env, denv)
2380 | _ => NONE)
2381 handle CUnify (c1, c2, err) =>
2382 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2383 SOME (env, denv))
2384 else
2385 NONE
2358 | _ => NONE) 2386 | _ => NONE)
2359 2387
2360 | L'.SgiStr (x, n2, sgn2) => 2388 | L'.SgiStr (x, n2, sgn2) =>
2361 seek (fn sgi1All as (sgi1, _) => 2389 seek (fn sgi1All as (sgi1, _) =>
2362 case sgi1 of 2390 case sgi1 of
2426 [] => SOME (env, denv) 2454 [] => SOME (env, denv)
2427 | _ => NONE) 2455 | _ => NONE)
2428 handle CUnify (c1, c2, err) => 2456 handle CUnify (c1, c2, err) =>
2429 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2457 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2430 SOME (env, denv)) 2458 SOME (env, denv))
2459 else
2460 NONE
2461 | _ => NONE)
2462
2463 | L'.SgiSequence (_, x, n2) =>
2464 seek (fn sgi1All as (sgi1, _) =>
2465 case sgi1 of
2466 L'.SgiSequence (_, x', n1) =>
2467 if x = x' then
2468 SOME (env, denv)
2431 else 2469 else
2432 NONE 2470 NONE
2433 | _ => NONE) 2471 | _ => NONE)
2434 2472
2435 | L'.SgiClassAbs (x, n2) => 2473 | L'.SgiClassAbs (x, n2) =>
3021 val (c', k, gs') = elabCon (env, denv) c 3059 val (c', k, gs') = elabCon (env, denv) c
3022 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc) 3060 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
3023 in 3061 in
3024 checkKind env c' k (L'.KRecord (L'.KType, loc), loc); 3062 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
3025 ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs)) 3063 ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
3064 end
3065 | L.DSequence x =>
3066 let
3067 val (env, n) = E.pushENamed env x (sequenceOf ())
3068 in
3069 ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs))
3026 end 3070 end
3027 3071
3028 | L.DClass (x, c) => 3072 | L.DClass (x, c) =>
3029 let 3073 let
3030 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 3074 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
3145 else 3189 else
3146 (SS.add (vals, x), x) 3190 (SS.add (vals, x), x)
3147 in 3191 in
3148 ((L'.SgiTable (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs) 3192 ((L'.SgiTable (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs)
3149 end 3193 end
3194 | L'.SgiSequence (tn, x, n) =>
3195 let
3196 val (vals, x) =
3197 if SS.member (vals, x) then
3198 (vals, "?" ^ x)
3199 else
3200 (SS.add (vals, x), x)
3201 in
3202 ((L'.SgiSequence (tn, x, n), loc) :: sgis, cons, vals, sgns, strs)
3203 end
3150 | L'.SgiClassAbs (x, n) => 3204 | L'.SgiClassAbs (x, n) =>
3151 let 3205 let
3152 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 3206 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
3153 3207
3154 val (cons, x) = 3208 val (cons, x) =