changeset 422:0ce90d4d9ae7

Crud2 demo
author Adam Chlipala <adamc@hcoop.net>
date Thu, 23 Oct 2008 18:45:10 -0400
parents 0767d7ad0c3a
children 82067ea6e723
files demo/crud2.sql demo/crud2.ur demo/crud2.urp demo/prose lib/basis.urs lib/top.ur lib/top.urs src/monoize.sml
diffstat 8 files changed, 64 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/crud2.sql	Thu Oct 23 18:45:10 2008 -0400
@@ -0,0 +1,6 @@
+CREATE TABLE uw_Crud2_t(uw_id int8 NOT NULL, uw_nam text NOT NULL, 
+                         uw_ready bool NOT NULL);
+ 
+ CREATE SEQUENCE uw_Crud2_Crud_Make_seq;
+  
+  
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/crud2.ur	Thu Oct 23 18:45:10 2008 -0400
@@ -0,0 +1,34 @@
+table t : {Id : int, Nam : string, Ready : bool}
+
+open Crud.Make(struct
+                   val tab = t
+                             
+                   val title = "Are you ready?"
+
+                   val cols = {Nam = Crud.string "Name",
+                               Ready = {Nam = "Ready",
+                                        Show = (fn b => if b then
+                                                            <xml>Ready!</xml>
+                                                        else
+                                                            <xml>Not ready</xml>),
+                                        Widget = (fn (nm :: Name) => <xml>
+                                          <select{nm}>
+                                            <option>Ready</option>
+                                            <option>Not ready</option>
+                                          </select>
+                                        </xml>),
+                                        WidgetPopulated = (fn (nm :: Name) b => <xml>
+                                          <select{nm}>
+                                            <option selected={b}>Ready</option>
+                                            <option selected={not b}>Not ready</option>
+                                          </select>
+                                        </xml>),
+                                        Parse = (fn s =>
+                                                    case s of
+                                                        "Ready" => True
+                                                      | "Not ready" => False
+                                                      | _ => error <xml>Invalid ready/not ready</xml>),
+                                        Inject = _
+                                       }
+                              }
+               end)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/crud2.urp	Thu Oct 23 18:45:10 2008 -0400
@@ -0,0 +1,5 @@
+database dbname=test
+sql crud2.sql
+
+crud
+crud2
--- a/demo/prose	Thu Oct 23 18:18:51 2008 -0400
+++ b/demo/prose	Thu Oct 23 18:45:10 2008 -0400
@@ -152,3 +152,7 @@
 <p>Looking at <tt>crud1.ur</tt>, we see that a use of the functor is almost trivial.  Only the value components of the argument structure must be provided.  The column row type is inferred, and the disjointness constraint is proved automatically.</p>
 
 <p>We won't go into detail on the implementation of <tt>Crud.Make</tt>.  The types of the functions used there can be found in the signatures of the built-in <tt>Basis</tt> module and the <tt>Top</tt> module from the standard library.  The signature of the first and the signature and implementation of the second can be found in the <tt>lib</tt> directory of the Ur/Web distribution.</p>
+
+crud2.urp
+
+<p>This example shows another application of <tt>Crud.Make</tt>.  We mix one standard column with one customized column.  We write an underscore for the <tt>Inject</tt> field of meta-data, since the type class facility can infer that witness.</p>
--- a/lib/basis.urs	Thu Oct 23 18:18:51 2008 -0400
+++ b/lib/basis.urs	Thu Oct 23 18:45:10 2008 -0400
@@ -18,6 +18,7 @@
 val eq_float : eq float
 val eq_string : eq string
 val eq_bool : eq bool
+val mkEq : t ::: Type -> (t -> t -> bool) -> eq t
 
 class num
 val zero : t ::: Type -> num t -> t
@@ -365,7 +366,7 @@
 
 con select = [Select]
 val select : formTag string select []
-val option : unit -> tag [Value = string] select [] [] []
+val option : unit -> tag [Value = string, Selected = bool] select [] [] []
 
 val submit : ctx ::: {Unit} ->  use ::: {Type}
              -> fn [[Form] ~ ctx] =>
--- a/lib/top.ur	Thu Oct 23 18:18:51 2008 -0400
+++ b/lib/top.ur	Thu Oct 23 18:45:10 2008 -0400
@@ -1,3 +1,5 @@
+fun not b = if b then False else True
+
 con idT (t :: Type) = t
 con record (t :: {Type}) = $t
 con fstTT (t :: (Type * Type)) = t.1
--- a/lib/top.urs	Thu Oct 23 18:18:51 2008 -0400
+++ b/lib/top.urs	Thu Oct 23 18:45:10 2008 -0400
@@ -1,3 +1,5 @@
+val not : bool -> bool
+
 con idT = fn t :: Type => t
 con record = fn t :: {Type} => $t
 con fstTT = fn t :: (Type * Type) => t.1
--- a/src/monoize.sml	Thu Oct 23 18:18:51 2008 -0400
+++ b/src/monoize.sml	Thu Oct 23 18:45:10 2008 -0400
@@ -597,6 +597,15 @@
                                  (L'.TFfi ("Basis", "bool"), loc),
                                  (L'.EBinop ("!strcmp", (L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc),
              fm)
+          | L.ECApp ((L.EFfi ("Basis", "mkEq"), _), t) =>
+            let
+                val t = monoType env t
+                val b = (L'.TFfi ("Basis", "bool"), loc)
+                val dom = (L'.TFun (t, (L'.TFun (t, b), loc)), loc)
+            in
+                ((L'.EAbs ("f", dom, dom,
+                           (L'.ERel 0, loc)), loc), fm)
+            end
 
           | L.ECApp ((L.EFfi ("Basis", "zero"), _), t) =>
             let