Mercurial > urweb
comparison src/sqlcache.sml @ 2221:278e10629ba1
Basic field-resolution invalidation.
author | Ziv Scully <ziv@mit.edu> |
---|---|
date | Sat, 29 Nov 2014 03:37:59 -0500 |
parents | ff38b3e0cdfd |
children | 9410959d296f |
comparison
equal
deleted
inserted
replaced
2220:794017f378de | 2221:278e10629ba1 |
---|---|
174 if n = norm then fss else cartesianProduct fss | 174 if n = norm then fss else cartesianProduct fss |
175 end | 175 end |
176 | 176 |
177 fun normalize negate norm = normalize' negate norm o flatten o pushNegate negate false | 177 fun normalize negate norm = normalize' negate norm o flatten o pushNegate negate false |
178 | 178 |
179 fun mapFormulaSigned positive mf = | 179 fun mapFormula mf = |
180 fn Atom x => Atom (mf (positive, x)) | 180 fn Atom x => Atom (mf x) |
181 | Negate f => Negate (mapFormulaSigned (not positive) mf f) | 181 | Negate f => Negate (mapFormula mf f) |
182 | Combo (n, fs) => Combo (n, map (mapFormulaSigned positive mf) fs) | 182 | Combo (n, fs) => Combo (n, map (mapFormula mf) fs) |
183 | |
184 fun mapFormula mf = mapFormulaSigned true (fn (_, x) => mf x) | |
185 | 183 |
186 (* SQL analysis. *) | 184 (* SQL analysis. *) |
187 | 185 |
188 val rec chooseTwos : 'a list -> ('a * 'a) list = | 186 val rec chooseTwos : 'a list -> ('a * 'a) list = |
189 fn [] => [] | 187 fn [] => [] |
223 | (Field (t1, f1), Field (t2, f2)) => String.compare (t1 ^ "." ^ f1, t2 ^ "." ^ f2) | 221 | (Field (t1, f1), Field (t2, f2)) => String.compare (t1 ^ "." ^ f1, t2 ^ "." ^ f2) |
224 | 222 |
225 end | 223 end |
226 | 224 |
227 structure UF = UnionFindFn(AtomExpKey) | 225 structure UF = UnionFindFn(AtomExpKey) |
228 | 226 val conflictMaps : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula |
229 (* val conflictMaps : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula *) | 227 * (Sql.cmp * Sql.sqexp * Sql.sqexp) formula |
230 (* * (Sql.cmp * Sql.sqexp * Sql.sqexp) formula *) | 228 -> atomExp IM.map list = |
231 (* -> Mono.exp' IM.map list = *) | 229 let |
232 (* let *) | |
233 val toKnownEquality = | 230 val toKnownEquality = |
234 (* [NONE] here means unkown. Anything that isn't a comparison between | 231 (* [NONE] here means unkown. Anything that isn't a comparison between |
235 two knowns shouldn't be used, and simply dropping unused terms is | 232 two knowns shouldn't be used, and simply dropping unused terms is |
236 okay in disjunctive normal form. *) | 233 okay in disjunctive normal form. *) |
237 fn (Sql.Eq, SOME e1, SOME e2) => SOME (e1, e2) | 234 fn (Sql.Eq, SOME e1, SOME e2) => SOME (e1, e2) |
295 -> atomExp IntBinaryMap.map option) = | 292 -> atomExp IntBinaryMap.map option) = |
296 List.foldr (fn (SOME eqs, SOME acc) => SOME (IM.unionWith #1 (eqs, acc)) | _ => NONE) | 293 List.foldr (fn (SOME eqs, SOME acc) => SOME (IM.unionWith #1 (eqs, acc)) | _ => NONE) |
297 (SOME IM.empty) | 294 (SOME IM.empty) |
298 fun dnf (fQuery, fDml) = | 295 fun dnf (fQuery, fDml) = |
299 normalize negateCmp Dnf (Combo (Cnf, [markQuery fQuery, markDml fDml])) | 296 normalize negateCmp Dnf (Combo (Cnf, [markQuery fQuery, markDml fDml])) |
300 (* in *) | 297 in |
301 val conflictMaps : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula | 298 (* val conflictMaps : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula *) |
302 * (Sql.cmp * Sql.sqexp * Sql.sqexp) formula | 299 (* * (Sql.cmp * Sql.sqexp * Sql.sqexp) formula *) |
303 -> atomExp IM.map list = | 300 (* -> atomExp IM.map list = *) |
304 List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf | 301 List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf |
305 (* end *) | 302 end |
306 | 303 |
307 val rec sqexpToFormula = | 304 val rec sqexpToFormula = |
308 fn Sql.SqTrue => Combo (Cnf, []) | 305 fn Sql.SqTrue => Combo (Cnf, []) |
309 | Sql.SqFalse => Combo (Dnf, []) | 306 | Sql.SqFalse => Combo (Dnf, []) |
310 | Sql.SqNot e => Negate (sqexpToFormula e) | 307 | Sql.SqNot e => Negate (sqexpToFormula e) |
336 | 333 |
337 fun valsToFormula (table, vals) = | 334 fun valsToFormula (table, vals) = |
338 Combo (Cnf, map (fn (field, v) => Atom (Sql.Eq, Sql.Field (table, field), v)) vals) | 335 Combo (Cnf, map (fn (field, v) => Atom (Sql.Eq, Sql.Field (table, field), v)) vals) |
339 | 336 |
340 val rec dmlToFormula = | 337 val rec dmlToFormula = |
341 fn Sql.Insert tableVals => valsToFormula tableVals | 338 fn Sql.Insert (table, vals) => valsToFormula (table, vals) |
342 | Sql.Delete (table, wher) => renameTables [(table, "T")] (sqexpToFormula wher) | 339 | Sql.Delete (table, wher) => renameTables [(table, "T")] (sqexpToFormula wher) |
343 (* TODO: refine formula for the vals part, which could take into account the wher part. *) | |
344 (* TODO: use pushNegate instead of mapFormulaSigned? *) | |
345 | Sql.Update (table, vals, wher) => | 340 | Sql.Update (table, vals, wher) => |
346 let | 341 let |
347 val f = sqexpToFormula wher | 342 val fWhere = sqexpToFormula wher |
348 fun update (positive, a) = | 343 val fVals = valsToFormula (table, vals) |
349 let | 344 (* TODO: don't use field name hack. *) |
350 fun updateIfNecessary field = | 345 val markField = |
351 case List.find (fn (f, _) => field = f) vals of | 346 fn Sql.Field (t, v) => Sql.Field (t, v ^ "*") |
352 SOME (_, v) => (if positive then Sql.Eq else Sql.Ne, | 347 | e => e |
353 Sql.Field (table, field), | 348 val mark = mapFormula (fn (cmp, e1, e2) => (cmp, markField e1, markField e2)) |
354 v) | |
355 | NONE => a | |
356 in | |
357 case a of | |
358 (_, Sql.Field (_, field), _) => updateIfNecessary field | |
359 | (_, _, Sql.Field (_, field)) => updateIfNecessary field | |
360 | _ => a | |
361 end | |
362 in | 349 in |
363 renameTables [(table, "T")] | 350 renameTables [(table, "T")] |
364 (Combo (Dnf, [f, | 351 (Combo (Dnf, [Combo (Cnf, [fVals, mark fWhere]), |
365 Combo (Cnf, [valsToFormula (table, vals), | 352 Combo (Cnf, [mark fVals, fWhere])])) |
366 mapFormulaSigned true update f])])) | |
367 end | 353 end |
368 | 354 |
369 val rec tablesQuery = | 355 val rec tablesQuery = |
370 fn Sql.Query1 {From = tablePairs, ...} => SS.fromList (map #1 tablePairs) | 356 fn Sql.Query1 {From = tablePairs, ...} => SS.fromList (map #1 tablePairs) |
371 | Sql.Union (q1, q2) => SS.union (tablesQuery q1, tablesQuery q2) | 357 | Sql.Union (q1, q2) => SS.union (tablesQuery q1, tablesQuery q2) |
480 Search.Continue x => x | 466 Search.Continue x => x |
481 | Search.Return _ => raise Match | 467 | Search.Return _ => raise Match |
482 | 468 |
483 fun fileMap doExp file = #1 (fileMapfold (fn x => fn _ => (doExp x, ())) file ()) | 469 fun fileMap doExp file = #1 (fileMapfold (fn x => fn _ => (doExp x, ())) file ()) |
484 | 470 |
471 fun factorOutNontrivial text = | |
472 let | |
473 val loc = ErrorMsg.dummySpan | |
474 fun strcat (e1, e2) = (EStrcat (e1, e2), loc) | |
475 val chunks = Sql.chunkify text | |
476 val (newText, newVariables) = | |
477 (* Important that this is foldr (to oppose foldl below). *) | |
478 List.foldr | |
479 (fn (chunk, (qText, newVars)) => | |
480 (* Variable bound to the head of newBs will have the lowest index. *) | |
481 case chunk of | |
482 Sql.Exp (e as (EPrim _, _)) => (strcat (e, qText), newVars) | |
483 | Sql.Exp e => | |
484 let | |
485 val n = length newVars | |
486 in | |
487 (* This is the (n + 1)th new variable, so there are | |
488 already n new variables bound, so we increment | |
489 indices by n. *) | |
490 (strcat ((ERel (~(n+1)), loc), qText), incRels n e :: newVars) | |
491 end | |
492 | Sql.String s => (strcat (stringExp s, qText), newVars)) | |
493 (stringExp "", []) | |
494 chunks | |
495 fun wrapLets e' = | |
496 (* Important that this is foldl (to oppose foldr above). *) | |
497 List.foldl (fn (v, e') => ELet ("sqlArgz", stringTyp, v, (e', loc))) | |
498 e' | |
499 newVariables | |
500 val numArgs = length newVariables | |
501 in | |
502 (newText, wrapLets, numArgs) | |
503 end | |
504 | |
485 fun addChecking file = | 505 fun addChecking file = |
486 let | 506 let |
487 fun doExp (queryInfo as (tableToIndices, indexToQuery)) = | 507 fun doExp (queryInfo as (tableToIndices, indexToQueryNumArgs)) = |
488 fn e' as ELet (v, t, | 508 fn e' as ELet (v, t, |
489 queryExp' as (EQuery {query = origQueryText, | 509 (EQuery {query = origQueryText, |
490 initial, body, state, tables, exps}, queryLoc), | 510 initial, body, state, tables, exps, sqlcacheInfo}, queryLoc), |
491 letBody) => | 511 letBody) => |
492 let | 512 let |
493 val loc = ErrorMsg.dummySpan | 513 val (newQueryText, wrapLets, numArgs) = factorOutNontrivial origQueryText |
494 val chunks = Sql.chunkify origQueryText | |
495 fun strcat (e1, e2) = (EStrcat (e1, e2), loc) | |
496 val (newQueryText, newVariables) = | |
497 (* Important that this is foldr (to oppose foldl below). *) | |
498 List.foldr | |
499 (fn (chunk, (qText, newVars)) => | |
500 (* Variable bound to the head of newBs will have the lowest index. *) | |
501 case chunk of | |
502 Sql.Exp (e as (EPrim _, _)) => (strcat (e, qText), newVars) | |
503 | Sql.Exp e => | |
504 let | |
505 val n = length newVars | |
506 in | |
507 (* This is the (n + 1)th new variable, so | |
508 there are already n new variables bound, | |
509 so we increment indices by n. *) | |
510 (strcat ((ERel (~(n+1)), loc), qText), incRels n e :: newVars) | |
511 end | |
512 | Sql.String s => (strcat (stringExp s, qText), newVars)) | |
513 (stringExp "", []) | |
514 chunks | |
515 fun wrapLets e' = | |
516 (* Important that this is foldl (to oppose foldr above). *) | |
517 List.foldl (fn (v, e') => ELet ("sqlArgz", stringTyp, v, (e', loc))) | |
518 e' | |
519 newVariables | |
520 val numArgs = length newVariables | |
521 (* Increment once for each new variable just made. *) | 514 (* Increment once for each new variable just made. *) |
522 val queryExp = incRels (length newVariables) | 515 val queryExp = incRels numArgs |
523 (EQuery {query = newQueryText, | 516 (EQuery {query = newQueryText, |
524 initial = initial, | 517 initial = initial, |
525 body = body, | 518 body = body, |
526 state = state, | 519 state = state, |
527 tables = tables, | 520 tables = tables, |
528 exps = exps}, | 521 exps = exps, |
522 sqlcacheInfo = sqlcacheInfo}, | |
529 queryLoc) | 523 queryLoc) |
530 val (EQuery {query = queryText, ...}, _) = queryExp | 524 val (EQuery {query = queryText, ...}, _) = queryExp |
531 val () = Print.preface ("sqlcache> ", (MonoPrint.p_exp MonoEnv.empty queryText)); | 525 val () = Print.preface ("sqlcache> ", (MonoPrint.p_exp MonoEnv.empty queryText)) |
532 val args = List.tabulate (numArgs, fn n => (ERel n, loc)) | 526 val args = List.tabulate (numArgs, fn n => (ERel n, ErrorMsg.dummySpan)) |
533 fun bind x f = Option.mapPartial f x | 527 fun bind x f = Option.mapPartial f x |
534 fun guard b x = if b then x else NONE | 528 fun guard b x = if b then x else NONE |
535 (* DEBUG: set first boolean argument to true to turn on printing. *) | 529 (* DEBUG: set first boolean argument to true to turn on printing. *) |
536 fun safe bound = not o effectful true (effectfulMap file) false bound | 530 fun safe bound = not o effectful true (effectfulMap file) false bound |
537 val attempt = | 531 val attempt = |
540 bind (Sql.parse Sql.query queryText) (fn queryParsed => | 534 bind (Sql.parse Sql.query queryText) (fn queryParsed => |
541 bind (indexOfName v) (fn index => | 535 bind (indexOfName v) (fn index => |
542 bind (IM.find (!urlifiedRel0s, index)) (fn urlifiedRel0 => | 536 bind (IM.find (!urlifiedRel0s, index)) (fn urlifiedRel0 => |
543 SOME (wrapLets (ELet (v, t, | 537 SOME (wrapLets (ELet (v, t, |
544 cacheWrap (queryExp, index, urlifiedRel0, args), | 538 cacheWrap (queryExp, index, urlifiedRel0, args), |
545 incRelsBound 1 (length newVariables) letBody)), | 539 incRelsBound 1 numArgs letBody)), |
546 (SS.foldr (fn (tab, qi) => SIMM.insert (qi, tab, index)) | 540 (SS.foldr (fn (tab, qi) => SIMM.insert (qi, tab, index)) |
547 tableToIndices | 541 tableToIndices |
548 (tablesQuery queryParsed), | 542 (tablesQuery queryParsed), |
549 IM.insert (indexToQuery, index, (queryParsed, numArgs)))))))) | 543 IM.insert (indexToQueryNumArgs, index, (queryParsed, numArgs)))))))) |
550 in | 544 in |
551 case attempt of | 545 case attempt of |
552 SOME pair => pair | 546 SOME pair => pair |
553 | NONE => (e', queryInfo) | 547 | NONE => (e', queryInfo) |
554 end | 548 end |
556 | e' => (e', queryInfo) | 550 | e' => (e', queryInfo) |
557 in | 551 in |
558 fileMapfold (fn exp => fn state => doExp state exp) file (SIMM.empty, IM.empty) | 552 fileMapfold (fn exp => fn state => doExp state exp) file (SIMM.empty, IM.empty) |
559 end | 553 end |
560 | 554 |
555 val gunk : (Sql.query * Sql.dml * Mono.exp list list) list ref = ref [] | |
556 | |
561 val gunk' : (((Sql.cmp * Sql.sqexp * Sql.sqexp) formula) | 557 val gunk' : (((Sql.cmp * Sql.sqexp * Sql.sqexp) formula) |
562 * ((Sql.cmp * Sql.sqexp * Sql.sqexp) formula)) list ref = ref [] | 558 * ((Sql.cmp * Sql.sqexp * Sql.sqexp) formula)) list ref = ref [] |
563 | 559 |
564 fun invalidations (nQueryArgs, query, dml) = | 560 fun invalidations ((query, numArgs), dml) = |
565 let | 561 let |
566 val loc = ErrorMsg.dummySpan | 562 val loc = ErrorMsg.dummySpan |
567 val optionAtomExpToExp = | 563 val optionAtomExpToExp = |
568 fn NONE => (ENone stringTyp, loc) | 564 fn NONE => (ENone stringTyp, loc) |
569 | SOME e => (ESome (stringTyp, | 565 | SOME e => (ESome (stringTyp, |
576 loc) | 572 loc) |
577 fun eqsToInvalidation eqs = | 573 fun eqsToInvalidation eqs = |
578 let | 574 let |
579 fun inv n = if n < 0 then [] else IM.find (eqs, n) :: inv (n - 1) | 575 fun inv n = if n < 0 then [] else IM.find (eqs, n) :: inv (n - 1) |
580 in | 576 in |
581 inv (nQueryArgs - 1) | 577 inv (numArgs - 1) |
582 end | 578 end |
583 (* *) | 579 (* Tests if [ys] makes [xs] a redundant cache invalidation. [NONE] here |
580 represents unknown, which means a wider invalidation. *) | |
584 val rec madeRedundantBy : atomExp option list * atomExp option list -> bool = | 581 val rec madeRedundantBy : atomExp option list * atomExp option list -> bool = |
585 fn ([], []) => true | 582 fn ([], []) => true |
586 | (NONE :: xs, _ :: ys) => madeRedundantBy (xs, ys) | 583 | (NONE :: xs, _ :: ys) => madeRedundantBy (xs, ys) |
587 | (SOME x :: xs, SOME y :: ys) => equalAtomExp (x, y) andalso madeRedundantBy (xs, ys) | 584 | (SOME x :: xs, SOME y :: ys) => equalAtomExp (x, y) andalso madeRedundantBy (xs, ys) |
588 | _ => false | 585 | _ => false |
599 in | 596 in |
600 gunk' := (queryToFormula query, dmlToFormula dml) :: !gunk'; | 597 gunk' := (queryToFormula query, dmlToFormula dml) :: !gunk'; |
601 (map (map optionAtomExpToExp) o removeRedundant o map eqsToInvalidation) eqss | 598 (map (map optionAtomExpToExp) o removeRedundant o map eqsToInvalidation) eqss |
602 end | 599 end |
603 | 600 |
604 val gunk : Mono.exp list list list ref = ref [] | 601 |
605 | 602 (* gunk := (queryParsed, dmlParsed, invalidations (numArgs, queryParsed, dmlParsed)) :: !gunk); *) |
606 fun addFlushing (file, queryInfo as (tableToIndices, indexToQuery)) = | 603 |
607 let | 604 fun addFlushing (file, (tableToIndices, indexToQueryNumArgs)) = |
608 val allIndices = SM.foldr (fn (x, acc) => IS.listItems x @ acc) [] tableToIndices | 605 let |
609 val flushes = map (fn i => ffiAppCache' ("flush", i, [])) | 606 (* TODO: write this. *) |
607 val allInvs = () (* SM.foldr (fn (x, acc) => IS.listItems x @ acc) [] tableToIndices *) | |
608 val flushes = List.concat o | |
609 map (fn (i, argss) => | |
610 map (fn args => | |
611 ffiAppCache' ("flush", i, | |
612 map (fn arg => (arg, stringTyp)) args)) argss) | |
610 val doExp = | 613 val doExp = |
611 fn dmlExp as EDml (dmlText, _) => | 614 fn EDml (origDmlText, failureMode) => |
612 let | 615 let |
613 val indices = | 616 val (newDmlText, wrapLets, numArgs) = factorOutNontrivial origDmlText |
617 val dmlText = incRels numArgs newDmlText | |
618 val dmlExp = EDml (dmlText, failureMode) | |
619 val () = Print.preface ("sqlcache> ", (MonoPrint.p_exp MonoEnv.empty dmlText)) | |
620 val invs = | |
614 case Sql.parse Sql.dml dmlText of | 621 case Sql.parse Sql.dml dmlText of |
615 SOME dmlParsed => | 622 SOME dmlParsed => |
616 map (fn i => ((case IM.find (indexToQuery, i) of | 623 map (fn i => (case IM.find (indexToQueryNumArgs, i) of |
617 NONE => () | 624 SOME queryNumArgs => |
618 | SOME (queryParsed, numArgs) => | 625 (i, invalidations (queryNumArgs, dmlParsed)) |
619 gunk := invalidations (numArgs, queryParsed, dmlParsed) :: !gunk); | 626 (* TODO: fail more gracefully. *) |
620 i)) (SIMM.findList (tableToIndices, tableDml dmlParsed)) | 627 | NONE => raise Match)) |
621 | NONE => allIndices | 628 (SIMM.findList (tableToIndices, tableDml dmlParsed)) |
629 (* TODO: fail more gracefully. *) | |
630 | NONE => raise Match | |
622 in | 631 in |
623 sequence (flushes indices @ [dmlExp]) | 632 wrapLets (sequence (flushes invs @ [dmlExp])) |
624 end | 633 end |
625 | e' => e' | 634 | e' => e' |
626 in | 635 in |
627 fileMap doExp file | 636 fileMap doExp file |
628 end | 637 end |
629 | 638 |
639 val inlineSql = | |
640 let | |
641 val doExp = | |
642 (* TODO: EQuery, too? *) | |
643 (* ASK: should this live in [MonoOpt]? *) | |
644 fn EDml ((ECase (disc, cases, {disc = dTyp, ...}), loc), failureMode) => | |
645 let | |
646 val newCases = map (fn (p, e) => (p, (EDml (e, failureMode), loc))) cases | |
647 in | |
648 ECase (disc, newCases, {disc = dTyp, result = (TRecord [], loc)}) | |
649 end | |
650 | e => e | |
651 in | |
652 fileMap doExp | |
653 end | |
654 | |
630 fun go file = | 655 fun go file = |
631 let | 656 let |
632 val () = Sql.sqlcacheMode := true | 657 val () = Sql.sqlcacheMode := true |
633 val file' = addFlushing (addChecking file) | 658 val file' = addFlushing (addChecking (inlineSql file)) |
634 val () = Sql.sqlcacheMode := false | 659 val () = Sql.sqlcacheMode := false |
635 in | 660 in |
636 file' | 661 file' |
637 end | 662 end |
638 | 663 |
639 end | 664 end |