annotate demo/more/versioned.ur @ 993:10114d7b7477

SELECT DISTINCT; eta expansion during Cjrization
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Oct 2009 15:39:27 -0400
parents
children 166ea3944b91
rev   line source
adamc@993 1 functor Make(M : sig
adamc@993 2 con key :: {Type}
adamc@993 3 con data :: {Type}
adamc@993 4 constraint key ~ data
adamc@993 5 constraint [When] ~ (key ++ data)
adamc@993 6
adamc@993 7 val key : $(map sql_injectable key)
adamc@993 8 val data : $(map (fn t => {Inj : sql_injectable_prim t,
adamc@993 9 Eq : eq t}) data)
adamc@993 10
adamc@993 11 val keyFolder : folder key
adamc@993 12 val dataFolder : folder data
adamc@993 13 end) = struct
adamc@993 14 con all = [When = time] ++ M.key ++ map option M.data
adamc@993 15 table t : all
adamc@993 16
adamc@993 17 val keys = List.mapQuery (SELECT DISTINCT t.{{M.key}} FROM t) (fn r => r.T)
adamc@993 18
adamc@993 19 con dmeta = fn t => {Inj : sql_injectable_prim t,
adamc@993 20 Eq : eq t}
adamc@993 21
adamc@993 22 fun keyRecd (r : $(M.key ++ M.data)) =
adamc@993 23 map2 [sql_injectable] [id] [sql_exp [] [] []]
adamc@993 24 (fn [t] => @sql_inject)
adamc@993 25 [_] M.keyFolder M.key (r --- M.data)
adamc@993 26
adamc@993 27 fun insert r = dml (Basis.insert t
adamc@993 28 ({When = (SQL CURRENT_TIMESTAMP)}
adamc@993 29 ++ keyRecd r
adamc@993 30 ++ map2 [dmeta] [id]
adamc@993 31 [fn t => sql_exp [] [] [] (option t)]
adamc@993 32 (fn [t] x v => @sql_inject (@sql_option_prim x.Inj)
adamc@993 33 (Some v))
adamc@993 34 [_] M.dataFolder M.data (r --- M.key)))
adamc@993 35
adamc@993 36 fun keyExp (r : $M.key) : sql_exp [T = all] [] [] bool =
adamc@993 37 foldR2 [sql_injectable] [id] [fn before => after :: {Type} -> [before ~ after]
adamc@993 38 => sql_exp [T = before ++ after] [] [] bool]
adamc@993 39 (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before]
adamc@993 40 (inj : sql_injectable t) (v : t)
adamc@993 41 (e : after :: {Type} -> [before ~ after]
adamc@993 42 => sql_exp [T = before ++ after] [] [] bool)
adamc@993 43 [after :: {Type}] [[nm = t] ++ before ~ after] =>
adamc@993 44 (SQL t.{nm} = {[v]} AND {e [[nm = t] ++ after] !}))
adamc@993 45 (fn [after :: {Type}] [[] ~ after] => (SQL TRUE))
adamc@993 46 [_] M.keyFolder M.key r
adamc@993 47 [_] !
adamc@993 48
adamc@993 49 fun current k =
adamc@993 50 let
adamc@993 51 fun current' timeOpt r =
adamc@993 52 let
adamc@993 53 val complete = foldR [option] [fn ts => option $ts]
adamc@993 54 (fn [nm :: Name] [v :: Type] [r :: {Type}] [[nm] ~ r]
adamc@993 55 v r =>
adamc@993 56 case (v, r) of
adamc@993 57 (Some v, Some r) => Some ({nm = v} ++ r)
adamc@993 58 | _ => None)
adamc@993 59 (Some {}) [_] M.dataFolder r
adamc@993 60 in
adamc@993 61 case complete of
adamc@993 62 Some r => return (Some r)
adamc@993 63 | None =>
adamc@993 64 let
adamc@993 65 val filter = case timeOpt of
adamc@993 66 None => (WHERE TRUE)
adamc@993 67 | Some time => (WHERE t.When < {[time]})
adamc@993 68 in
adamc@993 69 ro <- oneOrNoRows (SELECT t.When, t.{{map option M.data}}
adamc@993 70 FROM t
adamc@993 71 WHERE {filter}
adamc@993 72 AND {keyExp k}
adamc@993 73 ORDER BY t.When DESC
adamc@993 74 LIMIT 1);
adamc@993 75 case ro of
adamc@993 76 None => return None
adamc@993 77 | Some r' =>
adamc@993 78 let
adamc@993 79 val r = map2 [option] [option] [option]
adamc@993 80 (fn [t ::: Type] old new =>
adamc@993 81 case old of
adamc@993 82 None => new
adamc@993 83 | Some _ => old)
adamc@993 84 [_] M.dataFolder r (r'.T -- #When)
adamc@993 85 in
adamc@993 86 current' (Some r'.T.When) r
adamc@993 87 end
adamc@993 88 end
adamc@993 89 end
adamc@993 90 in
adamc@993 91 current' None (map0 [option] (fn [t :: Type] => None : option t) [_] M.dataFolder)
adamc@993 92 end
adamc@993 93
adamc@993 94 fun update r =
adamc@993 95 cur <- current (r --- M.data);
adamc@993 96 case cur of
adamc@993 97 None => error <xml>Tried to update nonexistent key</xml>
adamc@993 98 | Some cur =>
adamc@993 99 let
adamc@993 100 val r' = map3 [dmeta] [id] [id] [fn t => sql_exp [] [] [] (option t)]
adamc@993 101 (fn [t] (meta : dmeta t) old new =>
adamc@993 102 @sql_inject (@sql_option_prim meta.Inj)
adamc@993 103 (if @@eq [_] meta.Eq old new then
adamc@993 104 None
adamc@993 105 else
adamc@993 106 Some new))
adamc@993 107 [_] M.dataFolder M.data cur (r --- M.key)
adamc@993 108 val r' = {When = (SQL CURRENT_TIMESTAMP)}
adamc@993 109 ++ keyRecd r
adamc@993 110 ++ r'
adamc@993 111 in
adamc@993 112 dml (Basis.insert t r')
adamc@993 113 end
adamc@993 114 end