Mercurial > urweb
changeset 203:dd82457fda82
Parsing and elaborating 'table'
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 14 Aug 2008 13:20:29 -0400 |
| parents | af5bd54cbbd7 |
| children | 241c9a0e3397 |
| files | lib/basis.lig src/elab.sml src/elab_env.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml src/lacweb.grm src/lacweb.lex src/source.sml src/source_print.sml tests/table.lac |
| diffstat | 12 files changed, 157 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/basis.lig Tue Aug 12 14:55:05 2008 -0400 +++ b/lib/basis.lig Thu Aug 14 13:20:29 2008 -0400 @@ -7,6 +7,13 @@ datatype bool = False | True +(** SQL *) + +con sql_table :: {Type} -> Type + + +(** XML *) + con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
--- a/src/elab.sml Tue Aug 12 14:55:05 2008 -0400 +++ b/src/elab.sml Thu Aug 14 13:20:29 2008 -0400 @@ -119,6 +119,7 @@ | SgiStr of string * int * sgn | SgiSgn of string * int * sgn | SgiConstraint of con * con + | SgiTable of string * int * con and sgn' = SgnConst of sgn_item list @@ -142,6 +143,7 @@ | DFfiStr of string * int * sgn | DConstraint of con * con | DExport of int * sgn * str + | DTable of string * int * con and str' = StrConst of decl list
--- a/src/elab_env.sml Tue Aug 12 14:55:05 2008 -0400 +++ b/src/elab_env.sml Thu Aug 14 13:20:29 2008 -0400 @@ -404,6 +404,16 @@ | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn | SgiConstraint _ => env + | SgiTable (x, n, c) => + (case lookupStr env "Basis" of + NONE => raise Fail "ElabEnv.sgiBinds: Can't find Basis" + | SOME (n, _) => + let + val t = (CApp ((CModProj (n, [], "table"), loc), c), loc) + in + pushENamedAs env x n t + end) + fun sgnSeek f sgis = let fun seek (sgis, sgns, strs, cons) = @@ -431,6 +441,7 @@ | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons) | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons) | SgiConstraint _ => seek (sgis, sgns, strs, cons) + | SgiTable _ => seek (sgis, sgns, strs, cons) in seek (sgis, IM.empty, IM.empty, IM.empty) end @@ -666,6 +677,7 @@ | SgiVal _ => seek (sgis, sgns, strs, cons, acc) | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) + | SgiTable _ => seek (sgis, sgns, strs, cons, acc) in seek (sgis, IM.empty, IM.empty, IM.empty, []) end @@ -725,5 +737,14 @@ | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn | DConstraint _ => env | DExport _ => env + | DTable (x, n, c) => + (case lookupStr env "Basis" of + NONE => raise Fail "ElabEnv.declBinds: Can't find Basis" + | SOME (n, _) => + let + val t = (CApp ((CModProj (n, [], "table"), loc), c), loc) + in + pushENamedAs env x n t + end) end
--- a/src/elab_print.sml Tue Aug 12 14:55:05 2008 -0400 +++ b/src/elab_print.sml Thu Aug 14 13:20:29 2008 -0400 @@ -447,6 +447,13 @@ string "~", space, p_con env c2] + | SgiTable (x, n, c) => box [string "table", + space, + p_named x n, + space, + string ":", + space, + p_con env c] and p_sgn env (sgn, _) = case sgn of @@ -596,6 +603,13 @@ string ":", space, p_sgn env sgn] + | DTable (x, n, c) => box [string "table", + space, + p_named x n, + space, + string ":", + space, + p_con env c] and p_str env (str, _) = case str of
--- a/src/elab_util.sml Tue Aug 12 14:55:05 2008 -0400 +++ b/src/elab_util.sml Thu Aug 14 13:20:29 2008 -0400 @@ -436,6 +436,10 @@ S.map2 (con ctx c2, fn c2' => (SgiConstraint (c1', c2'), loc))) + | SgiTable (x, n, c) => + S.map2 (con ctx c, + fn c' => + (SgiTable (x, n, c'), loc)) and sg ctx s acc = S.bindP (sg' ctx s acc, sgn ctx) @@ -458,7 +462,8 @@ bind (ctx, Str (x, sgn)) | SgiSgn (x, _, sgn) => bind (ctx, Sgn (x, sgn)) - | SgiConstraint _ => ctx, + | SgiConstraint _ => ctx + | SgiTable _ => ctx, sgi ctx si)) ctx sgis, fn sgis' => (SgnConst sgis', loc)) @@ -594,7 +599,8 @@ | DFfiStr (x, _, sgn) => bind (ctx, Str (x, sgn)) | DConstraint _ => ctx - | DExport _ => ctx, + | DExport _ => ctx + | DTable _ => ctx, mfd ctx d)) ctx ds, fn ds' => (StrConst ds', loc)) | StrVar _ => S.return2 strAll @@ -682,6 +688,11 @@ fn str' => (DExport (en, sgn', str'), loc))) + | DTable (x, n, c) => + S.map2 (mfc ctx c, + fn c' => + (DTable (x, n, c'), loc)) + and mfvi ctx (x, n, c, e) = S.bind2 (mfc ctx c, fn c' =>
--- a/src/elaborate.sml Tue Aug 12 14:55:05 2008 -0400 +++ b/src/elaborate.sml Thu Aug 14 13:20:29 2008 -0400 @@ -163,6 +163,7 @@ val int = ref cerror val float = ref cerror val string = ref cerror +val table = ref cerror local val count = ref 0 @@ -1735,6 +1736,15 @@ ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3)) end + | L.SgiTable (x, c) => + let + val (c', k, gs) = elabCon (env, denv) c + val (env, n) = E.pushENamed env x c' + in + checkKind env c' k (L'.KRecord (L'.KType, loc), loc); + ([(L'.SgiTable (x, n, c'), loc)], (env, denv, gs)) + end + and elabSgn (env, denv) (sgn, loc) = case sgn of L.SgnConst sgis => @@ -1795,7 +1805,13 @@ else (); (cons, vals, sgns, SS.add (strs, x))) - | L'.SgiConstraint _ => (cons, vals, sgns, strs)) + | L'.SgiConstraint _ => (cons, vals, sgns, strs) + | L'.SgiTable (x, _, _) => + (if SS.member (vals, x) then + sgnError env (DuplicateVal (loc, x)) + else + (); + (cons, SS.add (vals, x), sgns, strs))) (SS.empty, SS.empty, SS.empty, SS.empty) sgis' in ((L'.SgnConst sgis', loc), gs) @@ -1894,6 +1910,11 @@ | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs} end +fun tableOf env = + case E.lookupStr env "Basis" of + NONE => raise Fail "Elaborate.tableOf: Can't find Basis" + | SOME (n, _) => (L'.CModProj (n, [], "sql_table"), ErrorMsg.dummySpan) + fun dopen (env, denv) {str, strs, sgn} = let val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) @@ -1925,6 +1946,9 @@ (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc) | L'.SgiConstraint (c1, c2) => (L'.DConstraint (c1, c2), loc) + | L'.SgiTable (x, n, c) => + (L'.DVal (x, n, (L'.CApp (tableOf env, c), loc), + (L'.EModProj (str, strs, x), loc)), loc) in (d, (E.declBinds env' d, denv')) end) @@ -1977,6 +2001,7 @@ | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] | L'.DExport _ => [] + | L'.DTable (x, n, c) => [(L'.SgiTable (x, n, c), loc)] fun sgiBindsD (env, denv) (sgi, _) = case sgi of @@ -2169,6 +2194,16 @@ SOME (env, denv)) else NONE + | L'.SgiTable (x', n1, c1) => + if x = x' then + (case unifyCons (env, denv) (L'.CApp (tableOf env, c1), loc) c2 of + [] => SOME (env, denv) + | _ => NONE) + handle CUnify (c1, c2, err) => + (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); + SOME (env, denv)) + else + NONE | _ => NONE) | L'.SgiStr (x, n2, sgn2) => @@ -2230,6 +2265,21 @@ else NONE | _ => NONE) + + | L'.SgiTable (x, n2, c2) => + seek (fn sgi1All as (sgi1, _) => + case sgi1 of + L'.SgiTable (x', n1, c1) => + if x = x' then + (case unifyCons (env, denv) c1 c2 of + [] => SOME (env, denv) + | _ => NONE) + handle CUnify (c1, c2, err) => + (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); + SOME (env, denv)) + else + NONE + | _ => NONE) end in ignore (foldl folder (env, denv) sgis2) @@ -2579,6 +2629,15 @@ ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs)) end + | L.DTable (x, c) => + let + val (c', k, gs) = elabCon (env, denv) c + val (env, n) = E.pushENamed env x c' + in + checkKind env c' k (L'.KRecord (L'.KType, loc), loc); + ([(L'.DTable (x, n, c'), loc)], (env, denv, gs)) + end + and elabStr (env, denv) (str, loc) = case str of L.StrConst ds => @@ -2669,7 +2728,17 @@ in ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) end - | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)) + | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs) + | L'.SgiTable (x, n, c) => + let + val (vals, x) = + if SS.member (vals, x) then + (vals, "?" ^ x) + else + (SS.add (vals, x), x) + in + ((L'.SgiTable (x, n, c), loc) :: sgis, cons, vals, sgns, strs) + end) ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis in @@ -2751,6 +2820,7 @@ val () = discoverC int "int" val () = discoverC float "float" val () = discoverC string "string" + val () = discoverC table "sql_table" fun elabDecl' (d, (env, gs)) = let
--- a/src/explify.sml Tue Aug 12 14:55:05 2008 -0400 +++ b/src/explify.sml Thu Aug 14 13:20:29 2008 -0400 @@ -123,6 +123,7 @@ | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc) | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc) | L.SgiConstraint _ => NONE + | L.SgiTable _ => raise Fail "Explify SgiTable" and explifySgn (sgn, loc) = case sgn of @@ -151,6 +152,7 @@ | L.DFfiStr (x, n, sgn) => SOME (L'.DFfiStr (x, n, explifySgn sgn), loc) | L.DConstraint (c1, c2) => NONE | L.DExport (en, sgn, str) => SOME (L'.DExport (en, explifySgn sgn, explifyStr str), loc) + | L.DTable _ => raise Fail "Explify DTable" and explifyStr (str, loc) = case str of
--- a/src/lacweb.grm Tue Aug 12 14:55:05 2008 -0400 +++ b/src/lacweb.grm Thu Aug 14 13:20:29 2008 -0400 @@ -34,6 +34,11 @@ fun uppercaseFirst "" = "" | uppercaseFirst s = str (Char.toUpper (String.sub (s, 0))) ^ String.extract (s, 1, NONE) +fun entable t = + case #1 t of + TRecord c => c + | _ => t + %% %header (functor LacwebLrValsFn(structure Token : TOKEN)) @@ -50,7 +55,7 @@ | ARROW | LARROW | DARROW | STAR | FN | PLUSPLUS | MINUSMINUS | DOLLAR | TWIDDLE | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN - | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT + | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT | TABLE | CASE | IF | THEN | ELSE | XML_BEGIN of string | XML_END @@ -177,6 +182,7 @@ | m :: ms => (DOpenConstraints (m, ms), s (OPENleft, mpathright))) | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright)) | EXPORT spath (DExport spath, s (EXPORTleft, spathright)) + | TABLE SYMBOL COLON cexp (DTable (SYMBOL, entable cexp), s (TABLEleft, cexpright)) dargs : ([]) | SYMBOL dargs (SYMBOL :: dargs) @@ -234,6 +240,7 @@ s (FUNCTORleft, sgn2right)) | INCLUDE sgn (SgiInclude sgn, s (INCLUDEleft, sgnright)) | CONSTRAINT cterm TWIDDLE cterm (SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright)) + | TABLE SYMBOL COLON cexp (SgiTable (SYMBOL, entable cexp), s (TABLEleft, cexpright)) sgis : ([]) | sgi sgis (sgi :: sgis)
--- a/src/lacweb.lex Tue Aug 12 14:55:05 2008 -0400 +++ b/src/lacweb.lex Thu Aug 14 13:20:29 2008 -0400 @@ -279,6 +279,7 @@ <INITIAL> "constraint"=> (Tokens.CONSTRAINT (pos yypos, pos yypos + size yytext)); <INITIAL> "constraints"=> (Tokens.CONSTRAINTS (pos yypos, pos yypos + size yytext)); <INITIAL> "export" => (Tokens.EXPORT (pos yypos, pos yypos + size yytext)); +<INITIAL> "table" => (Tokens.TABLE (pos yypos, pos yypos + size yytext)); <INITIAL> "Type" => (Tokens.TYPE (pos yypos, pos yypos + size yytext)); <INITIAL> "Name" => (Tokens.NAME (pos yypos, pos yypos + size yytext));
--- a/src/source.sml Tue Aug 12 14:55:05 2008 -0400 +++ b/src/source.sml Thu Aug 14 13:20:29 2008 -0400 @@ -78,6 +78,7 @@ | SgiSgn of string * sgn | SgiInclude of sgn | SgiConstraint of con * con + | SgiTable of string * con and sgn' = SgnConst of sgn_item list @@ -131,6 +132,7 @@ | DConstraint of con * con | DOpenConstraints of string * string list | DExport of str + | DTable of string * con and str' = StrConst of decl list
--- a/src/source_print.sml Tue Aug 12 14:55:05 2008 -0400 +++ b/src/source_print.sml Thu Aug 14 13:20:29 2008 -0400 @@ -360,6 +360,13 @@ string "~", space, p_con c2] + | SgiTable (x, c) => box [string "table", + space, + string x, + space, + string ":", + space, + p_con c] and p_sgn (sgn, _) = case sgn of @@ -505,6 +512,13 @@ | DExport str => box [string "export", space, p_str str] + | DTable (x, c) => box [string "table", + space, + string x, + space, + string ":", + space, + p_con c] and p_str (str, _) = case str of