Mercurial > urweb
comparison src/sqlcache.sml @ 2243:da7d026d1a94
Fix possible formula simplification bug with extra formula' type.
author | Ziv Scully <ziv@mit.edu> |
---|---|
date | Mon, 20 Jul 2015 19:49:13 -0700 |
parents | 88cc0f44c940 |
children | e4a7e3cd6f11 |
comparison
equal
deleted
inserted
replaced
2242:200a7ed4343b | 2243:da7d026d1a94 |
---|---|
143 datatype 'atom formula = | 143 datatype 'atom formula = |
144 Atom of 'atom | 144 Atom of 'atom |
145 | Negate of 'atom formula | 145 | Negate of 'atom formula |
146 | Combo of junctionType * 'atom formula list | 146 | Combo of junctionType * 'atom formula list |
147 | 147 |
148 (* Guaranteed to have all negation pushed to the atoms. *) | |
149 datatype 'atom formula' = | |
150 Atom' of 'atom | |
151 | Combo' of junctionType * 'atom formula' list | |
152 | |
148 val flipJt = fn Conj => Disj | Disj => Conj | 153 val flipJt = fn Conj => Disj | Disj => Conj |
149 | 154 |
150 fun concatMap f xs = List.concat (map f xs) | 155 fun concatMap f xs = List.concat (map f xs) |
151 | 156 |
152 val rec cartesianProduct : 'a list list -> 'a list list = | 157 val rec cartesianProduct : 'a list list -> 'a list list = |
154 | (xs :: xss) => concatMap (fn ys => concatMap (fn x => [x :: ys]) xs) | 159 | (xs :: xss) => concatMap (fn ys => concatMap (fn x => [x :: ys]) xs) |
155 (cartesianProduct xss) | 160 (cartesianProduct xss) |
156 | 161 |
157 (* Pushes all negation to the atoms.*) | 162 (* Pushes all negation to the atoms.*) |
158 fun pushNegate (negate : 'atom -> 'atom) (negating : bool) = | 163 fun pushNegate (negate : 'atom -> 'atom) (negating : bool) = |
159 fn Atom x => Atom (if negating then negate x else x) | 164 fn Atom x => Atom' (if negating then negate x else x) |
160 | Negate f => pushNegate negate (not negating) f | 165 | Negate f => pushNegate negate (not negating) f |
161 | Combo (n, fs) => Combo (if negating then flipJt n else n, map (pushNegate negate negating) fs) | 166 | Combo (j, fs) => Combo' (if negating then flipJt j else j, map (pushNegate negate negating) fs) |
162 | 167 |
163 val rec flatten = | 168 val rec flatten = |
164 fn Combo (_, [f]) => flatten f | 169 fn Combo' (_, [f]) => flatten f |
165 | Combo (j, fs) => | 170 | Combo' (j, fs) => |
166 Combo (j, List.foldr (fn (f, acc) => | 171 Combo' (j, List.foldr (fn (f, acc) => |
167 case f of | 172 case f of |
168 Combo (j', fs') => | 173 Combo' (j', fs') => |
169 if j = j' orelse length fs' = 1 | 174 if j = j' orelse length fs' = 1 |
170 then fs' @ acc | 175 then fs' @ acc |
171 else f :: acc | 176 else f :: acc |
172 | _ => f :: acc) | 177 | _ => f :: acc) |
173 [] | 178 [] |
174 (map flatten fs)) | 179 (map flatten fs)) |
175 | f => f | 180 | f => f |
176 | 181 |
182 (* [simplify] operates on the desired normal form. E.g., if [junc] is [Disj], | |
183 consider the list of lists to be a disjunction of conjunctions. *) | |
177 fun normalize' (simplify : 'a list list -> 'a list list) | 184 fun normalize' (simplify : 'a list list -> 'a list list) |
178 (negate : 'a -> 'a) | |
179 (junc : junctionType) = | 185 (junc : junctionType) = |
180 let | 186 let |
181 fun norm junc = | 187 fun norm junc = |
182 simplify | 188 simplify |
183 o (fn Atom x => [[x]] | 189 o (fn Atom' x => [[x]] |
184 | Negate f => map (map negate) (norm (flipJt junc) f) | 190 | Combo' (j, fs) => |
185 | Combo (j, fs) => | |
186 let | 191 let |
187 val fss = map (norm junc) fs | 192 val fss = map (norm junc) fs |
188 in | 193 in |
189 if j = junc | 194 if j = junc |
190 then List.concat fss | 195 then List.concat fss |
193 in | 198 in |
194 norm junc | 199 norm junc |
195 end | 200 end |
196 | 201 |
197 fun normalize simplify negate junc = | 202 fun normalize simplify negate junc = |
198 normalize' simplify negate junc | 203 normalize' simplify junc |
199 o flatten | 204 o flatten |
200 o pushNegate negate false | 205 o pushNegate negate false |
201 | 206 |
202 fun mapFormula mf = | 207 fun mapFormula mf = |
203 fn Atom x => Atom (mf x) | 208 fn Atom x => Atom (mf x) |
229 | (_, Sql.Gt) => GREATER | 234 | (_, Sql.Gt) => GREATER |
230 | (Sql.Ge, Sql.Ge) => EQUAL | 235 | (Sql.Ge, Sql.Ge) => EQUAL |
231 | 236 |
232 end | 237 end |
233 | 238 |
234 (* | |
235 functor ListKeyFn (K : ORD_KEY) : ORD_KEY = struct | |
236 | |
237 type ord_key = K.ord_key list | |
238 | |
239 val rec compare = | |
240 fn ([], []) => EQUAL | |
241 | ([], _) => LESS | |
242 | (_, []) => GREATER | |
243 | (x :: xs, y :: ys) => (case K.compare (x, y) of | |
244 EQUAL => compare (xs, ys) | |
245 | ord => ord) | |
246 | |
247 end | |
248 *) | |
249 | |
250 val rec chooseTwos : 'a list -> ('a * 'a) list = | 239 val rec chooseTwos : 'a list -> ('a * 'a) list = |
251 fn [] => [] | 240 fn [] => [] |
252 | x :: ys => map (fn y => (x, y)) ys @ chooseTwos ys | 241 | x :: ys => map (fn y => (x, y)) ys @ chooseTwos ys |
253 | 242 |
254 fun removeRedundant madeRedundantBy zs = | 243 fun removeRedundant madeRedundantBy zs = |
298 | 287 |
299 structure TK = TripleKeyFn(structure I = CmpKey | 288 structure TK = TripleKeyFn(structure I = CmpKey |
300 structure J = OptionKeyFn(AtomExpKey) | 289 structure J = OptionKeyFn(AtomExpKey) |
301 structure K = OptionKeyFn(AtomExpKey)) | 290 structure K = OptionKeyFn(AtomExpKey)) |
302 structure TS = BinarySetFn(TK) | 291 structure TS = BinarySetFn(TK) |
303 (* structure TLS = BinarySetFn(ListKeyFn(TK)) *) | |
304 | 292 |
305 val toKnownEquality = | 293 val toKnownEquality = |
306 (* [NONE] here means unkown. Anything that isn't a comparison between two | 294 (* [NONE] here means unkown. Anything that isn't a comparison between two |
307 knowns shouldn't be used, and simply dropping unused terms is okay in | 295 knowns shouldn't be used, and simply dropping unused terms is okay in |
308 disjunctive normal form. *) | 296 disjunctive normal form. *) |