From 3a94a798557f71cba0fdfdb54cdf431c44a4ef1d Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 10 Mar 2009 16:38:38 -0400 Subject: BatchG demo --- demo/batchFun.ur | 162 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ demo/batchFun.urs | 27 +++++++++ demo/batchG.ur | 8 +++ demo/batchG.urp | 5 ++ demo/batchG.urs | 1 + demo/prose | 17 ++++++ 6 files changed, 220 insertions(+) create mode 100644 demo/batchFun.ur create mode 100644 demo/batchFun.urs create mode 100644 demo/batchG.ur create mode 100644 demo/batchG.urp create mode 100644 demo/batchG.urs (limited to 'demo') diff --git a/demo/batchFun.ur b/demo/batchFun.ur new file mode 100644 index 00000000..2eed464b --- /dev/null +++ b/demo/batchFun.ur @@ -0,0 +1,162 @@ +con colMeta = fn t_state :: (Type * Type) => + {Nam : string, + Show : t_state.1 -> xbody, + Inject : sql_injectable t_state.1, + + NewState : transaction t_state.2, + Widget : t_state.2 -> xbody, + ReadState : t_state.2 -> transaction t_state.1} +con colsMeta = fn cols :: {(Type * Type)} => $(map colMeta cols) + +fun default (t ::: Type) (sh : show t) (rd : read t) (inj : sql_injectable t) + name : colMeta (t, source string) = + {Nam = name, + Show = txt, + Inject = _, + + NewState = source "", + Widget = fn s => , + ReadState = fn s => v <- get s; return (readError v)} + +val int = default +val float = default +val string = default + +functor Make(M : sig + con cols :: {(Type * Type)} + constraint [Id] ~ cols + val fl : folder cols + + val tab : sql_table ([Id = int] ++ map fst cols) + + val title : string + + val cols : colsMeta cols + end) = struct + + open constraints M + val t = M.tab + + datatype list t = Nil | Cons of t * list t + + fun allRows () = + query (SELECT * FROM t) + (fn r acc => return (Cons (r.T, acc))) + Nil + + fun add r = + dml (insert t + (foldR2 [fst] [colMeta] + [fn cols => $(map (fn t :: (Type * Type) => + sql_exp [] [] [] t.1) cols)] + (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) + [[nm] ~ rest] input col acc => + acc ++ {nm = @sql_inject col.Inject input}) + {} [M.cols] M.fl (r -- #Id) M.cols + ++ {Id = (SQL {[r.Id]})})) + + fun doBatch ls = + case ls of + Nil => return () + | Cons (r, ls') => + add r; + doBatch ls' + + fun del id = + dml (DELETE FROM t WHERE t.Id = {[id]}) + + fun show withDel lss = + let + fun show' ls = + case ls of + Nil => + | Cons (r, ls) => + + {[r.Id]} + {foldRX2 [colMeta] [fst] [_] + (fn (nm :: Name) (p :: (Type * Type)) (rest :: {(Type * Type)}) + [[nm] ~ rest] m v => + {m.Show v}) + [M.cols] M.fl M.cols (r -- #Id)} + {if withDel then +