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