# HG changeset patch # User Adam Chlipala # Date 1224629092 14400 # Node ID c5a3d223f157ea0da2c80d1ea1eba41a96e0002c # Parent 81d9f42bb64122a482516bb344af403962d39fa2 Sql demo diff -r 81d9f42bb641 -r c5a3d223f157 demo/prose --- 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 @@

The ListFun module defines a functor for building list editing sub-applications. An argument to the functor Make 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.

The ListShop modules ties everything together by instantiating ListFun.Make with structures for integers and strings. show and read can be used for marshaling and unmarshaling in both cases because they are type-class-generic.

+ +sql.urp + +

We see a simple example of accessing a SQL database. The project file specifies the database to connect to.

+ +

A table 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).

+ +

The list function implements an HTML table view of all rows in the SQL table. The queryX 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.

+ +

Other functions demonstrate use of the dml 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.

+ +

diff -r 81d9f42bb641 -r c5a3d223f157 demo/sql.ur --- /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 => + {[row.T.A]} {[row.T.B]} {[row.T.C]} {[row.T.D]} + [delete] + ); + return + + + {rows} +
A B C D
+ +

+ + + + +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 +

Row added.

+ + {xml} + + +and delete a = + () <- dml (DELETE FROM t + WHERE t.A = {a}); + xml <- list (); + return +

Row deleted.

+ + {xml} + + +fun main () = + xml <- list (); + return + {xml} + diff -r 81d9f42bb641 -r c5a3d223f157 demo/sql.urp --- /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 diff -r 81d9f42bb641 -r c5a3d223f157 demo/sql.urs --- /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 diff -r 81d9f42bb641 -r c5a3d223f157 lib/basis.urs --- 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} diff -r 81d9f42bb641 -r c5a3d223f157 src/demo.sml --- 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 diff -r 81d9f42bb641 -r c5a3d223f157 src/monoize.sml --- 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 ""), loc), fm) + "submit" => normal ("input type=\"submit\"", NONE) | "textbox" => (case targs of diff -r 81d9f42bb641 -r c5a3d223f157 src/termination.sml --- 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)

A:
B:
C:
D: