From bfeac162a328dba937a28e747e4fc4006fac500c Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 10 Oct 2010 13:07:38 -0400
Subject: Flex kinds for type-level tuples; ::_ notation

---
 demo/batchFun.ur | 22 ++++++++--------------
 demo/crud.ur     | 46 ++++++++++++++++++----------------------------
 demo/metaform.ur |  6 +++---
 3 files changed, 29 insertions(+), 45 deletions(-)

(limited to 'demo')

diff --git a/demo/batchFun.ur b/demo/batchFun.ur
index f665b132..ca48c7dc 100644
--- a/demo/batchFun.ur
+++ b/demo/batchFun.ur
@@ -6,7 +6,7 @@ con colMeta = fn (db :: Type, state :: Type) =>
                   NewState : transaction state,
                   Widget : state -> xbody,
                   ReadState : state -> transaction db}
-con colsMeta = fn cols :: {(Type * Type)} => $(map colMeta cols)
+con colsMeta = fn cols => $(map colMeta cols)
 
 fun default [t] (sh : show t) (rd : read t) (inj : sql_injectable t)
             name : colMeta (t, source string) =
@@ -46,10 +46,8 @@ functor Make(M : sig
     fun add r =
         dml (insert t
                     (@foldR2 [fst] [colMeta]
-                      [fn cols => $(map (fn t :: (Type * Type) =>
-                                            sql_exp [] [] [] t.1) cols)]
-                      (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
-                                       [[nm] ~ rest] input col acc =>
+                      [fn cols => $(map (fn t => sql_exp [] [] [] t.1) cols)]
+                      (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] input col acc =>
                           acc ++ {nm = @sql_inject col.Inject input})
                       {} M.fl (r -- #Id) M.cols
                       ++ {Id = (SQL {[r.Id]})}))
@@ -73,8 +71,7 @@ functor Make(M : sig
                     <tr>
                       <td>{[r.Id]}</td>
                       {@mapX2 [colMeta] [fst] [_]
-                        (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
-                                         [[nm] ~ rest] m v =>
+                        (fn [nm :: Name] [p ::_] [rest ::_] [[nm] ~ rest] m v =>
                             <xml><td>{m.Show v}</td></xml>)
                         M.fl M.cols (r -- #Id)}
                       {if withDel then
@@ -89,8 +86,7 @@ functor Make(M : sig
               <tr>
                 <th>Id</th>
                 {@mapX [colMeta] [_]
-                  (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
-                                   [[nm] ~ rest] m =>
+                  (fn [nm :: Name] [p ::_] [rest ::_] [[nm] ~ rest] m =>
                       <xml><th>{[m.Nam]}</th></xml>)
                   M.fl M.cols}
               </tr>
@@ -104,7 +100,7 @@ functor Make(M : sig
 
         id <- source "";
         inps <- @foldR [colMeta] [fn r => transaction ($(map snd r))]
-                 (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] m acc =>
+                 (fn [nm :: Name] [p ::_] [rest ::_] [[nm] ~ rest] m acc =>
                      s <- m.NewState;
                      r <- acc;
                      return ({nm = s} ++ r))
@@ -115,8 +111,7 @@ functor Make(M : sig
             fun add () =
                 id <- get id;
                 vs <- @foldR2 [colMeta] [snd] [fn r => transaction ($(map fst r))]
-                       (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
-                                        [[nm] ~ rest] m s acc =>
+                       (fn [nm :: Name] [p ::_] [rest ::_] [[nm] ~ rest] m s acc =>
                            v <- m.ReadState s;
                            r <- acc;
                            return ({nm = v} ++ r))
@@ -145,8 +140,7 @@ functor Make(M : sig
               <table>
                 <tr> <th>Id:</th> <td><ctextbox source={id}/></td> </tr>
                 {@mapX2 [colMeta] [snd] [_]
-                  (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
-                                   [[nm] ~ rest] m s =>
+                  (fn [nm :: Name] [p ::_] [rest ::_] [[nm] ~ rest] m s =>
                       <xml><tr> <th>{[m.Nam]}:</th> <td>{m.Widget s}</td> </tr></xml>)
                   M.fl M.cols inps}
                 <tr> <th/> <td><button value="Batch it" onclick={add ()}/></td> </tr>
diff --git a/demo/crud.ur b/demo/crud.ur
index 82739772..2fc82c1b 100644
--- a/demo/crud.ur
+++ b/demo/crud.ur
@@ -5,7 +5,7 @@ con colMeta = fn (db :: Type, widget :: Type) =>
                   WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget],
                   Parse : widget -> db,
                   Inject : sql_injectable db}
-con colsMeta = fn cols :: {(Type * Type)} => $(map colMeta cols)
+con colsMeta = fn cols => $(map colMeta cols)
 
 fun default [t] (sh : show t) (rd : read t) (inj : sql_injectable t)
             name : colMeta (t, string) =
@@ -51,10 +51,9 @@ functor Make(M : sig
                          <tr>
                            <td>{[fs.T.Id]}</td>
                            {@mapX2 [fst] [colMeta] [tr]
-                             (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
-                                              [[nm] ~ rest] v col => <xml>
-                                                <td>{col.Show v}</td>
-                                              </xml>)
+                             (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] v col => <xml>
+                               <td>{col.Show v}</td>
+                             </xml>)
                              M.fl (fs.T -- #Id) M.cols}
                            <td>
                              <a link={upd fs.T.Id}>[Update]</a>
@@ -67,10 +66,9 @@ functor Make(M : sig
             <tr>
               <th>ID</th>
               {@mapX [colMeta] [tr]
-                (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
-                                 [[nm] ~ rest] col => <xml>
-                                   <th>{cdata col.Nam}</th>
-                                 </xml>)
+                (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] col => <xml>
+                  <th>{cdata col.Nam}</th>
+                </xml>)
                 M.fl M.cols}
             </tr>
             {rows}
@@ -79,12 +77,11 @@ functor Make(M : sig
           <br/><hr/><br/>
 
           <form>
-            {@foldR [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map snd cols)]
-              (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
-                               [[nm] ~ rest] (col : colMeta t) (acc : xml form [] (map snd rest)) => <xml>
-                                 <li> {cdata col.Nam}: {col.Widget [nm]}</li>
-                                 {useMore acc}
-                               </xml>)
+            {@foldR [colMeta] [fn cols => xml form [] (map snd cols)]
+              (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] (col : colMeta t) (acc : xml form [] (map snd rest)) => <xml>
+                <li> {cdata col.Nam}: {col.Widget [nm]}</li>
+                {useMore acc}
+              </xml>)
               <xml/>
               M.fl M.cols}
             
@@ -96,10 +93,8 @@ functor Make(M : sig
         id <- nextval seq;
         dml (insert tab
                     (@foldR2 [snd] [colMeta]
-                      [fn cols => $(map (fn t :: (Type * Type) =>
-                                            sql_exp [] [] [] t.1) cols)]
-                      (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
-                                       [[nm] ~ rest] =>
+                      [fn cols => $(map (fn t => sql_exp [] [] [] t.1) cols)]
+                      (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] =>
                        fn input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)})
                       {} M.fl inputs M.cols
                      ++ {Id = (SQL {[id]})}));
@@ -115,12 +110,8 @@ functor Make(M : sig
             fun save (inputs : $(map snd M.cols)) =
                 dml (update [map fst M.cols]
                             (@foldR2 [snd] [colMeta]
-                              [fn cols => $(map (fn t :: (Type * Type) =>
-                                                    sql_exp [T = [Id = int]
-                                                                     ++ map fst M.cols]
-                                                            [] [] t.1) cols)]
-                              (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
-                                               [[nm] ~ rest] =>
+                              [fn cols => $(map (fn t => sql_exp [T = [Id = int] ++ map fst M.cols] [] [] t.1) cols)]
+                              (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] =>
                                fn input col acc => acc ++ {nm =
                                                            @sql_inject col.Inject (col.Parse input)})
                               {} M.fl inputs M.cols)
@@ -136,9 +127,8 @@ functor Make(M : sig
             case fso : (Basis.option {Tab : $(map fst M.cols)}) of
                 None => return <xml><body>Not found!</body></xml>
               | Some fs => return <xml><body><form>
-                {@foldR2 [fst] [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map snd cols)]
-                  (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}]
-                                   [[nm] ~ rest] (v : t.1) (col : colMeta t)
+                {@foldR2 [fst] [colMeta] [fn cols => xml form [] (map snd cols)]
+                  (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] (v : t.1) (col : colMeta t)
                                    (acc : xml form [] (map snd rest)) =>
                       <xml>
                         <li> {cdata col.Nam}: {col.WidgetPopulated [nm] v}</li>
diff --git a/demo/metaform.ur b/demo/metaform.ur
index 0a664005..729b7d08 100644
--- a/demo/metaform.ur
+++ b/demo/metaform.ur
@@ -6,7 +6,7 @@ functor Make (M : sig
 
     fun handler values = return <xml><body>
       {@mapUX2 [string] [string] [body]
-        (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] name value => <xml>
+        (fn [nm :: Name] [rest ::_] [[nm] ~ rest] name value => <xml>
           <li> {[name]} = {[value]}</li>
         </xml>)
         M.fl M.names values}
@@ -14,8 +14,8 @@ functor Make (M : sig
 
     fun main () = return <xml><body>
       <form>
-        {@foldUR [string] [fn cols :: {Unit} => xml form [] (mapU string cols)]
-          (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] name
+        {@foldUR [string] [fn cols => xml form [] (mapU string cols)]
+          (fn [nm :: Name] [rest ::_] [[nm] ~ rest] name
                            (acc : xml form [] (mapU string rest)) => <xml>
                              <li> {[name]}: <textbox{nm}/></li>
                              {useMore acc}
-- 
cgit v1.2.3