Mercurial > urweb
changeset 334:9601c717d2f3
queryX
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 13 Sep 2008 19:49:53 -0400 |
| parents | c655eddc3795 |
| children | bc5015b89dd2 |
| files | lib/top.ur lib/top.urs src/disjoint.sml src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml src/mono_opt.sml tests/crud.ur |
| diffstat | 10 files changed, 65 insertions(+), 33 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/top.ur Sat Sep 13 14:58:57 2008 -0400 +++ b/lib/top.ur Sat Sep 13 19:49:53 2008 -0400 @@ -26,3 +26,11 @@ [[nm] ~ rest] => fn r1 r2 acc => <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) <xml></xml> + +fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) (q : sql_query tables exps) = + [tables ~ exps] => + fn (f : $(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables) + -> xml ctx [] []) => + query q + (fn fs acc => return <xml>{acc}{f fs}</xml>) + <xml></xml>
--- a/lib/top.urs Sat Sep 13 14:58:57 2008 -0400 +++ b/lib/top.urs Sat Sep 13 19:49:53 2008 -0400 @@ -19,3 +19,9 @@ -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest -> tf1 t -> tf2 t -> xml ctx [] []) -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] [] + +val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} + -> sql_query tables exps -> tables ~ exps + -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables) + -> xml ctx [] []) + -> transaction (xml ctx [] [])
--- a/src/disjoint.sml Sat Sep 13 14:58:57 2008 -0400 +++ b/src/disjoint.sml Sat Sep 13 19:49:53 2008 -0400 @@ -314,7 +314,7 @@ in case c of CDisjoint cs => doDisj cs - | TDisjoint cs => doDisj cs + | TDisjoint (Instantiate, c1, c2, c) => doDisj (c1, c2, c) | _ => (cAll, []) end
--- a/src/elab.sml Sat Sep 13 14:58:57 2008 -0400 +++ b/src/elab.sml Sat Sep 13 19:49:53 2008 -0400 @@ -46,10 +46,14 @@ Explicit | Implicit +datatype auto_instantiate = + Instantiate + | LeaveAlone + datatype con' = TFun of con * con | TCFun of explicitness * string * kind * con - | TDisjoint of con * con * con + | TDisjoint of auto_instantiate * con * con * con | TRecord of con | CRel of int
--- a/src/elab_print.sml Sat Sep 13 14:58:57 2008 -0400 +++ b/src/elab_print.sml Sat Sep 13 19:49:53 2008 -0400 @@ -80,15 +80,15 @@ string "->", space, p_con (E.pushCRel env x k) c]) - | TDisjoint (c1, c2, c3) => parenIf par (box [p_con env c1, - space, - string "~", - space, - p_con env c2, - space, - string "->", - space, - p_con env c3]) + | TDisjoint (_, c1, c2, c3) => parenIf par (box [p_con env c1, + space, + string "~", + space, + p_con env c2, + space, + string "->", + space, + p_con env c3]) | TRecord (CRecord (_, xcs), _) => box [string "{", p_list (fn (x, c) => box [p_name env x,
--- a/src/elab_util.sml Sat Sep 13 14:58:57 2008 -0400 +++ b/src/elab_util.sml Sat Sep 13 19:49:53 2008 -0400 @@ -119,14 +119,14 @@ S.map2 (mfc (bind (ctx, Rel (x, k))) c, fn c' => (TCFun (e, x, k', c'), loc))) - | TDisjoint (c1, c2, c3) => + | TDisjoint (ai, c1, c2, c3) => S.bind2 (mfc ctx c1, fn c1' => S.bind2 (mfc ctx c2, fn c2' => S.map2 (mfc ctx c3, fn c3' => - (TDisjoint (c1', c2', c3'), loc)))) + (TDisjoint (ai, c1', c2', c3'), loc)))) | TRecord c => S.map2 (mfc ctx c, fn c' =>
--- a/src/elaborate.sml Sat Sep 13 14:58:57 2008 -0400 +++ b/src/elaborate.sml Sat Sep 13 19:49:53 2008 -0400 @@ -239,7 +239,7 @@ checkKind env c1' k1 (L'.KRecord ku1, loc); checkKind env c2' k2 (L'.KRecord ku2, loc); - ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4) + ((L'.TDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4) end | L.TRecord c => let @@ -824,7 +824,7 @@ and unifyCons' (env, denv) c1 c2 = case (#1 c1, #1 c2) of - (L'.TDisjoint (x1, y1, t1), L'.TDisjoint (x2, y2, t2)) => + (L'.TDisjoint (_, x1, y1, t1), L'.TDisjoint (_, x2, y2, t2)) => let val gs1 = unifyCons' (env, denv) x1 x2 val gs2 = unifyCons' (env, denv) y1 y2 @@ -983,7 +983,8 @@ (L'.TCFun (L'.Explicit, "v", dom, (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc), (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc), - (L'.TDisjoint ((L'.CRecord + (L'.TDisjoint (L'.Instantiate, + (L'.CRecord ((L'.KUnit, loc), [((L'.CRel 2, loc), (L'.CUnit, loc))]), loc), @@ -1523,7 +1524,7 @@ checkKind env c1' k1 (L'.KRecord ku1, loc); checkKind env c2' k2 (L'.KRecord ku2, loc); - (e', (L'.TDisjoint (c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4) + (e', (L'.TDisjoint (L'.LeaveAlone, c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4) end | L.ERecord xes => @@ -2661,6 +2662,17 @@ | _ => str) | _ => str +val makeInstantiable = + let + fun kind k = k + fun con c = + case c of + L'.TDisjoint (L'.LeaveAlone, c1, c2, c) => L'.TDisjoint (L'.Instantiate, c1, c2, c) + | _ => c + in + U.Con.map {kind = kind, con = con} + end + fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = let (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*) @@ -2792,6 +2804,7 @@ val gs3 = checkCon (env, denv) e' et c' val (c', gs4) = normClassConstraint (env, denv) c' val (env', n) = E.pushENamed env x c' + val c' = makeInstantiable c' in (*prefaces "DVal" [("x", Print.PD.string x), ("c'", p_con env c')];*) @@ -2828,6 +2841,8 @@ val (e', et, gs1) = elabExp (env, denv) e val gs2 = checkCon (env, denv) e' et c' + + val c' = makeInstantiable c' in if allowable e then ()
--- a/src/explify.sml Sat Sep 13 14:58:57 2008 -0400 +++ b/src/explify.sml Sat Sep 13 19:49:53 2008 -0400 @@ -49,7 +49,7 @@ case c of L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc) | L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc) - | L.TDisjoint (_, _, c) => explifyCon c + | L.TDisjoint (_, _, _, c) => explifyCon c | L.TRecord c => (L'.TRecord (explifyCon c), loc) | L.CRel n => (L'.CRel n, loc)
--- a/src/mono_opt.sml Sat Sep 13 14:58:57 2008 -0400 +++ b/src/mono_opt.sml Sat Sep 13 19:49:53 2008 -0400 @@ -293,6 +293,14 @@ else e + | EWrite (EQuery {exps, tables, state, query, + initial = (EPrim (Prim.String ""), _), + body = (EStrcat ((ERel 0, _), e'), _)}, loc) => + EQuery {exps = exps, tables = tables, query = query, + state = (TRecord [], loc), + initial = (ERecord [], loc), + body = (optExp (EWrite e', loc), loc)} + | _ => e and optExp e = #1 (U.Exp.map {typ = typ, exp = exp} e)
--- a/tests/crud.ur Sat Sep 13 14:58:57 2008 -0400 +++ b/tests/crud.ur Sat Sep 13 19:49:53 2008 -0400 @@ -14,10 +14,9 @@ open constraints M val tab = M.tab -fun list () = - rows <- query (SELECT * FROM tab AS T) - (fn (fs : {T : $([Id = int] ++ M.cols)}) acc => return <body> - {acc} +fun main () : transaction page = + rows <- queryX (SELECT * FROM tab AS T) + (fn (fs : {T : $([Id = int] ++ M.cols)}) => <body> <tr> <td>{txt _ fs.T.Id}</td> {foldTRX2 [idT] [colMeta'] [tr] @@ -28,13 +27,13 @@ </tr>) [M.cols] (fs.T -- #Id) M.cols} </tr> - </body>) <body></body>; + </body>); return <html><head> - <title>List</title> + <title>{cdata M.title}</title> </head><body> - <h1>List</h1> + <h1>{cdata M.title}</h1> <table border={1}> <tr> <th>ID</th> </tr> @@ -42,12 +41,4 @@ </table> </body></html> -fun main () : transaction page = return <html><head> - <title>{cdata M.title}</title> - </head><body> - <h1>{cdata M.title}</h1> - - <li> <a link={list ()}>List all rows</a></li> -</body></html> - end