Mercurial > urweb

comparison src/elaborate.sml @ 203:dd82457fda82

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parsing and elaborating 'table'
author Adam Chlipala <adamc@hcoop.net>
date Thu, 14 Aug 2008 13:20:29 -0400
parents df5fd8f6913a
children cb8f69556975
comparison
equal deleted inserted replaced
202:af5bd54cbbd7 203:dd82457fda82
161 val strerror = (L'.StrError, dummy) 161 val strerror = (L'.StrError, dummy)
162 162
163 val int = ref cerror 163 val int = ref cerror
164 val float = ref cerror 164 val float = ref cerror
165 val string = ref cerror 165 val string = ref cerror
166 val table = ref cerror
166 167
167 local 168 local
168 val count = ref 0 169 val count = ref 0
169 in 170 in
170 171
1733 checkKind env c2' k2 (L'.KRecord (kunif loc), loc); 1734 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
1734 1735
1735 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3)) 1736 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3))
1736 end 1737 end
1737 1738
1739 | L.SgiTable (x, c) =>
1740 let
1741 val (c', k, gs) = elabCon (env, denv) c
1742 val (env, n) = E.pushENamed env x c'
1743 in
1744 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
1745 ([(L'.SgiTable (x, n, c'), loc)], (env, denv, gs))
1746 end
1747
1738 and elabSgn (env, denv) (sgn, loc) = 1748 and elabSgn (env, denv) (sgn, loc) =
1739 case sgn of 1749 case sgn of
1740 L.SgnConst sgis => 1750 L.SgnConst sgis =>
1741 let 1751 let
1742 val (sgis', (_, _, gs)) = ListUtil.foldlMapConcat elabSgn_item (env, denv, []) sgis 1752 val (sgis', (_, _, gs)) = ListUtil.foldlMapConcat elabSgn_item (env, denv, []) sgis
1793 (if SS.member (strs, x) then 1803 (if SS.member (strs, x) then
1794 sgnError env (DuplicateStr (loc, x)) 1804 sgnError env (DuplicateStr (loc, x))
1795 else 1805 else
1796 (); 1806 ();
1797 (cons, vals, sgns, SS.add (strs, x))) 1807 (cons, vals, sgns, SS.add (strs, x)))
1798 | L'.SgiConstraint _ => (cons, vals, sgns, strs)) 1808 | L'.SgiConstraint _ => (cons, vals, sgns, strs)
1809 | L'.SgiTable (x, _, _) =>
1810 (if SS.member (vals, x) then
1811 sgnError env (DuplicateVal (loc, x))
1812 else
1813 ();
1814 (cons, SS.add (vals, x), sgns, strs)))
1799 (SS.empty, SS.empty, SS.empty, SS.empty) sgis' 1815 (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
1800 in 1816 in
1801 ((L'.SgnConst sgis', loc), gs) 1817 ((L'.SgnConst sgis', loc), gs)
1802 end 1818 end
1803 | L.SgnVar x => 1819 | L.SgnVar x =>
1891 in 1907 in
1892 case self str of 1908 case self str of
1893 NONE => sgn 1909 NONE => sgn
1894 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs} 1910 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
1895 end 1911 end
1912
1913 fun tableOf env =
1914 case E.lookupStr env "Basis" of
1915 NONE => raise Fail "Elaborate.tableOf: Can't find Basis"
1916 | SOME (n, _) => (L'.CModProj (n, [], "sql_table"), ErrorMsg.dummySpan)
1896 1917
1897 fun dopen (env, denv) {str, strs, sgn} = 1918 fun dopen (env, denv) {str, strs, sgn} =
1898 let 1919 let
1899 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) 1920 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
1900 (L'.StrVar str, #2 sgn) strs 1921 (L'.StrVar str, #2 sgn) strs
1923 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc) 1944 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)
1924 | L'.SgiSgn (x, n, sgn) => 1945 | L'.SgiSgn (x, n, sgn) =>
1925 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc) 1946 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
1926 | L'.SgiConstraint (c1, c2) => 1947 | L'.SgiConstraint (c1, c2) =>
1927 (L'.DConstraint (c1, c2), loc) 1948 (L'.DConstraint (c1, c2), loc)
1949 | L'.SgiTable (x, n, c) =>
1950 (L'.DVal (x, n, (L'.CApp (tableOf env, c), loc),
1951 (L'.EModProj (str, strs, x), loc)), loc)
1928 in 1952 in
1929 (d, (E.declBinds env' d, denv')) 1953 (d, (E.declBinds env' d, denv'))
1930 end) 1954 end)
1931 (env, denv) sgis 1955 (env, denv) sgis
1932 | _ => (strError env (UnOpenable sgn); 1956 | _ => (strError env (UnOpenable sgn);
1975 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)] 1999 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
1976 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)] 2000 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)]
1977 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] 2001 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
1978 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] 2002 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
1979 | L'.DExport _ => [] 2003 | L'.DExport _ => []
2004 | L'.DTable (x, n, c) => [(L'.SgiTable (x, n, c), loc)]
1980 2005
1981 fun sgiBindsD (env, denv) (sgi, _) = 2006 fun sgiBindsD (env, denv) (sgi, _) =
1982 case sgi of 2007 case sgi of
1983 L'.SgiConstraint (c1, c2) => 2008 L'.SgiConstraint (c1, c2) =>
1984 (case D.assert env denv (c1, c2) of 2009 (case D.assert env denv (c1, c2) of
2167 handle CUnify (c1, c2, err) => 2192 handle CUnify (c1, c2, err) =>
2168 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2193 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2169 SOME (env, denv)) 2194 SOME (env, denv))
2170 else 2195 else
2171 NONE 2196 NONE
2197 | L'.SgiTable (x', n1, c1) =>
2198 if x = x' then
2199 (case unifyCons (env, denv) (L'.CApp (tableOf env, c1), loc) c2 of
2200 [] => SOME (env, denv)
2201 | _ => NONE)
2202 handle CUnify (c1, c2, err) =>
2203 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2204 SOME (env, denv))
2205 else
2206 NONE
2172 | _ => NONE) 2207 | _ => NONE)
2173 2208
2174 | L'.SgiStr (x, n2, sgn2) => 2209 | L'.SgiStr (x, n2, sgn2) =>
2175 seek (fn sgi1All as (sgi1, _) => 2210 seek (fn sgi1All as (sgi1, _) =>
2176 case sgi1 of 2211 case sgi1 of
2225 [] => () 2260 [] => ()
2226 | _ => raise Fail "subSgn: Sub-constraints remain"; 2261 | _ => raise Fail "subSgn: Sub-constraints remain";
2227 2262
2228 SOME (env, denv) 2263 SOME (env, denv)
2229 end 2264 end
2265 else
2266 NONE
2267 | _ => NONE)
2268
2269 | L'.SgiTable (x, n2, c2) =>
2270 seek (fn sgi1All as (sgi1, _) =>
2271 case sgi1 of
2272 L'.SgiTable (x', n1, c1) =>
2273 if x = x' then
2274 (case unifyCons (env, denv) c1 c2 of
2275 [] => SOME (env, denv)
2276 | _ => NONE)
2277 handle CUnify (c1, c2, err) =>
2278 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2279 SOME (env, denv))
2230 else 2280 else
2231 NONE 2281 NONE
2232 | _ => NONE) 2282 | _ => NONE)
2233 end 2283 end
2234 in 2284 in
2575 (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc) 2625 (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc)
2576 end 2626 end
2577 | _ => sgn 2627 | _ => sgn
2578 in 2628 in
2579 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs)) 2629 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs))
2630 end
2631
2632 | L.DTable (x, c) =>
2633 let
2634 val (c', k, gs) = elabCon (env, denv) c
2635 val (env, n) = E.pushENamed env x c'
2636 in
2637 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
2638 ([(L'.DTable (x, n, c'), loc)], (env, denv, gs))
2580 end 2639 end
2581 2640
2582 and elabStr (env, denv) (str, loc) = 2641 and elabStr (env, denv) (str, loc) =
2583 case str of 2642 case str of
2584 L.StrConst ds => 2643 L.StrConst ds =>
2667 else 2726 else
2668 (SS.add (strs, x), x) 2727 (SS.add (strs, x), x)
2669 in 2728 in
2670 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) 2729 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
2671 end 2730 end
2672 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)) 2731 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)
2732 | L'.SgiTable (x, n, c) =>
2733 let
2734 val (vals, x) =
2735 if SS.member (vals, x) then
2736 (vals, "?" ^ x)
2737 else
2738 (SS.add (vals, x), x)
2739 in
2740 ((L'.SgiTable (x, n, c), loc) :: sgis, cons, vals, sgns, strs)
2741 end)
2673 2742
2674 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis 2743 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
2675 in 2744 in
2676 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs) 2745 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs)
2677 end 2746 end
2749 | E.Named (n, (_, loc)) => r := (L'.CNamed n, loc) 2818 | E.Named (n, (_, loc)) => r := (L'.CNamed n, loc)
2750 2819
2751 val () = discoverC int "int" 2820 val () = discoverC int "int"
2752 val () = discoverC float "float" 2821 val () = discoverC float "float"
2753 val () = discoverC string "string" 2822 val () = discoverC string "string"
2823 val () = discoverC table "sql_table"
2754 2824
2755 fun elabDecl' (d, (env, gs)) = 2825 fun elabDecl' (d, (env, gs)) =
2756 let 2826 let
2757 val () = resetKunif () 2827 val () = resetKunif ()
2758 val () = resetCunif () 2828 val () = resetCunif ()