Mercurial > urweb
comparison src/sqlcache.sml @ 2234:2f7ed04332a0
Progress on LRU cache but still more known bugs to fix.
author | Ziv Scully <ziv@mit.edu> |
---|---|
date | Sun, 28 Jun 2015 12:46:51 -0700 |
parents | af1585e7d645 |
children | 0aae15c2a05a |
comparison
equal
deleted
inserted
replaced
2233:af1585e7d645 | 2234:2f7ed04332a0 |
---|---|
37 in | 37 in |
38 fn (m, f) => Settings.isEffectful (m, f) | 38 fn (m, f) => Settings.isEffectful (m, f) |
39 andalso not (m = "Basis" andalso SS.member (fs, f)) | 39 andalso not (m = "Basis" andalso SS.member (fs, f)) |
40 end | 40 end |
41 | 41 |
42 val cache = ref ToyCache.cache | 42 val cache = ref LruCache.cache |
43 fun setCache c = cache := c | 43 fun setCache c = cache := c |
44 fun getCache () = !cache | 44 fun getCache () = !cache |
45 | 45 |
46 | 46 |
47 (* Effect analysis. *) | 47 (* Effect analysis. *) |
50 fun effectful doPrint (effs : IS.set) (inFunction : bool) (bound : int) : exp -> bool = | 50 fun effectful doPrint (effs : IS.set) (inFunction : bool) (bound : int) : exp -> bool = |
51 (* If result is true, expression is definitely effectful. If result is | 51 (* If result is true, expression is definitely effectful. If result is |
52 false, then expression is definitely not effectful if effs is fully | 52 false, then expression is definitely not effectful if effs is fully |
53 populated. The intended pattern is to use this a number of times equal | 53 populated. The intended pattern is to use this a number of times equal |
54 to the number of declarations in a file, Bellman-Ford style. *) | 54 to the number of declarations in a file, Bellman-Ford style. *) |
55 (* TODO: make incrementing of bound less janky, probably by using [MonoUtil] | 55 (* TODO: make incrementing of the number of bound variables cleaner, |
56 instead of all this. *) | 56 probably by using [MonoUtil] instead of all this. *) |
57 let | 57 let |
58 (* DEBUG: remove printing when done. *) | 58 (* DEBUG: remove printing when done. *) |
59 fun tru msg = if doPrint then (print (msg ^ "\n"); true) else true | 59 fun tru msg = if doPrint then (print (msg ^ "\n"); true) else true |
60 val rec eff' = | 60 val rec eff' = |
61 (* ASK: is there a better way? *) | 61 (* ASK: is there a better way? *) |
136 end | 136 end |
137 | 137 |
138 | 138 |
139 (* Boolean formula normalization. *) | 139 (* Boolean formula normalization. *) |
140 | 140 |
141 datatype normalForm = Cnf | Dnf | 141 datatype junctionType = Conj | Disj |
142 | 142 |
143 datatype 'atom formula = | 143 datatype 'atom formula = |
144 Atom of 'atom | 144 Atom of 'atom |
145 | Negate of 'atom formula | 145 | Negate of 'atom formula |
146 | Combo of normalForm * 'atom formula list | 146 | Combo of junctionType * 'atom formula list |
147 | 147 |
148 val flipNf = fn Cnf => Dnf | Dnf => Cnf | 148 val flipJt = fn Conj => Disj | Disj => Conj |
149 | 149 |
150 fun bind xs f = List.concat (map f xs) | 150 fun bind 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 [] => [[]] |
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 flipNf 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 (n, fs) => |
165 Combo (n, List.foldr (fn (f, acc) => | 165 Combo (n, List.foldr (fn (f, acc) => |
166 case f of | 166 case f of |
168 | _ => f :: acc) | 168 | _ => f :: acc) |
169 [] | 169 [] |
170 (map flatten fs)) | 170 (map flatten fs)) |
171 | f => f | 171 | f => f |
172 | 172 |
173 fun normalize' (negate : 'atom -> 'atom) (norm : normalForm) = | 173 fun normalize' (negate : 'atom -> 'atom) (junc : junctionType) = |
174 fn Atom x => [[x]] | 174 fn Atom x => [[x]] |
175 | Negate f => map (map negate) (normalize' negate (flipNf norm) f) | 175 | Negate f => map (map negate) (normalize' negate (flipJt junc) f) |
176 | Combo (n, fs) => | 176 | Combo (j, fs) => |
177 let | 177 let |
178 val fss = bind fs (normalize' negate n) | 178 val fss = bind fs (normalize' negate j) |
179 in | 179 in |
180 if n = norm then fss else cartesianProduct fss | 180 if j = junc then fss else cartesianProduct fss |
181 end | 181 end |
182 | 182 |
183 fun normalize negate norm = normalize' negate norm o flatten o pushNegate negate false | 183 fun normalize negate junc = normalize' negate junc o flatten o pushNegate negate false |
184 | 184 |
185 fun mapFormula mf = | 185 fun mapFormula mf = |
186 fn Atom x => Atom (mf x) | 186 fn Atom x => Atom (mf x) |
187 | Negate f => Negate (mapFormula mf f) | 187 | Negate f => Negate (mapFormula mf f) |
188 | Combo (n, fs) => Combo (n, map (mapFormula mf) fs) | 188 | Combo (n, fs) => Combo (n, map (mapFormula mf) fs) |
198 QueryArg of int | 198 QueryArg of int |
199 | DmlRel of int | 199 | DmlRel of int |
200 | Prim of Prim.t | 200 | Prim of Prim.t |
201 | Field of string * string | 201 | Field of string * string |
202 | 202 |
203 val equalAtomExp = | |
204 let | |
205 val isEqual = fn EQUAL => true | _ => false | |
206 in | |
207 fn (QueryArg n1, QueryArg n2) => n1 = n2 | |
208 | (DmlRel n1, DmlRel n2) => n1 = n2 | |
209 | (Prim p1, Prim p2) => isEqual (Prim.compare (p1, p2)) | |
210 | (Field (t1, f1), Field (t2, f2)) => isEqual (String.compare (t1 ^ "." ^ f1, t2 ^ "." ^ f2)) | |
211 | _ => false | |
212 end | |
213 | |
214 structure AtomExpKey : ORD_KEY = struct | 203 structure AtomExpKey : ORD_KEY = struct |
215 | 204 |
216 type ord_key = atomExp | 205 type ord_key = atomExp |
217 | 206 |
218 val compare = | 207 val compare = |
219 fn (QueryArg n1, QueryArg n2) => Int.compare (n1, n2) | 208 fn (QueryArg n1, QueryArg n2) => Int.compare (n1, n2) |
220 | (QueryArg _, _) => LESS | 209 | (QueryArg _, _) => LESS |
221 | (_, QueryArg _) => GREATER | 210 | (_, QueryArg _) => GREATER |
222 | (DmlRel n1, DmlRel n2) => Int.compare (n1, n2) | 211 | (DmlRel n1, DmlRel n2) => Int.compare (n1, n2) |
223 | (DmlRel _, _) => LESS | 212 | (DmlRel _, _) => LESS |
224 | (_, DmlRel _) => GREATER | 213 | (_, DmlRel _) => GREATER |
225 | (Prim p1, Prim p2) => Prim.compare (p1, p2) | 214 | (Prim p1, Prim p2) => Prim.compare (p1, p2) |
226 | (Prim _, _) => LESS | 215 | (Prim _, _) => LESS |
227 | (_, Prim _) => GREATER | 216 | (_, Prim _) => GREATER |
228 | (Field (t1, f1), Field (t2, f2)) => String.compare (t1 ^ "." ^ f1, t2 ^ "." ^ f2) | 217 | (Field (t1, f1), Field (t2, f2)) => |
218 case String.compare (t1, t2) of | |
219 EQUAL => String.compare (f1, f2) | |
220 | ord => ord | |
229 | 221 |
230 end | 222 end |
231 | 223 |
232 structure UF = UnionFindFn(AtomExpKey) | 224 structure UF = UnionFindFn(AtomExpKey) |
225 | |
233 val conflictMaps : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula | 226 val conflictMaps : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula |
234 * (Sql.cmp * Sql.sqexp * Sql.sqexp) formula | 227 * (Sql.cmp * Sql.sqexp * Sql.sqexp) formula |
235 -> atomExp IM.map list = | 228 -> atomExp IM.map list = |
236 let | 229 let |
237 val toKnownEquality = | 230 val toKnownEquality = |
244 UF.classes | 237 UF.classes |
245 o List.foldl UF.union' UF.empty | 238 o List.foldl UF.union' UF.empty |
246 o List.mapPartial toKnownEquality | 239 o List.mapPartial toKnownEquality |
247 fun addToEqs (eqs, n, e) = | 240 fun addToEqs (eqs, n, e) = |
248 case IM.find (eqs, n) of | 241 case IM.find (eqs, n) of |
249 (* Comparing to a constant seems better? *) | 242 (* Comparing to a constant is probably better than comparing to |
243 a variable? Checking that an existing constant matches a new | |
244 one is handled by [accumulateEqs]. *) | |
250 SOME (Prim _) => eqs | 245 SOME (Prim _) => eqs |
251 | _ => IM.insert (eqs, n, e) | 246 | _ => IM.insert (eqs, n, e) |
252 val accumulateEqs = | 247 val accumulateEqs = |
253 (* [NONE] means we have a contradiction. *) | 248 (* [NONE] means we have a contradiction. *) |
254 fn (_, NONE) => NONE | 249 fn (_, NONE) => NONE |
261 | ((Prim p, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, Prim p)) | 256 | ((Prim p, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, Prim p)) |
262 | ((DmlRel r, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r)) | 257 | ((DmlRel r, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r)) |
263 (* TODO: deal with equalities involving just [DmlRel]s and [Prim]s. | 258 (* TODO: deal with equalities involving just [DmlRel]s and [Prim]s. |
264 This would involve guarding the invalidation with a check for the | 259 This would involve guarding the invalidation with a check for the |
265 relevant comparisons. *) | 260 relevant comparisons. *) |
261 (* DEBUG: remove these print statements. *) | |
262 (* | ((DmlRel r, Prim p), eqso) => (print ("sadness " ^ Int.toString r ^ " = " ^ Prim.toString p ^ "\n"); eqso) *) | |
263 (* | ((Prim p, DmlRel r), eqso) => (print ("sadness " ^ Int.toString r ^ " = " ^ Prim.toString p ^ "\n"); eqso) *) | |
266 | (_, eqso) => eqso | 264 | (_, eqso) => eqso |
267 val eqsOfClass : atomExp list -> atomExp IM.map option = | 265 val eqsOfClass : atomExp list -> atomExp IM.map option = |
268 List.foldl accumulateEqs (SOME IM.empty) | 266 List.foldl accumulateEqs (SOME IM.empty) |
269 o chooseTwos | 267 o chooseTwos |
270 fun toAtomExps rel (cmp, e1, e2) = | 268 fun toAtomExps rel (cmp, e1, e2) = |
273 (* Here [NONE] means unkown. *) | 271 (* Here [NONE] means unkown. *) |
274 fn Sql.SqConst p => SOME (Prim p) | 272 fn Sql.SqConst p => SOME (Prim p) |
275 | Sql.Field tf => SOME (Field tf) | 273 | Sql.Field tf => SOME (Field tf) |
276 | Sql.Inj (EPrim p, _) => SOME (Prim p) | 274 | Sql.Inj (EPrim p, _) => SOME (Prim p) |
277 | Sql.Inj (ERel n, _) => SOME (rel n) | 275 | Sql.Inj (ERel n, _) => SOME (rel n) |
278 (* We can't deal with anything else. *) | 276 (* We can't deal with anything else, e.g., CURRENT_TIMESTAMP |
277 becomes Sql.Unmodeled, which becomes NONE here. *) | |
279 | _ => NONE | 278 | _ => NONE |
280 in | 279 in |
281 (cmp, qa e1, qa e2) | 280 (cmp, qa e1, qa e2) |
282 end | 281 end |
283 fun negateCmp (cmp, e1, e2) = | 282 fun negateCmp (cmp, e1, e2) = |
300 val mergeEqs : (atomExp IntBinaryMap.map option list | 299 val mergeEqs : (atomExp IntBinaryMap.map option list |
301 -> atomExp IntBinaryMap.map option) = | 300 -> atomExp IntBinaryMap.map option) = |
302 List.foldr (fn (SOME eqs, SOME acc) => SOME (IM.unionWith #1 (eqs, acc)) | _ => NONE) | 301 List.foldr (fn (SOME eqs, SOME acc) => SOME (IM.unionWith #1 (eqs, acc)) | _ => NONE) |
303 (SOME IM.empty) | 302 (SOME IM.empty) |
304 fun dnf (fQuery, fDml) = | 303 fun dnf (fQuery, fDml) = |
305 normalize negateCmp Dnf (Combo (Cnf, [markQuery fQuery, markDml fDml])) | 304 normalize negateCmp Disj (Combo (Conj, [markQuery fQuery, markDml fDml])) |
306 in | 305 in |
307 List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf | 306 List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf |
308 end | 307 end |
309 | 308 |
310 val rec sqexpToFormula = | 309 val rec sqexpToFormula = |
311 fn Sql.SqTrue => Combo (Cnf, []) | 310 fn Sql.SqTrue => Combo (Conj, []) |
312 | Sql.SqFalse => Combo (Dnf, []) | 311 | Sql.SqFalse => Combo (Disj, []) |
313 | Sql.SqNot e => Negate (sqexpToFormula e) | 312 | Sql.SqNot e => Negate (sqexpToFormula e) |
314 | Sql.Binop (Sql.RCmp c, e1, e2) => Atom (c, e1, e2) | 313 | Sql.Binop (Sql.RCmp c, e1, e2) => Atom (c, e1, e2) |
315 | Sql.Binop (Sql.RLop l, p1, p2) => Combo (case l of Sql.And => Cnf | Sql.Or => Dnf, | 314 | Sql.Binop (Sql.RLop l, p1, p2) => Combo (case l of Sql.And => Conj | Sql.Or => Disj, |
316 [sqexpToFormula p1, sqexpToFormula p2]) | 315 [sqexpToFormula p1, sqexpToFormula p2]) |
317 (* ASK: any other sqexps that can be props? *) | 316 (* ASK: any other sqexps that can be props? *) |
318 | _ => raise Match | 317 | _ => raise Match |
319 | 318 |
320 fun renameTables tablePairs = | 319 fun renameTables tablePairs = |
330 in | 329 in |
331 mapFormula renameAtom | 330 mapFormula renameAtom |
332 end | 331 end |
333 | 332 |
334 val rec queryToFormula = | 333 val rec queryToFormula = |
335 fn Sql.Query1 {Where = NONE, ...} => Combo (Cnf, []) | 334 fn Sql.Query1 {Where = NONE, ...} => Combo (Conj, []) |
336 | Sql.Query1 {From = tablePairs, Where = SOME e, ...} => | 335 | Sql.Query1 {From = tablePairs, Where = SOME e, ...} => |
337 renameTables tablePairs (sqexpToFormula e) | 336 renameTables tablePairs (sqexpToFormula e) |
338 | Sql.Union (q1, q2) => Combo (Dnf, [queryToFormula q1, queryToFormula q2]) | 337 | Sql.Union (q1, q2) => Combo (Disj, [queryToFormula q1, queryToFormula q2]) |
339 | 338 |
340 fun valsToFormula (table, vals) = | 339 fun valsToFormula (table, vals) = |
341 Combo (Cnf, map (fn (field, v) => Atom (Sql.Eq, Sql.Field (table, field), v)) vals) | 340 Combo (Conj, map (fn (field, v) => Atom (Sql.Eq, Sql.Field (table, field), v)) vals) |
342 | 341 |
343 val rec dmlToFormula = | 342 val rec dmlToFormula = |
344 fn Sql.Insert (table, vals) => valsToFormula (table, vals) | 343 fn Sql.Insert (table, vals) => valsToFormula (table, vals) |
345 | Sql.Delete (table, wher) => renameTables [(table, "T")] (sqexpToFormula wher) | 344 | Sql.Delete (table, wher) => renameTables [(table, "T")] (sqexpToFormula wher) |
346 | Sql.Update (table, vals, wher) => | 345 | Sql.Update (table, vals, wher) => |
352 fn Sql.Field (t, v) => Sql.Field (t, v ^ "*") | 351 fn Sql.Field (t, v) => Sql.Field (t, v ^ "*") |
353 | e => e | 352 | e => e |
354 val mark = mapFormula (fn (cmp, e1, e2) => (cmp, markField e1, markField e2)) | 353 val mark = mapFormula (fn (cmp, e1, e2) => (cmp, markField e1, markField e2)) |
355 in | 354 in |
356 renameTables [(table, "T")] | 355 renameTables [(table, "T")] |
357 (Combo (Dnf, [Combo (Cnf, [fVals, mark fWhere]), | 356 (Combo (Disj, [Combo (Conj, [fVals, mark fWhere]), |
358 Combo (Cnf, [mark fVals, fWhere])])) | 357 Combo (Conj, [mark fVals, fWhere])])) |
359 end | 358 end |
360 | 359 |
361 val rec tablesQuery = | 360 val rec tablesQuery = |
362 fn Sql.Query1 {From = tablePairs, ...} => SS.fromList (map #1 tablePairs) | 361 fn Sql.Query1 {From = tablePairs, ...} => SS.fromList (map #1 tablePairs) |
363 | Sql.Union (q1, q2) => SS.union (tablesQuery q1, tablesQuery q2) | 362 | Sql.Union (q1, q2) => SS.union (tablesQuery q1, tablesQuery q2) |
367 | Sql.Delete (tab, _) => tab | 366 | Sql.Delete (tab, _) => tab |
368 | Sql.Update (tab, _, _) => tab | 367 | Sql.Update (tab, _, _) => tab |
369 | 368 |
370 | 369 |
371 (* Program instrumentation. *) | 370 (* Program instrumentation. *) |
371 | |
372 val varName = | |
373 let | |
374 val varNumber = ref 0 | |
375 in | |
376 fn s => (varNumber := !varNumber + 1; s ^ Int.toString (!varNumber)) | |
377 end | |
372 | 378 |
373 val {check, store, flush, ...} = getCache () | 379 val {check, store, flush, ...} = getCache () |
374 | 380 |
375 val dummyLoc = ErrorMsg.dummySpan | 381 val dummyLoc = ErrorMsg.dummySpan |
376 | 382 |
410 val store = (store (i, argsInc, urlifiedRel0), dummyLoc) | 416 val store = (store (i, argsInc, urlifiedRel0), dummyLoc) |
411 val rel0 = (ERel 0, loc) | 417 val rel0 = (ERel 0, loc) |
412 in | 418 in |
413 ECase (check, | 419 ECase (check, |
414 [((PNone stringTyp, loc), | 420 [((PNone stringTyp, loc), |
415 (ELet ("q", resultTyp, query, (ESeq (store, rel0), loc)), loc)), | 421 (ELet (varName "q", resultTyp, query, (ESeq (store, rel0), loc)), loc)), |
416 ((PSome (stringTyp, (PVar ("hit", stringTyp), loc)), loc), | 422 ((PSome (stringTyp, (PVar (varName "hit", stringTyp), loc)), loc), |
417 (* Boolean is false because we're not unurlifying from a cookie. *) | 423 (* Boolean is false because we're not unurlifying from a cookie. *) |
418 (EUnurlify (rel0, resultTyp, false), loc))], | 424 (EUnurlify (rel0, resultTyp, false), loc))], |
419 {disc = stringTyp, result = resultTyp}) | 425 {disc = stringTyp, result = resultTyp}) |
420 end | 426 end |
421 | 427 |
452 | Sql.String s => (strcat (stringExp s, qText), newVars)) | 458 | Sql.String s => (strcat (stringExp s, qText), newVars)) |
453 (stringExp "", []) | 459 (stringExp "", []) |
454 chunks | 460 chunks |
455 fun wrapLets e' = | 461 fun wrapLets e' = |
456 (* Important that this is foldl (to oppose foldr above). *) | 462 (* Important that this is foldl (to oppose foldr above). *) |
457 List.foldl (fn (v, e') => ELet ("sqlArg", stringTyp, v, (e', loc))) | 463 List.foldl (fn (v, e') => ELet (varName "sqlArg", stringTyp, v, (e', loc))) |
458 e' | 464 e' |
459 newVariables | 465 newVariables |
460 val numArgs = length newVariables | 466 val numArgs = length newVariables |
461 in | 467 in |
462 (newText, wrapLets, numArgs) | 468 (newText, wrapLets, numArgs) |
480 body = body, | 486 body = body, |
481 tables = tables, | 487 tables = tables, |
482 exps = exps}, | 488 exps = exps}, |
483 dummyLoc) | 489 dummyLoc) |
484 val (EQuery {query = queryText, ...}, _) = queryExp | 490 val (EQuery {query = queryText, ...}, _) = queryExp |
491 (* DEBUG: we can remove the following line at some point. *) | |
485 val () = Print.preface ("sqlcache> ", (MonoPrint.p_exp MonoEnv.empty queryText)) | 492 val () = Print.preface ("sqlcache> ", (MonoPrint.p_exp MonoEnv.empty queryText)) |
486 val args = List.tabulate (numArgs, fn n => (ERel n, dummyLoc)) | 493 val args = List.tabulate (numArgs, fn n => (ERel n, dummyLoc)) |
487 fun bind x f = Option.mapPartial f x | 494 fun bind x f = Option.mapPartial f x |
488 fun guard b x = if b then x else NONE | 495 fun guard b x = if b then x else NONE |
489 (* DEBUG: set first boolean argument to true to turn on printing. *) | 496 (* DEBUG: set first boolean argument to true to turn on printing. *) |
528 inv (numArgs - 1) | 535 inv (numArgs - 1) |
529 end | 536 end |
530 (* Tests if [ys] makes [xs] a redundant cache invalidation. [NONE] here | 537 (* Tests if [ys] makes [xs] a redundant cache invalidation. [NONE] here |
531 represents unknown, which means a wider invalidation. *) | 538 represents unknown, which means a wider invalidation. *) |
532 val rec madeRedundantBy : atomExp option list * atomExp option list -> bool = | 539 val rec madeRedundantBy : atomExp option list * atomExp option list -> bool = |
533 fn ([], []) => true | 540 fn ([], []) => (print "hey!\n"; true) |
534 | (NONE :: xs, _ :: ys) => madeRedundantBy (xs, ys) | 541 | (NONE :: xs, _ :: ys) => madeRedundantBy (xs, ys) |
535 | (SOME x :: xs, SOME y :: ys) => equalAtomExp (x, y) andalso madeRedundantBy (xs, ys) | 542 | (SOME x :: xs, SOME y :: ys) => (case AtomExpKey.compare (x, y) of |
543 EQUAL => madeRedundantBy (xs, ys) | |
544 | _ => false) | |
536 | _ => false | 545 | _ => false |
537 fun removeRedundant' (xss, yss) = | 546 fun removeRedundant' (xss, yss) = |
538 case xss of | 547 case xss of |
539 [] => yss | 548 [] => yss |
540 | xs :: xss' => | 549 | xs :: xss' => |