Mercurial > urweb
comparison demo/more/versioned.ur @ 1093:8d3aa6c7cee0
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') |