annotate demo/more/dbgrid.ur @ 936:6966d98c80b5

Include 'key' type in Grid
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Sep 2009 09:45:46 -0400
parents 2422360c78a3
children 37dd42935dad
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@915 5 con colMeta' = fn (row :: {Type}) (t :: Type) =>
adamc@915 6 {Header : string,
adamc@915 7 Project : $row -> transaction t,
adamc@915 8 Update : $row -> t -> transaction ($row),
adamc@915 9 Display : t -> xbody,
adamc@915 10 Edit : t -> xbody,
adamc@915 11 Validate : t -> signal bool}
adamc@915 12
adamc@915 13 con colMeta = fn (row :: {Type}) (global_t :: (Type * Type)) =>
adamc@915 14 {Initialize : transaction global_t.1,
adamc@915 15 Handlers : global_t.1 -> colMeta' row global_t.2}
adamc@915 16
adamc@935 17 con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
adamc@935 18 {Initial : acc,
adamc@935 19 Step : $row -> acc -> acc,
adamc@935 20 Display : acc -> xbody}
adamc@935 21
adamc@915 22 structure Direct = struct
adamc@930 23 con metaBase = fn actual_input :: (Type * Type) =>
adamc@930 24 {Display : actual_input.2 -> xbody,
adamc@930 25 Edit : actual_input.2 -> xbody,
adamc@930 26 Initialize : actual_input.1 -> transaction actual_input.2,
adamc@930 27 Parse : actual_input.2 -> signal (option actual_input.1)}
adamc@930 28
adamc@930 29 datatype metaBoth actual input =
adamc@930 30 NonNull of metaBase (actual, input) * metaBase (option actual, input)
adamc@930 31 | Nullable of metaBase (actual, input)
adamc@930 32
adamc@915 33 con meta = fn global_actual_input :: (Type * Type * Type) =>
adamc@915 34 {Initialize : transaction global_actual_input.1,
adamc@915 35 Handlers : global_actual_input.1
adamc@930 36 -> metaBoth global_actual_input.2 global_actual_input.3}
adamc@915 37
adamc@915 38 con editableState (ts :: (Type * Type * Type)) = (ts.1, ts.3)
adamc@915 39 fun editable [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
adamc@915 40 (editableState ts) =
adamc@930 41 let
adamc@930 42 fun doMr mr = {Header = name,
adamc@930 43 Project = fn r => mr.Initialize r.nm,
adamc@930 44 Update = fn r s =>
adamc@930 45 vo <- current (mr.Parse s);
adamc@930 46 return (case vo of
adamc@930 47 None => r
adamc@930 48 | Some v => r -- nm ++ {nm = v}),
adamc@930 49 Display = mr.Display,
adamc@930 50 Edit = mr.Edit,
adamc@930 51 Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo)}
adamc@930 52 in
adamc@930 53 {Initialize = m.Initialize,
adamc@930 54 Handlers = fn data => case m.Handlers data of
adamc@930 55 NonNull (mr, _) => doMr mr
adamc@930 56 | Nullable mr => doMr mr}
adamc@930 57 end
adamc@915 58
adamc@915 59 con readOnlyState (ts :: (Type * Type * Type)) = (ts.1, ts.3)
adamc@915 60 fun readOnly [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
adamc@915 61 (readOnlyState ts) =
adamc@930 62 let
adamc@930 63 fun doMr mr = {Header = name,
adamc@930 64 Project = fn r => mr.Initialize r.nm,
adamc@930 65 Update = fn r _ => return r,
adamc@930 66 Display = mr.Display,
adamc@930 67 Edit = mr.Display,
adamc@930 68 Validate = fn _ => return True}
adamc@930 69 in
adamc@930 70 {Initialize = m.Initialize,
adamc@930 71 Handlers = fn data => case m.Handlers data of
adamc@930 72 NonNull (mr, _) => doMr mr
adamc@930 73 | Nullable mr => doMr mr}
adamc@930 74 end
adamc@915 75
adamc@915 76 con metaBasic = fn actual_input :: (Type * Type) =>
adamc@930 77 {Display : actual_input.2 -> xbody,
adamc@930 78 Edit : source actual_input.2 -> xbody,
adamc@930 79 Initialize : actual_input.1 -> actual_input.2,
adamc@930 80 InitializeNull : actual_input.2,
adamc@930 81 IsNull : actual_input.2 -> bool,
adamc@930 82 Parse : actual_input.2 -> option actual_input.1}
adamc@915 83
adamc@915 84 con basicState = source
adamc@915 85 fun basic [ts ::: (Type * Type)] (m : metaBasic ts) : meta (unit, ts.1, basicState ts.2) =
adamc@915 86 {Initialize = return (),
adamc@930 87 Handlers = fn () => NonNull (
adamc@930 88 {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>,
adamc@915 89 Edit = m.Edit,
adamc@915 90 Initialize = fn v => source (m.Initialize v),
adamc@930 91 Parse = fn s => v <- signal s; return (m.Parse v)},
adamc@930 92 {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>,
adamc@930 93 Edit = m.Edit,
adamc@930 94 Initialize = fn v => source (case v of
adamc@930 95 None => m.InitializeNull
adamc@930 96 | Some v => m.Initialize v),
adamc@930 97 Parse = fn s => v <- signal s;
adamc@930 98 return (if m.IsNull v then
adamc@930 99 Some None
adamc@930 100 else
adamc@930 101 case m.Parse v of
adamc@930 102 None => None
adamc@930 103 | Some v' => Some (Some v'))})}
adamc@930 104
adamc@930 105 fun nullable [global] [actual] [input] (m : meta (global, actual, input)) =
adamc@930 106 {Initialize = m.Initialize,
adamc@930 107 Handlers = fn d => case m.Handlers d of
adamc@930 108 Nullable _ => error <xml>Don't stack calls to Direct.nullable!</xml>
adamc@930 109 | NonNull (_, ho) => Nullable ho}
adamc@915 110
adamc@915 111 type intGlobal = unit
adamc@915 112 type intInput = basicState string
adamc@915 113 val int : meta (intGlobal, int, intInput) =
adamc@915 114 basic {Display = fn s => <xml>{[s]}</xml>,
adamc@915 115 Edit = fn s => <xml><ctextbox source={s}/></xml>,
adamc@915 116 Initialize = fn n => show n,
adamc@930 117 InitializeNull = "",
adamc@930 118 IsNull = eq "",
adamc@915 119 Parse = fn v => read v}
adamc@915 120
adamc@915 121 type stringGlobal = unit
adamc@915 122 type stringInput = basicState string
adamc@915 123 val string : meta (stringGlobal, string, stringInput) =
adamc@915 124 basic {Display = fn s => <xml>{[s]}</xml>,
adamc@915 125 Edit = fn s => <xml><ctextbox source={s}/></xml>,
adamc@915 126 Initialize = fn s => s,
adamc@930 127 InitializeNull = "",
adamc@930 128 IsNull = eq "",
adamc@915 129 Parse = fn s => Some s}
adamc@915 130
adamc@915 131 type boolGlobal = unit
adamc@915 132 type boolInput = basicState bool
adamc@915 133 val bool : meta (boolGlobal, bool, boolInput) =
adamc@915 134 basic {Display = fn b => <xml>{[b]}</xml>,
adamc@915 135 Edit = fn s => <xml><ccheckbox source={s}/></xml>,
adamc@915 136 Initialize = fn b => b,
adamc@930 137 InitializeNull = False,
adamc@930 138 IsNull = fn _ => False,
adamc@915 139 Parse = fn b => Some b}
adamc@915 140
adamc@915 141 functor Foreign (M : sig
adamc@915 142 con row :: {Type}
adamc@915 143 con t :: Type
adamc@915 144 val show_t : show t
adamc@915 145 val read_t : read t
adamc@915 146 val eq_t : eq t
adamc@915 147 val inj_t : sql_injectable t
adamc@915 148 con nm :: Name
adamc@915 149 constraint [nm] ~ row
adamc@915 150 table tab : ([nm = t] ++ row)
adamc@915 151 val render : $([nm = t] ++ row) -> string
adamc@915 152 end) = struct
adamc@915 153 open M
adamc@915 154
adamc@915 155 con global = list (t * string)
adamc@930 156 con input = source string * option (t * $row)
adamc@915 157
adamc@915 158 val getChoices = List.mapQuery (SELECT * FROM tab AS T)
adamc@915 159 (fn r => (r.T.nm, render r.T))
adamc@915 160
adamc@915 161 fun getChoice k =
adamc@915 162 r <- oneRow (SELECT T.{{row}} FROM tab AS T WHERE T.{nm} = {[k]});
adamc@915 163 return r.T
adamc@915 164
adamc@930 165 val meta : meta (global, M.t, input) =
adamc@915 166 {Initialize = getChoices,
adamc@915 167 Handlers = fn choices =>
adamc@930 168 NonNull (
adamc@930 169 {Display = fn (_, kr) => case kr of
adamc@930 170 None => error <xml>Unexpected Foreign null</xml>
adamc@930 171 | Some (k, r) => <xml>{[render ({nm = k} ++ r)]}</xml>,
adamc@930 172 Edit = fn (s, kr) =>
adamc@915 173 <xml><cselect source={s}>
adamc@915 174 {List.mapX (fn (k', rend) =>
adamc@930 175 <xml><coption value={show k'} selected={case kr of
adamc@930 176 None => False
adamc@930 177 | Some (k, _) =>
adamc@930 178 k' = k}>{[rend]}</coption>
adamc@915 179 </xml>)
adamc@915 180 choices}
adamc@915 181 </cselect></xml>,
adamc@915 182 Initialize = fn k => s <- source (show k);
adamc@915 183 r <- rpc (getChoice k);
adamc@930 184 return (s, Some (k, r)),
adamc@930 185 Parse = fn (s, _) => k <- signal s; return (read k : option t)},
adamc@930 186 {Display = fn (_, kr) => case kr of
adamc@930 187 None => <xml>NULL</xml>
adamc@930 188 | Some (k, r) => <xml>{[render ({nm = k} ++ r)]}</xml>,
adamc@930 189 Edit = fn (s, kr) =>
adamc@930 190 <xml><cselect source={s}>
adamc@930 191 <coption value="" selected={case kr of
adamc@930 192 None => True
adamc@930 193 | _ => False}>NULL</coption>
adamc@930 194 {List.mapX (fn (k', rend) =>
adamc@930 195 <xml><coption value={show k'} selected={case kr of
adamc@930 196 None => False
adamc@930 197 | Some (k, _) =>
adamc@930 198 k' = k}>{[rend]}</coption>
adamc@930 199 </xml>)
adamc@930 200 choices}
adamc@930 201 </cselect></xml>,
adamc@930 202 Initialize = fn k => case k of
adamc@930 203 None =>
adamc@930 204 s <- source "";
adamc@930 205 return (s, None)
adamc@930 206 | Some k =>
adamc@930 207 s <- source (show k);
adamc@930 208 r <- rpc (getChoice k);
adamc@930 209 return (s, Some (k, r)),
adamc@930 210 Parse = fn (s, _) => ks <- signal s;
adamc@930 211 return (case ks of
adamc@930 212 "" => Some None
adamc@930 213 | _ => case read ks : option t of
adamc@930 214 None => None
adamc@930 215 | Some k => Some (Some k))})}
adamc@915 216 end
adamc@915 217 end
adamc@915 218
adamc@915 219 con computedState = (unit, xbody)
adamc@915 220 fun computed [row] [t] (_ : show t) name (f : $row -> t) : colMeta row computedState =
adamc@915 221 {Initialize = return (),
adamc@915 222 Handlers = fn () => {Header = name,
adamc@915 223 Project = fn r => return <xml>{[f r]}</xml>,
adamc@915 224 Update = fn r _ => return r,
adamc@915 225 Display = fn x => x,
adamc@915 226 Edit = fn _ => <xml>...</xml>,
adamc@915 227 Validate = fn _ => return True}}
adamc@915 228 fun computedHtml [row] name (f : $row -> xbody) : colMeta row computedState =
adamc@915 229 {Initialize = return (),
adamc@915 230 Handlers = fn () => {Header = name,
adamc@915 231 Project = fn r => return (f r),
adamc@915 232 Update = fn r _ => return r,
adamc@915 233 Display = fn x => x,
adamc@915 234 Edit = fn _ => <xml>...</xml>,
adamc@915 235 Validate = fn _ => return True}}
adamc@915 236
adamc@915 237 functor Make(M : sig
adamc@915 238 con key :: {Type}
adamc@915 239 con row :: {Type}
adamc@915 240 constraint key ~ row
adamc@915 241 table tab : (key ++ row)
adamc@915 242
adamc@915 243 val raw : $(map rawMeta (key ++ row))
adamc@915 244
adamc@915 245 con cols :: {(Type * Type)}
adamc@915 246 val cols : $(map (colMeta (key ++ row)) cols)
adamc@915 247
adamc@915 248 val keyFolder : folder key
adamc@915 249 val rowFolder : folder row
adamc@915 250 val colsFolder : folder cols
adamc@935 251
adamc@935 252 con aggregates :: {Type}
adamc@935 253 val aggregates : $(map (aggregateMeta (key ++ row)) aggregates)
adamc@915 254 end) = struct
adamc@915 255 open Grid.Make(struct
adamc@936 256 fun keyOf r = r --- M.row
adamc@936 257
adamc@915 258 val list = query (SELECT * FROM {{M.tab}} AS T) (fn r rs => return (r.T :: rs)) []
adamc@915 259
adamc@915 260 val wholeRow = @Folder.concat ! M.keyFolder M.rowFolder
adamc@915 261
adamc@915 262 fun ensql [env] (r : $(M.key ++ M.row)) =
adamc@915 263 map2 [rawMeta] [id] [sql_exp env [] []]
adamc@915 264 (fn [t] meta v => @sql_inject meta.Inj v)
adamc@915 265 [_] wholeRow M.raw r
adamc@915 266
adamc@915 267 val new =
adamc@915 268 row <- Monad.mapR [rawMeta] [id]
adamc@915 269 (fn [nm :: Name] [t :: Type] meta => meta.New)
adamc@915 270 [_] wholeRow M.raw;
adamc@915 271 dml (insert M.tab (ensql row));
adamc@915 272 return row
adamc@915 273
adamc@936 274 fun selector (r : $M.key) : sql_exp [T = M.key ++ M.row] [] [] bool =
adamc@915 275 foldR2 [rawMeta] [id]
adamc@915 276 [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool]
adamc@915 277 (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
adamc@915 278 (meta : rawMeta t) (v : t)
adamc@915 279 (exp : rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool)
adamc@915 280 [rest :: {Type}] [rest ~ [nm = t] ++ key] =>
adamc@915 281 (WHERE T.{nm} = {@sql_inject meta.Inj v} AND {exp [[nm = t] ++ rest] !}))
adamc@915 282 (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE))
adamc@936 283 [_] M.keyFolder (M.raw --- map rawMeta M.row) r
adamc@915 284 [_] !
adamc@915 285
adamc@936 286 fun save key row =
adamc@915 287 dml (update [M.key ++ M.row] !
adamc@936 288 (ensql row)
adamc@915 289 M.tab
adamc@936 290 (selector key))
adamc@915 291
adamc@936 292 fun delete key =
adamc@936 293 dml (Basis.delete M.tab (selector key))
adamc@915 294
adamc@915 295 val cols = M.cols
adamc@915 296
adamc@915 297 val folder = M.colsFolder
adamc@935 298
adamc@935 299 val aggregates = M.aggregates
adamc@915 300 end)
adamc@915 301 end