Mercurial > urweb
comparison src/sqlcache.sml @ 2235:0aae15c2a05a
Refactored a lot and fixed an and/or swap, but still not good on current test.
author | Ziv Scully <ziv@mit.edu> |
---|---|
date | Mon, 29 Jun 2015 01:33:47 -0700 |
parents | 2f7ed04332a0 |
children | fab8c1f131a5 |
comparison
equal
deleted
inserted
replaced
2234:2f7ed04332a0 | 2235:0aae15c2a05a |
---|---|
1 structure Sqlcache :> SQLCACHE = struct | 1 structure Sqlcache (* DEBUG: add back :> SQLCACHE. *) = struct |
2 | 2 |
3 open Mono | 3 open Mono |
4 | 4 |
5 structure IS = IntBinarySet | 5 structure IS = IntBinarySet |
6 structure IM = IntBinaryMap | 6 structure IM = IntBinaryMap |
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 val flipJt = fn Conj => Disj | Disj => Conj | 148 val flipJt = fn Conj => Disj | Disj => Conj |
149 | 149 |
150 fun bind xs f = List.concat (map f xs) | 150 fun listBind xs f = List.concat (map f xs) |
151 | 151 |
152 val rec cartesianProduct : 'a list list -> 'a list list = | 152 val rec cartesianProduct : 'a list list -> 'a list list = |
153 fn [] => [[]] | 153 fn [] => [[]] |
154 | (xs :: xss) => bind (cartesianProduct xss) | 154 | (xs :: xss) => listBind (cartesianProduct xss) |
155 (fn ys => bind xs (fn x => [x :: ys])) | 155 (fn ys => listBind xs (fn x => [x :: ys])) |
156 | 156 |
157 (* Pushes all negation to the atoms.*) | 157 (* Pushes all negation to the atoms.*) |
158 fun pushNegate (negate : 'atom -> 'atom) (negating : bool) = | 158 fun pushNegate (negate : 'atom -> 'atom) (negating : bool) = |
159 fn Atom x => Atom (if negating then negate x else x) | 159 fn Atom x => Atom (if negating then negate x else x) |
160 | Negate f => pushNegate negate (not negating) f | 160 | Negate f => pushNegate negate (not negating) f |
161 | Combo (n, fs) => Combo (if negating then flipJt n else n, map (pushNegate negate negating) fs) | 161 | Combo (n, fs) => Combo (if negating then flipJt n else n, map (pushNegate negate negating) fs) |
162 | 162 |
163 val rec flatten = | 163 val rec flatten = |
164 fn Combo (n, fs) => | 164 fn Combo (_, [f]) => flatten f |
165 Combo (n, List.foldr (fn (f, acc) => | 165 | Combo (j, fs) => |
166 Combo (j, List.foldr (fn (f, acc) => | |
166 case f of | 167 case f of |
167 Combo (n', fs') => if n = n' then fs' @ acc else f :: acc | 168 Combo (j', fs') => |
169 if j = j' orelse length fs' = 1 | |
170 then fs' @ acc | |
171 else f :: acc | |
168 | _ => f :: acc) | 172 | _ => f :: acc) |
169 [] | 173 [] |
170 (map flatten fs)) | 174 (map flatten fs)) |
171 | f => f | 175 | f => f |
172 | 176 |
173 fun normalize' (negate : 'atom -> 'atom) (junc : junctionType) = | 177 fun normalize' ((simplifyLists, simplifyAtomsConj, simplifyAtomsDisj, negate) |
174 fn Atom x => [[x]] | 178 : ('a list list -> 'a list list) |
175 | Negate f => map (map negate) (normalize' negate (flipJt junc) f) | 179 * ('a list -> 'a list) |
176 | Combo (j, fs) => | 180 * ('a list -> 'a list) |
177 let | 181 * ('a -> 'a)) |
178 val fss = bind fs (normalize' negate j) | 182 (junc : junctionType) = |
179 in | 183 let |
180 if j = junc then fss else cartesianProduct fss | 184 fun simplify junc = simplifyLists o map (case junc of |
181 end | 185 Conj => simplifyAtomsConj |
182 | 186 | Disj => simplifyAtomsDisj) |
183 fun normalize negate junc = normalize' negate junc o flatten o pushNegate negate false | 187 fun norm junc = |
188 simplify junc | |
189 o (fn Atom x => [[x]] | |
190 | Negate f => map (map negate) (norm (flipJt junc) f) | |
191 | Combo (j, fs) => | |
192 let | |
193 val fss = listBind fs (norm j) | |
194 in | |
195 if j = junc then fss else cartesianProduct fss | |
196 end) | |
197 in | |
198 norm junc | |
199 end | |
200 | |
201 fun normalize (simplifyLists, simplifyAtomsConj, simplifyAtomsDisj, negate, junc) = | |
202 (normalize' (simplifyLists, simplifyAtomsConj, simplifyAtomsDisj, negate) junc) | |
203 o flatten | |
204 o pushNegate negate false | |
184 | 205 |
185 fun mapFormula mf = | 206 fun mapFormula mf = |
186 fn Atom x => Atom (mf x) | 207 fn Atom x => Atom (mf x) |
187 | Negate f => Negate (mapFormula mf f) | 208 | Negate f => Negate (mapFormula mf f) |
188 | Combo (n, fs) => Combo (n, map (mapFormula mf) fs) | 209 | Combo (j, fs) => Combo (j, map (mapFormula mf) fs) |
189 | 210 |
190 | 211 |
191 (* SQL analysis. *) | 212 (* SQL analysis. *) |
213 | |
214 structure CmpKey : ORD_KEY = struct | |
215 | |
216 type ord_key = Sql.cmp | |
217 | |
218 val compare = | |
219 fn (Sql.Eq, Sql.Eq) => EQUAL | |
220 | (Sql.Eq, _) => LESS | |
221 | (_, Sql.Eq) => GREATER | |
222 | (Sql.Ne, Sql.Ne) => EQUAL | |
223 | (Sql.Ne, _) => LESS | |
224 | (_, Sql.Ne) => GREATER | |
225 | (Sql.Lt, Sql.Lt) => EQUAL | |
226 | (Sql.Lt, _) => LESS | |
227 | (_, Sql.Lt) => GREATER | |
228 | (Sql.Le, Sql.Le) => EQUAL | |
229 | (Sql.Le, _) => LESS | |
230 | (_, Sql.Le) => GREATER | |
231 | (Sql.Gt, Sql.Gt) => EQUAL | |
232 | (Sql.Gt, _) => LESS | |
233 | (_, Sql.Gt) => GREATER | |
234 | (Sql.Ge, Sql.Ge) => EQUAL | |
235 | |
236 end | |
237 | |
238 | |
239 functor ListKeyFn (K : ORD_KEY) : ORD_KEY = struct | |
240 | |
241 type ord_key = K.ord_key list | |
242 | |
243 val rec compare = | |
244 fn ([], []) => EQUAL | |
245 | ([], _) => LESS | |
246 | (_, []) => GREATER | |
247 | (x :: xs, y :: ys) => (case K.compare (x, y) of | |
248 EQUAL => compare (xs, ys) | |
249 | ord => ord) | |
250 | |
251 end | |
252 | |
253 functor OptionKeyFn (K : ORD_KEY) : ORD_KEY = struct | |
254 | |
255 type ord_key = K.ord_key option | |
256 | |
257 val compare = | |
258 fn (NONE, NONE) => EQUAL | |
259 | (NONE, _) => LESS | |
260 | (_, NONE) => GREATER | |
261 | (SOME x, SOME y) => K.compare (x, y) | |
262 | |
263 end | |
264 | |
265 functor TripleKeyFn (structure I : ORD_KEY | |
266 structure J : ORD_KEY | |
267 structure K : ORD_KEY) | |
268 : ORD_KEY where type ord_key = I.ord_key * J.ord_key * K.ord_key = struct | |
269 | |
270 type ord_key = I.ord_key * J.ord_key * K.ord_key | |
271 | |
272 fun compare ((i1, j1, k1), (i2, j2, k2)) = | |
273 case I.compare (i1, i2) of | |
274 EQUAL => (case J.compare (j1, j2) of | |
275 EQUAL => K.compare (k1, k2) | |
276 | ord => ord) | |
277 | ord => ord | |
278 | |
279 end | |
192 | 280 |
193 val rec chooseTwos : 'a list -> ('a * 'a) list = | 281 val rec chooseTwos : 'a list -> ('a * 'a) list = |
194 fn [] => [] | 282 fn [] => [] |
195 | x :: ys => map (fn y => (x, y)) ys @ chooseTwos ys | 283 | x :: ys => map (fn y => (x, y)) ys @ chooseTwos ys |
196 | 284 |
221 | 309 |
222 end | 310 end |
223 | 311 |
224 structure UF = UnionFindFn(AtomExpKey) | 312 structure UF = UnionFindFn(AtomExpKey) |
225 | 313 |
226 val conflictMaps : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula | 314 structure ConflictMaps = struct |
227 * (Sql.cmp * Sql.sqexp * Sql.sqexp) formula | 315 |
228 -> atomExp IM.map list = | 316 structure TK = TripleKeyFn(structure I = CmpKey |
229 let | 317 structure J = OptionKeyFn(AtomExpKey) |
230 val toKnownEquality = | 318 structure K = OptionKeyFn(AtomExpKey)) |
231 (* [NONE] here means unkown. Anything that isn't a comparison between | 319 structure TS = BinarySetFn(TK) |
232 two knowns shouldn't be used, and simply dropping unused terms is | 320 structure TLS = BinarySetFn(ListKeyFn(TK)) |
233 okay in disjunctive normal form. *) | 321 |
234 fn (Sql.Eq, SOME e1, SOME e2) => SOME (e1, e2) | 322 val toKnownEquality = |
235 | _ => NONE | 323 (* [NONE] here means unkown. Anything that isn't a comparison between two |
236 val equivClasses : (Sql.cmp * atomExp option * atomExp option) list -> atomExp list list = | 324 knowns shouldn't be used, and simply dropping unused terms is okay in |
237 UF.classes | 325 disjunctive normal form. *) |
238 o List.foldl UF.union' UF.empty | 326 fn (Sql.Eq, SOME e1, SOME e2) => SOME (e1, e2) |
239 o List.mapPartial toKnownEquality | 327 | _ => NONE |
240 fun addToEqs (eqs, n, e) = | 328 |
241 case IM.find (eqs, n) of | 329 val equivClasses : (Sql.cmp * atomExp option * atomExp option) list -> atomExp list list = |
242 (* Comparing to a constant is probably better than comparing to | 330 UF.classes |
243 a variable? Checking that an existing constant matches a new | 331 o List.foldl UF.union' UF.empty |
244 one is handled by [accumulateEqs]. *) | 332 o List.mapPartial toKnownEquality |
245 SOME (Prim _) => eqs | 333 |
246 | _ => IM.insert (eqs, n, e) | 334 fun addToEqs (eqs, n, e) = |
247 val accumulateEqs = | 335 case IM.find (eqs, n) of |
248 (* [NONE] means we have a contradiction. *) | 336 (* Comparing to a constant is probably better than comparing to a |
249 fn (_, NONE) => NONE | 337 variable? Checking that existing constants match a new ones is |
250 | ((Prim p1, Prim p2), eqso) => | 338 handled by [accumulateEqs]. *) |
251 (case Prim.compare (p1, p2) of | 339 SOME (Prim _) => eqs |
252 EQUAL => eqso | 340 | _ => IM.insert (eqs, n, e) |
253 | _ => NONE) | 341 |
254 | ((QueryArg n, Prim p), SOME eqs) => SOME (addToEqs (eqs, n, Prim p)) | 342 val accumulateEqs = |
255 | ((QueryArg n, DmlRel r), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r)) | 343 (* [NONE] means we have a contradiction. *) |
256 | ((Prim p, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, Prim p)) | 344 fn (_, NONE) => NONE |
257 | ((DmlRel r, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r)) | 345 | ((Prim p1, Prim p2), eqso) => |
258 (* TODO: deal with equalities involving just [DmlRel]s and [Prim]s. | 346 (case Prim.compare (p1, p2) of |
259 This would involve guarding the invalidation with a check for the | 347 EQUAL => eqso |
260 relevant comparisons. *) | 348 | _ => NONE) |
261 (* DEBUG: remove these print statements. *) | 349 | ((QueryArg n, Prim p), SOME eqs) => SOME (addToEqs (eqs, n, Prim p)) |
262 (* | ((DmlRel r, Prim p), eqso) => (print ("sadness " ^ Int.toString r ^ " = " ^ Prim.toString p ^ "\n"); eqso) *) | 350 | ((QueryArg n, DmlRel r), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r)) |
263 (* | ((Prim p, DmlRel r), eqso) => (print ("sadness " ^ Int.toString r ^ " = " ^ Prim.toString p ^ "\n"); eqso) *) | 351 | ((Prim p, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, Prim p)) |
264 | (_, eqso) => eqso | 352 | ((DmlRel r, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r)) |
265 val eqsOfClass : atomExp list -> atomExp IM.map option = | 353 (* TODO: deal with equalities between [DmlRel]s and [Prim]s. |
266 List.foldl accumulateEqs (SOME IM.empty) | 354 This would involve guarding the invalidation with a check for the |
267 o chooseTwos | 355 relevant comparisons. *) |
268 fun toAtomExps rel (cmp, e1, e2) = | 356 (* DEBUG: remove these print statements. *) |
269 let | 357 (* | ((DmlRel r, Prim p), eqso) => (print ("sadness " ^ Int.toString r ^ " = " ^ Prim.toString p ^ "\n"); eqso) *) |
270 val qa = | 358 (* | ((Prim p, DmlRel r), eqso) => (print ("sadness " ^ Int.toString r ^ " = " ^ Prim.toString p ^ "\n"); eqso) *) |
271 (* Here [NONE] means unkown. *) | 359 | (_, eqso) => eqso |
272 fn Sql.SqConst p => SOME (Prim p) | 360 |
273 | Sql.Field tf => SOME (Field tf) | 361 val eqsOfClass : atomExp list -> atomExp IM.map option = |
274 | Sql.Inj (EPrim p, _) => SOME (Prim p) | 362 List.foldl accumulateEqs (SOME IM.empty) |
275 | Sql.Inj (ERel n, _) => SOME (rel n) | 363 o chooseTwos |
276 (* We can't deal with anything else, e.g., CURRENT_TIMESTAMP | 364 |
277 becomes Sql.Unmodeled, which becomes NONE here. *) | 365 fun toAtomExps rel (cmp, e1, e2) = |
278 | _ => NONE | 366 let |
279 in | 367 val qa = |
280 (cmp, qa e1, qa e2) | 368 (* Here [NONE] means unkown. *) |
281 end | 369 fn Sql.SqConst p => SOME (Prim p) |
282 fun negateCmp (cmp, e1, e2) = | 370 | Sql.Field tf => SOME (Field tf) |
283 (case cmp of | 371 | Sql.Inj (EPrim p, _) => SOME (Prim p) |
284 Sql.Eq => Sql.Ne | 372 | Sql.Inj (ERel n, _) => SOME (rel n) |
285 | Sql.Ne => Sql.Eq | 373 (* We can't deal with anything else, e.g., CURRENT_TIMESTAMP |
286 | Sql.Lt => Sql.Ge | 374 becomes Sql.Unmodeled, which becomes NONE here. *) |
287 | Sql.Le => Sql.Gt | 375 | _ => NONE |
288 | Sql.Gt => Sql.Le | 376 in |
289 | Sql.Ge => Sql.Lt, | 377 (cmp, qa e1, qa e2) |
290 e1, e2) | 378 end |
291 val markQuery : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula -> | 379 |
292 (Sql.cmp * atomExp option * atomExp option) formula = | 380 fun negateCmp (cmp, e1, e2) = |
293 mapFormula (toAtomExps QueryArg) | 381 (case cmp of |
294 val markDml : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula -> | 382 Sql.Eq => Sql.Ne |
295 (Sql.cmp * atomExp option * atomExp option) formula = | 383 | Sql.Ne => Sql.Eq |
296 mapFormula (toAtomExps DmlRel) | 384 | Sql.Lt => Sql.Ge |
297 (* No eqs should have key conflicts because no variable is in two | 385 | Sql.Le => Sql.Gt |
298 equivalence classes, so the [#1] can be anything. *) | 386 | Sql.Gt => Sql.Le |
299 val mergeEqs : (atomExp IntBinaryMap.map option list | 387 | Sql.Ge => Sql.Lt, |
300 -> atomExp IntBinaryMap.map option) = | 388 e1, e2) |
301 List.foldr (fn (SOME eqs, SOME acc) => SOME (IM.unionWith #1 (eqs, acc)) | _ => NONE) | 389 |
302 (SOME IM.empty) | 390 val markQuery : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula -> |
303 fun dnf (fQuery, fDml) = | 391 (Sql.cmp * atomExp option * atomExp option) formula = |
304 normalize negateCmp Disj (Combo (Conj, [markQuery fQuery, markDml fDml])) | 392 mapFormula (toAtomExps QueryArg) |
305 in | 393 |
306 List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf | 394 val markDml : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula -> |
307 end | 395 (Sql.cmp * atomExp option * atomExp option) formula = |
396 mapFormula (toAtomExps DmlRel) | |
397 (* No eqs should have key conflicts because no variable is in two | |
398 equivalence classes, so the [#1] could be [#2]. *) | |
399 | |
400 val mergeEqs : (atomExp IntBinaryMap.map option list | |
401 -> atomExp IntBinaryMap.map option) = | |
402 List.foldr (fn (SOME eqs, SOME acc) => SOME (IM.unionWith #1 (eqs, acc)) | _ => NONE) | |
403 (SOME IM.empty) | |
404 | |
405 fun dnf (fQuery, fDml) = | |
406 let | |
407 val isStar = | |
408 (* TODO: decide if this is okay and, if so, factor out magic | |
409 string "*" to a common location. *) | |
410 (* First guess: definitely okay for conservative approximation, | |
411 though information lost might be useful even in current | |
412 implementation for finding an extra equality. *) | |
413 fn SOME (Field (_, field)) => String.isSuffix "*" field | |
414 | _ => false | |
415 fun canIgnore (_, a1, a2) = isStar a1 orelse isStar a2 | |
416 fun simplifyLists xs = TLS.listItems (TLS.addList (TLS.empty, xs)) | |
417 fun simplifyAtomsConj xs = TS.listItems (TS.addList (TS.empty, xs)) | |
418 val simplifyAtomsDisj = simplifyAtomsConj o List.filter canIgnore | |
419 in | |
420 normalize (simplifyLists, simplifyAtomsConj, simplifyAtomsDisj, negateCmp, Disj) | |
421 (Combo (Conj, [markQuery fQuery, markDml fDml])) | |
422 end | |
423 | |
424 val conflictMaps = List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf | |
425 | |
426 end | |
427 | |
428 val conflictMaps = ConflictMaps.conflictMaps | |
308 | 429 |
309 val rec sqexpToFormula = | 430 val rec sqexpToFormula = |
310 fn Sql.SqTrue => Combo (Conj, []) | 431 fn Sql.SqTrue => Combo (Conj, []) |
311 | Sql.SqFalse => Combo (Disj, []) | 432 | Sql.SqFalse => Combo (Disj, []) |
312 | Sql.SqNot e => Negate (sqexpToFormula e) | 433 | Sql.SqNot e => Negate (sqexpToFormula e) |
486 body = body, | 607 body = body, |
487 tables = tables, | 608 tables = tables, |
488 exps = exps}, | 609 exps = exps}, |
489 dummyLoc) | 610 dummyLoc) |
490 val (EQuery {query = queryText, ...}, _) = queryExp | 611 val (EQuery {query = queryText, ...}, _) = queryExp |
491 (* DEBUG: we can remove the following line at some point. *) | 612 (* DEBUG *) |
492 val () = Print.preface ("sqlcache> ", (MonoPrint.p_exp MonoEnv.empty queryText)) | 613 val () = Print.preface ("sqlcache> ", (MonoPrint.p_exp MonoEnv.empty queryText)) |
493 val args = List.tabulate (numArgs, fn n => (ERel n, dummyLoc)) | 614 val args = List.tabulate (numArgs, fn n => (ERel n, dummyLoc)) |
494 fun bind x f = Option.mapPartial f x | 615 fun bind x f = Option.mapPartial f x |
495 fun guard b x = if b then x else NONE | 616 fun guard b x = if b then x else NONE |
496 (* DEBUG: set first boolean argument to true to turn on printing. *) | 617 (* DEBUG: set first boolean argument to true to turn on printing. *) |
513 | e' => (e', queryInfo) | 634 | e' => (e', queryInfo) |
514 in | 635 in |
515 fileMapfold (fn exp => fn state => doExp state exp) file (SIMM.empty, IM.empty, 0) | 636 fileMapfold (fn exp => fn state => doExp state exp) file (SIMM.empty, IM.empty, 0) |
516 end | 637 end |
517 | 638 |
518 fun invalidations ((query, numArgs), dml) = | 639 structure Invalidations = struct |
519 let | 640 |
520 val loc = dummyLoc | 641 val loc = dummyLoc |
521 val optionAtomExpToExp = | 642 |
522 fn NONE => (ENone stringTyp, loc) | 643 val optionAtomExpToExp = |
523 | SOME e => (ESome (stringTyp, | 644 fn NONE => (ENone stringTyp, loc) |
524 (case e of | 645 | SOME e => (ESome (stringTyp, |
525 DmlRel n => ERel n | 646 (case e of |
526 | Prim p => EPrim p | 647 DmlRel n => ERel n |
527 (* TODO: make new type containing only these two. *) | 648 | Prim p => EPrim p |
528 | _ => raise Match, | 649 (* TODO: make new type containing only these two. *) |
529 loc)), | 650 | _ => raise Match, |
530 loc) | 651 loc)), |
531 fun eqsToInvalidation eqs = | 652 loc) |
532 let | 653 |
533 fun inv n = if n < 0 then [] else IM.find (eqs, n) :: inv (n - 1) | 654 fun eqsToInvalidation numArgs eqs = |
534 in | 655 let |
535 inv (numArgs - 1) | 656 fun inv n = if n < 0 then [] else IM.find (eqs, n) :: inv (n - 1) |
536 end | 657 in |
537 (* Tests if [ys] makes [xs] a redundant cache invalidation. [NONE] here | 658 inv (numArgs - 1) |
538 represents unknown, which means a wider invalidation. *) | 659 end |
539 val rec madeRedundantBy : atomExp option list * atomExp option list -> bool = | 660 |
540 fn ([], []) => (print "hey!\n"; true) | 661 (* Tests if [ys] makes [xs] a redundant cache invalidation. [NONE] here |
541 | (NONE :: xs, _ :: ys) => madeRedundantBy (xs, ys) | 662 represents unknown, which means a wider invalidation. *) |
542 | (SOME x :: xs, SOME y :: ys) => (case AtomExpKey.compare (x, y) of | 663 val rec madeRedundantBy : atomExp option list * atomExp option list -> bool = |
543 EQUAL => madeRedundantBy (xs, ys) | 664 fn ([], []) => true |
544 | _ => false) | 665 | (NONE :: xs, _ :: ys) => madeRedundantBy (xs, ys) |
545 | _ => false | 666 | (SOME x :: xs, SOME y :: ys) => (case AtomExpKey.compare (x, y) of |
546 fun removeRedundant' (xss, yss) = | 667 EQUAL => madeRedundantBy (xs, ys) |
547 case xss of | 668 | _ => false) |
548 [] => yss | 669 | _ => false |
549 | xs :: xss' => | 670 |
550 removeRedundant' (xss', | 671 fun removeRedundant' (xss, yss) = |
551 if List.exists (fn ys => madeRedundantBy (xs, ys)) (xss' @ yss) | 672 case xss of |
552 then yss | 673 [] => yss |
553 else xs :: yss) | 674 | xs :: xss' => |
554 fun removeRedundant xss = removeRedundant' (xss, []) | 675 removeRedundant' (xss', |
555 val eqss = conflictMaps (queryToFormula query, dmlToFormula dml) | 676 if List.exists (fn ys => madeRedundantBy (xs, ys)) (xss' @ yss) |
556 in | 677 then yss |
557 (map (map optionAtomExpToExp) o removeRedundant o map eqsToInvalidation) eqss | 678 else xs :: yss) |
558 end | 679 |
680 fun removeRedundant xss = removeRedundant' (xss, []) | |
681 | |
682 fun eqss (query, dml) = conflictMaps (queryToFormula query, dmlToFormula dml) | |
683 | |
684 fun invalidations ((query, numArgs), dml) = | |
685 (map (map optionAtomExpToExp) | |
686 o removeRedundant | |
687 o map (eqsToInvalidation numArgs) | |
688 o eqss) | |
689 (query, dml) | |
690 | |
691 end | |
692 | |
693 val invalidations = Invalidations.invalidations | |
694 | |
695 (* DEBUG *) | |
696 val gunk : ((Sql.query * int) * Sql.dml) list ref = ref [] | |
559 | 697 |
560 fun addFlushing (file, (tableToIndices, indexToQueryNumArgs, _)) = | 698 fun addFlushing (file, (tableToIndices, indexToQueryNumArgs, _)) = |
561 let | 699 let |
562 val flushes = List.concat o | 700 val flushes = List.concat o |
563 map (fn (i, argss) => map (fn args => flush (i, args)) argss) | 701 map (fn (i, argss) => map (fn args => flush (i, args)) argss) |
565 fn EDml (origDmlText, failureMode) => | 703 fn EDml (origDmlText, failureMode) => |
566 let | 704 let |
567 val (newDmlText, wrapLets, numArgs) = factorOutNontrivial origDmlText | 705 val (newDmlText, wrapLets, numArgs) = factorOutNontrivial origDmlText |
568 val dmlText = incRels numArgs newDmlText | 706 val dmlText = incRels numArgs newDmlText |
569 val dmlExp = EDml (dmlText, failureMode) | 707 val dmlExp = EDml (dmlText, failureMode) |
570 (* DEBUG: we can remove the following line at some point. *) | 708 (* DEBUG *) |
571 val () = Print.preface ("sqlcache> ", (MonoPrint.p_exp MonoEnv.empty dmlText)) | 709 val () = Print.preface ("sqlcache> ", (MonoPrint.p_exp MonoEnv.empty dmlText)) |
572 val invs = | 710 val invs = |
573 case Sql.parse Sql.dml dmlText of | 711 case Sql.parse Sql.dml dmlText of |
574 SOME dmlParsed => | 712 SOME dmlParsed => |
575 map (fn i => (case IM.find (indexToQueryNumArgs, i) of | 713 map (fn i => (case IM.find (indexToQueryNumArgs, i) of |
576 SOME queryNumArgs => | 714 SOME queryNumArgs => |
577 (i, invalidations (queryNumArgs, dmlParsed)) | 715 (* DEBUG *) |
716 (gunk := (queryNumArgs, dmlParsed) :: !gunk; | |
717 (i, invalidations (queryNumArgs, dmlParsed))) | |
578 (* TODO: fail more gracefully. *) | 718 (* TODO: fail more gracefully. *) |
579 | NONE => raise Match)) | 719 | NONE => raise Match)) |
580 (SIMM.findList (tableToIndices, tableDml dmlParsed)) | 720 (SIMM.findList (tableToIndices, tableDml dmlParsed)) |
581 (* TODO: fail more gracefully. *) | 721 (* TODO: fail more gracefully. *) |
582 | NONE => raise Match | 722 | NONE => raise Match |
583 in | 723 in |
584 wrapLets (sequence (flushes invs @ [dmlExp])) | 724 wrapLets (sequence (flushes invs @ [dmlExp])) |
585 end | 725 end |
586 | e' => e' | 726 | e' => e' |
587 in | 727 in |
728 (* DEBUG *) | |
729 gunk := []; | |
588 fileMap doExp file | 730 fileMap doExp file |
589 end | 731 end |
590 | 732 |
591 val inlineSql = | 733 val inlineSql = |
592 let | 734 let |
604 fileMap doExp | 746 fileMap doExp |
605 end | 747 end |
606 | 748 |
607 fun go file = | 749 fun go file = |
608 let | 750 let |
609 (* TODO: do something nicer than having Sql be in one of two modes. *) | 751 (* TODO: do something nicer than [Sql] being in one of two modes. *) |
610 val () = (resetFfiInfo (); Sql.sqlcacheMode := true) | 752 val () = (resetFfiInfo (); Sql.sqlcacheMode := true) |
611 val file' = addFlushing (addChecking (inlineSql file)) | 753 val file' = addFlushing (addChecking (inlineSql file)) |
612 val () = Sql.sqlcacheMode := false | 754 val () = Sql.sqlcacheMode := false |
613 in | 755 in |
614 file' | 756 file' |