Mercurial > urweb
changeset 410:c5a3d223f157
Sql demo
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 21 Oct 2008 18:44:52 -0400 |
| parents | 81d9f42bb641 |
| children | 06fcddcd20d3 |
| files | demo/prose demo/sql.ur demo/sql.urp demo/sql.urs lib/basis.urs src/demo.sml src/monoize.sml src/termination.sml |
| diffstat | 8 files changed, 120 insertions(+), 22 deletions(-) [+] |
line wrap: on
line diff
--- a/demo/prose Tue Oct 21 17:49:14 2008 -0400 +++ b/demo/prose Tue Oct 21 18:44:52 2008 -0400 @@ -59,3 +59,15 @@ <p>The <tt>ListFun</tt> module defines a functor for building list editing sub-applications. An argument to the functor <tt>Make</tt> must give the type to be stored in the lists, along with marshaling and unmarshaling functions. In return, the functor returns an entry point function.</p> <p>The <tt>ListShop</tt> modules ties everything together by instantiating <tt>ListFun.Make</tt> with structures for integers and strings. <tt>show</tt> and <tt>read</tt> can be used for marshaling and unmarshaling in both cases because they are type-class-generic.</p> + +sql.urp + +<p>We see a simple example of accessing a SQL database. The project file specifies the database to connect to.</p> + +<p>A <tt>table</tt> declaration declares a SQL table with rows of a particular record type. We can use embedded SQL syntax in a way that leads to all of our queries and updates being type-checked. Indeed, Ur/Web makes strong guarantees that it is impossible to execute invalid SQL queries or make bad assumptions about the types of tables for marshaling and unmarshaling (which happen implicitly).</p> + +<p>The <tt>list</tt> function implements an HTML table view of all rows in the SQL table. The <tt>queryX</tt> function takes two arguments: a SQL query and a function for generating XML fragments from query result rows. The query is run, and the fragments for the rows are concatenated together.</p> + +<p>Other functions demonstrate use of the <tt>dml</tt> function, for building a transaction from a SQL DML command. It is easy to insert antiquoted Ur code into queries and DML commands, and the type-checker catches mistakes in the types of the expressions that we insert.</p> + +<p>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/sql.ur Tue Oct 21 18:44:52 2008 -0400 @@ -0,0 +1,52 @@ +table t : { A : int, B : float, C : string, D : bool } + +fun list () = + rows <- queryX (SELECT * FROM t) + (fn row => <xml><tr> + <td>{[row.T.A]}</td> <td>{[row.T.B]}</td> <td>{[row.T.C]}</td> <td>{[row.T.D]}</td> + <td><a link={delete row.T.A}>[delete]</a></td> + </tr></xml>); + return <xml> + <table border=1> + <tr> <th>A</th> <th>B</th> <th>C</th> <th>D</th> </tr> + {rows} + </table> + + <br/><hr/><br/> + + <form> + <table> + <tr> <th>A:</th> <td><textbox{#A}/></td> </tr> + <tr> <th>B:</th> <td><textbox{#B}/></td> </tr> + <tr> <th>C:</th> <td><textbox{#C}/></td> </tr> + <tr> <th>D:</th> <td><checkbox{#D}/></td> </tr> + <tr> <th/> <td><submit action={add} value="Add Row"/></td> </tr> + </table> + </form> + </xml> + +and add r = + () <- dml (INSERT INTO t (A, B, C, D) + VALUES ({readError r.A}, {readError r.B}, {r.C}, {r.D})); + xml <- list (); + return <xml><body> + <p>Row added.</p> + + {xml} + </body></xml> + +and delete a = + () <- dml (DELETE FROM t + WHERE t.A = {a}); + xml <- list (); + return <xml><body> + <p>Row deleted.</p> + + {xml} + </body></xml> + +fun main () = + xml <- list (); + return <xml><body> + {xml} + </body></xml>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/sql.urp Tue Oct 21 18:44:52 2008 -0400 @@ -0,0 +1,3 @@ +database dbname=test + +sql
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/sql.urs Tue Oct 21 18:44:52 2008 -0400 @@ -0,0 +1,1 @@ +val main : unit -> transaction page
--- a/lib/basis.urs Tue Oct 21 17:49:14 2008 -0400 +++ b/lib/basis.urs Tue Oct 21 18:44:52 2008 -0400 @@ -339,6 +339,8 @@ val h1 : bodyTag [] val li : bodyTag [] +val hr : bodyTag [] + val a : bodyTag [Link = transaction page] val form : ctx ::: {Unit} -> bind ::: {Type}
--- a/src/demo.sml Tue Oct 21 17:49:14 2008 -0400 +++ b/src/demo.sml Tue Oct 21 18:44:52 2008 -0400 @@ -271,6 +271,15 @@ fun highlight () = doit (fn (src, html) => let + val dirty = + let + val srcSt = Posix.FileSys.stat src + val htmlSt = Posix.FileSys.stat html + in + Time.> (Posix.FileSys.ST.mtime srcSt, + Posix.FileSys.ST.mtime htmlSt) + end handle OS.SysErr _ => true + val cmd = "emacs --eval \"(progn " ^ "(global-font-lock-mode t) " ^ "(add-to-list 'load-path \\\"" @@ -287,8 +296,11 @@ ^ "\\\") " ^ "(kill-emacs))\"" in - print (">>> " ^ cmd ^ "\n"); - ignore (OS.Process.system cmd) + if dirty then + (print (">>> " ^ cmd ^ "\n"); + ignore (OS.Process.system cmd)) + else + () end) in if OS.Path.base file = "demo" then
--- a/src/monoize.sml Tue Oct 21 17:49:14 2008 -0400 +++ b/src/monoize.sml Tue Oct 21 18:44:52 2008 -0400 @@ -1535,7 +1535,8 @@ val s = (L'.EPrim (Prim.String (String.concat ["<", tag])), loc) in - foldl (fn ((x, e, t), (s, fm)) => + foldl (fn (("Action", _, _), acc) => acc + | ((x, e, t), (s, fm)) => case t of (L'.TFfi ("Basis", "bool"), _) => let @@ -1567,7 +1568,6 @@ case x of "Href" => urlifyExp | "Link" => urlifyExp - | "Action" => urlifyExp | _ => attrifyExp val xp = " " ^ lowercaseFirst x ^ "=\"" @@ -1633,7 +1633,7 @@ end in case tag of - "submit" => ((L'.EPrim (Prim.String "<input type=\"submit\"/>"), loc), fm) + "submit" => normal ("input type=\"submit\"", NONE) | "textbox" => (case targs of
--- a/src/termination.sml Tue Oct 21 17:49:14 2008 -0400 +++ b/src/termination.sml Tue Oct 21 18:44:52 2008 -0400 @@ -31,6 +31,7 @@ structure E = ElabEnv structure IM = IntBinaryMap +structure IS = IntBinarySet datatype pedigree = Func of int @@ -118,7 +119,7 @@ | (_, PRecord xps) => foldl (fn ((_, pt', _), penv) => pat penv (Rabble, pt')) penv xps end - fun exp (penv, calls) e = + fun exp parent (penv, calls) e = let val default = (Rabble, calls) @@ -157,7 +158,7 @@ if checkName x then calls else - #2 (exp (penv, calls) e)) calls xets + #2 (exp parent (penv, calls) e)) calls xets in (Rabble, [Rabble], calls) end @@ -165,7 +166,7 @@ | EApp (e1, e2) => let val (p1, ps, calls) = combiner calls e1 - val (p2, calls) = exp (penv, calls) e2 + val (p2, calls) = exp parent (penv, calls) e2 val p = case p1 of Rabble => Rabble @@ -191,7 +192,7 @@ end | _ => let - val (p, calls) = exp (penv, calls) e + val (p, calls) = exp parent (penv, calls) e in (*Print.prefaces "Head" [("e", ElabPrint.p_exp env e)]; print (p2s p ^ "\n");*) @@ -205,7 +206,7 @@ [] => raise Fail "Termination: Empty ps" | f :: ps => case f of - Func i => (i, ps) :: calls + Func i => (parent, i, ps) :: calls | _ => calls in (p, calls) @@ -227,27 +228,27 @@ | EApp _ => apps () | EAbs (_, _, _, e) => let - val (_, calls) = exp (Rabble :: penv, calls) e + val (_, calls) = exp parent (Rabble :: penv, calls) e in (Rabble, calls) end | ECApp _ => apps () | ECAbs (_, _, _, e) => let - val (_, calls) = exp (penv, calls) e + val (_, calls) = exp parent (penv, calls) e in (Rabble, calls) end | ERecord xets => let - val calls = foldl (fn ((_, e, _), calls) => #2 (exp (penv, calls) e)) calls xets + val calls = foldl (fn ((_, e, _), calls) => #2 (exp parent (penv, calls) e)) calls xets in (Rabble, calls) end | EField (e, x, _) => let - val (p, calls) = exp (penv, calls) e + val (p, calls) = exp parent (penv, calls) e val p = case p of Subarg (i, j, (TRecord (CRecord (_, xts), _), _)) => @@ -260,14 +261,14 @@ end | ECut (e, _, _) => let - val (_, calls) = exp (penv, calls) e + val (_, calls) = exp parent (penv, calls) e in (Rabble, calls) end | EWith (e1, _, e2, _) => let - val (_, calls) = exp (penv, calls) e1 - val (_, calls) = exp (penv, calls) e2 + val (_, calls) = exp parent (penv, calls) e1 + val (_, calls) = exp parent (penv, calls) e2 in (Rabble, calls) end @@ -275,12 +276,12 @@ | ECase (e, pes, _) => let - val (p, calls) = exp (penv, calls) e + val (p, calls) = exp parent (penv, calls) e val calls = foldl (fn ((pt, e), calls) => let val penv = pat penv (p, pt) - val (_, calls) = exp (penv, calls) e + val (_, calls) = exp parent (penv, calls) e in calls end) calls pes @@ -289,7 +290,7 @@ end | EError => (Rabble, calls) - | EUnif (ref (SOME e)) => exp (penv, calls) e + | EUnif (ref (SOME e)) => exp parent (penv, calls) e | EUnif (ref NONE) => (Rabble, calls) end @@ -301,20 +302,35 @@ unravel (e, j + 1, Arg (i, j, t) :: penv) | ECAbs (_, _, _, e) => unravel (e, j, penv) - | _ => (j, #2 (exp (penv, calls) e)) + | _ => (j, #2 (exp f (penv, calls) e)) in unravel (e, 0, []) end val (ns, calls) = ListUtil.foldliMap doVali [] vis + fun isRecursive (from, to, _) = + let + fun search (at, soFar) = + at = from + orelse List.exists (fn (from', to', _) => + from' = at + andalso not (IS.member (soFar, to')) + andalso search (to', IS.add (soFar, to'))) + calls + in + search (to, IS.empty) + end + + val calls = List.filter isRecursive calls + fun search (ns, choices) = case ns of [] => let val choices = rev choices in - List.all (fn (f, args) => + List.all (fn (_, f, args) => let val recArg = List.nth (choices, f)