Mercurial > urweb

annotate demo/more/dbgrid.ur @ 955:01a4d936395a

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