Mercurial > urweb

annotate src/sqlcache.sml @ 2237:e79ef5792c8b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix bug in redundancy checking and use finer formula for UPDATE statements.
author Ziv Scully <ziv@mit.edu>
date Sun, 05 Jul 2015 23:57:28 -0700
parents fab8c1f131a5
children f70a91f7810d
rev   line source
ziv@2235 1 structure Sqlcache (* DEBUG: add back :> SQLCACHE. *) = struct
ziv@2209 2
ziv@2209 3 open Mono
ziv@2209 4
ziv@2209 5 structure IS = IntBinarySet
ziv@2209 6 structure IM = IntBinaryMap
ziv@2213 7 structure SK = struct type ord_key = string val compare = String.compare end
ziv@2213 8 structure SS = BinarySetFn(SK)
ziv@2213 9 structure SM = BinaryMapFn(SK)
ziv@2213 10 structure SIMM = MultimapFn(structure KeyMap = SM structure ValSet = IS)
ziv@2209 11
ziv@2216 12 (* Filled in by [cacheWrap] during [Sqlcache]. *)
ziv@2213 13 val ffiInfo : {index : int, params : int} list ref = ref []
ziv@2209 14
ziv@2227 15 fun resetFfiInfo () = ffiInfo := []
ziv@2227 16
ziv@2213 17 fun getFfiInfo () = !ffiInfo
ziv@2213 18
ziv@2215 19 (* Some FFIs have writing as their only effect, which the caching records. *)
ziv@2215 20 val ffiEffectful =
ziv@2223 21 (* ASK: how can this be less hard-coded? *)
ziv@2215 22 let
ziv@2215 23 val fs = SS.fromList ["htmlifyInt_w",
ziv@2215 24 "htmlifyFloat_w",
ziv@2215 25 "htmlifyString_w",
ziv@2215 26 "htmlifyBool_w",
ziv@2215 27 "htmlifyTime_w",
ziv@2215 28 "attrifyInt_w",
ziv@2215 29 "attrifyFloat_w",
ziv@2215 30 "attrifyString_w",
ziv@2215 31 "attrifyChar_w",
ziv@2215 32 "urlifyInt_w",
ziv@2215 33 "urlifyFloat_w",
ziv@2215 34 "urlifyString_w",
ziv@2215 35 "urlifyBool_w",
ziv@2215 36 "urlifyChannel_w"]
ziv@2215 37 in
ziv@2215 38 fn (m, f) => Settings.isEffectful (m, f)
ziv@2215 39 andalso not (m = "Basis" andalso SS.member (fs, f))
ziv@2215 40 end
ziv@2215 41
ziv@2234 42 val cache = ref LruCache.cache
ziv@2233 43 fun setCache c = cache := c
ziv@2233 44 fun getCache () = !cache
ziv@2233 45
ziv@2215 46
ziv@2215 47 (* Effect analysis. *)
ziv@2215 48
ziv@2216 49 (* Makes an exception for [EWrite] (which is recorded when caching). *)
ziv@2230 50 fun effectful doPrint (effs : IS.set) (inFunction : bool) (bound : int) : exp -> bool =
ziv@2215 51 (* If result is true, expression is definitely effectful. If result is
ziv@2215 52 false, then expression is definitely not effectful if effs is fully
ziv@2215 53 populated. The intended pattern is to use this a number of times equal
ziv@2215 54 to the number of declarations in a file, Bellman-Ford style. *)
ziv@2234 55 (* TODO: make incrementing of the number of bound variables cleaner,
ziv@2234 56 probably by using [MonoUtil] instead of all this. *)
ziv@2215 57 let
ziv@2215 58 (* DEBUG: remove printing when done. *)
ziv@2215 59 fun tru msg = if doPrint then (print (msg ^ "\n"); true) else true
ziv@2215 60 val rec eff' =
ziv@2215 61 (* ASK: is there a better way? *)
ziv@2215 62 fn EPrim _ => false
ziv@2215 63 (* We don't know if local functions have effects when applied. *)
ziv@2215 64 | ERel idx => if inFunction andalso idx >= bound
ziv@2215 65 then tru ("rel" ^ Int.toString idx) else false
ziv@2215 66 | ENamed name => if IS.member (effs, name) then tru "named" else false
ziv@2215 67 | ECon (_, _, NONE) => false
ziv@2215 68 | ECon (_, _, SOME e) => eff e
ziv@2215 69 | ENone _ => false
ziv@2215 70 | ESome (_, e) => eff e
ziv@2215 71 | EFfi (m, f) => if ffiEffectful (m, f) then tru "ffi" else false
ziv@2215 72 | EFfiApp (m, f, _) => if ffiEffectful (m, f) then tru "ffiapp" else false
ziv@2215 73 (* ASK: we're calling functions effectful if they have effects when
ziv@2215 74 applied or if the function expressions themselves have effects.
ziv@2215 75 Is that okay? *)
ziv@2215 76 (* This is okay because the values we ultimately care about aren't
ziv@2215 77 functions, and this is a conservative approximation, anyway. *)
ziv@2215 78 | EApp (eFun, eArg) => effectful doPrint effs true bound eFun orelse eff eArg
ziv@2215 79 | EAbs (_, _, _, e) => effectful doPrint effs inFunction (bound+1) e
ziv@2215 80 | EUnop (_, e) => eff e
ziv@2215 81 | EBinop (_, _, e1, e2) => eff e1 orelse eff e2
ziv@2215 82 | ERecord xs => List.exists (fn (_, e, _) => eff e) xs
ziv@2215 83 | EField (e, _) => eff e
ziv@2215 84 (* If any case could be effectful, consider it effectful. *)
ziv@2215 85 | ECase (e, xs, _) => eff e orelse List.exists (fn (_, e) => eff e) xs
ziv@2215 86 | EStrcat (e1, e2) => eff e1 orelse eff e2
ziv@2215 87 (* ASK: how should we treat these three? *)
ziv@2215 88 | EError _ => tru "error"
ziv@2215 89 | EReturnBlob _ => tru "blob"
ziv@2215 90 | ERedirect _ => tru "redirect"
ziv@2215 91 (* EWrite is a special exception because we record writes when caching. *)
ziv@2215 92 | EWrite _ => false
ziv@2215 93 | ESeq (e1, e2) => eff e1 orelse eff e2
ziv@2215 94 (* TODO: keep context of which local variables aren't effectful? Only
ziv@2215 95 makes a difference for function expressions, though. *)
ziv@2215 96 | ELet (_, _, eBind, eBody) => eff eBind orelse
ziv@2215 97 effectful doPrint effs inFunction (bound+1) eBody
ziv@2215 98 | EClosure (_, es) => List.exists eff es
ziv@2215 99 (* TODO: deal with EQuery. *)
ziv@2215 100 | EQuery _ => tru "query"
ziv@2215 101 | EDml _ => tru "dml"
ziv@2215 102 | ENextval _ => tru "nextval"
ziv@2215 103 | ESetval _ => tru "setval"
ziv@2215 104 | EUnurlify (e, _, _) => eff e
ziv@2215 105 (* ASK: how should we treat this? *)
ziv@2215 106 | EJavaScript _ => tru "javascript"
ziv@2215 107 (* ASK: these are all effectful, right? *)
ziv@2215 108 | ESignalReturn _ => tru "signalreturn"
ziv@2215 109 | ESignalBind _ => tru "signalbind"
ziv@2215 110 | ESignalSource _ => tru "signalsource"
ziv@2215 111 | EServerCall _ => tru "servercall"
ziv@2215 112 | ERecv _ => tru "recv"
ziv@2215 113 | ESleep _ => tru "sleep"
ziv@2215 114 | ESpawn _ => tru "spawn"
ziv@2215 115 and eff = fn (e', _) => eff' e'
ziv@2215 116 in
ziv@2215 117 eff
ziv@2215 118 end
ziv@2215 119
ziv@2215 120 (* TODO: test this. *)
ziv@2215 121 val effectfulMap =
ziv@2215 122 let
ziv@2215 123 fun doVal ((_, name, _, e, _), effMap) =
ziv@2215 124 if effectful false effMap false 0 e
ziv@2215 125 then IS.add (effMap, name)
ziv@2215 126 else effMap
ziv@2215 127 val doDecl =
ziv@2215 128 fn (DVal v, effMap) => doVal (v, effMap)
ziv@2215 129 (* Repeat the list of declarations a number of times equal to its size. *)
ziv@2215 130 | (DValRec vs, effMap) =>
ziv@2215 131 List.foldl doVal effMap (List.concat (List.map (fn _ => vs) vs))
ziv@2215 132 (* ASK: any other cases? *)
ziv@2215 133 | (_, effMap) => effMap
ziv@2215 134 in
ziv@2215 135 MonoUtil.File.fold {typ = #2, exp = #2, decl = doDecl} IS.empty
ziv@2215 136 end
ziv@2215 137
ziv@2215 138
ziv@2216 139 (* Boolean formula normalization. *)
ziv@2216 140
ziv@2234 141 datatype junctionType = Conj | Disj
ziv@2216 142
ziv@2216 143 datatype 'atom formula =
ziv@2216 144 Atom of 'atom
ziv@2216 145 | Negate of 'atom formula
ziv@2234 146 | Combo of junctionType * 'atom formula list
ziv@2216 147
ziv@2234 148 val flipJt = fn Conj => Disj | Disj => Conj
ziv@2216 149
ziv@2236 150 fun concatMap f xs = List.concat (map f xs)
ziv@2216 151
ziv@2216 152 val rec cartesianProduct : 'a list list -> 'a list list =
ziv@2216 153 fn [] => [[]]
ziv@2236 154 | (xs :: xss) => concatMap (fn ys => concatMap (fn x => [x :: ys]) xs)
ziv@2236 155 (cartesianProduct xss)
ziv@2216 156
ziv@2218 157 (* Pushes all negation to the atoms.*)
ziv@2218 158 fun pushNegate (negate : 'atom -> 'atom) (negating : bool) =
ziv@2218 159 fn Atom x => Atom (if negating then negate x else x)
ziv@2218 160 | Negate f => pushNegate negate (not negating) f
ziv@2234 161 | Combo (n, fs) => Combo (if negating then flipJt n else n, map (pushNegate negate negating) fs)
ziv@2218 162
ziv@2218 163 val rec flatten =
ziv@2235 164 fn Combo (_, [f]) => flatten f
ziv@2235 165 | Combo (j, fs) =>
ziv@2235 166 Combo (j, List.foldr (fn (f, acc) =>
ziv@2218 167 case f of
ziv@2235 168 Combo (j', fs') =>
ziv@2235 169 if j = j' orelse length fs' = 1
ziv@2235 170 then fs' @ acc
ziv@2235 171 else f :: acc
ziv@2218 172 | _ => f :: acc)
ziv@2218 173 []
ziv@2218 174 (map flatten fs))
ziv@2218 175 | f => f
ziv@2218 176
ziv@2237 177 fun normalize' (simplify : 'a list list -> 'a list list)
ziv@2237 178 (negate : 'a -> 'a)
ziv@2235 179 (junc : junctionType) =
ziv@2216 180 let
ziv@2235 181 fun norm junc =
ziv@2237 182 simplify
ziv@2235 183 o (fn Atom x => [[x]]
ziv@2235 184 | Negate f => map (map negate) (norm (flipJt junc) f)
ziv@2235 185 | Combo (j, fs) =>
ziv@2235 186 let
ziv@2236 187 val fss = map (norm junc) fs
ziv@2235 188 in
ziv@2236 189 if j = junc
ziv@2236 190 then List.concat fss
ziv@2236 191 else map List.concat (cartesianProduct fss)
ziv@2235 192 end)
ziv@2216 193 in
ziv@2235 194 norm junc
ziv@2216 195 end
ziv@2216 196
ziv@2237 197 fun normalize simplify negate junc =
ziv@2237 198 normalize' simplify negate junc
ziv@2235 199 o flatten
ziv@2235 200 o pushNegate negate false
ziv@2216 201
ziv@2221 202 fun mapFormula mf =
ziv@2221 203 fn Atom x => Atom (mf x)
ziv@2221 204 | Negate f => Negate (mapFormula mf f)
ziv@2235 205 | Combo (j, fs) => Combo (j, map (mapFormula mf) fs)
ziv@2216 206
ziv@2230 207
ziv@2215 208 (* SQL analysis. *)
ziv@2213 209
ziv@2235 210 structure CmpKey : ORD_KEY = struct
ziv@2235 211
ziv@2235 212 type ord_key = Sql.cmp
ziv@2235 213
ziv@2235 214 val compare =
ziv@2235 215 fn (Sql.Eq, Sql.Eq) => EQUAL
ziv@2235 216 | (Sql.Eq, _) => LESS
ziv@2235 217 | (_, Sql.Eq) => GREATER
ziv@2235 218 | (Sql.Ne, Sql.Ne) => EQUAL
ziv@2235 219 | (Sql.Ne, _) => LESS
ziv@2235 220 | (_, Sql.Ne) => GREATER
ziv@2235 221 | (Sql.Lt, Sql.Lt) => EQUAL
ziv@2235 222 | (Sql.Lt, _) => LESS
ziv@2235 223 | (_, Sql.Lt) => GREATER
ziv@2235 224 | (Sql.Le, Sql.Le) => EQUAL
ziv@2235 225 | (Sql.Le, _) => LESS
ziv@2235 226 | (_, Sql.Le) => GREATER
ziv@2235 227 | (Sql.Gt, Sql.Gt) => EQUAL
ziv@2235 228 | (Sql.Gt, _) => LESS
ziv@2235 229 | (_, Sql.Gt) => GREATER
ziv@2235 230 | (Sql.Ge, Sql.Ge) => EQUAL
ziv@2235 231
ziv@2235 232 end
ziv@2235 233
ziv@2237 234 (*
ziv@2235 235 functor ListKeyFn (K : ORD_KEY) : ORD_KEY = struct
ziv@2235 236
ziv@2235 237 type ord_key = K.ord_key list
ziv@2235 238
ziv@2235 239 val rec compare =
ziv@2235 240 fn ([], []) => EQUAL
ziv@2235 241 | ([], _) => LESS
ziv@2235 242 | (_, []) => GREATER
ziv@2235 243 | (x :: xs, y :: ys) => (case K.compare (x, y) of
ziv@2235 244 EQUAL => compare (xs, ys)
ziv@2235 245 | ord => ord)
ziv@2235 246
ziv@2235 247 end
ziv@2237 248 *)
ziv@2235 249
ziv@2235 250 functor OptionKeyFn (K : ORD_KEY) : ORD_KEY = struct
ziv@2235 251
ziv@2235 252 type ord_key = K.ord_key option
ziv@2235 253
ziv@2235 254 val compare =
ziv@2235 255 fn (NONE, NONE) => EQUAL
ziv@2235 256 | (NONE, _) => LESS
ziv@2235 257 | (_, NONE) => GREATER
ziv@2235 258 | (SOME x, SOME y) => K.compare (x, y)
ziv@2235 259
ziv@2235 260 end
ziv@2235 261
ziv@2235 262 functor TripleKeyFn (structure I : ORD_KEY
ziv@2235 263 structure J : ORD_KEY
ziv@2235 264 structure K : ORD_KEY)
ziv@2235 265 : ORD_KEY where type ord_key = I.ord_key * J.ord_key * K.ord_key = struct
ziv@2235 266
ziv@2235 267 type ord_key = I.ord_key * J.ord_key * K.ord_key
ziv@2235 268
ziv@2235 269 fun compare ((i1, j1, k1), (i2, j2, k2)) =
ziv@2235 270 case I.compare (i1, i2) of
ziv@2235 271 EQUAL => (case J.compare (j1, j2) of
ziv@2235 272 EQUAL => K.compare (k1, k2)
ziv@2235 273 | ord => ord)
ziv@2235 274 | ord => ord
ziv@2235 275
ziv@2235 276 end
ziv@2235 277
ziv@2216 278 val rec chooseTwos : 'a list -> ('a * 'a) list =
ziv@2216 279 fn [] => []
ziv@2216 280 | x :: ys => map (fn y => (x, y)) ys @ chooseTwos ys
ziv@2213 281
ziv@2237 282 fun removeRedundant madeRedundantBy zs =
ziv@2237 283 let
ziv@2237 284 fun removeRedundant' (xs, ys) =
ziv@2237 285 case xs of
ziv@2237 286 [] => ys
ziv@2237 287 | x :: xs' =>
ziv@2237 288 removeRedundant' (xs',
ziv@2237 289 if List.exists (fn y => madeRedundantBy (x, y)) (xs' @ ys)
ziv@2237 290 then ys
ziv@2237 291 else x :: ys)
ziv@2237 292 in
ziv@2237 293 removeRedundant' (zs, [])
ziv@2237 294 end
ziv@2237 295
ziv@2216 296 datatype atomExp =
ziv@2216 297 QueryArg of int
ziv@2216 298 | DmlRel of int
ziv@2216 299 | Prim of Prim.t
ziv@2216 300 | Field of string * string
ziv@2216 301
ziv@2216 302 structure AtomExpKey : ORD_KEY = struct
ziv@2216 303
ziv@2234 304 type ord_key = atomExp
ziv@2216 305
ziv@2234 306 val compare =
ziv@2234 307 fn (QueryArg n1, QueryArg n2) => Int.compare (n1, n2)
ziv@2234 308 | (QueryArg _, _) => LESS
ziv@2234 309 | (_, QueryArg _) => GREATER
ziv@2234 310 | (DmlRel n1, DmlRel n2) => Int.compare (n1, n2)
ziv@2234 311 | (DmlRel _, _) => LESS
ziv@2234 312 | (_, DmlRel _) => GREATER
ziv@2234 313 | (Prim p1, Prim p2) => Prim.compare (p1, p2)
ziv@2234 314 | (Prim _, _) => LESS
ziv@2234 315 | (_, Prim _) => GREATER
ziv@2234 316 | (Field (t1, f1), Field (t2, f2)) =>
ziv@2234 317 case String.compare (t1, t2) of
ziv@2234 318 EQUAL => String.compare (f1, f2)
ziv@2234 319 | ord => ord
ziv@2216 320
ziv@2216 321 end
ziv@2216 322
ziv@2216 323 structure UF = UnionFindFn(AtomExpKey)
ziv@2234 324
ziv@2235 325 structure ConflictMaps = struct
ziv@2235 326
ziv@2235 327 structure TK = TripleKeyFn(structure I = CmpKey
ziv@2235 328 structure J = OptionKeyFn(AtomExpKey)
ziv@2235 329 structure K = OptionKeyFn(AtomExpKey))
ziv@2235 330 structure TS = BinarySetFn(TK)
ziv@2237 331 (* structure TLS = BinarySetFn(ListKeyFn(TK)) *)
ziv@2235 332
ziv@2235 333 val toKnownEquality =
ziv@2235 334 (* [NONE] here means unkown. Anything that isn't a comparison between two
ziv@2235 335 knowns shouldn't be used, and simply dropping unused terms is okay in
ziv@2235 336 disjunctive normal form. *)
ziv@2235 337 fn (Sql.Eq, SOME e1, SOME e2) => SOME (e1, e2)
ziv@2235 338 | _ => NONE
ziv@2235 339
ziv@2235 340 val equivClasses : (Sql.cmp * atomExp option * atomExp option) list -> atomExp list list =
ziv@2235 341 UF.classes
ziv@2235 342 o List.foldl UF.union' UF.empty
ziv@2235 343 o List.mapPartial toKnownEquality
ziv@2235 344
ziv@2235 345 fun addToEqs (eqs, n, e) =
ziv@2235 346 case IM.find (eqs, n) of
ziv@2235 347 (* Comparing to a constant is probably better than comparing to a
ziv@2235 348 variable? Checking that existing constants match a new ones is
ziv@2235 349 handled by [accumulateEqs]. *)
ziv@2235 350 SOME (Prim _) => eqs
ziv@2235 351 | _ => IM.insert (eqs, n, e)
ziv@2235 352
ziv@2235 353 val accumulateEqs =
ziv@2235 354 (* [NONE] means we have a contradiction. *)
ziv@2235 355 fn (_, NONE) => NONE
ziv@2235 356 | ((Prim p1, Prim p2), eqso) =>
ziv@2235 357 (case Prim.compare (p1, p2) of
ziv@2235 358 EQUAL => eqso
ziv@2235 359 | _ => NONE)
ziv@2235 360 | ((QueryArg n, Prim p), SOME eqs) => SOME (addToEqs (eqs, n, Prim p))
ziv@2235 361 | ((QueryArg n, DmlRel r), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r))
ziv@2235 362 | ((Prim p, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, Prim p))
ziv@2235 363 | ((DmlRel r, QueryArg n), SOME eqs) => SOME (addToEqs (eqs, n, DmlRel r))
ziv@2235 364 (* TODO: deal with equalities between [DmlRel]s and [Prim]s.
ziv@2235 365 This would involve guarding the invalidation with a check for the
ziv@2235 366 relevant comparisons. *)
ziv@2235 367 | (_, eqso) => eqso
ziv@2235 368
ziv@2235 369 val eqsOfClass : atomExp list -> atomExp IM.map option =
ziv@2235 370 List.foldl accumulateEqs (SOME IM.empty)
ziv@2235 371 o chooseTwos
ziv@2235 372
ziv@2235 373 fun toAtomExps rel (cmp, e1, e2) =
ziv@2235 374 let
ziv@2235 375 val qa =
ziv@2235 376 (* Here [NONE] means unkown. *)
ziv@2235 377 fn Sql.SqConst p => SOME (Prim p)
ziv@2235 378 | Sql.Field tf => SOME (Field tf)
ziv@2235 379 | Sql.Inj (EPrim p, _) => SOME (Prim p)
ziv@2235 380 | Sql.Inj (ERel n, _) => SOME (rel n)
ziv@2235 381 (* We can't deal with anything else, e.g., CURRENT_TIMESTAMP
ziv@2235 382 becomes Sql.Unmodeled, which becomes NONE here. *)
ziv@2235 383 | _ => NONE
ziv@2235 384 in
ziv@2235 385 (cmp, qa e1, qa e2)
ziv@2235 386 end
ziv@2235 387
ziv@2235 388 fun negateCmp (cmp, e1, e2) =
ziv@2235 389 (case cmp of
ziv@2235 390 Sql.Eq => Sql.Ne
ziv@2235 391 | Sql.Ne => Sql.Eq
ziv@2235 392 | Sql.Lt => Sql.Ge
ziv@2235 393 | Sql.Le => Sql.Gt
ziv@2235 394 | Sql.Gt => Sql.Le
ziv@2235 395 | Sql.Ge => Sql.Lt,
ziv@2235 396 e1, e2)
ziv@2235 397
ziv@2235 398 val markQuery : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula ->
ziv@2235 399 (Sql.cmp * atomExp option * atomExp option) formula =
ziv@2235 400 mapFormula (toAtomExps QueryArg)
ziv@2235 401
ziv@2235 402 val markDml : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula ->
ziv@2235 403 (Sql.cmp * atomExp option * atomExp option) formula =
ziv@2235 404 mapFormula (toAtomExps DmlRel)
ziv@2235 405 (* No eqs should have key conflicts because no variable is in two
ziv@2235 406 equivalence classes, so the [#1] could be [#2]. *)
ziv@2235 407
ziv@2235 408 val mergeEqs : (atomExp IntBinaryMap.map option list
ziv@2235 409 -> atomExp IntBinaryMap.map option) =
ziv@2235 410 List.foldr (fn (SOME eqs, SOME acc) => SOME (IM.unionWith #1 (eqs, acc)) | _ => NONE)
ziv@2235 411 (SOME IM.empty)
ziv@2235 412
ziv@2235 413 fun dnf (fQuery, fDml) =
ziv@2235 414 let
ziv@2237 415 val simplify =
ziv@2237 416 map TS.listItems
ziv@2237 417 o removeRedundant (fn (x, y) => TS.isSubset (y, x))
ziv@2237 418 o map (fn xs => TS.addList (TS.empty, xs))
ziv@2235 419 in
ziv@2237 420 normalize simplify negateCmp Disj (Combo (Conj, [markQuery fQuery, markDml fDml]))
ziv@2235 421 end
ziv@2235 422
ziv@2235 423 val conflictMaps = List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf
ziv@2235 424
ziv@2235 425 end
ziv@2235 426
ziv@2235 427 val conflictMaps = ConflictMaps.conflictMaps
ziv@2213 428
ziv@2216 429 val rec sqexpToFormula =
ziv@2234 430 fn Sql.SqTrue => Combo (Conj, [])
ziv@2234 431 | Sql.SqFalse => Combo (Disj, [])
ziv@2216 432 | Sql.SqNot e => Negate (sqexpToFormula e)
ziv@2216 433 | Sql.Binop (Sql.RCmp c, e1, e2) => Atom (c, e1, e2)
ziv@2234 434 | Sql.Binop (Sql.RLop l, p1, p2) => Combo (case l of Sql.And => Conj | Sql.Or => Disj,
ziv@2216 435 [sqexpToFormula p1, sqexpToFormula p2])
ziv@2216 436 (* ASK: any other sqexps that can be props? *)
ziv@2216 437 | _ => raise Match
ziv@2213 438
ziv@2218 439 fun renameTables tablePairs =
ziv@2216 440 let
ziv@2216 441 fun renameString table =
ziv@2216 442 case List.find (fn (_, t) => table = t) tablePairs of
ziv@2216 443 NONE => table
ziv@2216 444 | SOME (realTable, _) => realTable
ziv@2216 445 val renameSqexp =
ziv@2216 446 fn Sql.Field (table, field) => Sql.Field (renameString table, field)
ziv@2216 447 | e => e
ziv@2218 448 fun renameAtom (cmp, e1, e2) = (cmp, renameSqexp e1, renameSqexp e2)
ziv@2216 449 in
ziv@2218 450 mapFormula renameAtom
ziv@2216 451 end
ziv@2218 452
ziv@2218 453 val rec queryToFormula =
ziv@2234 454 fn Sql.Query1 {Where = NONE, ...} => Combo (Conj, [])
ziv@2218 455 | Sql.Query1 {From = tablePairs, Where = SOME e, ...} =>
ziv@2218 456 renameTables tablePairs (sqexpToFormula e)
ziv@2234 457 | Sql.Union (q1, q2) => Combo (Disj, [queryToFormula q1, queryToFormula q2])
ziv@2216 458
ziv@2218 459 fun valsToFormula (table, vals) =
ziv@2234 460 Combo (Conj, map (fn (field, v) => Atom (Sql.Eq, Sql.Field (table, field), v)) vals)
ziv@2218 461
ziv@2216 462 val rec dmlToFormula =
ziv@2221 463 fn Sql.Insert (table, vals) => valsToFormula (table, vals)
ziv@2218 464 | Sql.Delete (table, wher) => renameTables [(table, "T")] (sqexpToFormula wher)
ziv@2218 465 | Sql.Update (table, vals, wher) =>
ziv@2218 466 let
ziv@2221 467 val fWhere = sqexpToFormula wher
ziv@2221 468 val fVals = valsToFormula (table, vals)
ziv@2237 469 val modifiedFields = SS.addList (SS.empty, map #1 vals)
ziv@2221 470 (* TODO: don't use field name hack. *)
ziv@2221 471 val markField =
ziv@2237 472 fn e as Sql.Field (t, v) => if SS.member (modifiedFields, v)
ziv@2237 473 then Sql.Field (t, v ^ "'")
ziv@2237 474 else e
ziv@2221 475 | e => e
ziv@2221 476 val mark = mapFormula (fn (cmp, e1, e2) => (cmp, markField e1, markField e2))
ziv@2218 477 in
ziv@2218 478 renameTables [(table, "T")]
ziv@2234 479 (Combo (Disj, [Combo (Conj, [fVals, mark fWhere]),
ziv@2234 480 Combo (Conj, [mark fVals, fWhere])]))
ziv@2218 481 end
ziv@2213 482
ziv@2213 483 val rec tablesQuery =
ziv@2216 484 fn Sql.Query1 {From = tablePairs, ...} => SS.fromList (map #1 tablePairs)
ziv@2216 485 | Sql.Union (q1, q2) => SS.union (tablesQuery q1, tablesQuery q2)
ziv@2213 486
ziv@2213 487 val tableDml =
ziv@2216 488 fn Sql.Insert (tab, _) => tab
ziv@2216 489 | Sql.Delete (tab, _) => tab
ziv@2216 490 | Sql.Update (tab, _, _) => tab
ziv@2213 491
ziv@2213 492
ziv@2213 493 (* Program instrumentation. *)
ziv@2213 494
ziv@2234 495 val varName =
ziv@2234 496 let
ziv@2234 497 val varNumber = ref 0
ziv@2234 498 in
ziv@2234 499 fn s => (varNumber := !varNumber + 1; s ^ Int.toString (!varNumber))
ziv@2234 500 end
ziv@2234 501
ziv@2233 502 val {check, store, flush, ...} = getCache ()
ziv@2233 503
ziv@2230 504 val dummyLoc = ErrorMsg.dummySpan
ziv@2216 505
ziv@2230 506 fun stringExp s = (EPrim (Prim.String (Prim.Normal, s)), dummyLoc)
ziv@2230 507
ziv@2230 508 val stringTyp = (TFfi ("Basis", "string"), dummyLoc)
ziv@2213 509
ziv@2213 510 val sequence =
ziv@2213 511 fn (exp :: exps) =>
ziv@2213 512 let
ziv@2230 513 val loc = dummyLoc
ziv@2213 514 in
ziv@2213 515 List.foldl (fn (e', seq) => ESeq ((seq, loc), (e', loc))) exp exps
ziv@2213 516 end
ziv@2213 517 | _ => raise Match
ziv@2213 518
ziv@2215 519 (* Always increments negative indices because that's what we need later. *)
ziv@2215 520 fun incRelsBound bound inc =
ziv@2215 521 MonoUtil.Exp.mapB
ziv@2215 522 {typ = fn x => x,
ziv@2215 523 exp = fn level =>
ziv@2215 524 (fn ERel n => ERel (if n >= level orelse n < 0 then n + inc else n)
ziv@2215 525 | x => x),
ziv@2215 526 bind = fn (level, MonoUtil.Exp.RelE _) => level + 1 | (level, _) => level}
ziv@2215 527 bound
ziv@2215 528
ziv@2215 529 val incRels = incRelsBound 0
ziv@2213 530
ziv@2223 531 fun cacheWrap (query, i, urlifiedRel0, resultTyp, args) =
ziv@2213 532 let
ziv@2223 533 val () = ffiInfo := {index = i, params = length args} :: !ffiInfo
ziv@2230 534 val loc = dummyLoc
ziv@2223 535 (* We ensure before this step that all arguments aren't effectful.
ziv@2227 536 by turning them into local variables as needed. *)
ziv@2230 537 val argsInc = map (incRels 1) args
ziv@2233 538 val check = (check (i, args), dummyLoc)
ziv@2233 539 val store = (store (i, argsInc, urlifiedRel0), dummyLoc)
ziv@2223 540 val rel0 = (ERel 0, loc)
ziv@2213 541 in
ziv@2223 542 ECase (check,
ziv@2223 543 [((PNone stringTyp, loc),
ziv@2234 544 (ELet (varName "q", resultTyp, query, (ESeq (store, rel0), loc)), loc)),
ziv@2234 545 ((PSome (stringTyp, (PVar (varName "hit", stringTyp), loc)), loc),
ziv@2223 546 (* Boolean is false because we're not unurlifying from a cookie. *)
ziv@2223 547 (EUnurlify (rel0, resultTyp, false), loc))],
ziv@2223 548 {disc = stringTyp, result = resultTyp})
ziv@2213 549 end
ziv@2213 550
ziv@2213 551 fun fileMapfold doExp file start =
ziv@2213 552 case MonoUtil.File.mapfold {typ = Search.return2,
ziv@2213 553 exp = fn x => (fn s => Search.Continue (doExp x s)),
ziv@2213 554 decl = Search.return2} file start of
ziv@2213 555 Search.Continue x => x
ziv@2213 556 | Search.Return _ => raise Match
ziv@2213 557
ziv@2213 558 fun fileMap doExp file = #1 (fileMapfold (fn x => fn _ => (doExp x, ())) file ())
ziv@2213 559
ziv@2221 560 fun factorOutNontrivial text =
ziv@2221 561 let
ziv@2230 562 val loc = dummyLoc
ziv@2221 563 fun strcat (e1, e2) = (EStrcat (e1, e2), loc)
ziv@2221 564 val chunks = Sql.chunkify text
ziv@2221 565 val (newText, newVariables) =
ziv@2221 566 (* Important that this is foldr (to oppose foldl below). *)
ziv@2221 567 List.foldr
ziv@2221 568 (fn (chunk, (qText, newVars)) =>
ziv@2221 569 (* Variable bound to the head of newBs will have the lowest index. *)
ziv@2221 570 case chunk of
ziv@2221 571 Sql.Exp (e as (EPrim _, _)) => (strcat (e, qText), newVars)
ziv@2221 572 | Sql.Exp e =>
ziv@2221 573 let
ziv@2221 574 val n = length newVars
ziv@2221 575 in
ziv@2221 576 (* This is the (n + 1)th new variable, so there are
ziv@2221 577 already n new variables bound, so we increment
ziv@2221 578 indices by n. *)
ziv@2221 579 (strcat ((ERel (~(n+1)), loc), qText), incRels n e :: newVars)
ziv@2221 580 end
ziv@2221 581 | Sql.String s => (strcat (stringExp s, qText), newVars))
ziv@2221 582 (stringExp "", [])
ziv@2221 583 chunks
ziv@2221 584 fun wrapLets e' =
ziv@2221 585 (* Important that this is foldl (to oppose foldr above). *)
ziv@2234 586 List.foldl (fn (v, e') => ELet (varName "sqlArg", stringTyp, v, (e', loc)))
ziv@2221 587 e'
ziv@2221 588 newVariables
ziv@2221 589 val numArgs = length newVariables
ziv@2221 590 in
ziv@2221 591 (newText, wrapLets, numArgs)
ziv@2221 592 end
ziv@2221 593
ziv@2215 594 fun addChecking file =
ziv@2213 595 let
ziv@2223 596 fun doExp (queryInfo as (tableToIndices, indexToQueryNumArgs, index)) =
ziv@2223 597 fn e' as EQuery {query = origQueryText,
ziv@2223 598 sqlcacheInfo = urlifiedRel0,
ziv@2223 599 state = resultTyp,
ziv@2223 600 initial, body, tables, exps} =>
ziv@2213 601 let
ziv@2221 602 val (newQueryText, wrapLets, numArgs) = factorOutNontrivial origQueryText
ziv@2215 603 (* Increment once for each new variable just made. *)
ziv@2221 604 val queryExp = incRels numArgs
ziv@2215 605 (EQuery {query = newQueryText,
ziv@2223 606 sqlcacheInfo = urlifiedRel0,
ziv@2223 607 state = resultTyp,
ziv@2215 608 initial = initial,
ziv@2215 609 body = body,
ziv@2215 610 tables = tables,
ziv@2223 611 exps = exps},
ziv@2230 612 dummyLoc)
ziv@2215 613 val (EQuery {query = queryText, ...}, _) = queryExp
ziv@2235 614 (* DEBUG *)
ziv@2221 615 val () = Print.preface ("sqlcache> ", (MonoPrint.p_exp MonoEnv.empty queryText))
ziv@2230 616 val args = List.tabulate (numArgs, fn n => (ERel n, dummyLoc))
ziv@2213 617 fun bind x f = Option.mapPartial f x
ziv@2215 618 fun guard b x = if b then x else NONE
ziv@2215 619 (* DEBUG: set first boolean argument to true to turn on printing. *)
ziv@2215 620 fun safe bound = not o effectful true (effectfulMap file) false bound
ziv@2213 621 val attempt =
ziv@2213 622 (* Ziv misses Haskell's do notation.... *)
ziv@2215 623 guard (safe 0 queryText andalso safe 0 initial andalso safe 2 body) (
ziv@2216 624 bind (Sql.parse Sql.query queryText) (fn queryParsed =>
ziv@2223 625 SOME (wrapLets (cacheWrap (queryExp, index, urlifiedRel0, resultTyp, args)),
ziv@2218 626 (SS.foldr (fn (tab, qi) => SIMM.insert (qi, tab, index))
ziv@2218 627 tableToIndices
ziv@2218 628 (tablesQuery queryParsed),
ziv@2223 629 IM.insert (indexToQueryNumArgs, index, (queryParsed, numArgs)),
ziv@2223 630 index + 1))))
ziv@2213 631 in
ziv@2213 632 case attempt of
ziv@2213 633 SOME pair => pair
ziv@2213 634 | NONE => (e', queryInfo)
ziv@2213 635 end
ziv@2213 636 | e' => (e', queryInfo)
ziv@2213 637 in
ziv@2223 638 fileMapfold (fn exp => fn state => doExp state exp) file (SIMM.empty, IM.empty, 0)
ziv@2213 639 end
ziv@2213 640
ziv@2235 641 structure Invalidations = struct
ziv@2235 642
ziv@2235 643 val loc = dummyLoc
ziv@2235 644
ziv@2235 645 val optionAtomExpToExp =
ziv@2235 646 fn NONE => (ENone stringTyp, loc)
ziv@2235 647 | SOME e => (ESome (stringTyp,
ziv@2235 648 (case e of
ziv@2235 649 DmlRel n => ERel n
ziv@2235 650 | Prim p => EPrim p
ziv@2235 651 (* TODO: make new type containing only these two. *)
ziv@2235 652 | _ => raise Match,
ziv@2235 653 loc)),
ziv@2235 654 loc)
ziv@2235 655
ziv@2235 656 fun eqsToInvalidation numArgs eqs =
ziv@2235 657 let
ziv@2235 658 fun inv n = if n < 0 then [] else IM.find (eqs, n) :: inv (n - 1)
ziv@2235 659 in
ziv@2235 660 inv (numArgs - 1)
ziv@2235 661 end
ziv@2235 662
ziv@2235 663 (* Tests if [ys] makes [xs] a redundant cache invalidation. [NONE] here
ziv@2235 664 represents unknown, which means a wider invalidation. *)
ziv@2235 665 val rec madeRedundantBy : atomExp option list * atomExp option list -> bool =
ziv@2235 666 fn ([], []) => true
ziv@2237 667 | (_ :: xs, NONE :: ys) => madeRedundantBy (xs, ys)
ziv@2235 668 | (SOME x :: xs, SOME y :: ys) => (case AtomExpKey.compare (x, y) of
ziv@2235 669 EQUAL => madeRedundantBy (xs, ys)
ziv@2235 670 | _ => false)
ziv@2235 671 | _ => false
ziv@2235 672
ziv@2235 673 fun eqss (query, dml) = conflictMaps (queryToFormula query, dmlToFormula dml)
ziv@2235 674
ziv@2235 675 fun invalidations ((query, numArgs), dml) =
ziv@2235 676 (map (map optionAtomExpToExp)
ziv@2237 677 o removeRedundant madeRedundantBy
ziv@2235 678 o map (eqsToInvalidation numArgs)
ziv@2235 679 o eqss)
ziv@2235 680 (query, dml)
ziv@2235 681
ziv@2235 682 end
ziv@2235 683
ziv@2235 684 val invalidations = Invalidations.invalidations
ziv@2235 685
ziv@2235 686 (* DEBUG *)
ziv@2235 687 val gunk : ((Sql.query * int) * Sql.dml) list ref = ref []
ziv@2216 688
ziv@2223 689 fun addFlushing (file, (tableToIndices, indexToQueryNumArgs, _)) =
ziv@2213 690 let
ziv@2221 691 val flushes = List.concat o
ziv@2233 692 map (fn (i, argss) => map (fn args => flush (i, args)) argss)
ziv@2213 693 val doExp =
ziv@2221 694 fn EDml (origDmlText, failureMode) =>
ziv@2213 695 let
ziv@2221 696 val (newDmlText, wrapLets, numArgs) = factorOutNontrivial origDmlText
ziv@2221 697 val dmlText = incRels numArgs newDmlText
ziv@2221 698 val dmlExp = EDml (dmlText, failureMode)
ziv@2235 699 (* DEBUG *)
ziv@2221 700 val () = Print.preface ("sqlcache> ", (MonoPrint.p_exp MonoEnv.empty dmlText))
ziv@2221 701 val invs =
ziv@2216 702 case Sql.parse Sql.dml dmlText of
ziv@2218 703 SOME dmlParsed =>
ziv@2221 704 map (fn i => (case IM.find (indexToQueryNumArgs, i) of
ziv@2221 705 SOME queryNumArgs =>
ziv@2235 706 (* DEBUG *)
ziv@2235 707 (gunk := (queryNumArgs, dmlParsed) :: !gunk;
ziv@2235 708 (i, invalidations (queryNumArgs, dmlParsed)))
ziv@2221 709 (* TODO: fail more gracefully. *)
ziv@2221 710 | NONE => raise Match))
ziv@2221 711 (SIMM.findList (tableToIndices, tableDml dmlParsed))
ziv@2221 712 (* TODO: fail more gracefully. *)
ziv@2221 713 | NONE => raise Match
ziv@2213 714 in
ziv@2221 715 wrapLets (sequence (flushes invs @ [dmlExp]))
ziv@2213 716 end
ziv@2213 717 | e' => e'
ziv@2213 718 in
ziv@2235 719 (* DEBUG *)
ziv@2235 720 gunk := [];
ziv@2213 721 fileMap doExp file
ziv@2213 722 end
ziv@2213 723
ziv@2221 724 val inlineSql =
ziv@2221 725 let
ziv@2221 726 val doExp =
ziv@2221 727 (* TODO: EQuery, too? *)
ziv@2221 728 (* ASK: should this live in [MonoOpt]? *)
ziv@2221 729 fn EDml ((ECase (disc, cases, {disc = dTyp, ...}), loc), failureMode) =>
ziv@2221 730 let
ziv@2221 731 val newCases = map (fn (p, e) => (p, (EDml (e, failureMode), loc))) cases
ziv@2221 732 in
ziv@2221 733 ECase (disc, newCases, {disc = dTyp, result = (TRecord [], loc)})
ziv@2221 734 end
ziv@2221 735 | e => e
ziv@2221 736 in
ziv@2221 737 fileMap doExp
ziv@2221 738 end
ziv@2221 739
ziv@2213 740 fun go file =
ziv@2213 741 let
ziv@2235 742 (* TODO: do something nicer than [Sql] being in one of two modes. *)
ziv@2227 743 val () = (resetFfiInfo (); Sql.sqlcacheMode := true)
ziv@2221 744 val file' = addFlushing (addChecking (inlineSql file))
ziv@2215 745 val () = Sql.sqlcacheMode := false
ziv@2213 746 in
ziv@2221 747 file'
ziv@2213 748 end
ziv@2213 749
ziv@2209 750 end