comparison demo/more/grid.ur @ 1093:8d3aa6c7cee0

Make summary unification more conservative; infer implicit arguments after applications
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Dec 2009 11:56:40 -0500
parents bb3fc575cfe7
children ad15700272f6
comparison
equal deleted inserted replaced
1092:6f4b05fc4361 1093:8d3aa6c7cee0
47 style agg 47 style agg
48 48
49 fun make (row : M.row) [input] [filter] (m : colMeta' M.row input filter) : transaction input = m.Project row 49 fun make (row : M.row) [input] [filter] (m : colMeta' M.row input filter) : transaction input = m.Project row
50 50
51 fun makeAll cols row = @@Monad.exec [transaction] _ [map snd3 M.cols] 51 fun makeAll cols row = @@Monad.exec [transaction] _ [map snd3 M.cols]
52 (map2 [fst3] [colMeta M.row] [fn p => transaction (snd3 p)] 52 (@map2 [fst3] [colMeta M.row] [fn p => transaction (snd3 p)]
53 (fn [p] data meta => make row [_] [_] (meta.Handlers data)) 53 (fn [p] data meta => make row(meta.Handlers data))
54 [_] M.folder cols M.cols) 54 M.folder cols M.cols)
55 (@@Folder.mp [_] [_] M.folder) 55 (@@Folder.mp [_] [_] M.folder)
56 56
57 type grid = {Cols : $(map fst3 M.cols), 57 type grid = {Cols : $(map fst3 M.cols),
58 Rows : Dlist.dlist {Row : source M.row, 58 Rows : Dlist.dlist {Row : source M.row,
59 Cols : source ($(map snd3 M.cols)), 59 Cols : source ($(map snd3 M.cols)),
78 fun addRow cols rows row = 78 fun addRow cols rows row =
79 r <- newRow cols row; 79 r <- newRow cols row;
80 Monad.ignore (Dlist.append rows r) 80 Monad.ignore (Dlist.append rows r)
81 81
82 val grid = 82 val grid =
83 cols <- Monad.mapR [colMeta M.row] [fst3] 83 cols <- @Monad.mapR _ [colMeta M.row] [fst3]
84 (fn [nm :: Name] [p :: (Type * Type * Type)] meta => meta.Initialize) 84 (fn [nm :: Name] [p :: (Type * Type * Type)] meta => meta.Initialize)
85 [_] M.folder M.cols; 85 M.folder M.cols;
86 86
87 filters <- Monad.mapR2 [colMeta M.row] [fst3] [thd3] 87 filters <- @Monad.mapR2 _ [colMeta M.row] [fst3] [thd3]
88 (fn [nm :: Name] [p :: (Type * Type * Type)] meta state => 88 (fn [nm :: Name] [p :: (Type * Type * Type)] meta state =>
89 (meta.Handlers state).CreateFilter) 89 (meta.Handlers state).CreateFilter)
90 [_] M.folder M.cols cols; 90 M.folder M.cols cols;
91 91
92 rows <- Dlist.create; 92 rows <- Dlist.create;
93 sel <- source False; 93 sel <- source False;
94 sort <- source None; 94 sort <- source None;
95 pos <- source 0; 95 pos <- source 0;
107 rs <- List.mapM (newRow cols) init; 107 rs <- List.mapM (newRow cols) init;
108 Dlist.replace rows rs 108 Dlist.replace rows rs
109 109
110 fun myFilter grid all = 110 fun myFilter grid all =
111 row <- signal all.Row; 111 row <- signal all.Row;
112 foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool] 112 @foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool]
113 (fn [nm :: Name] [p :: (Type * Type * Type)] 113 (fn [nm :: Name] [p :: (Type * Type * Type)]
114 [rest :: {(Type * Type * Type)}] [[nm] ~ rest] 114 [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
115 meta state filter combinedFilter row => 115 meta state filter combinedFilter row =>
116 previous <- combinedFilter row; 116 previous <- combinedFilter row;
117 this <- (meta.Handlers state).Filter filter row; 117 this <- (meta.Handlers state).Filter filter row;
118 return (previous && this)) 118 return (previous && this))
119 (fn _ => return True) 119 (fn _ => return True)
120 [_] M.folder M.cols grid.Cols grid.Filters row 120 M.folder M.cols grid.Cols grid.Filters row
121 121
122 fun render (grid : grid) = <xml> 122 fun render (grid : grid) = <xml>
123 <table class={tabl}> 123 <table class={tabl}>
124 <tr class={tr}> 124 <tr class={tr}>
125 <th/> <th/> <th><button value="No sort" onclick={set grid.Sort None}/></th> 125 <th/> <th/> <th><button value="No sort" onclick={set grid.Sort None}/></th>
126 {foldRX2 [fst3] [colMeta M.row] [_] 126 {@foldRX2 [fst3] [colMeta M.row] [_]
127 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest] 127 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
128 data (meta : colMeta M.row p) => 128 data (meta : colMeta M.row p) =>
129 <xml><th class={th}> 129 <xml><th class={th}>
130 {case (meta.Handlers data).Sort of 130 {case (meta.Handlers data).Sort of
131 None => txt (meta.Handlers data).Header 131 None => txt (meta.Handlers data).Header
132 | sort => <xml><button value={(meta.Handlers data).Header} 132 | sort => <xml><button value={(meta.Handlers data).Header}
133 onclick={set grid.Sort sort}/></xml>} 133 onclick={set grid.Sort sort}/></xml>}
134 </th></xml>) 134 </th></xml>)
135 [_] M.folder grid.Cols M.cols} 135 M.folder grid.Cols M.cols}
136 </tr> 136 </tr>
137 137
138 {Dlist.render (fn {Row = rowS, Cols = colsS, Updating = ud, Selected = sd} pos => 138 {Dlist.render (fn {Row = rowS, Cols = colsS, Updating = ud, Selected = sd} pos =>
139 let 139 let
140 val delete = 140 val delete =
150 cols <- makeAll grid.Cols row; 150 cols <- makeAll grid.Cols row;
151 set colsS cols 151 set colsS cols
152 152
153 val save = 153 val save =
154 cols <- get colsS; 154 cols <- get colsS;
155 errors <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => option string] 155 errors <- @Monad.foldR3 _ [fst3] [colMeta M.row] [snd3] [fn _ => option string]
156 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] 156 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}]
157 [[nm] ~ rest] data meta v errors => 157 [[nm] ~ rest] data meta v errors =>
158 b <- current ((meta.Handlers data).Validate v); 158 b <- current ((meta.Handlers data).Validate v);
159 return (if b then 159 return (if b then
160 errors 160 errors
161 else 161 else
162 case errors of 162 case errors of
163 None => Some ((meta.Handlers data).Header) 163 None => Some ((meta.Handlers data).Header)
164 | Some s => Some ((meta.Handlers data).Header 164 | Some s => Some ((meta.Handlers data).Header
165 ^ ", " ^ s))) 165 ^ ", " ^ s)))
166 None [_] M.folder grid.Cols M.cols cols; 166 None M.folder grid.Cols M.cols cols;
167 167
168 case errors of 168 case errors of
169 Some s => alert ("Can't save because the following columns have invalid values:\n" 169 Some s => alert ("Can't save because the following columns have invalid values:\n"
170 ^ s) 170 ^ s)
171 | None => 171 | None =>
172 set ud False; 172 set ud False;
173 row <- get rowS; 173 row <- get rowS;
174 row' <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => M.row] 174 row' <- @Monad.foldR3 _ [fst3] [colMeta M.row] [snd3] [fn _ => M.row]
175 (fn [nm :: Name] [t :: (Type * Type * Type)] 175 (fn [nm :: Name] [t :: (Type * Type * Type)]
176 [rest :: {(Type * Type * Type)}] 176 [rest :: {(Type * Type * Type)}]
177 [[nm] ~ rest] data meta v row' => 177 [[nm] ~ rest] data meta v row' =>
178 (meta.Handlers data).Update row' v) 178 (meta.Handlers data).Update row' v)
179 row [_] M.folder grid.Cols M.cols cols; 179 row M.folder grid.Cols M.cols cols;
180 rpc (M.save (M.keyOf row) row'); 180 rpc (M.save (M.keyOf row) row');
181 set rowS row'; 181 set rowS row';
182 182
183 cols <- makeAll grid.Cols row'; 183 cols <- makeAll grid.Cols row';
184 set colsS cols 184 set colsS cols
206 else 206 else
207 <xml><button value="Delete" onclick={delete}/></xml>)}/> 207 <xml><button value="Delete" onclick={delete}/></xml>)}/>
208 </td> 208 </td>
209 209
210 <dyn signal={cols <- signal colsS; 210 <dyn signal={cols <- signal colsS;
211 return (foldRX3 [fst3] [colMeta M.row] [snd3] [_] 211 return (@foldRX3 [fst3] [colMeta M.row] [snd3] [_]
212 (fn [nm :: Name] [t :: (Type * Type * Type)] 212 (fn [nm :: Name] [t :: (Type * Type * Type)]
213 [rest :: {(Type * Type * Type)}] 213 [rest :: {(Type * Type * Type)}]
214 [[nm] ~ rest] data meta v => 214 [[nm] ~ rest] data meta v =>
215 <xml><td class={td}> 215 <xml><td class={td}>
216 <dyn signal={b <- signal ud; 216 <dyn signal={b <- signal ud;
217 return (if b then 217 return (if b then
218 (meta.Handlers data).Edit v 218 (meta.Handlers data).Edit v
219 else 219 else
220 (meta.Handlers data).Display 220 (meta.Handlers data).Display
221 v)}/> 221 v)}/>
222 <dyn signal={b <- signal ud; 222 <dyn signal={b <- signal ud;
223 if b then 223 if b then
224 valid <- 224 valid <-
225 (meta.Handlers data).Validate v; 225 (meta.Handlers data).Validate v;
226 return (if valid then 226 return (if valid then
227 <xml/> 227 <xml/>
228 else 228 else
229 <xml>!</xml>) 229 <xml>!</xml>)
230 else 230 else
231 return <xml/>}/> 231 return <xml/>}/>
232 </td></xml>) 232 </td></xml>)
233 [_] M.folder grid.Cols M.cols cols)}/> 233 M.folder grid.Cols M.cols cols)}/>
234 </tr></xml> 234 </tr></xml>
235 end) 235 end)
236 {StartPosition = case M.pageLength of 236 {StartPosition = case M.pageLength of
237 None => return None 237 None => return None
238 | Some len => 238 | Some len =>
248 return (Option.mp (fn f r1 r2 => r1 <- signal r1.Row; 248 return (Option.mp (fn f r1 r2 => r1 <- signal r1.Row;
249 r2 <- signal r2.Row; 249 r2 <- signal r2.Row;
250 return (f r1 r2)) f)} 250 return (f r1 r2)) f)}
251 grid.Rows} 251 grid.Rows}
252 252
253 <dyn signal={rows <- Dlist.foldl (fn row => Monad.mapR2 [aggregateMeta M.row] [id] [id] 253 <dyn signal={rows <- Dlist.foldl (fn row => @Monad.mapR2 _ [aggregateMeta M.row] [id] [id]
254 (fn [nm :: Name] [t :: Type] meta acc => 254 (fn [nm :: Name] [t :: Type] meta acc =>
255 Monad.mp (fn v => meta.Step v acc) 255 Monad.mp (fn v => meta.Step v acc)
256 (signal row.Row)) 256 (signal row.Row))
257 [_] M.aggFolder M.aggregates) 257 M.aggFolder M.aggregates)
258 (mp [aggregateMeta M.row] [id] 258 (@mp [aggregateMeta M.row] [id]
259 (fn [t] meta => meta.Initial) 259 (fn [t] meta => meta.Initial)
260 [_] M.aggFolder M.aggregates) grid.Rows; 260 M.aggFolder M.aggregates) grid.Rows;
261 return <xml><tr> 261 return <xml><tr>
262 <th colspan={3}>Aggregates</th> 262 <th colspan={3}>Aggregates</th>
263 {foldRX2 [aggregateMeta M.row] [id] [_] 263 {@foldRX2 [aggregateMeta M.row] [id] [_]
264 (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest] meta acc => 264 (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest] meta acc =>
265 <xml><td class={agg}>{meta.Display acc}</td></xml>) 265 <xml><td class={agg}>{meta.Display acc}</td></xml>)
266 [_] M.aggFolder M.aggregates rows} 266 M.aggFolder M.aggregates rows}
267 </tr></xml>}/> 267 </tr></xml>}/>
268 268
269 <tr><th colspan={3}>Filters</th> 269 <tr><th colspan={3}>Filters</th>
270 {foldRX3 [colMeta M.row] [fst3] [thd3] [_] 270 {@foldRX3 [colMeta M.row] [fst3] [thd3] [_]
271 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest] 271 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
272 meta state filter => <xml><td>{(meta.Handlers state).DisplayFilter filter}</td></xml>) 272 meta state filter => <xml><td>{(meta.Handlers state).DisplayFilter filter}</td></xml>)
273 [_] M.folder M.cols grid.Cols grid.Filters} 273 M.folder M.cols grid.Cols grid.Filters}
274 </tr> 274 </tr>
275 </table> 275 </table>
276 276
277 {case M.pageLength of 277 {case M.pageLength of
278 None => <xml/> 278 None => <xml/>