changeset 418:ad7e854a518c

Metaform demos, minus prose
author Adam Chlipala <adamc@hcoop.net>
date Thu, 23 Oct 2008 14:03:12 -0400
parents e0e9e9eca1cb
children cb5897276abf
files demo/metaform.ur demo/metaform.urs demo/metaform1.ur demo/metaform1.urp demo/metaform1.urs demo/metaform2.ur demo/metaform2.urp demo/metaform2.urs demo/prose lib/top.ur lib/top.urs src/cjr_print.sml
diffstat 12 files changed, 95 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/metaform.ur	Thu Oct 23 14:03:12 2008 -0400
@@ -0,0 +1,28 @@
+functor Make (M : sig
+                  con fs :: {Unit}
+                  val names : $(mapUT string fs)
+              end) = struct
+
+    fun handler values = return <xml><body>
+      {foldURX2 [string] [string] [body]
+       (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] name value => <xml>
+         <li> {[name]} = {[value]}</li>
+       </xml>)
+       [M.fs] M.names values}
+    </body></xml>
+
+    fun main () = return <xml><body>
+      <form>
+        {foldUR [string] [fn cols :: {Unit} => xml form [] (mapUT string cols)]
+                (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] name
+                                 (acc : xml form [] (mapUT string rest)) => <xml>
+                                   <li> {[name]}: <textbox{nm}/></li>
+                                   {useMore acc}
+                                 </xml>)
+                <xml/>
+                [M.fs] M.names}
+        <submit action={handler}/>
+      </form>
+    </body></xml>
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/metaform.urs	Thu Oct 23 14:03:12 2008 -0400
@@ -0,0 +1,6 @@
+functor Make (M : sig
+                  con fs :: {Unit}
+                  val names : $(mapUT string fs)
+              end) : sig
+    val main : unit -> transaction page
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/metaform1.ur	Thu Oct 23 14:03:12 2008 -0400
@@ -0,0 +1,3 @@
+open Metaform.Make(struct
+                       val names = {A = "Tic", B = "Tac", C = "Toe"}
+                   end)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/metaform1.urp	Thu Oct 23 14:03:12 2008 -0400
@@ -0,0 +1,3 @@
+
+metaform
+metaform1
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/metaform1.urs	Thu Oct 23 14:03:12 2008 -0400
@@ -0,0 +1,1 @@
+val main : unit -> transaction page
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/metaform2.ur	Thu Oct 23 14:03:12 2008 -0400
@@ -0,0 +1,12 @@
+structure MM = Metaform.Make(struct
+                                 val names = {X = "x", Y = "y"}
+                             end)
+
+fun diversion () = return <xml><body>
+  Welcome to the diversion.
+</body></xml>
+
+fun main () = return <xml><body>
+  <li> <a link={diversion ()}>See something shiny!</a></li>
+  <li> <a link={MM.main ()}>Fill out a form!</a></li>
+</body></xml>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/metaform2.urp	Thu Oct 23 14:03:12 2008 -0400
@@ -0,0 +1,3 @@
+
+metaform
+metaform2
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/metaform2.urs	Thu Oct 23 14:03:12 2008 -0400
@@ -0,0 +1,1 @@
+val main : unit -> transaction page
--- a/demo/prose	Thu Oct 23 12:58:35 2008 -0400
+++ b/demo/prose	Thu Oct 23 14:03:12 2008 -0400
@@ -104,3 +104,7 @@
 tcSum.urp
 
 <p>It's easy to adapt the last example to use type classes, such that we can sum the fields of records based on any numeric type.</p>
+
+metaform1.urp
+
+metaform2.urp
--- a/lib/top.ur	Thu Oct 23 12:58:35 2008 -0400
+++ b/lib/top.ur	Thu Oct 23 14:03:12 2008 -0400
@@ -36,6 +36,26 @@
                  f [nm] [rest] r.nm (acc (r -- nm)))
              (fn _ => i)
 
+fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type)
+           (f : nm :: Name -> rest :: {Unit}
+                -> fn [[nm] ~ rest] =>
+                      tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
+           (i : tr []) =
+    fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r]
+             (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
+                              [[nm] ~ rest] r1 r2 =>
+                 f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+             (fn _ _ => i)
+
+fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit})
+           (f : nm :: Name -> rest :: {Unit}
+                -> fn [[nm] ~ rest] =>
+                      tf1 -> tf2 -> xml ctx [] []) =
+    foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
+            (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] v1 v2 acc =>
+                <xml>{f [nm] [rest] v1 v2}{acc}</xml>)
+            <xml/>
+
 fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
            (f : nm :: Name -> t :: Type -> rest :: {Type}
                 -> fn [[nm] ~ rest] =>
--- a/lib/top.urs	Thu Oct 23 12:58:35 2008 -0400
+++ b/lib/top.urs	Thu Oct 23 14:03:12 2008 -0400
@@ -29,6 +29,18 @@
                        tf -> tr rest -> tr ([nm] ++ rest))
              -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r
 
+val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
+             -> (nm :: Name -> rest :: {Unit}
+                 -> fn [[nm] ~ rest] =>
+                       tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
+             -> tr [] -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
+
+val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
+              -> (nm :: Name -> rest :: {Unit}
+                  -> fn [[nm] ~ rest] =>
+                        tf1 -> tf2 -> xml ctx [] [])
+              -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
+
 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
              -> (nm :: Name -> t :: Type -> rest :: {Type}
                  -> fn [[nm] ~ rest] =>
--- a/src/cjr_print.sml	Thu Oct 23 12:58:35 2008 -0400
+++ b/src/cjr_print.sml	Thu Oct 23 14:03:12 2008 -0400
@@ -1466,7 +1466,8 @@
             let
                 fun unurlify' rf t =
                     case t of
-                        TFfi (m, t) => string ("uw_" ^ ident m ^ "_unurlify" ^ capitalize t ^ "(ctx, &request)")
+                        TFfi ("Basis", "unit") => string ("uw_unit_v")
+                      | TFfi (m, t) => string ("uw_" ^ ident m ^ "_unurlify" ^ capitalize t ^ "(ctx, &request)")
 
                       | TRecord 0 => string "uw_unit_v"
                       | TRecord i =>