Mercurial > urweb

annotate demo/more/dbgrid.ur @ 1886:b7cd3c7c7edd

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