From eafb2bfc151efd5fe9a18dd5bba14141a1b832cf Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 20 Oct 2009 10:19:00 -0400
Subject: Add tuple pattern-matching at the constructor level

---
 demo/more/conference.ur  | 33 +++++++++++++++++++++++++++++++++
 demo/more/conference.urp |  2 ++
 demo/more/conference.urs | 20 ++++++++++++++++++++
 3 files changed, 55 insertions(+)
 create mode 100644 demo/more/conference.ur
 create mode 100644 demo/more/conference.urp
 create mode 100644 demo/more/conference.urs

(limited to 'demo')

diff --git a/demo/more/conference.ur b/demo/more/conference.ur
new file mode 100644
index 00000000..a028bc41
--- /dev/null
+++ b/demo/more/conference.ur
@@ -0,0 +1,33 @@
+con reviewMeta = fn (db :: Type, widget :: Type) =>
+                    {Show : db -> xbody,
+                     Widget : nm :: Name -> xml form [] [nm = widget],
+                     WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget],
+                     Parse : widget -> db,
+                     Inject : sql_injectable db}
+
+fun default [t] (sh : show t) (rd : read t) (inj : sql_injectable t) : reviewMeta (t, string) =
+    {Show = txt,
+     Widget = fn [nm :: Name] => <xml><textbox{nm}/></xml>,
+     WidgetPopulated = fn [nm :: Name] n =>
+                          <xml><textbox{nm} value={show n}/></xml>,
+     Parse = readError,
+     Inject = _}
+
+val int = default
+val float = default
+val string = default
+val bool = {Show = txt,
+            Widget = fn [nm :: Name] => <xml><checkbox{nm}/></xml>,
+            WidgetPopulated = fn [nm :: Name] b =>
+                                 <xml><checkbox{nm} checked={b}/></xml>,
+            Parse = fn x => x,
+            Inject = _}
+
+functor Make(M : sig
+                 con review :: {(Type * Type)}
+                 val review : $(map reviewMeta review)
+             end) = struct
+
+    fun main () = return <xml/>
+
+end
diff --git a/demo/more/conference.urp b/demo/more/conference.urp
new file mode 100644
index 00000000..399721d4
--- /dev/null
+++ b/demo/more/conference.urp
@@ -0,0 +1,2 @@
+
+conference
diff --git a/demo/more/conference.urs b/demo/more/conference.urs
new file mode 100644
index 00000000..696b8b32
--- /dev/null
+++ b/demo/more/conference.urs
@@ -0,0 +1,20 @@
+con reviewMeta = fn (db :: Type, widget :: Type) =>
+                    {Show : db -> xbody,
+                     Widget : nm :: Name -> xml form [] [nm = widget],
+                     WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget],
+                     Parse : widget -> db,
+                     Inject : sql_injectable db}
+
+val int : reviewMeta (int, string)
+val float : reviewMeta (float, string)
+val string : reviewMeta (string, string)
+val bool : reviewMeta (bool, bool)
+
+functor Make(M : sig
+                 con review :: {(Type * Type)}
+                 val review : $(map reviewMeta review)
+             end) : sig
+
+    val main : unit -> transaction page
+
+end
-- 
cgit v1.2.3