Mercurial > urweb
comparison src/sqlcache.sml @ 2244:e4a7e3cd6f11
Use uniform representation of comparisons for better simplification.
author | Ziv Scully <ziv@mit.edu> |
---|---|
date | Mon, 20 Jul 2015 23:25:44 -0700 |
parents | da7d026d1a94 |
children | e09c3dc102ef |
comparison
equal
deleted
inserted
replaced
2243:da7d026d1a94 | 2244:e4a7e3cd6f11 |
---|---|
158 fn [] => [[]] | 158 fn [] => [[]] |
159 | (xs :: xss) => concatMap (fn ys => concatMap (fn x => [x :: ys]) xs) | 159 | (xs :: xss) => concatMap (fn ys => concatMap (fn x => [x :: ys]) xs) |
160 (cartesianProduct xss) | 160 (cartesianProduct xss) |
161 | 161 |
162 (* Pushes all negation to the atoms.*) | 162 (* Pushes all negation to the atoms.*) |
163 fun pushNegate (negate : 'atom -> 'atom) (negating : bool) = | 163 fun pushNegate (normalizeAtom : bool * 'atom -> 'atom) (negating : bool) = |
164 fn Atom x => Atom' (if negating then negate x else x) | 164 fn Atom x => Atom' (normalizeAtom (negating, x)) |
165 | Negate f => pushNegate negate (not negating) f | 165 | Negate f => pushNegate normalizeAtom (not negating) f |
166 | Combo (j, fs) => Combo' (if negating then flipJt j else j, map (pushNegate negate negating) fs) | 166 | Combo (j, fs) => Combo' (if negating then flipJt j else j, |
167 map (pushNegate normalizeAtom negating) fs) | |
167 | 168 |
168 val rec flatten = | 169 val rec flatten = |
169 fn Combo' (_, [f]) => flatten f | 170 fn Combo' (_, [f]) => flatten f |
170 | Combo' (j, fs) => | 171 | Combo' (j, fs) => |
171 Combo' (j, List.foldr (fn (f, acc) => | 172 Combo' (j, List.foldr (fn (f, acc) => |
197 end) | 198 end) |
198 in | 199 in |
199 norm junc | 200 norm junc |
200 end | 201 end |
201 | 202 |
202 fun normalize simplify negate junc = | 203 fun normalize simplify normalizeAtom junc = |
203 normalize' simplify junc | 204 normalize' simplify junc |
204 o flatten | 205 o flatten |
205 o pushNegate negate false | 206 o pushNegate normalizeAtom false |
206 | 207 |
207 fun mapFormula mf = | 208 fun mapFormula mf = |
208 fn Atom x => Atom (mf x) | 209 fn Atom x => Atom (mf x) |
209 | Negate f => Negate (mapFormula mf f) | 210 | Negate f => Negate (mapFormula mf f) |
210 | Combo (j, fs) => Combo (j, map (mapFormula mf) fs) | 211 | Combo (j, fs) => Combo (j, map (mapFormula mf) fs) |
279 EQUAL => String.compare (f1, f2) | 280 EQUAL => String.compare (f1, f2) |
280 | ord => ord | 281 | ord => ord |
281 | 282 |
282 end | 283 end |
283 | 284 |
285 structure AtomOptionKey = OptionKeyFn(AtomExpKey) | |
286 | |
284 structure UF = UnionFindFn(AtomExpKey) | 287 structure UF = UnionFindFn(AtomExpKey) |
285 | 288 |
286 structure ConflictMaps = struct | 289 structure ConflictMaps = struct |
287 | 290 |
288 structure TK = TripleKeyFn(structure I = CmpKey | 291 structure TK = TripleKeyFn(structure I = CmpKey |
289 structure J = OptionKeyFn(AtomExpKey) | 292 structure J = AtomOptionKey |
290 structure K = OptionKeyFn(AtomExpKey)) | 293 structure K = AtomOptionKey) |
291 structure TS = BinarySetFn(TK) | 294 structure TS : ORD_SET = BinarySetFn(TK) |
292 | 295 |
293 val toKnownEquality = | 296 val toKnownEquality = |
294 (* [NONE] here means unkown. Anything that isn't a comparison between two | 297 (* [NONE] here means unkown. Anything that isn't a comparison between two |
295 knowns shouldn't be used, and simply dropping unused terms is okay in | 298 knowns shouldn't be used, and simply dropping unused terms is okay in |
296 disjunctive normal form. *) | 299 disjunctive normal form. *) |
343 | _ => NONE | 346 | _ => NONE |
344 in | 347 in |
345 (cmp, qa e1, qa e2) | 348 (cmp, qa e1, qa e2) |
346 end | 349 end |
347 | 350 |
348 fun negateCmp (cmp, e1, e2) = | 351 val negateCmp = |
349 (case cmp of | 352 fn Sql.Eq => Sql.Ne |
350 Sql.Eq => Sql.Ne | 353 | Sql.Ne => Sql.Eq |
351 | Sql.Ne => Sql.Eq | 354 | Sql.Lt => Sql.Ge |
352 | Sql.Lt => Sql.Ge | 355 | Sql.Le => Sql.Gt |
353 | Sql.Le => Sql.Gt | 356 | Sql.Gt => Sql.Le |
354 | Sql.Gt => Sql.Le | 357 | Sql.Ge => Sql.Lt |
355 | Sql.Ge => Sql.Lt, | 358 |
356 e1, e2) | 359 fun normalizeAtom (negating, (cmp, e1, e2)) = |
360 (* Restricting to Le/Lt and sorting the expressions in Eq/Ne helps with | |
361 simplification, where we put the triples in sets. *) | |
362 case (if negating then negateCmp cmp else cmp) of | |
363 Sql.Eq => (case AtomOptionKey.compare (e1, e2) of | |
364 LESS => (Sql.Eq, e2, e1) | |
365 | _ => (Sql.Eq, e1, e2)) | |
366 | Sql.Ne => (case AtomOptionKey.compare (e1, e2) of | |
367 LESS => (Sql.Ne, e2, e1) | |
368 | _ => (Sql.Ne, e1, e2)) | |
369 | Sql.Lt => (Sql.Lt, e1, e2) | |
370 | Sql.Le => (Sql.Le, e1, e2) | |
371 | Sql.Gt => (Sql.Lt, e2, e1) | |
372 | Sql.Ge => (Sql.Le, e2, e1) | |
357 | 373 |
358 val markQuery : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula -> | 374 val markQuery : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula -> |
359 (Sql.cmp * atomExp option * atomExp option) formula = | 375 (Sql.cmp * atomExp option * atomExp option) formula = |
360 mapFormula (toAtomExps QueryArg) | 376 mapFormula (toAtomExps QueryArg) |
361 | 377 |
374 map TS.listItems | 390 map TS.listItems |
375 o removeRedundant (fn (x, y) => TS.isSubset (y, x)) | 391 o removeRedundant (fn (x, y) => TS.isSubset (y, x)) |
376 o map (fn xs => TS.addList (TS.empty, xs)) | 392 o map (fn xs => TS.addList (TS.empty, xs)) |
377 | 393 |
378 fun dnf (fQuery, fDml) = | 394 fun dnf (fQuery, fDml) = |
379 normalize simplify negateCmp Disj (Combo (Conj, [markQuery fQuery, markDml fDml])) | 395 normalize simplify normalizeAtom Disj (Combo (Conj, [markQuery fQuery, markDml fDml])) |
380 | 396 |
381 val conflictMaps = List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf | 397 val conflictMaps = List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf |
382 | 398 |
383 end | 399 end |
384 | 400 |
433 | e => e | 449 | e => e |
434 val mark = mapFormula (fn (cmp, e1, e2) => (cmp, markField e1, markField e2)) | 450 val mark = mapFormula (fn (cmp, e1, e2) => (cmp, markField e1, markField e2)) |
435 in | 451 in |
436 renameTables [(table, "T")] | 452 renameTables [(table, "T")] |
437 (Combo (Disj, [Combo (Conj, [fVals, mark fWhere]), | 453 (Combo (Disj, [Combo (Conj, [fVals, mark fWhere]), |
438 Combo (Conj, [mark fVals, fWhere])])) | 454 Combo (Conj, [mark fVals, fWhere])])) |
439 end | 455 end |
440 | 456 |
441 val rec tablesQuery = | 457 val rec tablesQuery = |
442 fn Sql.Query1 {From = tablePairs, ...} => SS.fromList (map #1 tablePairs) | 458 fn Sql.Query1 {From = tablePairs, ...} => SS.fromList (map #1 tablePairs) |
443 | Sql.Union (q1, q2) => SS.union (tablesQuery q1, tablesQuery q2) | 459 | Sql.Union (q1, q2) => SS.union (tablesQuery q1, tablesQuery q2) |