diff demo/more/grid.ur @ 944:da3ec6014d2f

Filters implementation type-checking
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Sep 2009 15:48:53 -0400
parents e2194a6793ae
children 103ac1792c41
line wrap: on
line diff
--- a/demo/more/grid.ur	Tue Sep 15 13:07:57 2009 -0400
+++ b/demo/more/grid.ur	Tue Sep 15 15:48:53 2009 -0400
@@ -1,14 +1,17 @@
-con colMeta' = fn (row :: Type) (t :: Type) =>
+con colMeta' = fn (row :: Type) (input :: Type) (filter :: Type) =>
                   {Header : string,
-                   Project : row -> transaction t,
-                   Update : row -> t -> transaction row,
-                   Display : t -> xbody,
-                   Edit : t -> xbody,
-                   Validate : t -> signal bool}
-
-con colMeta = fn (row :: Type) (global_t :: (Type * Type)) =>
-                 {Initialize : transaction global_t.1,
-                  Handlers : global_t.1 -> colMeta' row global_t.2}                  
+                   Project : row -> transaction input,
+                   Update : row -> input -> transaction row,
+                   Display : input -> xbody,
+                   Edit : input -> xbody,
+                   Validate : input -> signal bool,
+                   CreateFilter : transaction filter,
+                   DisplayFilter : filter -> xbody,
+                   Filter : filter -> row -> signal bool}
+                  
+con colMeta = fn (row :: Type) (global_input_filter :: (Type * Type * Type)) =>
+                 {Initialize : transaction global_input_filter.1,
+                  Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3}
 
 con aggregateMeta = fn (row :: Type) (acc :: Type) =>
                        {Initial : acc,
@@ -25,7 +28,7 @@
                  val save : key -> row -> transaction unit
                  val delete : key -> transaction unit
 
-                 con cols :: {(Type * Type)}
+                 con cols :: {(Type * Type * Type)}
                  val cols : $(map (colMeta row) cols)
 
                  val folder : folder cols
@@ -40,20 +43,21 @@
     style td
     style agg
 
-    fun make (row : M.row) [t] (m : colMeta' M.row t) : transaction t = m.Project row
+    fun make (row : M.row) [input] [filter] (m : colMeta' M.row input filter) : transaction input = m.Project row
 
-    fun makeAll cols row = @@Monad.exec [transaction] _ [map snd M.cols]
-                               (map2 [fst] [colMeta M.row] [fn p :: (Type * Type) => transaction p.2]
-                                     (fn [p] data meta => make row [_] (meta.Handlers data))
+    fun makeAll cols row = @@Monad.exec [transaction] _ [map snd3 M.cols]
+                               (map2 [fst3] [colMeta M.row] [fn p => transaction (snd3 p)]
+                                     (fn [p] data meta => make row [_] [_] (meta.Handlers data))
                                      [_] M.folder cols M.cols)
                                (@@Folder.mp [_] [_] M.folder)
 
-    type grid = {Cols : $(map fst M.cols),
+    type grid = {Cols : $(map fst3 M.cols),
                  Rows : Dlist.dlist {Row : source M.row,
-                                     Cols : source ($(map snd M.cols)),
+                                     Cols : source ($(map snd3 M.cols)),
                                      Updating : source bool,
                                      Selected : source bool},
-                 Selection : source bool}
+                 Selection : source bool,
+                 Filters : $(map thd3 M.cols)}
 
     fun addRow cols rows row =
         rowS <- source row;
@@ -66,15 +70,29 @@
                                          Updating = ud,
                                          Selected = sd})
 
-    val createMetas = Monad.mapR [colMeta M.row] [fst]
-                           (fn [nm :: Name] [p :: (Type * Type)] meta => meta.Initialize)
-                           [_] M.folder M.cols
+    val grid =
+        cols <- Monad.mapR [colMeta M.row] [fst3]
+                           (fn [nm :: Name] [p :: (Type * Type * Type)] meta => meta.Initialize)
+                           [_] M.folder M.cols;
 
-    val grid =
-        cols <- createMetas;
-        rows <- Dlist.create;
+        filters <- Monad.mapR2 [colMeta M.row] [fst3] [thd3]
+                               (fn [nm :: Name] [p :: (Type * Type * Type)] meta state =>
+                                   (meta.Handlers state).CreateFilter)
+                               [_] M.folder M.cols cols;
+
+        rows <- Dlist.create {Filter = fn all =>
+                                          row <- signal all.Row;
+                                          foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool]
+                                                 (fn [nm :: Name] [p :: (Type * Type * Type)]
+                                                                  [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
+                                                                  meta state filter combinedFilter row =>
+                                                     previous <- combinedFilter row;
+                                                     this <- (meta.Handlers state).Filter filter row;
+                                                     return (previous && this))
+                                                 (fn _ => return True)
+                                                 [_] M.folder M.cols cols filters row};
         sel <- source False;
-        return {Cols = cols, Rows = rows, Selection = sel}
+        return {Cols = cols, Rows = rows, Selection = sel, Filters = filters}
 
     fun sync {Cols = cols, Rows = rows, ...} =
         Dlist.clear rows;
@@ -85,8 +103,8 @@
       <table class={tabl}>
         <tr class={tr}>
           <th/> <th/> <th/>
-          {foldRX2 [fst] [colMeta M.row] [_]
-                   (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest]
+          {foldRX2 [fst3] [colMeta M.row] [_]
+                   (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
                                     data (meta : colMeta M.row p) =>
                        <xml><th class={th}>{[(meta.Handlers data).Header]}</th></xml>)
                    [_] M.folder grid.Cols M.cols}
@@ -109,8 +127,8 @@
                                   
                               val save =
                                   cols <- get colsS;
-                                  errors <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => option string]
-                                                         (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
+                                  errors <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => option string]
+                                                         (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}]
                                                                           [[nm] ~ rest] data meta v errors =>
                                                              b <- current ((meta.Handlers data).Validate v);
                                                              return (if b then
@@ -128,9 +146,9 @@
                                     | None =>
                                       set ud False;
                                       row <- get rowS;
-                                      row' <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => M.row]
-                                                           (fn [nm :: Name] [t :: (Type * Type)]
-                                                                            [rest :: {(Type * Type)}]
+                                      row' <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => M.row]
+                                                           (fn [nm :: Name] [t :: (Type * Type * Type)]
+                                                                            [rest :: {(Type * Type * Type)}]
                                                                             [[nm] ~ rest] data meta v row' =>
                                                                (meta.Handlers data).Update row' v)
                                                            row [_] M.folder grid.Cols M.cols cols;
@@ -165,9 +183,9 @@
                                 </td>
 
                                 <dyn signal={cols <- signal colsS;
-                                             return (foldRX3 [fst] [colMeta M.row] [snd] [_]
-                                                             (fn [nm :: Name] [t :: (Type * Type)]
-                                                                              [rest :: {(Type * Type)}]
+                                             return (foldRX3 [fst3] [colMeta M.row] [snd3] [_]
+                                                             (fn [nm :: Name] [t :: (Type * Type * Type)]
+                                                                              [rest :: {(Type * Type * Type)}]
                                                                               [[nm] ~ rest] data meta v =>
                                                                  <xml><td class={td}>
                                                                    <dyn signal={b <- signal ud;
@@ -206,6 +224,13 @@
                                         <xml><td class={agg}>{meta.Display acc}</td></xml>)
                                     [_] M.aggFolder M.aggregates rows}
                          </tr></xml>}/>
+
+              <tr><th colspan={3}>Filters</th>
+                {foldRX3 [colMeta M.row] [fst3] [thd3] [_]
+                 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
+                                  meta state filter => <xml><td>{(meta.Handlers state).DisplayFilter filter}</td></xml>)
+                 [_] M.folder M.cols grid.Cols grid.Filters}
+              </tr>
           </table>
           
           <button value="New row" onclick={row <- rpc M.new;