Mercurial > urweb

comparison demo/more/dbgrid.ur @ 944:da3ec6014d2f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Filters implementation type-checking
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Sep 2009 15:48:53 -0400
parents 37dd42935dad
children 2412cb10c97c
comparison
equal deleted inserted replaced
943:e2194a6793ae 944:da3ec6014d2f
1 con rawMeta = fn t :: Type => 1 con rawMeta = fn t :: Type =>
2 {New : transaction t, 2 {New : transaction t,
3 Inj : sql_injectable t} 3 Inj : sql_injectable t}
4 4
5 con colMeta' = fn (row :: {Type}) (t :: Type) => 5 con colMeta' = fn (row :: {Type}) (input :: Type) (filter :: Type) =>
6 {Header : string, 6 {Header : string,
7 Project : $row -> transaction t, 7 Project : $row -> transaction input,
8 Update : $row -> t -> transaction ($row), 8 Update : $row -> input -> transaction ($row),
9 Display : t -> xbody, 9 Display : input -> xbody,
10 Edit : t -> xbody, 10 Edit : input -> xbody,
11 Validate : t -> signal bool} 11 Validate : input -> signal bool,
12 12 CreateFilter : transaction filter,
13 con colMeta = fn (row :: {Type}) (global_t :: (Type * Type)) => 13 DisplayFilter : filter -> xbody,
14 {Initialize : transaction global_t.1, 14 Filter : filter -> $row -> signal bool}
15 Handlers : global_t.1 -> colMeta' row global_t.2} 15
16 con colMeta = fn (row :: {Type}) (global_input_filter :: (Type * Type * Type)) =>
17 {Initialize : transaction global_input_filter.1,
18 Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3}
16 19
17 con aggregateMeta = fn (row :: {Type}) (acc :: Type) => 20 con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
18 {Initial : acc, 21 {Initial : acc,
19 Step : $row -> acc -> acc, 22 Step : $row -> acc -> acc,
20 Display : acc -> xbody} 23 Display : acc -> xbody}
21 24
22 structure Direct = struct 25 structure Direct = struct
23 con metaBase = fn actual_input :: (Type * Type) => 26 con metaBase = fn actual_input_filter :: (Type * Type * Type) =>
24 {Display : actual_input.2 -> xbody, 27 {Display : actual_input_filter.2 -> xbody,
25 Edit : actual_input.2 -> xbody, 28 Edit : actual_input_filter.2 -> xbody,
26 Initialize : actual_input.1 -> transaction actual_input.2, 29 Initialize : actual_input_filter.1 -> transaction actual_input_filter.2,
27 Parse : actual_input.2 -> signal (option actual_input.1)} 30 Parse : actual_input_filter.2 -> signal (option actual_input_filter.1),
28 31 CreateFilter : transaction actual_input_filter.3,
29 datatype metaBoth actual input = 32 DisplayFilter : actual_input_filter.3 -> xbody,
30 NonNull of metaBase (actual, input) * metaBase (option actual, input) 33 Filter : actual_input_filter.3 -> actual_input_filter.1 -> signal bool}
31 | Nullable of metaBase (actual, input) 34
32 35 datatype metaBoth actual input filter =
33 con meta = fn global_actual_input :: (Type * Type * Type) => 36 NonNull of metaBase (actual, input, filter) * metaBase (option actual, input, filter)
34 {Initialize : transaction global_actual_input.1, 37 | Nullable of metaBase (actual, input, filter)
35 Handlers : global_actual_input.1 38
36 -> metaBoth global_actual_input.2 global_actual_input.3} 39 con meta = fn global_actual_input_filter :: (Type * Type * Type * Type) =>
37 40 {Initialize : transaction global_actual_input_filter.1,
38 con editableState (ts :: (Type * Type * Type)) = (ts.1, ts.3) 41 Handlers : global_actual_input_filter.1
42 -> metaBoth global_actual_input_filter.2 global_actual_input_filter.3
43 global_actual_input_filter.4}
44
45 con editableState (ts :: (Type * Type * Type * Type)) = (ts.1, ts.3, ts.4)
39 fun editable [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest) 46 fun editable [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
40 (editableState ts) = 47 (editableState ts) =
41 let 48 let
42 fun doMr mr = {Header = name, 49 fun doMr mr = {Header = name,
43 Project = fn r => mr.Initialize r.nm, 50 Project = fn r => mr.Initialize r.nm,
46 return (case vo of 53 return (case vo of
47 None => r 54 None => r
48 | Some v => r -- nm ++ {nm = v}), 55 | Some v => r -- nm ++ {nm = v}),
49 Display = mr.Display, 56 Display = mr.Display,
50 Edit = mr.Edit, 57 Edit = mr.Edit,
51 Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo)} 58 Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo),
59 CreateFilter = mr.CreateFilter,
60 DisplayFilter = mr.DisplayFilter,
61 Filter = fn i r => mr.Filter i r.nm}
52 in 62 in
53 {Initialize = m.Initialize, 63 {Initialize = m.Initialize,
54 Handlers = fn data => case m.Handlers data of 64 Handlers = fn data => case m.Handlers data of
55 NonNull (mr, _) => doMr mr 65 NonNull (mr, _) => doMr mr
56 | Nullable mr => doMr mr} 66 | Nullable mr => doMr mr}
57 end 67 end
58 68
59 con readOnlyState (ts :: (Type * Type * Type)) = (ts.1, ts.3) 69 con readOnlyState (ts :: (Type * Type * Type * Type)) = (ts.1, ts.3, ts.4)
60 fun readOnly [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest) 70 fun readOnly [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
61 (readOnlyState ts) = 71 (readOnlyState ts) =
62 let 72 let
63 fun doMr mr = {Header = name, 73 fun doMr mr = {Header = name,
64 Project = fn r => mr.Initialize r.nm, 74 Project = fn r => mr.Initialize r.nm,
65 Update = fn r _ => return r, 75 Update = fn r _ => return r,
66 Display = mr.Display, 76 Display = mr.Display,
67 Edit = mr.Display, 77 Edit = mr.Display,
68 Validate = fn _ => return True} 78 Validate = fn _ => return True,
79 CreateFilter = mr.CreateFilter,
80 DisplayFilter = mr.DisplayFilter,
81 Filter = fn i r => mr.Filter i r.nm}
69 in 82 in
70 {Initialize = m.Initialize, 83 {Initialize = m.Initialize,
71 Handlers = fn data => case m.Handlers data of 84 Handlers = fn data => case m.Handlers data of
72 NonNull (mr, _) => doMr mr 85 NonNull (mr, _) => doMr mr
73 | Nullable mr => doMr mr} 86 | Nullable mr => doMr mr}
74 end 87 end
75 88
76 con metaBasic = fn actual_input :: (Type * Type) => 89 con metaBasic = fn actual_input_filter :: (Type * Type * Type) =>
77 {Display : actual_input.2 -> xbody, 90 {Display : actual_input_filter.2 -> xbody,
78 Edit : source actual_input.2 -> xbody, 91 Edit : source actual_input_filter.2 -> xbody,
79 Initialize : actual_input.1 -> actual_input.2, 92 Initialize : actual_input_filter.1 -> actual_input_filter.2,
80 InitializeNull : actual_input.2, 93 InitializeNull : actual_input_filter.2,
81 IsNull : actual_input.2 -> bool, 94 IsNull : actual_input_filter.2 -> bool,
82 Parse : actual_input.2 -> option actual_input.1} 95 Parse : actual_input_filter.2 -> option actual_input_filter.1,
96 CreateFilter : actual_input_filter.3,
97 DisplayFilter : source actual_input_filter.3 -> xbody,
98 Filter : actual_input_filter.3 -> actual_input_filter.1 -> bool,
99 FilterIsNull : actual_input_filter.3 -> bool}
83 100
84 con basicState = source 101 con basicState = source
85 fun basic [ts ::: (Type * Type)] (m : metaBasic ts) : meta (unit, ts.1, basicState ts.2) = 102 con basicFilter = source
103 fun basic [ts ::: (Type * Type * Type)] (m : metaBasic ts) : meta (unit, ts.1, basicState ts.2, basicFilter ts.3) =
86 {Initialize = return (), 104 {Initialize = return (),
87 Handlers = fn () => NonNull ( 105 Handlers = fn () => NonNull (
88 {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>, 106 {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>,
89 Edit = m.Edit, 107 Edit = m.Edit,
90 Initialize = fn v => source (m.Initialize v), 108 Initialize = fn v => source (m.Initialize v),
91 Parse = fn s => v <- signal s; return (m.Parse v)}, 109 Parse = fn s => v <- signal s; return (m.Parse v),
110 CreateFilter = source m.CreateFilter,
111 DisplayFilter = m.DisplayFilter,
112 Filter = fn f v => f <- signal f; return (m.Filter f v)},
92 {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>, 113 {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>,
93 Edit = m.Edit, 114 Edit = m.Edit,
94 Initialize = fn v => source (case v of 115 Initialize = fn v => source (case v of
95 None => m.InitializeNull 116 None => m.InitializeNull
96 | Some v => m.Initialize v), 117 | Some v => m.Initialize v),
98 return (if m.IsNull v then 119 return (if m.IsNull v then
99 Some None 120 Some None
100 else 121 else
101 case m.Parse v of 122 case m.Parse v of
102 None => None 123 None => None
103 | Some v' => Some (Some v'))})} 124 | Some v' => Some (Some v')),
104 125 CreateFilter = source m.CreateFilter,
105 fun nullable [global] [actual] [input] (m : meta (global, actual, input)) = 126 DisplayFilter = m.DisplayFilter,
127 Filter = fn f v => f <- signal f;
128 return (if m.FilterIsNull f then
129 Option.isNone v
130 else
131 case v of
132 None => False
133 | Some v => m.Filter f v) : signal bool})}
134
135 fun nullable [global] [actual] [input] [filter] (m : meta (global, actual, input, filter)) =
106 {Initialize = m.Initialize, 136 {Initialize = m.Initialize,
107 Handlers = fn d => case m.Handlers d of 137 Handlers = fn d => case m.Handlers d of
108 Nullable _ => error <xml>Don't stack calls to Direct.nullable!</xml> 138 Nullable _ => error <xml>Don't stack calls to Direct.nullable!</xml>
109 | NonNull (_, ho) => Nullable ho} 139 | NonNull (_, ho) => Nullable ho}
110 140
111 type intGlobal = unit 141 type intGlobal = unit
112 type intInput = basicState string 142 type intInput = basicState string
113 val int : meta (intGlobal, int, intInput) = 143 type intFilter = basicFilter string
144 val int : meta (intGlobal, int, intInput, intFilter) =
114 basic {Display = fn s => <xml>{[s]}</xml>, 145 basic {Display = fn s => <xml>{[s]}</xml>,
115 Edit = fn s => <xml><ctextbox source={s}/></xml>, 146 Edit = fn s => <xml><ctextbox source={s}/></xml>,
116 Initialize = fn n => show n, 147 Initialize = fn n => show n,
117 InitializeNull = "", 148 InitializeNull = "",
118 IsNull = eq "", 149 IsNull = eq "",
119 Parse = fn v => read v} 150 Parse = fn v => read v,
151 CreateFilter = "",
152 DisplayFilter = fn s => <xml><ctextbox source={s}/></xml> : xbody,
153 Filter = fn s n =>
154 case read s of
155 None => True
156 | Some n' => n' = n,
157 FilterIsNull = eq ""}
120 158
121 type stringGlobal = unit 159 type stringGlobal = unit
122 type stringInput = basicState string 160 type stringInput = basicState string
123 val string : meta (stringGlobal, string, stringInput) = 161 type stringFilter = basicFilter string
162 val string : meta (stringGlobal, string, stringInput, stringFilter) =
124 basic {Display = fn s => <xml>{[s]}</xml>, 163 basic {Display = fn s => <xml>{[s]}</xml>,
125 Edit = fn s => <xml><ctextbox source={s}/></xml>, 164 Edit = fn s => <xml><ctextbox source={s}/></xml>,
126 Initialize = fn s => s, 165 Initialize = fn s => s,
127 InitializeNull = "", 166 InitializeNull = "",
128 IsNull = eq "", 167 IsNull = eq "",
129 Parse = fn s => Some s} 168 Parse = fn s => Some s,
169 CreateFilter = "",
170 DisplayFilter = fn s => <xml><ctextbox source={s}/></xml> : xbody,
171 Filter = fn s n =>
172 case read s of
173 None => True
174 | Some n' => n' = n,
175 FilterIsNull = eq ""}
130 176
131 type boolGlobal = unit 177 type boolGlobal = unit
132 type boolInput = basicState bool 178 type boolInput = basicState bool
133 val bool : meta (boolGlobal, bool, boolInput) = 179 type boolFilter = basicFilter string
180 val bool : meta (boolGlobal, bool, boolInput, boolFilter) =
134 basic {Display = fn b => <xml>{[b]}</xml>, 181 basic {Display = fn b => <xml>{[b]}</xml>,
135 Edit = fn s => <xml><ccheckbox source={s}/></xml>, 182 Edit = fn s => <xml><ccheckbox source={s}/></xml>,
136 Initialize = fn b => b, 183 Initialize = fn b => b,
137 InitializeNull = False, 184 InitializeNull = False,
138 IsNull = fn _ => False, 185 IsNull = fn _ => False,
139 Parse = fn b => Some b} 186 Parse = fn b => Some b,
187 CreateFilter = "",
188 DisplayFilter = fn s => <xml><cselect source={s}>
189 <coption/>
190 <coption value="0">False</coption>
191 <coption value="1">True</coption>
192 </cselect></xml> : xbody,
193 Filter = fn s b =>
194 case s of
195 "0" => b = False
196 | "1" => b = True
197 | _ => True,
198 FilterIsNull = eq ""}
140 199
141 functor Foreign (M : sig 200 functor Foreign (M : sig
142 con row :: {Type} 201 con row :: {Type}
143 con t :: Type 202 con t :: Type
144 val show_t : show t 203 val show_t : show t
150 table tab : ([nm = t] ++ row) 209 table tab : ([nm = t] ++ row)
151 val render : $([nm = t] ++ row) -> string 210 val render : $([nm = t] ++ row) -> string
152 end) = struct 211 end) = struct
153 open M 212 open M
154 213
155 con global = list (t * string) 214 type global = list (t * string)
156 con input = source string * option (t * $row) 215 type input = source string * option (t * $row)
216 type filter = source string
157 217
158 val getChoices = List.mapQuery (SELECT * FROM tab AS T) 218 val getChoices = List.mapQuery (SELECT * FROM tab AS T)
159 (fn r => (r.T.nm, render r.T)) 219 (fn r => (r.T.nm, render r.T))
160 220
161 fun getChoice k = 221 fun getChoice k =
162 r <- oneRow (SELECT T.{{row}} FROM tab AS T WHERE T.{nm} = {[k]}); 222 r <- oneRow (SELECT T.{{row}} FROM tab AS T WHERE T.{nm} = {[k]});
163 return r.T 223 return r.T
164 224
165 val meta : meta (global, M.t, input) = 225 val meta : meta (global, M.t, input, filter) =
166 {Initialize = getChoices, 226 {Initialize = getChoices,
167 Handlers = fn choices => 227 Handlers = fn choices =>
168 NonNull ( 228 NonNull (
169 {Display = fn (_, kr) => case kr of 229 {Display = fn (_, kr) => case kr of
170 None => error <xml>Unexpected Foreign null</xml> 230 None => error <xml>Unexpected Foreign null</xml>
180 choices} 240 choices}
181 </cselect></xml>, 241 </cselect></xml>,
182 Initialize = fn k => s <- source (show k); 242 Initialize = fn k => s <- source (show k);
183 r <- rpc (getChoice k); 243 r <- rpc (getChoice k);
184 return (s, Some (k, r)), 244 return (s, Some (k, r)),
185 Parse = fn (s, _) => k <- signal s; return (read k : option t)}, 245 Parse = fn (s, _) => k <- signal s; return (read k : option t),
246 CreateFilter = source "",
247 DisplayFilter = fn s =>
248 <xml><cselect source={s}>
249 <coption/>
250 {List.mapX (fn (k, rend) =>
251 <xml><coption value={show k}>{[rend]}</coption></xml>)
252 choices}
253 </cselect></xml> : xbody,
254 Filter = fn s k => s <- signal s;
255 return (case read s : option t of
256 None => True
257 | Some k' => k' = k)},
186 {Display = fn (_, kr) => case kr of 258 {Display = fn (_, kr) => case kr of
187 None => <xml>NULL</xml> 259 None => <xml>NULL</xml>
188 | Some (k, r) => <xml>{[render ({nm = k} ++ r)]}</xml>, 260 | Some (k, r) => <xml>{[render ({nm = k} ++ r)]}</xml>,
189 Edit = fn (s, kr) => 261 Edit = fn (s, kr) =>
190 <xml><cselect source={s}> 262 <xml><cselect source={s}>
210 Parse = fn (s, _) => ks <- signal s; 282 Parse = fn (s, _) => ks <- signal s;
211 return (case ks of 283 return (case ks of
212 "" => Some None 284 "" => Some None
213 | _ => case read ks : option t of 285 | _ => case read ks : option t of
214 None => None 286 None => None
215 | Some k => Some (Some k))})} 287 | Some k => Some (Some k)),
288 CreateFilter = source "",
289 DisplayFilter = fn s =>
290 <xml><cselect source={s}>
291 <coption/>
292 <coption value="0">NULL</coption>
293 {List.mapX (fn (k, rend) =>
294 <xml><coption value={"1" ^ show k}>{[rend]}</coption>
295 </xml>)
296 choices}
297 </cselect></xml> : xbody,
298 Filter = fn s ko => s <- signal s;
299 return (case s of
300 "" => True
301 | "0" => ko = None
302 | _ =>
303 case read (String.substring s {Start = 1,
304 Len = String.length s - 1})
305 : option t of
306 None => True
307 | Some k => ko = Some k)})}
216 end 308 end
217 end 309 end
218 310
219 con computedState = (unit, xbody) 311 con computedState = (unit, xbody, unit)
220 fun computed [row] [t] (_ : show t) name (f : $row -> t) : colMeta row computedState = 312 fun computed [row] [t] (_ : show t) name (f : $row -> t) : colMeta row computedState =
221 {Initialize = return (), 313 {Initialize = return (),
222 Handlers = fn () => {Header = name, 314 Handlers = fn () => {Header = name,
223 Project = fn r => return <xml>{[f r]}</xml>, 315 Project = fn r => return <xml>{[f r]}</xml>,
224 Update = fn r _ => return r, 316 Update = fn r _ => return r,
225 Display = fn x => x, 317 Display = fn x => x,
226 Edit = fn _ => <xml>...</xml>, 318 Edit = fn _ => <xml>...</xml>,
227 Validate = fn _ => return True}} 319 Validate = fn _ => return True,
320 CreateFilter = return (),
321 DisplayFilter = fn _ => <xml/>,
322 Filter = fn _ _ => return True}}
228 fun computedHtml [row] name (f : $row -> xbody) : colMeta row computedState = 323 fun computedHtml [row] name (f : $row -> xbody) : colMeta row computedState =
229 {Initialize = return (), 324 {Initialize = return (),
230 Handlers = fn () => {Header = name, 325 Handlers = fn () => {Header = name,
231 Project = fn r => return (f r), 326 Project = fn r => return (f r),
232 Update = fn r _ => return r, 327 Update = fn r _ => return r,
233 Display = fn x => x, 328 Display = fn x => x,
234 Edit = fn _ => <xml>...</xml>, 329 Edit = fn _ => <xml>...</xml>,
235 Validate = fn _ => return True}} 330 Validate = fn _ => return True,
331 CreateFilter = return (),
332 DisplayFilter = fn _ => <xml/>,
333 Filter = fn _ _ => return True}}
236 334
237 functor Make(M : sig 335 functor Make(M : sig
238 con key :: {Type} 336 con key :: {Type}
239 con row :: {Type} 337 con row :: {Type}
240 constraint key ~ row 338 constraint key ~ row
241 table tab : (key ++ row) 339 table tab : (key ++ row)
242 340
243 val raw : $(map rawMeta (key ++ row)) 341 val raw : $(map rawMeta (key ++ row))
244 342
245 con cols :: {(Type * Type)} 343 con cols :: {(Type * Type * Type)}
246 val cols : $(map (colMeta (key ++ row)) cols) 344 val cols : $(map (colMeta (key ++ row)) cols)
247 345
248 val keyFolder : folder key 346 val keyFolder : folder key
249 val rowFolder : folder row 347 val rowFolder : folder row
250 val colsFolder : folder cols 348 val colsFolder : folder cols