summaryrefslogtreecommitdiff
path: root/src/sqlcache.sml
diff options
context:
space:
mode:
authorGravatar Ziv Scully <ziv@mit.edu>2015-07-05 23:57:28 -0700
committerGravatar Ziv Scully <ziv@mit.edu>2015-07-05 23:57:28 -0700
commit1622d36926c950ed34757dea78edfb4cd3463578 (patch)
tree9010d5e4b80c82c0db5c981cd6628dad17ccf4cc /src/sqlcache.sml
parentfdcc98562df1f37600d9b944371adcb08c3741f0 (diff)
Fix bug in redundancy checking and use finer formula for UPDATE statements.
Diffstat (limited to 'src/sqlcache.sml')
-rw-r--r--src/sqlcache.sml86
1 files changed, 33 insertions, 53 deletions
diff --git a/src/sqlcache.sml b/src/sqlcache.sml
index f06a9085..d5f6c1c0 100644
--- a/src/sqlcache.sml
+++ b/src/sqlcache.sml
@@ -174,28 +174,12 @@ val rec flatten =
(map flatten fs))
| f => f
-fun normPlz (junc : junctionType) =
- fn Atom x => [[x]]
- | Combo (j, fs) =>
- let
- val fss = map (normPlz junc) fs
- in
- if j = junc
- then List.concat fss
- else map List.concat (cartesianProduct fss)
- end
- (* Excluded by pushNegate. *)
- | Negate _ => raise Match
-
-fun normalize' ((simplifyLists, simplifyAtoms, negate)
- : ('a list list -> 'a list list)
- * ('a list -> 'a list)
- * ('a -> 'a))
+fun normalize' (simplify : 'a list list -> 'a list list)
+ (negate : 'a -> 'a)
(junc : junctionType) =
let
- fun simplify junc = simplifyLists o map simplifyAtoms
fun norm junc =
- simplify junc
+ simplify
o (fn Atom x => [[x]]
| Negate f => map (map negate) (norm (flipJt junc) f)
| Combo (j, fs) =>
@@ -210,8 +194,8 @@ fun normalize' ((simplifyLists, simplifyAtoms, negate)
norm junc
end
-fun normalize (simplifyLists, simplifyAtoms, negate, junc) =
- (normalize' (simplifyLists, simplifyAtoms, negate) junc)
+fun normalize simplify negate junc =
+ normalize' simplify negate junc
o flatten
o pushNegate negate false
@@ -247,7 +231,7 @@ structure CmpKey : ORD_KEY = struct
end
-
+(*
functor ListKeyFn (K : ORD_KEY) : ORD_KEY = struct
type ord_key = K.ord_key list
@@ -261,6 +245,7 @@ functor ListKeyFn (K : ORD_KEY) : ORD_KEY = struct
| ord => ord)
end
+*)
functor OptionKeyFn (K : ORD_KEY) : ORD_KEY = struct
@@ -294,6 +279,20 @@ val rec chooseTwos : 'a list -> ('a * 'a) list =
fn [] => []
| x :: ys => map (fn y => (x, y)) ys @ chooseTwos ys
+fun removeRedundant madeRedundantBy zs =
+ let
+ fun removeRedundant' (xs, ys) =
+ case xs of
+ [] => ys
+ | x :: xs' =>
+ removeRedundant' (xs',
+ if List.exists (fn y => madeRedundantBy (x, y)) (xs' @ ys)
+ then ys
+ else x :: ys)
+ in
+ removeRedundant' (zs, [])
+ end
+
datatype atomExp =
QueryArg of int
| DmlRel of int
@@ -329,7 +328,7 @@ structure ConflictMaps = struct
structure J = OptionKeyFn(AtomExpKey)
structure K = OptionKeyFn(AtomExpKey))
structure TS = BinarySetFn(TK)
- structure TLS = BinarySetFn(ListKeyFn(TK))
+ (* structure TLS = BinarySetFn(ListKeyFn(TK)) *)
val toKnownEquality =
(* [NONE] here means unkown. Anything that isn't a comparison between two
@@ -365,9 +364,6 @@ structure ConflictMaps = struct
(* 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 =
@@ -416,20 +412,12 @@ structure ConflictMaps = struct
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 simplifyAtoms xs = TS.listItems (TS.addList (TS.empty, xs))
+ val simplify =
+ map TS.listItems
+ o removeRedundant (fn (x, y) => TS.isSubset (y, x))
+ o map (fn xs => TS.addList (TS.empty, xs))
in
- normalize (simplifyLists, simplifyAtoms, negateCmp, Disj)
- (Combo (Conj, [markQuery fQuery, markDml fDml]))
+ normalize simplify negateCmp Disj (Combo (Conj, [markQuery fQuery, markDml fDml]))
end
val conflictMaps = List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf
@@ -478,9 +466,12 @@ val rec dmlToFormula =
let
val fWhere = sqexpToFormula wher
val fVals = valsToFormula (table, vals)
+ val modifiedFields = SS.addList (SS.empty, map #1 vals)
(* TODO: don't use field name hack. *)
val markField =
- fn Sql.Field (t, v) => Sql.Field (t, v ^ "*")
+ fn e as Sql.Field (t, v) => if SS.member (modifiedFields, v)
+ then Sql.Field (t, v ^ "'")
+ else e
| e => e
val mark = mapFormula (fn (cmp, e1, e2) => (cmp, markField e1, markField e2))
in
@@ -673,28 +664,17 @@ structure Invalidations = struct
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)
+ | (_ :: xs, NONE :: 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 removeRedundant madeRedundantBy
o map (eqsToInvalidation numArgs)
o eqss)
(query, dml)