annotate demo/batchFun.ur @ 732:5819fb63c93a

Effectness analysis
author Adam Chlipala <adamc@hcoop.net>
date Thu, 16 Apr 2009 15:29:39 -0400
parents 1fb318c17546
children 669ac5e9a69e
rev   line source
adamc@650 1 con colMeta = fn t_state :: (Type * Type) =>
adamc@650 2 {Nam : string,
adamc@650 3 Show : t_state.1 -> xbody,
adamc@650 4 Inject : sql_injectable t_state.1,
adamc@650 5
adamc@650 6 NewState : transaction t_state.2,
adamc@650 7 Widget : t_state.2 -> xbody,
adamc@650 8 ReadState : t_state.2 -> transaction t_state.1}
adamc@650 9 con colsMeta = fn cols :: {(Type * Type)} => $(map colMeta cols)
adamc@650 10
adamc@650 11 fun default (t ::: Type) (sh : show t) (rd : read t) (inj : sql_injectable t)
adamc@650 12 name : colMeta (t, source string) =
adamc@650 13 {Nam = name,
adamc@650 14 Show = txt,
adamc@650 15 Inject = _,
adamc@650 16
adamc@650 17 NewState = source "",
adamc@650 18 Widget = fn s => <xml><ctextbox source={s}/></xml>,
adamc@650 19 ReadState = fn s => v <- get s; return (readError v)}
adamc@650 20
adamc@650 21 val int = default
adamc@650 22 val float = default
adamc@650 23 val string = default
adamc@650 24
adamc@650 25 functor Make(M : sig
adamc@650 26 con cols :: {(Type * Type)}
adamc@650 27 constraint [Id] ~ cols
adamc@650 28 val fl : folder cols
adamc@650 29
adamc@706 30 table tab : ([Id = int] ++ map fst cols)
adamc@650 31
adamc@650 32 val title : string
adamc@650 33
adamc@650 34 val cols : colsMeta cols
adamc@650 35 end) = struct
adamc@650 36
adamc@650 37 open constraints M
adamc@650 38 val t = M.tab
adamc@650 39
adamc@650 40 datatype list t = Nil | Cons of t * list t
adamc@650 41
adamc@650 42 fun allRows () =
adamc@650 43 query (SELECT * FROM t)
adamc@650 44 (fn r acc => return (Cons (r.T, acc)))
adamc@650 45 Nil
adamc@650 46
adamc@650 47 fun add r =
adamc@650 48 dml (insert t
adamc@650 49 (foldR2 [fst] [colMeta]
adamc@650 50 [fn cols => $(map (fn t :: (Type * Type) =>
adamc@650 51 sql_exp [] [] [] t.1) cols)]
adamc@650 52 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
adamc@650 53 [[nm] ~ rest] input col acc =>
adamc@650 54 acc ++ {nm = @sql_inject col.Inject input})
adamc@650 55 {} [M.cols] M.fl (r -- #Id) M.cols
adamc@650 56 ++ {Id = (SQL {[r.Id]})}))
adamc@650 57
adamc@650 58 fun doBatch ls =
adamc@650 59 case ls of
adamc@650 60 Nil => return ()
adamc@650 61 | Cons (r, ls') =>
adamc@650 62 add r;
adamc@650 63 doBatch ls'
adamc@650 64
adamc@650 65 fun del id =
adamc@650 66 dml (DELETE FROM t WHERE t.Id = {[id]})
adamc@650 67
adamc@650 68 fun show withDel lss =
adamc@650 69 let
adamc@650 70 fun show' ls =
adamc@650 71 case ls of
adamc@650 72 Nil => <xml/>
adamc@650 73 | Cons (r, ls) => <xml>
adamc@650 74 <tr>
adamc@650 75 <td>{[r.Id]}</td>
adamc@650 76 {foldRX2 [colMeta] [fst] [_]
adamc@650 77 (fn (nm :: Name) (p :: (Type * Type)) (rest :: {(Type * Type)})
adamc@650 78 [[nm] ~ rest] m v =>
adamc@650 79 <xml><td>{m.Show v}</td></xml>)
adamc@650 80 [M.cols] M.fl M.cols (r -- #Id)}
adamc@650 81 {if withDel then
adamc@650 82 <xml><td><button value="Delete" onclick={del r.Id}/></td></xml>
adamc@650 83 else
adamc@650 84 <xml/>}
adamc@650 85 </tr>
adamc@650 86 {show' ls}
adamc@650 87 </xml>
adamc@650 88 in
adamc@650 89 <xml><dyn signal={ls <- signal lss; return <xml><table>
adamc@650 90 <tr>
adamc@650 91 <th>Id</th>
adamc@650 92 {foldRX [colMeta] [_]
adamc@650 93 (fn (nm :: Name) (p :: (Type * Type)) (rest :: {(Type * Type)})
adamc@650 94 [[nm] ~ rest] m =>
adamc@650 95 <xml><th>{[m.Nam]}</th></xml>)
adamc@650 96 [M.cols] M.fl M.cols}
adamc@650 97 </tr>
adamc@650 98 {show' ls}
adamc@650 99 </table></xml>}/></xml>
adamc@650 100 end
adamc@650 101
adamc@650 102 fun main () =
adamc@650 103 lss <- source Nil;
adamc@650 104 batched <- source Nil;
adamc@650 105
adamc@650 106 id <- source "";
adamc@650 107 inps <- foldR [colMeta] [fn r => transaction ($(map snd r))]
adamc@650 108 (fn (nm :: Name) (p :: (Type * Type)) (rest :: {(Type * Type)}) [[nm] ~ rest] m acc =>
adamc@650 109 s <- m.NewState;
adamc@650 110 r <- acc;
adamc@650 111 return ({nm = s} ++ r))
adamc@650 112 (return {})
adamc@650 113 [M.cols] M.fl M.cols;
adamc@650 114
adamc@650 115 let
adamc@650 116 fun add () =
adamc@650 117 id <- get id;
adamc@650 118 vs <- foldR2 [colMeta] [snd] [fn r => transaction ($(map fst r))]
adamc@650 119 (fn (nm :: Name) (p :: (Type * Type)) (rest :: {(Type * Type)})
adamc@650 120 [[nm] ~ rest] m s acc =>
adamc@650 121 v <- m.ReadState s;
adamc@650 122 r <- acc;
adamc@650 123 return ({nm = v} ++ r))
adamc@650 124 (return {})
adamc@650 125 [M.cols] M.fl M.cols inps;
adamc@650 126 ls <- get batched;
adamc@650 127
adamc@650 128 set batched (Cons ({Id = readError id} ++ vs, ls))
adamc@650 129
adamc@650 130 fun exec () =
adamc@650 131 ls <- get batched;
adamc@650 132
adamc@650 133 doBatch ls;
adamc@650 134 set batched Nil
adamc@650 135 in
adamc@650 136 return <xml><body>
adamc@650 137 <h2>Rows</h2>
adamc@650 138
adamc@650 139 {show True lss}
adamc@650 140
adamc@650 141 <button value="Update" onclick={ls <- allRows (); set lss ls}/><br/>
adamc@650 142 <br/>
adamc@650 143
adamc@650 144 <h2>Batch new rows to add</h2>
adamc@650 145
adamc@650 146 <table>
adamc@650 147 <tr> <th>Id:</th> <td><ctextbox source={id}/></td> </tr>
adamc@650 148 {foldRX2 [colMeta] [snd] [_]
adamc@650 149 (fn (nm :: Name) (p :: (Type * Type)) (rest :: {(Type * Type)})
adamc@650 150 [[nm] ~ rest] m s =>
adamc@650 151 <xml><tr> <th>{[m.Nam]}:</th> <td>{m.Widget s}</td> </tr></xml>)
adamc@650 152 [M.cols] M.fl M.cols inps}
adamc@650 153 <tr> <th/> <td><button value="Batch it" onclick={add ()}/></td> </tr>
adamc@650 154 </table>
adamc@650 155
adamc@650 156 <h2>Already batched:</h2>
adamc@650 157 {show False batched}
adamc@650 158 <button value="Execute" onclick={exec ()}/>
adamc@650 159 </body></xml>
adamc@650 160 end
adamc@650 161
adamc@650 162 end