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)