Ur/Web: src/sqlcache.sml comparison

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

-:2f7ed04332a0
+:0aae15c2a05a
-structure Sqlcache :> SQLCACHE = struct
+structure Sqlcache (* DEBUG: add back :> SQLCACHE. *) = struct
 open Mono
 structure IS = IntBinarySet
 structure IM = IntBinaryMap
 | Negate of 'atom formula
 | Combo of junctionType * 'atom formula list
 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)
+| (xs :: xss) => listBind (cartesianProduct xss)
-(fn ys => bind xs (fn x => [x :: ys]))
+(fn ys => listBind xs (fn x => [x :: ys]))
 (* Pushes all negation to the atoms.*)
 fun pushNegate (negate : 'atom -> 'atom) (negating : bool) =
 fn Atom x => Atom (if negating then negate x else x)
 | Negate f => pushNegate negate (not negating) f
 | Combo (n, fs) => Combo (if negating then flipJt n else n, map (pushNegate negate negating) fs)
 val rec flatten =
-fn Combo (n, fs) =>
+fn Combo (_, [f]) => flatten f
-Combo (n, List.foldr (fn (f, acc) =>
+| 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) =
+fun normalize' ((simplifyLists, simplifyAtomsConj, simplifyAtomsDisj, negate)
-fn Atom x => [[x]]
+: ('a list list -> 'a list list)
-| Negate f => map (map negate) (normalize' negate (flipJt junc) f)
+* ('a list -> 'a list)
-| Combo (j, fs) =>
+* ('a list -> 'a list)
-let
+* ('a -> 'a))
-val fss = bind fs (normalize' negate j)
+(junc : junctionType) =
-in
+let
-if j = junc then fss else cartesianProduct fss
+fun simplify junc = simplifyLists o map (case junc of
-end
+Conj => simplifyAtomsConj
+| Disj => simplifyAtomsDisj)
-fun normalize negate junc = normalize' negate junc o flatten o pushNegate negate false
+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
+norm junc
+end
+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
 end
 structure UF = UnionFindFn(AtomExpKey)
-val conflictMaps : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula
+structure ConflictMaps = struct
-* (Sql.cmp * Sql.sqexp * Sql.sqexp) formula
--> atomExp IM.map list =
+structure TK = TripleKeyFn(structure I = CmpKey
-let
+structure J = OptionKeyFn(AtomExpKey)
-val toKnownEquality =
+structure K = OptionKeyFn(AtomExpKey))
-(* [NONE] here means unkown. Anything that isn't a comparison between
+structure TS = BinarySetFn(TK)
-two knowns shouldn't be used, and simply dropping unused terms is
+structure TLS = BinarySetFn(ListKeyFn(TK))
-okay in disjunctive normal form. *)
-fn (Sql.Eq, SOME e1, SOME e2) => SOME (e1, e2)
+val toKnownEquality =
-| _ => NONE
+(* [NONE] here means unkown. Anything that isn't a comparison between two
-val equivClasses : (Sql.cmp * atomExp option * atomExp option) list -> atomExp list list =
+knowns shouldn't be used, and simply dropping unused terms is okay in
-UF.classes
+disjunctive normal form. *)
-o List.foldl UF.union' UF.empty
+fn (Sql.Eq, SOME e1, SOME e2) => SOME (e1, e2)
-o List.mapPartial toKnownEquality
+| _ => NONE
-fun addToEqs (eqs, n, e) =
-case IM.find (eqs, n) of
+val equivClasses : (Sql.cmp * atomExp option * atomExp option) list -> atomExp list list =
-(* Comparing to a constant is probably better than comparing to
+UF.classes
-a variable? Checking that an existing constant matches a new
+o List.foldl UF.union' UF.empty
-one is handled by [accumulateEqs]. *)
+o List.mapPartial toKnownEquality
-SOME (Prim _) => eqs
-| _ => IM.insert (eqs, n, e)
+fun addToEqs (eqs, n, e) =
-val accumulateEqs =
+case IM.find (eqs, n) of
-(* [NONE] means we have a contradiction. *)
+(* Comparing to a constant is probably better than comparing to a
-fn (_, NONE) => NONE
+variable? Checking that existing constants match a new ones is
-| ((Prim p1, Prim p2), eqso) =>
+handled by [accumulateEqs]. *)
-(case Prim.compare (p1, p2) of
+SOME (Prim _) => eqs
-EQUAL => eqso
+| _ => IM.insert (eqs, n, e)
-| _ => NONE)
-| ((QueryArg n, Prim p), SOME eqs) => SOME (addToEqs (eqs, n, Prim p))
+val accumulateEqs =
-| ((QueryArg n, DmlRel r), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r))
+(* [NONE] means we have a contradiction. *)
-| ((Prim p, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, Prim p))
+fn (_, NONE) => NONE
-| ((DmlRel r, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r))
+| ((Prim p1, Prim p2), eqso) =>
-(* TODO: deal with equalities involving just [DmlRel]s and [Prim]s.
+(case Prim.compare (p1, p2) of
-This would involve guarding the invalidation with a check for the
+EQUAL => eqso
-relevant comparisons. *)
+| _ => NONE)
-(* DEBUG: remove these print statements. *)
+| ((QueryArg n, Prim p), SOME eqs) => SOME (addToEqs (eqs, n, Prim p))
-(* | ((DmlRel r, Prim p), eqso) => (print ("sadness " ^ Int.toString r ^ " = " ^ Prim.toString p ^ "\n"); eqso) *)
+| ((QueryArg n, DmlRel r), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r))
-(* | ((Prim p, DmlRel r), eqso) => (print ("sadness " ^ Int.toString r ^ " = " ^ Prim.toString p ^ "\n"); eqso) *)
+| ((Prim p, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, Prim p))
-| (_, eqso) => eqso
+| ((DmlRel r, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r))
-val eqsOfClass : atomExp list -> atomExp IM.map option =
+(* TODO: deal with equalities between [DmlRel]s and [Prim]s.
-List.foldl accumulateEqs (SOME IM.empty)
+This would involve guarding the invalidation with a check for the
-o chooseTwos
+relevant comparisons. *)
-fun toAtomExps rel (cmp, e1, e2) =
+(* DEBUG: remove these print statements. *)
-let
+(* | ((DmlRel r, Prim p), eqso) => (print ("sadness " ^ Int.toString r ^ " = " ^ Prim.toString p ^ "\n"); eqso) *)
-val qa =
+(* | ((Prim p, DmlRel r), eqso) => (print ("sadness " ^ Int.toString r ^ " = " ^ Prim.toString p ^ "\n"); eqso) *)
-(* Here [NONE] means unkown. *)
+| (_, eqso) => eqso
-fn Sql.SqConst p => SOME (Prim p)
-| Sql.Field tf => SOME (Field tf)
+val eqsOfClass : atomExp list -> atomExp IM.map option =
-| Sql.Inj (EPrim p, _) => SOME (Prim p)
+List.foldl accumulateEqs (SOME IM.empty)
-| Sql.Inj (ERel n, _) => SOME (rel n)
+o chooseTwos
-(* We can't deal with anything else, e.g., CURRENT_TIMESTAMP
-becomes Sql.Unmodeled, which becomes NONE here. *)
+fun toAtomExps rel (cmp, e1, e2) =
-| _ => NONE
+let
-in
+val qa =
-(cmp, qa e1, qa e2)
+(* Here [NONE] means unkown. *)
-end
+fn Sql.SqConst p => SOME (Prim p)
-fun negateCmp (cmp, e1, e2) =
+| Sql.Field tf => SOME (Field tf)
-(case cmp of
+| Sql.Inj (EPrim p, _) => SOME (Prim p)
-Sql.Eq => Sql.Ne
+| Sql.Inj (ERel n, _) => SOME (rel n)
-| Sql.Ne => Sql.Eq
+(* We can't deal with anything else, e.g., CURRENT_TIMESTAMP
-| Sql.Lt => Sql.Ge
+becomes Sql.Unmodeled, which becomes NONE here. *)
-| Sql.Le => Sql.Gt
+| _ => NONE
-| Sql.Gt => Sql.Le
+in
-| Sql.Ge => Sql.Lt,
+(cmp, qa e1, qa e2)
-e1, e2)
+end
-val markQuery : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula ->
-(Sql.cmp * atomExp option * atomExp option) formula =
+fun negateCmp (cmp, e1, e2) =
-mapFormula (toAtomExps QueryArg)
+(case cmp of
-val markDml : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula ->
+Sql.Eq => Sql.Ne
-(Sql.cmp * atomExp option * atomExp option) formula =
+| Sql.Ne => Sql.Eq
-mapFormula (toAtomExps DmlRel)
+| Sql.Lt => Sql.Ge
-(* No eqs should have key conflicts because no variable is in two
+| Sql.Le => Sql.Gt
-equivalence classes, so the [#1] can be anything. *)
+| Sql.Gt => Sql.Le
-val mergeEqs : (atomExp IntBinaryMap.map option list
+| Sql.Ge => Sql.Lt,
--> atomExp IntBinaryMap.map option) =
+e1, e2)
-List.foldr (fn (SOME eqs, SOME acc) => SOME (IM.unionWith #1 (eqs, acc)) | _ => NONE)
-(SOME IM.empty)
+val markQuery : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula ->
-fun dnf (fQuery, fDml) =
+(Sql.cmp * atomExp option * atomExp option) formula =
-normalize negateCmp Disj (Combo (Conj, [markQuery fQuery, markDml fDml]))
+mapFormula (toAtomExps QueryArg)
-in
-List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf
+val markDml : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula ->
-end
+(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, [])
 | Sql.SqFalse => Combo (Disj, [])
 | Sql.SqNot e => Negate (sqexpToFormula e)
 body = body,
 tables = tables,
 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
 fun guard b x = if b then x else NONE
 (* DEBUG: set first boolean argument to true to turn on printing. *)
 | e' => (e', queryInfo)
 in
 fileMapfold (fn exp => fn state => doExp state exp) file (SIMM.empty, IM.empty, 0)
 end
-fun invalidations ((query, numArgs), dml) =
+structure Invalidations = struct
-let
 val loc = dummyLoc
-val optionAtomExpToExp =
-fn NONE => (ENone stringTyp, loc)
+val optionAtomExpToExp =
-| SOME e => (ESome (stringTyp,
+fn NONE => (ENone stringTyp, loc)
-(case e of
+| SOME e => (ESome (stringTyp,
-DmlRel n => ERel n
+(case e of
-| Prim p => EPrim p
+DmlRel n => ERel n
-(* TODO: make new type containing only these two. *)
+| Prim p => EPrim p
-| _ => raise Match,
+(* TODO: make new type containing only these two. *)
-loc)),
+| _ => raise Match,
-loc)
+loc)),
-fun eqsToInvalidation eqs =
+loc)
-let
-fun inv n = if n < 0 then [] else IM.find (eqs, n) :: inv (n - 1)
+fun eqsToInvalidation numArgs eqs =
-in
+let
-inv (numArgs - 1)
+fun inv n = if n < 0 then [] else IM.find (eqs, n) :: inv (n - 1)
-end
+in
-(* Tests if [ys] makes [xs] a redundant cache invalidation. [NONE] here
+inv (numArgs - 1)
-represents unknown, which means a wider invalidation. *)
+end
-val rec madeRedundantBy : atomExp option list * atomExp option list -> bool =
-fn ([], []) => (print "hey!\n"; true)
+(* Tests if [ys] makes [xs] a redundant cache invalidation. [NONE] here
-| (NONE :: xs, _ :: ys) => madeRedundantBy (xs, ys)
+represents unknown, which means a wider invalidation. *)
-| (SOME x :: xs, SOME y :: ys) => (case AtomExpKey.compare (x, y) of
+val rec madeRedundantBy : atomExp option list * atomExp option list -> bool =
-EQUAL => madeRedundantBy (xs, ys)
+fn ([], []) => true
-| _ => false)
+| (NONE :: xs, _ :: ys) => madeRedundantBy (xs, ys)
-| _ => false
+| (SOME x :: xs, SOME y :: ys) => (case AtomExpKey.compare (x, y) of
-fun removeRedundant' (xss, yss) =
+EQUAL => madeRedundantBy (xs, ys)
-case xss of
+| _ => false)
-[] => yss
+| _ => false
-| xs :: xss' =>
-removeRedundant' (xss',
+fun removeRedundant' (xss, yss) =
-if List.exists (fn ys => madeRedundantBy (xs, ys)) (xss' @ yss)
+case xss of
-then yss
+[] => yss
-else xs :: yss)
+| xs :: xss' =>
-fun removeRedundant xss = removeRedundant' (xss, [])
+removeRedundant' (xss',
-val eqss = conflictMaps (queryToFormula query, dmlToFormula dml)
+if List.exists (fn ys => madeRedundantBy (xs, ys)) (xss' @ yss)
-in
+then yss
-(map (map optionAtomExpToExp) o removeRedundant o map eqsToInvalidation) eqss
+else xs :: yss)
-end
+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
 val flushes = List.concat o
 map (fn (i, argss) => map (fn args => flush (i, args)) argss)
 fn EDml (origDmlText, failureMode) =>
 let
 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))
 (* TODO: fail more gracefully. *)
 | NONE => raise Match
 in
 wrapLets (sequence (flushes invs @ [dmlExp]))
 end
 | e' => e'
 in
+(* DEBUG *)
+gunk := [];
 fileMap doExp file
 end
 val inlineSql =
 let
 fileMap doExp
 end
 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
 in
 file'

Mercurial > urweb

comparison src/sqlcache.sml @ 2235:0aae15c2a05a