Mercurial > urweb

annotate demo/more/dbgrid.ur @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
parents fbc3a0eef45a
children 8d3aa6c7cee0
rev   line source
adamc@915 1 con rawMeta = fn t :: Type =>
adamc@915 2 {New : transaction t,
adamc@915 3 Inj : sql_injectable t}
adamc@915 4
adamc@944 5 con colMeta' = fn (row :: {Type}) (input :: Type) (filter :: Type) =>
adamc@915 6 {Header : string,
adamc@944 7 Project : $row -> transaction input,
adamc@944 8 Update : $row -> input -> transaction ($row),
adamc@944 9 Display : input -> xbody,
adamc@944 10 Edit : input -> xbody,
adamc@944 11 Validate : input -> signal bool,
adamc@944 12 CreateFilter : transaction filter,
adamc@944 13 DisplayFilter : filter -> xbody,
adamc@961 14 Filter : filter -> $row -> signal bool,
adamc@961 15 Sort : option ($row -> $row -> bool)}
adamc@915 16
adamc@944 17 con colMeta = fn (row :: {Type}) (global_input_filter :: (Type * Type * Type)) =>
adamc@944 18 {Initialize : transaction global_input_filter.1,
adamc@944 19 Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3}
adamc@915 20
adamc@935 21 con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
adamc@935 22 {Initial : acc,
adamc@935 23 Step : $row -> acc -> acc,
adamc@935 24 Display : acc -> xbody}
adamc@935 25
adamc@915 26 structure Direct = struct
adamc@944 27 con metaBase = fn actual_input_filter :: (Type * Type * Type) =>
adamc@944 28 {Display : actual_input_filter.2 -> xbody,
adamc@944 29 Edit : actual_input_filter.2 -> xbody,
adamc@944 30 Initialize : actual_input_filter.1 -> transaction actual_input_filter.2,
adamc@944 31 Parse : actual_input_filter.2 -> signal (option actual_input_filter.1),
adamc@944 32 CreateFilter : transaction actual_input_filter.3,
adamc@944 33 DisplayFilter : actual_input_filter.3 -> xbody,
adamc@961 34 Filter : actual_input_filter.3 -> actual_input_filter.1 -> signal bool,
adamc@961 35 Sort : actual_input_filter.1 -> actual_input_filter.1 -> bool}
adamc@930 36
adamc@944 37 datatype metaBoth actual input filter =
adamc@944 38 NonNull of metaBase (actual, input, filter) * metaBase (option actual, input, filter)
adamc@944 39 | Nullable of metaBase (actual, input, filter)
adamc@930 40
adamc@944 41 con meta = fn global_actual_input_filter :: (Type * Type * Type * Type) =>
adamc@944 42 {Initialize : transaction global_actual_input_filter.1,
adamc@944 43 Handlers : global_actual_input_filter.1
adamc@944 44 -> metaBoth global_actual_input_filter.2 global_actual_input_filter.3
adamc@944 45 global_actual_input_filter.4}
adamc@915 46
adamc@944 47 con editableState (ts :: (Type * Type * Type * Type)) = (ts.1, ts.3, ts.4)
adamc@915 48 fun editable [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
adamc@915 49 (editableState ts) =
adamc@930 50 let
adamc@930 51 fun doMr mr = {Header = name,
adamc@930 52 Project = fn r => mr.Initialize r.nm,
adamc@930 53 Update = fn r s =>
adamc@930 54 vo <- current (mr.Parse s);
adamc@930 55 return (case vo of
adamc@930 56 None => r
adamc@930 57 | Some v => r -- nm ++ {nm = v}),
adamc@930 58 Display = mr.Display,
adamc@930 59 Edit = mr.Edit,
adamc@944 60 Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo),
adamc@944 61 CreateFilter = mr.CreateFilter,
adamc@944 62 DisplayFilter = mr.DisplayFilter,
adamc@961 63 Filter = fn i r => mr.Filter i r.nm,
adamc@961 64 Sort = Some (fn r1 r2 => mr.Sort r1.nm r2.nm)}
adamc@930 65 in
adamc@930 66 {Initialize = m.Initialize,
adamc@930 67 Handlers = fn data => case m.Handlers data of
adamc@930 68 NonNull (mr, _) => doMr mr
adamc@930 69 | Nullable mr => doMr mr}
adamc@930 70 end
adamc@915 71
adamc@944 72 con readOnlyState (ts :: (Type * Type * Type * Type)) = (ts.1, ts.3, ts.4)
adamc@915 73 fun readOnly [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
adamc@915 74 (readOnlyState ts) =
adamc@930 75 let
adamc@930 76 fun doMr mr = {Header = name,
adamc@930 77 Project = fn r => mr.Initialize r.nm,
adamc@930 78 Update = fn r _ => return r,
adamc@930 79 Display = mr.Display,
adamc@930 80 Edit = mr.Display,
adamc@944 81 Validate = fn _ => return True,
adamc@944 82 CreateFilter = mr.CreateFilter,
adamc@944 83 DisplayFilter = mr.DisplayFilter,
adamc@961 84 Filter = fn i r => mr.Filter i r.nm,
adamc@961 85 Sort = Some (fn r1 r2 => mr.Sort r1.nm r2.nm)}
adamc@930 86 in
adamc@930 87 {Initialize = m.Initialize,
adamc@930 88 Handlers = fn data => case m.Handlers data of
adamc@930 89 NonNull (mr, _) => doMr mr
adamc@930 90 | Nullable mr => doMr mr}
adamc@930 91 end
adamc@915 92
adamc@944 93 con metaBasic = fn actual_input_filter :: (Type * Type * Type) =>
adamc@944 94 {Display : actual_input_filter.2 -> xbody,
adamc@944 95 Edit : source actual_input_filter.2 -> xbody,
adamc@944 96 Initialize : actual_input_filter.1 -> actual_input_filter.2,
adamc@944 97 InitializeNull : actual_input_filter.2,
adamc@944 98 IsNull : actual_input_filter.2 -> bool,
adamc@944 99 Parse : actual_input_filter.2 -> option actual_input_filter.1,
adamc@944 100 CreateFilter : actual_input_filter.3,
adamc@944 101 DisplayFilter : source actual_input_filter.3 -> xbody,
adamc@944 102 Filter : actual_input_filter.3 -> actual_input_filter.1 -> bool,
adamc@961 103 FilterIsNull : actual_input_filter.3 -> bool,
adamc@961 104 Sort : actual_input_filter.1 -> actual_input_filter.1 -> bool}
adamc@915 105
adamc@915 106 con basicState = source
adamc@944 107 con basicFilter = source
adamc@944 108 fun basic [ts ::: (Type * Type * Type)] (m : metaBasic ts) : meta (unit, ts.1, basicState ts.2, basicFilter ts.3) =
adamc@915 109 {Initialize = return (),
adamc@930 110 Handlers = fn () => NonNull (
adamc@930 111 {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>,
adamc@915 112 Edit = m.Edit,
adamc@915 113 Initialize = fn v => source (m.Initialize v),
adamc@944 114 Parse = fn s => v <- signal s; return (m.Parse v),
adamc@944 115 CreateFilter = source m.CreateFilter,
adamc@944 116 DisplayFilter = m.DisplayFilter,
adamc@946 117 Filter = fn f v => f <- signal f;
adamc@946 118 return (if m.FilterIsNull f then
adamc@946 119 True
adamc@946 120 else
adamc@961 121 m.Filter f v),
adamc@961 122 Sort = m.Sort},
adamc@930 123 {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>,
adamc@930 124 Edit = m.Edit,
adamc@930 125 Initialize = fn v => source (case v of
adamc@930 126 None => m.InitializeNull
adamc@930 127 | Some v => m.Initialize v),
adamc@930 128 Parse = fn s => v <- signal s;
adamc@930 129 return (if m.IsNull v then
adamc@930 130 Some None
adamc@930 131 else
adamc@930 132 case m.Parse v of
adamc@930 133 None => None
adamc@944 134 | Some v' => Some (Some v')),
adamc@944 135 CreateFilter = source m.CreateFilter,
adamc@944 136 DisplayFilter = m.DisplayFilter,
adamc@944 137 Filter = fn f v => f <- signal f;
adamc@944 138 return (if m.FilterIsNull f then
adamc@946 139 True
adamc@944 140 else
adamc@944 141 case v of
adamc@944 142 None => False
adamc@961 143 | Some v => m.Filter f v),
adamc@961 144 Sort = fn x y =>
adamc@961 145 case (x, y) of
adamc@961 146 (None, _) => True
adamc@961 147 | (Some x', Some y') => m.Sort x' y'
adamc@961 148 | _ => False})}
adamc@930 149
adamc@944 150 fun nullable [global] [actual] [input] [filter] (m : meta (global, actual, input, filter)) =
adamc@930 151 {Initialize = m.Initialize,
adamc@930 152 Handlers = fn d => case m.Handlers d of
adamc@930 153 Nullable _ => error <xml>Don't stack calls to Direct.nullable!</xml>
adamc@930 154 | NonNull (_, ho) => Nullable ho}
adamc@915 155
adamc@915 156 type intGlobal = unit
adamc@915 157 type intInput = basicState string
adamc@944 158 type intFilter = basicFilter string
adamc@944 159 val int : meta (intGlobal, int, intInput, intFilter) =
adamc@915 160 basic {Display = fn s => <xml>{[s]}</xml>,
adamc@946 161 Edit = fn s => <xml><ctextbox size={5} source={s}/></xml>,
adamc@915 162 Initialize = fn n => show n,
adamc@930 163 InitializeNull = "",
adamc@930 164 IsNull = eq "",
adamc@944 165 Parse = fn v => read v,
adamc@944 166 CreateFilter = "",
adamc@946 167 DisplayFilter = fn s => <xml><ctextbox size={5} source={s}/></xml> : xbody,
adamc@944 168 Filter = fn s n =>
adamc@944 169 case read s of
adamc@944 170 None => True
adamc@944 171 | Some n' => n' = n,
adamc@961 172 FilterIsNull = eq "",
adamc@961 173 Sort = le}
adamc@915 174
adamc@915 175 type stringGlobal = unit
adamc@915 176 type stringInput = basicState string
adamc@944 177 type stringFilter = basicFilter string
adamc@944 178 val string : meta (stringGlobal, string, stringInput, stringFilter) =
adamc@915 179 basic {Display = fn s => <xml>{[s]}</xml>,
adamc@915 180 Edit = fn s => <xml><ctextbox source={s}/></xml>,
adamc@915 181 Initialize = fn s => s,
adamc@930 182 InitializeNull = "",
adamc@930 183 IsNull = eq "",
adamc@944 184 Parse = fn s => Some s,
adamc@944 185 CreateFilter = "",
adamc@944 186 DisplayFilter = fn s => <xml><ctextbox source={s}/></xml> : xbody,
adamc@944 187 Filter = fn s n =>
adamc@944 188 case read s of
adamc@944 189 None => True
adamc@944 190 | Some n' => n' = n,
adamc@961 191 FilterIsNull = eq "",
adamc@961 192 Sort = le}
adamc@915 193
adamc@915 194 type boolGlobal = unit
adamc@915 195 type boolInput = basicState bool
adamc@944 196 type boolFilter = basicFilter string
adamc@944 197 val bool : meta (boolGlobal, bool, boolInput, boolFilter) =
adamc@915 198 basic {Display = fn b => <xml>{[b]}</xml>,
adamc@915 199 Edit = fn s => <xml><ccheckbox source={s}/></xml>,
adamc@915 200 Initialize = fn b => b,
adamc@930 201 InitializeNull = False,
adamc@930 202 IsNull = fn _ => False,
adamc@944 203 Parse = fn b => Some b,
adamc@944 204 CreateFilter = "",
adamc@944 205 DisplayFilter = fn s => <xml><cselect source={s}>
adamc@944 206 <coption/>
adamc@944 207 <coption value="0">False</coption>
adamc@944 208 <coption value="1">True</coption>
adamc@944 209 </cselect></xml> : xbody,
adamc@944 210 Filter = fn s b =>
adamc@944 211 case s of
adamc@944 212 "0" => b = False
adamc@944 213 | "1" => b = True
adamc@944 214 | _ => True,
adamc@961 215 FilterIsNull = eq "",
adamc@961 216 Sort = le}
adamc@915 217
adamc@915 218 functor Foreign (M : sig
adamc@915 219 con row :: {Type}
adamc@915 220 con t :: Type
adamc@915 221 val show_t : show t
adamc@915 222 val read_t : read t
adamc@915 223 val eq_t : eq t
adamc@961 224 val ord_t : ord t
adamc@915 225 val inj_t : sql_injectable t
adamc@915 226 con nm :: Name
adamc@915 227 constraint [nm] ~ row
adamc@915 228 table tab : ([nm = t] ++ row)
adamc@915 229 val render : $([nm = t] ++ row) -> string
adamc@915 230 end) = struct
adamc@915 231 open M
adamc@915 232
adamc@944 233 type global = list (t * string)
adamc@944 234 type input = source string * option (t * $row)
adamc@944 235 type filter = source string
adamc@915 236
adamc@915 237 val getChoices = List.mapQuery (SELECT * FROM tab AS T)
adamc@915 238 (fn r => (r.T.nm, render r.T))
adamc@915 239
adamc@915 240 fun getChoice k =
adamc@915 241 r <- oneRow (SELECT T.{{row}} FROM tab AS T WHERE T.{nm} = {[k]});
adamc@915 242 return r.T
adamc@915 243
adamc@944 244 val meta : meta (global, M.t, input, filter) =
adamc@915 245 {Initialize = getChoices,
adamc@915 246 Handlers = fn choices =>
adamc@930 247 NonNull (
adamc@930 248 {Display = fn (_, kr) => case kr of
adamc@930 249 None => error <xml>Unexpected Foreign null</xml>
adamc@930 250 | Some (k, r) => <xml>{[render ({nm = k} ++ r)]}</xml>,
adamc@930 251 Edit = fn (s, kr) =>
adamc@915 252 <xml><cselect source={s}>
adamc@915 253 {List.mapX (fn (k', rend) =>
adamc@930 254 <xml><coption value={show k'} selected={case kr of
adamc@930 255 None => False
adamc@930 256 | Some (k, _) =>
adamc@930 257 k' = k}>{[rend]}</coption>
adamc@915 258 </xml>)
adamc@915 259 choices}
adamc@915 260 </cselect></xml>,
adamc@915 261 Initialize = fn k => s <- source (show k);
adamc@915 262 r <- rpc (getChoice k);
adamc@930 263 return (s, Some (k, r)),
adamc@944 264 Parse = fn (s, _) => k <- signal s; return (read k : option t),
adamc@944 265 CreateFilter = source "",
adamc@944 266 DisplayFilter = fn s =>
adamc@944 267 <xml><cselect source={s}>
adamc@944 268 <coption/>
adamc@944 269 {List.mapX (fn (k, rend) =>
adamc@944 270 <xml><coption value={show k}>{[rend]}</coption></xml>)
adamc@944 271 choices}
adamc@944 272 </cselect></xml> : xbody,
adamc@944 273 Filter = fn s k => s <- signal s;
adamc@944 274 return (case read s : option t of
adamc@944 275 None => True
adamc@961 276 | Some k' => k' = k),
adamc@961 277 Sort = le},
adamc@930 278 {Display = fn (_, kr) => case kr of
adamc@930 279 None => <xml>NULL</xml>
adamc@930 280 | Some (k, r) => <xml>{[render ({nm = k} ++ r)]}</xml>,
adamc@930 281 Edit = fn (s, kr) =>
adamc@930 282 <xml><cselect source={s}>
adamc@930 283 <coption value="" selected={case kr of
adamc@930 284 None => True
adamc@930 285 | _ => False}>NULL</coption>
adamc@930 286 {List.mapX (fn (k', rend) =>
adamc@930 287 <xml><coption value={show k'} selected={case kr of
adamc@930 288 None => False
adamc@930 289 | Some (k, _) =>
adamc@930 290 k' = k}>{[rend]}</coption>
adamc@930 291 </xml>)
adamc@930 292 choices}
adamc@930 293 </cselect></xml>,
adamc@930 294 Initialize = fn k => case k of
adamc@930 295 None =>
adamc@930 296 s <- source "";
adamc@930 297 return (s, None)
adamc@930 298 | Some k =>
adamc@930 299 s <- source (show k);
adamc@930 300 r <- rpc (getChoice k);
adamc@930 301 return (s, Some (k, r)),
adamc@930 302 Parse = fn (s, _) => ks <- signal s;
adamc@930 303 return (case ks of
adamc@930 304 "" => Some None
adamc@930 305 | _ => case read ks : option t of
adamc@930 306 None => None
adamc@944 307 | Some k => Some (Some k)),
adamc@944 308 CreateFilter = source "",
adamc@944 309 DisplayFilter = fn s =>
adamc@944 310 <xml><cselect source={s}>
adamc@944 311 <coption/>
adamc@944 312 <coption value="0">NULL</coption>
adamc@944 313 {List.mapX (fn (k, rend) =>
adamc@944 314 <xml><coption value={"1" ^ show k}>{[rend]}</coption>
adamc@944 315 </xml>)
adamc@944 316 choices}
adamc@944 317 </cselect></xml> : xbody,
adamc@944 318 Filter = fn s ko => s <- signal s;
adamc@944 319 return (case s of
adamc@944 320 "" => True
adamc@944 321 | "0" => ko = None
adamc@944 322 | _ =>
adamc@944 323 case read (String.substring s {Start = 1,
adamc@944 324 Len = String.length s - 1})
adamc@944 325 : option t of
adamc@944 326 None => True
adamc@961 327 | Some k => ko = Some k),
adamc@961 328 Sort = le})}
adamc@915 329 end
adamc@915 330 end
adamc@915 331
adamc@944 332 con computedState = (unit, xbody, unit)
adamc@915 333 fun computed [row] [t] (_ : show t) name (f : $row -> t) : colMeta row computedState =
adamc@915 334 {Initialize = return (),
adamc@915 335 Handlers = fn () => {Header = name,
adamc@915 336 Project = fn r => return <xml>{[f r]}</xml>,
adamc@915 337 Update = fn r _ => return r,
adamc@915 338 Display = fn x => x,
adamc@915 339 Edit = fn _ => <xml>...</xml>,
adamc@944 340 Validate = fn _ => return True,
adamc@944 341 CreateFilter = return (),
adamc@944 342 DisplayFilter = fn _ => <xml/>,
adamc@961 343 Filter = fn _ _ => return True,
adamc@961 344 Sort = None}}
adamc@915 345 fun computedHtml [row] name (f : $row -> xbody) : colMeta row computedState =
adamc@915 346 {Initialize = return (),
adamc@915 347 Handlers = fn () => {Header = name,
adamc@915 348 Project = fn r => return (f r),
adamc@915 349 Update = fn r _ => return r,
adamc@915 350 Display = fn x => x,
adamc@915 351 Edit = fn _ => <xml>...</xml>,
adamc@944 352 Validate = fn _ => return True,
adamc@944 353 CreateFilter = return (),
adamc@944 354 DisplayFilter = fn _ => <xml/>,
adamc@961 355 Filter = fn _ _ => return True,
adamc@961 356 Sort = None}}
adamc@915 357
adamc@915 358 functor Make(M : sig
adamc@915 359 con key :: {Type}
adamc@915 360 con row :: {Type}
adamc@915 361 constraint key ~ row
adamc@915 362 table tab : (key ++ row)
adamc@915 363
adamc@915 364 val raw : $(map rawMeta (key ++ row))
adamc@915 365
adamc@944 366 con cols :: {(Type * Type * Type)}
adamc@915 367 val cols : $(map (colMeta (key ++ row)) cols)
adamc@915 368
adamc@915 369 val keyFolder : folder key
adamc@915 370 val rowFolder : folder row
adamc@915 371 val colsFolder : folder cols
adamc@935 372
adamc@935 373 con aggregates :: {Type}
adamc@935 374 val aggregates : $(map (aggregateMeta (key ++ row)) aggregates)
adamc@937 375 val aggFolder : folder aggregates
adamc@964 376
adamc@964 377 val pageLength : option int
adamc@915 378 end) = struct
adamc@915 379 open Grid.Make(struct
adamc@936 380 fun keyOf r = r --- M.row
adamc@936 381
adamc@915 382 val list = query (SELECT * FROM {{M.tab}} AS T) (fn r rs => return (r.T :: rs)) []
adamc@915 383
adamc@915 384 val wholeRow = @Folder.concat ! M.keyFolder M.rowFolder
adamc@915 385
adamc@915 386 fun ensql [env] (r : $(M.key ++ M.row)) =
adamc@915 387 map2 [rawMeta] [id] [sql_exp env [] []]
adamc@915 388 (fn [t] meta v => @sql_inject meta.Inj v)
adamc@915 389 [_] wholeRow M.raw r
adamc@915 390
adamc@915 391 val new =
adamc@915 392 row <- Monad.mapR [rawMeta] [id]
adamc@915 393 (fn [nm :: Name] [t :: Type] meta => meta.New)
adamc@915 394 [_] wholeRow M.raw;
adamc@915 395 dml (insert M.tab (ensql row));
adamc@915 396 return row
adamc@915 397
adamc@936 398 fun selector (r : $M.key) : sql_exp [T = M.key ++ M.row] [] [] bool =
adamc@915 399 foldR2 [rawMeta] [id]
adamc@915 400 [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool]
adamc@915 401 (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
adamc@915 402 (meta : rawMeta t) (v : t)
adamc@915 403 (exp : rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool)
adamc@915 404 [rest :: {Type}] [rest ~ [nm = t] ++ key] =>
adamc@915 405 (WHERE T.{nm} = {@sql_inject meta.Inj v} AND {exp [[nm = t] ++ rest] !}))
adamc@915 406 (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE))
adamc@936 407 [_] M.keyFolder (M.raw --- map rawMeta M.row) r
adamc@915 408 [_] !
adamc@915 409
adamc@936 410 fun save key row =
adamc@915 411 dml (update [M.key ++ M.row] !
adamc@936 412 (ensql row)
adamc@915 413 M.tab
adamc@936 414 (selector key))
adamc@915 415
adamc@936 416 fun delete key =
adamc@936 417 dml (Basis.delete M.tab (selector key))
adamc@915 418
adamc@915 419 val cols = M.cols
adamc@915 420
adamc@915 421 val folder = M.colsFolder
adamc@935 422
adamc@935 423 val aggregates = M.aggregates
adamc@937 424
adamc@937 425 val aggFolder = M.aggFolder
adamc@964 426
adamc@964 427 val pageLength = M.pageLength
adamc@915 428 end)
adamc@915 429 end