Mercurial > urweb
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/> |