diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/sql.sml | 4 | ||||
| -rw-r--r-- | src/sqlcache.sml | 426 |
2 files changed, 286 insertions, 144 deletions
diff --git a/src/sql.sml b/src/sql.sml index 59b4eac6..22ffea39 100644 --- a/src/sql.sml +++ b/src/sql.sml @@ -214,8 +214,8 @@ val sqbrel = altL [cmp "=" Eq, cmp "<" Lt, cmp ">=" Ge, cmp ">" Gt, - wrap (const "AND") (fn () => RLop Or), - wrap (const "OR") (fn () => RLop And)] + wrap (const "AND") (fn () => RLop And), + wrap (const "OR") (fn () => RLop Or)] datatype ('a, 'b) sum = inl of 'a | inr of 'b diff --git a/src/sqlcache.sml b/src/sqlcache.sml index bf9ee77a..b259f2cb 100644 --- a/src/sqlcache.sml +++ b/src/sqlcache.sml @@ -1,4 +1,4 @@ -structure Sqlcache :> SQLCACHE = struct +structure Sqlcache (* DEBUG: add back :> SQLCACHE. *) = struct open Mono @@ -147,12 +147,12 @@ datatype 'atom formula = val flipJt = fn Conj => Disj | Disj => Conj -fun bind xs f = List.concat (map f xs) +fun listBind xs f = List.concat (map f xs) val rec cartesianProduct : 'a list list -> 'a list list = fn [] => [[]] - | (xs :: xss) => bind (cartesianProduct xss) - (fn ys => bind xs (fn x => [x :: ys])) + | (xs :: xss) => listBind (cartesianProduct xss) + (fn ys => listBind xs (fn x => [x :: ys])) (* Pushes all negation to the atoms.*) fun pushNegate (negate : 'atom -> 'atom) (negating : bool) = @@ -161,35 +161,123 @@ fun pushNegate (negate : 'atom -> 'atom) (negating : bool) = | Combo (n, fs) => Combo (if negating then flipJt n else n, map (pushNegate negate negating) fs) val rec flatten = - fn Combo (n, fs) => - Combo (n, List.foldr (fn (f, acc) => + fn Combo (_, [f]) => flatten f + | Combo (j, fs) => + Combo (j, List.foldr (fn (f, acc) => case f of - Combo (n', fs') => if n = n' then fs' @ acc else f :: acc + Combo (j', fs') => + if j = j' orelse length fs' = 1 + then fs' @ acc + else f :: acc | _ => f :: acc) [] (map flatten fs)) | f => f -fun normalize' (negate : 'atom -> 'atom) (junc : junctionType) = - fn Atom x => [[x]] - | Negate f => map (map negate) (normalize' negate (flipJt junc) f) - | Combo (j, fs) => +fun normalize' ((simplifyLists, simplifyAtomsConj, simplifyAtomsDisj, negate) + : ('a list list -> 'a list list) + * ('a list -> 'a list) + * ('a list -> 'a list) + * ('a -> 'a)) + (junc : junctionType) = let - val fss = bind fs (normalize' negate j) + fun simplify junc = simplifyLists o map (case junc of + Conj => simplifyAtomsConj + | Disj => simplifyAtomsDisj) + fun norm junc = + simplify junc + o (fn Atom x => [[x]] + | Negate f => map (map negate) (norm (flipJt junc) f) + | Combo (j, fs) => + let + val fss = listBind fs (norm j) + in + if j = junc then fss else cartesianProduct fss + end) in - if j = junc then fss else cartesianProduct fss + norm junc end -fun normalize negate junc = normalize' negate junc o flatten o pushNegate negate false +fun normalize (simplifyLists, simplifyAtomsConj, simplifyAtomsDisj, negate, junc) = + (normalize' (simplifyLists, simplifyAtomsConj, simplifyAtomsDisj, negate) junc) + o flatten + o pushNegate negate false fun mapFormula mf = fn Atom x => Atom (mf x) | Negate f => Negate (mapFormula mf f) - | Combo (n, fs) => Combo (n, map (mapFormula mf) fs) + | Combo (j, fs) => Combo (j, map (mapFormula mf) fs) (* SQL analysis. *) +structure CmpKey : ORD_KEY = struct + + type ord_key = Sql.cmp + + val compare = + fn (Sql.Eq, Sql.Eq) => EQUAL + | (Sql.Eq, _) => LESS + | (_, Sql.Eq) => GREATER + | (Sql.Ne, Sql.Ne) => EQUAL + | (Sql.Ne, _) => LESS + | (_, Sql.Ne) => GREATER + | (Sql.Lt, Sql.Lt) => EQUAL + | (Sql.Lt, _) => LESS + | (_, Sql.Lt) => GREATER + | (Sql.Le, Sql.Le) => EQUAL + | (Sql.Le, _) => LESS + | (_, Sql.Le) => GREATER + | (Sql.Gt, Sql.Gt) => EQUAL + | (Sql.Gt, _) => LESS + | (_, Sql.Gt) => GREATER + | (Sql.Ge, Sql.Ge) => EQUAL + +end + + +functor ListKeyFn (K : ORD_KEY) : ORD_KEY = struct + + type ord_key = K.ord_key list + + val rec compare = + fn ([], []) => EQUAL + | ([], _) => LESS + | (_, []) => GREATER + | (x :: xs, y :: ys) => (case K.compare (x, y) of + EQUAL => compare (xs, ys) + | ord => ord) + +end + +functor OptionKeyFn (K : ORD_KEY) : ORD_KEY = struct + + type ord_key = K.ord_key option + + val compare = + fn (NONE, NONE) => EQUAL + | (NONE, _) => LESS + | (_, NONE) => GREATER + | (SOME x, SOME y) => K.compare (x, y) + +end + +functor TripleKeyFn (structure I : ORD_KEY + structure J : ORD_KEY + structure K : ORD_KEY) + : ORD_KEY where type ord_key = I.ord_key * J.ord_key * K.ord_key = struct + + type ord_key = I.ord_key * J.ord_key * K.ord_key + + fun compare ((i1, j1, k1), (i2, j2, k2)) = + case I.compare (i1, i2) of + EQUAL => (case J.compare (j1, j2) of + EQUAL => K.compare (k1, k2) + | ord => ord) + | ord => ord + +end + val rec chooseTwos : 'a list -> ('a * 'a) list = fn [] => [] | x :: ys => map (fn y => (x, y)) ys @ chooseTwos ys @@ -223,88 +311,121 @@ end structure UF = UnionFindFn(AtomExpKey) -val conflictMaps : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula - * (Sql.cmp * Sql.sqexp * Sql.sqexp) formula - -> atomExp IM.map list = - let - val toKnownEquality = - (* [NONE] here means unkown. Anything that isn't a comparison between - two knowns shouldn't be used, and simply dropping unused terms is - okay in disjunctive normal form. *) - fn (Sql.Eq, SOME e1, SOME e2) => SOME (e1, e2) - | _ => NONE - val equivClasses : (Sql.cmp * atomExp option * atomExp option) list -> atomExp list list = - UF.classes - o List.foldl UF.union' UF.empty - o List.mapPartial toKnownEquality - fun addToEqs (eqs, n, e) = - case IM.find (eqs, n) of - (* Comparing to a constant is probably better than comparing to - a variable? Checking that an existing constant matches a new - one is handled by [accumulateEqs]. *) - SOME (Prim _) => eqs - | _ => IM.insert (eqs, n, e) - val accumulateEqs = - (* [NONE] means we have a contradiction. *) - fn (_, NONE) => NONE - | ((Prim p1, Prim p2), eqso) => - (case Prim.compare (p1, p2) of - EQUAL => eqso - | _ => NONE) - | ((QueryArg n, Prim p), SOME eqs) => SOME (addToEqs (eqs, n, Prim p)) - | ((QueryArg n, DmlRel r), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r)) - | ((Prim p, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, Prim p)) - | ((DmlRel r, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r)) - (* TODO: deal with equalities involving just [DmlRel]s and [Prim]s. - This would involve guarding the invalidation with a check for the - relevant comparisons. *) - (* DEBUG: remove these print statements. *) - (* | ((DmlRel r, Prim p), eqso) => (print ("sadness " ^ Int.toString r ^ " = " ^ Prim.toString p ^ "\n"); eqso) *) - (* | ((Prim p, DmlRel r), eqso) => (print ("sadness " ^ Int.toString r ^ " = " ^ Prim.toString p ^ "\n"); eqso) *) - | (_, eqso) => eqso - val eqsOfClass : atomExp list -> atomExp IM.map option = - List.foldl accumulateEqs (SOME IM.empty) - o chooseTwos - fun toAtomExps rel (cmp, e1, e2) = - let - val qa = - (* Here [NONE] means unkown. *) - fn Sql.SqConst p => SOME (Prim p) - | Sql.Field tf => SOME (Field tf) - | Sql.Inj (EPrim p, _) => SOME (Prim p) - | Sql.Inj (ERel n, _) => SOME (rel n) - (* We can't deal with anything else, e.g., CURRENT_TIMESTAMP - becomes Sql.Unmodeled, which becomes NONE here. *) - | _ => NONE - in - (cmp, qa e1, qa e2) - end - fun negateCmp (cmp, e1, e2) = - (case cmp of - Sql.Eq => Sql.Ne - | Sql.Ne => Sql.Eq - | Sql.Lt => Sql.Ge - | Sql.Le => Sql.Gt - | Sql.Gt => Sql.Le - | Sql.Ge => Sql.Lt, - e1, e2) - val markQuery : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula -> - (Sql.cmp * atomExp option * atomExp option) formula = - mapFormula (toAtomExps QueryArg) - val markDml : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula -> - (Sql.cmp * atomExp option * atomExp option) formula = - mapFormula (toAtomExps DmlRel) - (* No eqs should have key conflicts because no variable is in two - equivalence classes, so the [#1] can be anything. *) - val mergeEqs : (atomExp IntBinaryMap.map option list - -> atomExp IntBinaryMap.map option) = - List.foldr (fn (SOME eqs, SOME acc) => SOME (IM.unionWith #1 (eqs, acc)) | _ => NONE) - (SOME IM.empty) - fun dnf (fQuery, fDml) = - normalize negateCmp Disj (Combo (Conj, [markQuery fQuery, markDml fDml])) - in - List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf - end +structure ConflictMaps = struct + + structure TK = TripleKeyFn(structure I = CmpKey + structure J = OptionKeyFn(AtomExpKey) + structure K = OptionKeyFn(AtomExpKey)) + structure TS = BinarySetFn(TK) + structure TLS = BinarySetFn(ListKeyFn(TK)) + + val toKnownEquality = + (* [NONE] here means unkown. Anything that isn't a comparison between two + knowns shouldn't be used, and simply dropping unused terms is okay in + disjunctive normal form. *) + fn (Sql.Eq, SOME e1, SOME e2) => SOME (e1, e2) + | _ => NONE + + val equivClasses : (Sql.cmp * atomExp option * atomExp option) list -> atomExp list list = + UF.classes + o List.foldl UF.union' UF.empty + o List.mapPartial toKnownEquality + + fun addToEqs (eqs, n, e) = + case IM.find (eqs, n) of + (* Comparing to a constant is probably better than comparing to a + variable? Checking that existing constants match a new ones is + handled by [accumulateEqs]. *) + SOME (Prim _) => eqs + | _ => IM.insert (eqs, n, e) + + val accumulateEqs = + (* [NONE] means we have a contradiction. *) + fn (_, NONE) => NONE + | ((Prim p1, Prim p2), eqso) => + (case Prim.compare (p1, p2) of + EQUAL => eqso + | _ => NONE) + | ((QueryArg n, Prim p), SOME eqs) => SOME (addToEqs (eqs, n, Prim p)) + | ((QueryArg n, DmlRel r), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r)) + | ((Prim p, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, Prim p)) + | ((DmlRel r, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r)) + (* TODO: deal with equalities between [DmlRel]s and [Prim]s. + This would involve guarding the invalidation with a check for the + relevant comparisons. *) + (* DEBUG: remove these print statements. *) + (* | ((DmlRel r, Prim p), eqso) => (print ("sadness " ^ Int.toString r ^ " = " ^ Prim.toString p ^ "\n"); eqso) *) + (* | ((Prim p, DmlRel r), eqso) => (print ("sadness " ^ Int.toString r ^ " = " ^ Prim.toString p ^ "\n"); eqso) *) + | (_, eqso) => eqso + + val eqsOfClass : atomExp list -> atomExp IM.map option = + List.foldl accumulateEqs (SOME IM.empty) + o chooseTwos + + fun toAtomExps rel (cmp, e1, e2) = + let + val qa = + (* Here [NONE] means unkown. *) + fn Sql.SqConst p => SOME (Prim p) + | Sql.Field tf => SOME (Field tf) + | Sql.Inj (EPrim p, _) => SOME (Prim p) + | Sql.Inj (ERel n, _) => SOME (rel n) + (* We can't deal with anything else, e.g., CURRENT_TIMESTAMP + becomes Sql.Unmodeled, which becomes NONE here. *) + | _ => NONE + in + (cmp, qa e1, qa e2) + end + + fun negateCmp (cmp, e1, e2) = + (case cmp of + Sql.Eq => Sql.Ne + | Sql.Ne => Sql.Eq + | Sql.Lt => Sql.Ge + | Sql.Le => Sql.Gt + | Sql.Gt => Sql.Le + | Sql.Ge => Sql.Lt, + e1, e2) + + val markQuery : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula -> + (Sql.cmp * atomExp option * atomExp option) formula = + mapFormula (toAtomExps QueryArg) + + val markDml : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula -> + (Sql.cmp * atomExp option * atomExp option) formula = + mapFormula (toAtomExps DmlRel) + (* No eqs should have key conflicts because no variable is in two + equivalence classes, so the [#1] could be [#2]. *) + + val mergeEqs : (atomExp IntBinaryMap.map option list + -> atomExp IntBinaryMap.map option) = + List.foldr (fn (SOME eqs, SOME acc) => SOME (IM.unionWith #1 (eqs, acc)) | _ => NONE) + (SOME IM.empty) + + fun dnf (fQuery, fDml) = + let + val isStar = + (* TODO: decide if this is okay and, if so, factor out magic + string "*" to a common location. *) + (* First guess: definitely okay for conservative approximation, + though information lost might be useful even in current + implementation for finding an extra equality. *) + fn SOME (Field (_, field)) => String.isSuffix "*" field + | _ => false + fun canIgnore (_, a1, a2) = isStar a1 orelse isStar a2 + fun simplifyLists xs = TLS.listItems (TLS.addList (TLS.empty, xs)) + fun simplifyAtomsConj xs = TS.listItems (TS.addList (TS.empty, xs)) + val simplifyAtomsDisj = simplifyAtomsConj o List.filter canIgnore + in + normalize (simplifyLists, simplifyAtomsConj, simplifyAtomsDisj, negateCmp, Disj) + (Combo (Conj, [markQuery fQuery, markDml fDml])) + end + + val conflictMaps = List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf + +end + +val conflictMaps = ConflictMaps.conflictMaps val rec sqexpToFormula = fn Sql.SqTrue => Combo (Conj, []) @@ -488,7 +609,7 @@ fun addChecking file = exps = exps}, dummyLoc) val (EQuery {query = queryText, ...}, _) = queryExp - (* DEBUG: we can remove the following line at some point. *) + (* DEBUG *) val () = Print.preface ("sqlcache> ", (MonoPrint.p_exp MonoEnv.empty queryText)) val args = List.tabulate (numArgs, fn n => (ERel n, dummyLoc)) fun bind x f = Option.mapPartial f x @@ -515,47 +636,64 @@ fun addChecking file = fileMapfold (fn exp => fn state => doExp state exp) file (SIMM.empty, IM.empty, 0) end -fun invalidations ((query, numArgs), dml) = - let - val loc = dummyLoc - val optionAtomExpToExp = - fn NONE => (ENone stringTyp, loc) - | SOME e => (ESome (stringTyp, - (case e of - DmlRel n => ERel n - | Prim p => EPrim p - (* TODO: make new type containing only these two. *) - | _ => raise Match, - loc)), - loc) - fun eqsToInvalidation eqs = - let - fun inv n = if n < 0 then [] else IM.find (eqs, n) :: inv (n - 1) - in - inv (numArgs - 1) - end - (* Tests if [ys] makes [xs] a redundant cache invalidation. [NONE] here - represents unknown, which means a wider invalidation. *) - val rec madeRedundantBy : atomExp option list * atomExp option list -> bool = - fn ([], []) => (print "hey!\n"; true) - | (NONE :: xs, _ :: ys) => madeRedundantBy (xs, ys) - | (SOME x :: xs, SOME y :: ys) => (case AtomExpKey.compare (x, y) of - EQUAL => madeRedundantBy (xs, ys) - | _ => false) - | _ => false - fun removeRedundant' (xss, yss) = - case xss of - [] => yss - | xs :: xss' => - removeRedundant' (xss', - if List.exists (fn ys => madeRedundantBy (xs, ys)) (xss' @ yss) - then yss - else xs :: yss) - fun removeRedundant xss = removeRedundant' (xss, []) - val eqss = conflictMaps (queryToFormula query, dmlToFormula dml) - in - (map (map optionAtomExpToExp) o removeRedundant o map eqsToInvalidation) eqss - end +structure Invalidations = struct + + val loc = dummyLoc + + val optionAtomExpToExp = + fn NONE => (ENone stringTyp, loc) + | SOME e => (ESome (stringTyp, + (case e of + DmlRel n => ERel n + | Prim p => EPrim p + (* TODO: make new type containing only these two. *) + | _ => raise Match, + loc)), + loc) + + fun eqsToInvalidation numArgs eqs = + let + fun inv n = if n < 0 then [] else IM.find (eqs, n) :: inv (n - 1) + in + inv (numArgs - 1) + end + + (* Tests if [ys] makes [xs] a redundant cache invalidation. [NONE] here + represents unknown, which means a wider invalidation. *) + val rec madeRedundantBy : atomExp option list * atomExp option list -> bool = + fn ([], []) => true + | (NONE :: xs, _ :: ys) => madeRedundantBy (xs, ys) + | (SOME x :: xs, SOME y :: ys) => (case AtomExpKey.compare (x, y) of + EQUAL => madeRedundantBy (xs, ys) + | _ => false) + | _ => false + + fun removeRedundant' (xss, yss) = + case xss of + [] => yss + | xs :: xss' => + removeRedundant' (xss', + if List.exists (fn ys => madeRedundantBy (xs, ys)) (xss' @ yss) + then yss + else xs :: yss) + + fun removeRedundant xss = removeRedundant' (xss, []) + + fun eqss (query, dml) = conflictMaps (queryToFormula query, dmlToFormula dml) + + fun invalidations ((query, numArgs), dml) = + (map (map optionAtomExpToExp) + o removeRedundant + o map (eqsToInvalidation numArgs) + o eqss) + (query, dml) + +end + +val invalidations = Invalidations.invalidations + +(* DEBUG *) +val gunk : ((Sql.query * int) * Sql.dml) list ref = ref [] fun addFlushing (file, (tableToIndices, indexToQueryNumArgs, _)) = let @@ -567,14 +705,16 @@ fun addFlushing (file, (tableToIndices, indexToQueryNumArgs, _)) = val (newDmlText, wrapLets, numArgs) = factorOutNontrivial origDmlText val dmlText = incRels numArgs newDmlText val dmlExp = EDml (dmlText, failureMode) - (* DEBUG: we can remove the following line at some point. *) + (* DEBUG *) val () = Print.preface ("sqlcache> ", (MonoPrint.p_exp MonoEnv.empty dmlText)) val invs = case Sql.parse Sql.dml dmlText of SOME dmlParsed => map (fn i => (case IM.find (indexToQueryNumArgs, i) of SOME queryNumArgs => - (i, invalidations (queryNumArgs, dmlParsed)) + (* DEBUG *) + (gunk := (queryNumArgs, dmlParsed) :: !gunk; + (i, invalidations (queryNumArgs, dmlParsed))) (* TODO: fail more gracefully. *) | NONE => raise Match)) (SIMM.findList (tableToIndices, tableDml dmlParsed)) @@ -585,6 +725,8 @@ fun addFlushing (file, (tableToIndices, indexToQueryNumArgs, _)) = end | e' => e' in + (* DEBUG *) + gunk := []; fileMap doExp file end @@ -606,7 +748,7 @@ val inlineSql = fun go file = let - (* TODO: do something nicer than having Sql be in one of two modes. *) + (* TODO: do something nicer than [Sql] being in one of two modes. *) val () = (resetFfiInfo (); Sql.sqlcacheMode := true) val file' = addFlushing (addChecking (inlineSql file)) val () = Sql.sqlcacheMode := false |