Mercurial > urweb

comparison demo/more/versioned.ur @ 1093:8d3aa6c7cee0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Make summary unification more conservative; infer implicit arguments after applications
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Dec 2009 11:56:40 -0500
parents 166ea3944b91
children e2611b5dafce
comparison
equal deleted inserted replaced
1092:6f4b05fc4361 1093:8d3aa6c7cee0
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] [id] [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] [id]
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] [id] [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)
49 [after :: {Type}] [[nm = t] ++ before ~ after] => 49 [after :: {Type}] [[nm = t] ++ before ~ after] =>
50 (SQL t.{nm} = {[v]} AND {e [[nm = t] ++ after] !})) 50 (SQL t.{nm} = {[v]} AND {e [[nm = t] ++ after] !}))
51 (fn [after :: {Type}] [[] ~ after] => (SQL TRUE)) 51 (fn [after :: {Type}] [[] ~ after] => (SQL TRUE))
52 [_] M.keyFolder M.key r 52 M.keyFolder M.key r
53 [_] ! 53 [_] !
54 54
55 datatype bound = 55 datatype bound =
56 NoBound 56 NoBound
57 | Lt of int 57 | Lt of int
58 | Le of int 58 | Le of int
59 59
60 fun seek vro k = 60 fun seek vro k =
61 let 61 let
62 fun current' vro r = 62 fun current' vro r =
63 let 63 let
64 val complete = foldR [option] [fn ts => option $ts] 64 val complete = @foldR [option] [fn ts => option $ts]
65 (fn [nm :: Name] [v :: Type] [r :: {Type}] [[nm] ~ r] 65 (fn [nm :: Name] [v :: Type] [r :: {Type}] [[nm] ~ r]
66 v r => 66 v r =>
67 case (v, r) of 67 case (v, r) of
68 (Some v, Some r) => Some ({nm = v} ++ r) 68 (Some v, Some r) => Some ({nm = v} ++ r)
69 | _ => None) 69 | _ => None)
70 (Some {}) [_] M.dataFolder r 70 (Some {}) M.dataFolder r
71 in 71 in
72 case complete of 72 case complete of
73 Some r => return (Some r) 73 Some r => return (Some r)
74 | None => 74 | None =>
75 let 75 let
86 LIMIT 1); 86 LIMIT 1);
87 case ro of 87 case ro of
88 None => return None 88 None => return None
89 | Some r' => 89 | Some r' =>
90 let 90 let
91 val r = map2 [option] [option] [option] 91 val r = @map2 [option] [option] [option]
92 (fn [t ::: Type] old new => 92 (fn [t ::: Type] old new =>
93 case old of 93 case old of
94 None => new 94 None => new
95 | Some _ => old) 95 | Some _ => old)
96 [_] M.dataFolder r (r'.T -- #Version) 96 M.dataFolder r (r'.T -- #Version)
97 in 97 in
98 current' (Lt r'.T.Version) r 98 current' (Lt r'.T.Version) r
99 end 99 end
100 end 100 end
101 end 101 end
102 in 102 in
103 current' vro (map0 [option] (fn [t :: Type] => None : option t) [_] M.dataFolder) 103 current' vro (@map0 [option] (fn [t :: Type] => None : option t) M.dataFolder)
104 end 104 end
105 105
106 val current = seek NoBound 106 val current = seek NoBound
107 fun archive vr = seek (Le vr) 107 fun archive vr = seek (Le vr)
108 108
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] [id] [id] [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
122 Some new)) 122 Some new))
123 [_] M.dataFolder M.data cur (r --- M.key) 123 M.dataFolder M.data cur (r --- M.key)
124 val r' = {Version = (SQL {[vr]}), When = (SQL CURRENT_TIMESTAMP)} 124 val r' = {Version = (SQL {[vr]}), When = (SQL CURRENT_TIMESTAMP)}
125 ++ keyRecd r 125 ++ keyRecd r
126 ++ r' 126 ++ r'
127 in 127 in
128 dml (Basis.insert t r') 128 dml (Basis.insert t r')