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