comparison 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
comparison
equal deleted inserted replaced
943:e2194a6793ae 944:da3ec6014d2f
1 con colMeta' = fn (row :: Type) (t :: Type) => 1 con colMeta' = fn (row :: Type) (input :: Type) (filter :: Type) =>
2 {Header : string, 2 {Header : string,
3 Project : row -> transaction t, 3 Project : row -> transaction input,
4 Update : row -> t -> transaction row, 4 Update : row -> input -> transaction row,
5 Display : t -> xbody, 5 Display : input -> xbody,
6 Edit : t -> xbody, 6 Edit : input -> xbody,
7 Validate : t -> signal bool} 7 Validate : input -> signal bool,
8 8 CreateFilter : transaction filter,
9 con colMeta = fn (row :: Type) (global_t :: (Type * Type)) => 9 DisplayFilter : filter -> xbody,
10 {Initialize : transaction global_t.1, 10 Filter : filter -> row -> signal bool}
11 Handlers : global_t.1 -> colMeta' row global_t.2} 11
12 con colMeta = fn (row :: Type) (global_input_filter :: (Type * Type * Type)) =>
13 {Initialize : transaction global_input_filter.1,
14 Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3}
12 15
13 con aggregateMeta = fn (row :: Type) (acc :: Type) => 16 con aggregateMeta = fn (row :: Type) (acc :: Type) =>
14 {Initial : acc, 17 {Initial : acc,
15 Step : row -> acc -> acc, 18 Step : row -> acc -> acc,
16 Display : acc -> xbody} 19 Display : acc -> xbody}
23 val list : transaction (list row) 26 val list : transaction (list row)
24 val new : transaction row 27 val new : transaction row
25 val save : key -> row -> transaction unit 28 val save : key -> row -> transaction unit
26 val delete : key -> transaction unit 29 val delete : key -> transaction unit
27 30
28 con cols :: {(Type * Type)} 31 con cols :: {(Type * Type * Type)}
29 val cols : $(map (colMeta row) cols) 32 val cols : $(map (colMeta row) cols)
30 33
31 val folder : folder cols 34 val folder : folder cols
32 35
33 con aggregates :: {Type} 36 con aggregates :: {Type}
38 style tr 41 style tr
39 style th 42 style th
40 style td 43 style td
41 style agg 44 style agg
42 45
43 fun make (row : M.row) [t] (m : colMeta' M.row t) : transaction t = m.Project row 46 fun make (row : M.row) [input] [filter] (m : colMeta' M.row input filter) : transaction input = m.Project row
44 47
45 fun makeAll cols row = @@Monad.exec [transaction] _ [map snd M.cols] 48 fun makeAll cols row = @@Monad.exec [transaction] _ [map snd3 M.cols]
46 (map2 [fst] [colMeta M.row] [fn p :: (Type * Type) => transaction p.2] 49 (map2 [fst3] [colMeta M.row] [fn p => transaction (snd3 p)]
47 (fn [p] data meta => make row [_] (meta.Handlers data)) 50 (fn [p] data meta => make row [_] [_] (meta.Handlers data))
48 [_] M.folder cols M.cols) 51 [_] M.folder cols M.cols)
49 (@@Folder.mp [_] [_] M.folder) 52 (@@Folder.mp [_] [_] M.folder)
50 53
51 type grid = {Cols : $(map fst M.cols), 54 type grid = {Cols : $(map fst3 M.cols),
52 Rows : Dlist.dlist {Row : source M.row, 55 Rows : Dlist.dlist {Row : source M.row,
53 Cols : source ($(map snd M.cols)), 56 Cols : source ($(map snd3 M.cols)),
54 Updating : source bool, 57 Updating : source bool,
55 Selected : source bool}, 58 Selected : source bool},
56 Selection : source bool} 59 Selection : source bool,
60 Filters : $(map thd3 M.cols)}
57 61
58 fun addRow cols rows row = 62 fun addRow cols rows row =
59 rowS <- source row; 63 rowS <- source row;
60 cols <- makeAll cols row; 64 cols <- makeAll cols row;
61 colsS <- source cols; 65 colsS <- source cols;
64 Monad.ignore (Dlist.append rows {Row = rowS, 68 Monad.ignore (Dlist.append rows {Row = rowS,
65 Cols = colsS, 69 Cols = colsS,
66 Updating = ud, 70 Updating = ud,
67 Selected = sd}) 71 Selected = sd})
68 72
69 val createMetas = Monad.mapR [colMeta M.row] [fst]
70 (fn [nm :: Name] [p :: (Type * Type)] meta => meta.Initialize)
71 [_] M.folder M.cols
72
73 val grid = 73 val grid =
74 cols <- createMetas; 74 cols <- Monad.mapR [colMeta M.row] [fst3]
75 rows <- Dlist.create; 75 (fn [nm :: Name] [p :: (Type * Type * Type)] meta => meta.Initialize)
76 [_] M.folder M.cols;
77
78 filters <- Monad.mapR2 [colMeta M.row] [fst3] [thd3]
79 (fn [nm :: Name] [p :: (Type * Type * Type)] meta state =>
80 (meta.Handlers state).CreateFilter)
81 [_] M.folder M.cols cols;
82
83 rows <- Dlist.create {Filter = fn all =>
84 row <- signal all.Row;
85 foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool]
86 (fn [nm :: Name] [p :: (Type * Type * Type)]
87 [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
88 meta state filter combinedFilter row =>
89 previous <- combinedFilter row;
90 this <- (meta.Handlers state).Filter filter row;
91 return (previous && this))
92 (fn _ => return True)
93 [_] M.folder M.cols cols filters row};
76 sel <- source False; 94 sel <- source False;
77 return {Cols = cols, Rows = rows, Selection = sel} 95 return {Cols = cols, Rows = rows, Selection = sel, Filters = filters}
78 96
79 fun sync {Cols = cols, Rows = rows, ...} = 97 fun sync {Cols = cols, Rows = rows, ...} =
80 Dlist.clear rows; 98 Dlist.clear rows;
81 init <- rpc M.list; 99 init <- rpc M.list;
82 List.app (addRow cols rows) init 100 List.app (addRow cols rows) init
83 101
84 fun render grid = <xml> 102 fun render grid = <xml>
85 <table class={tabl}> 103 <table class={tabl}>
86 <tr class={tr}> 104 <tr class={tr}>
87 <th/> <th/> <th/> 105 <th/> <th/> <th/>
88 {foldRX2 [fst] [colMeta M.row] [_] 106 {foldRX2 [fst3] [colMeta M.row] [_]
89 (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] 107 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
90 data (meta : colMeta M.row p) => 108 data (meta : colMeta M.row p) =>
91 <xml><th class={th}>{[(meta.Handlers data).Header]}</th></xml>) 109 <xml><th class={th}>{[(meta.Handlers data).Header]}</th></xml>)
92 [_] M.folder grid.Cols M.cols} 110 [_] M.folder grid.Cols M.cols}
93 </tr> 111 </tr>
94 112
107 cols <- makeAll grid.Cols row; 125 cols <- makeAll grid.Cols row;
108 set colsS cols 126 set colsS cols
109 127
110 val save = 128 val save =
111 cols <- get colsS; 129 cols <- get colsS;
112 errors <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => option string] 130 errors <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => option string]
113 (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] 131 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}]
114 [[nm] ~ rest] data meta v errors => 132 [[nm] ~ rest] data meta v errors =>
115 b <- current ((meta.Handlers data).Validate v); 133 b <- current ((meta.Handlers data).Validate v);
116 return (if b then 134 return (if b then
117 errors 135 errors
118 else 136 else
126 Some s => alert ("Can't save because the following columns have invalid values:\n" 144 Some s => alert ("Can't save because the following columns have invalid values:\n"
127 ^ s) 145 ^ s)
128 | None => 146 | None =>
129 set ud False; 147 set ud False;
130 row <- get rowS; 148 row <- get rowS;
131 row' <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => M.row] 149 row' <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => M.row]
132 (fn [nm :: Name] [t :: (Type * Type)] 150 (fn [nm :: Name] [t :: (Type * Type * Type)]
133 [rest :: {(Type * Type)}] 151 [rest :: {(Type * Type * Type)}]
134 [[nm] ~ rest] data meta v row' => 152 [[nm] ~ rest] data meta v row' =>
135 (meta.Handlers data).Update row' v) 153 (meta.Handlers data).Update row' v)
136 row [_] M.folder grid.Cols M.cols cols; 154 row [_] M.folder grid.Cols M.cols cols;
137 rpc (M.save (M.keyOf row) row'); 155 rpc (M.save (M.keyOf row) row');
138 set rowS row'; 156 set rowS row';
163 else 181 else
164 <xml><button value="Delete" onclick={delete}/></xml>)}/> 182 <xml><button value="Delete" onclick={delete}/></xml>)}/>
165 </td> 183 </td>
166 184
167 <dyn signal={cols <- signal colsS; 185 <dyn signal={cols <- signal colsS;
168 return (foldRX3 [fst] [colMeta M.row] [snd] [_] 186 return (foldRX3 [fst3] [colMeta M.row] [snd3] [_]
169 (fn [nm :: Name] [t :: (Type * Type)] 187 (fn [nm :: Name] [t :: (Type * Type * Type)]
170 [rest :: {(Type * Type)}] 188 [rest :: {(Type * Type * Type)}]
171 [[nm] ~ rest] data meta v => 189 [[nm] ~ rest] data meta v =>
172 <xml><td class={td}> 190 <xml><td class={td}>
173 <dyn signal={b <- signal ud; 191 <dyn signal={b <- signal ud;
174 return (if b then 192 return (if b then
175 (meta.Handlers data).Edit v 193 (meta.Handlers data).Edit v
204 {foldRX2 [aggregateMeta M.row] [id] [_] 222 {foldRX2 [aggregateMeta M.row] [id] [_]
205 (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest] meta acc => 223 (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest] meta acc =>
206 <xml><td class={agg}>{meta.Display acc}</td></xml>) 224 <xml><td class={agg}>{meta.Display acc}</td></xml>)
207 [_] M.aggFolder M.aggregates rows} 225 [_] M.aggFolder M.aggregates rows}
208 </tr></xml>}/> 226 </tr></xml>}/>
227
228 <tr><th colspan={3}>Filters</th>
229 {foldRX3 [colMeta M.row] [fst3] [thd3] [_]
230 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
231 meta state filter => <xml><td>{(meta.Handlers state).DisplayFilter filter}</td></xml>)
232 [_] M.folder M.cols grid.Cols grid.Filters}
233 </tr>
209 </table> 234 </table>
210 235
211 <button value="New row" onclick={row <- rpc M.new; 236 <button value="New row" onclick={row <- rpc M.new;
212 addRow grid.Cols grid.Rows row}/> 237 addRow grid.Cols grid.Rows row}/>
213 <button value="Refresh" onclick={sync grid}/> 238 <button value="Refresh" onclick={sync grid}/>