comparison demo/more/versioned.ur @ 1649:9253765d7724

Rename [Top.id] to avoid clash with [Basis.id]
author Adam Chlipala <adam@chlipala.net>
date Thu, 29 Dec 2011 14:12:03 -0500
parents e2611b5dafce
children 6bc2a8cb3a67
comparison
equal deleted inserted replaced
1648:bd7edca0aec1 1649:9253765d7724
22 22
23 con dmeta = fn t => {Inj : sql_injectable_prim t, 23 con dmeta = fn t => {Inj : sql_injectable_prim t,
24 Eq : eq t} 24 Eq : eq t}
25 25
26 fun keyRecd (r : $(M.key ++ M.data)) = 26 fun keyRecd (r : $(M.key ++ M.data)) =
27 @map2 [sql_injectable] [id] [sql_exp [] [] []] 27 @map2 [sql_injectable] [ident] [sql_exp [] [] []]
28 (fn [t] => @sql_inject) 28 (fn [t] => @sql_inject)
29 M.keyFolder M.key (r --- M.data) 29 M.keyFolder M.key (r --- M.data)
30 30
31 fun insert r = 31 fun insert r =
32 vr <- nextval s; 32 vr <- nextval s;
33 dml (Basis.insert t 33 dml (Basis.insert t
34 ({Version = (SQL {[vr]}), When = (SQL CURRENT_TIMESTAMP)} 34 ({Version = (SQL {[vr]}), When = (SQL CURRENT_TIMESTAMP)}
35 ++ keyRecd r 35 ++ keyRecd r
36 ++ @map2 [dmeta] [id] 36 ++ @map2 [dmeta] [ident]
37 [fn t => sql_exp [] [] [] (option t)] 37 [fn t => sql_exp [] [] [] (option t)]
38 (fn [t] x v => @sql_inject (@sql_option_prim x.Inj) 38 (fn [t] x v => @sql_inject (@sql_option_prim x.Inj)
39 (Some v)) 39 (Some v))
40 M.dataFolder M.data (r --- M.key))) 40 M.dataFolder M.data (r --- M.key)))
41 41
42 fun keyExp (r : $M.key) : sql_exp [T = all] [] [] bool = 42 fun keyExp (r : $M.key) : sql_exp [T = all] [] [] bool =
43 @foldR2 [sql_injectable] [id] [fn before => after :: {Type} -> [before ~ after] 43 @foldR2 [sql_injectable] [ident] [fn before => after :: {Type} -> [before ~ after]
44 => sql_exp [T = before ++ after] [] [] bool] 44 => sql_exp [T = before ++ after] [] [] bool]
45 (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before] 45 (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before]
46 (inj : sql_injectable t) (v : t) 46 (inj : sql_injectable t) (v : t)
47 (e : after :: {Type} -> [before ~ after] 47 (e : after :: {Type} -> [before ~ after]
48 => sql_exp [T = before ++ after] [] [] bool) 48 => sql_exp [T = before ++ after] [] [] bool)
111 case cur of 111 case cur of
112 None => error <xml>Tried to update nonexistent key</xml> 112 None => error <xml>Tried to update nonexistent key</xml>
113 | Some cur => 113 | Some cur =>
114 vr <- nextval s; 114 vr <- nextval s;
115 let 115 let
116 val r' = @map3 [dmeta] [id] [id] [fn t => sql_exp [] [] [] (option t)] 116 val r' = @map3 [dmeta] [ident] [ident] [fn t => sql_exp [] [] [] (option t)]
117 (fn [t] (meta : dmeta t) old new => 117 (fn [t] (meta : dmeta t) old new =>
118 @sql_inject (@sql_option_prim meta.Inj) 118 @sql_inject (@sql_option_prim meta.Inj)
119 (if @@eq [_] meta.Eq old new then 119 (if @@eq [_] meta.Eq old new then
120 None 120 None
121 else 121 else