summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Ziv Scully <ziv@mit.edu>2015-07-20 23:25:44 -0700
committerGravatar Ziv Scully <ziv@mit.edu>2015-07-20 23:25:44 -0700
commit4ff7cf9503b917dcc8db1de3ba03b513240f7dc8 (patch)
tree21db757c04d6064aee147c73a73f624753871ac1
parent0cfbe4639f076d50f2a3bbc9e6f566a452a43167 (diff)
Use uniform representation of comparisons for better simplification.
-rw-r--r--src/option_key_fn.sml3
-rw-r--r--src/sqlcache.sml56
2 files changed, 38 insertions, 21 deletions
diff --git a/src/option_key_fn.sml b/src/option_key_fn.sml
index ba636d4e..27ba9138 100644
--- a/src/option_key_fn.sml
+++ b/src/option_key_fn.sml
@@ -1,4 +1,5 @@
-functor OptionKeyFn(K : ORD_KEY) : ORD_KEY = struct
+functor OptionKeyFn(K : ORD_KEY)
+ : ORD_KEY where type ord_key = K.ord_key option = struct
type ord_key = K.ord_key option
diff --git a/src/sqlcache.sml b/src/sqlcache.sml
index fae8b5f3..a59f8b55 100644
--- a/src/sqlcache.sml
+++ b/src/sqlcache.sml
@@ -160,10 +160,11 @@ val rec cartesianProduct : 'a list list -> 'a list list =
(cartesianProduct xss)
(* 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 (j, fs) => Combo' (if negating then flipJt j else j, map (pushNegate negate negating) fs)
+fun pushNegate (normalizeAtom : bool * 'atom -> 'atom) (negating : bool) =
+ fn Atom x => Atom' (normalizeAtom (negating, x))
+ | Negate f => pushNegate normalizeAtom (not negating) f
+ | Combo (j, fs) => Combo' (if negating then flipJt j else j,
+ map (pushNegate normalizeAtom negating) fs)
val rec flatten =
fn Combo' (_, [f]) => flatten f
@@ -199,10 +200,10 @@ fun normalize' (simplify : 'a list list -> 'a list list)
norm junc
end
-fun normalize simplify negate junc =
+fun normalize simplify normalizeAtom junc =
normalize' simplify junc
o flatten
- o pushNegate negate false
+ o pushNegate normalizeAtom false
fun mapFormula mf =
fn Atom x => Atom (mf x)
@@ -281,14 +282,16 @@ structure AtomExpKey : ORD_KEY = struct
end
+structure AtomOptionKey = OptionKeyFn(AtomExpKey)
+
structure UF = UnionFindFn(AtomExpKey)
structure ConflictMaps = struct
structure TK = TripleKeyFn(structure I = CmpKey
- structure J = OptionKeyFn(AtomExpKey)
- structure K = OptionKeyFn(AtomExpKey))
- structure TS = BinarySetFn(TK)
+ structure J = AtomOptionKey
+ structure K = AtomOptionKey)
+ structure TS : ORD_SET = BinarySetFn(TK)
val toKnownEquality =
(* [NONE] here means unkown. Anything that isn't a comparison between two
@@ -345,15 +348,28 @@ structure ConflictMaps = struct
(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 negateCmp =
+ fn Sql.Eq => Sql.Ne
+ | Sql.Ne => Sql.Eq
+ | Sql.Lt => Sql.Ge
+ | Sql.Le => Sql.Gt
+ | Sql.Gt => Sql.Le
+ | Sql.Ge => Sql.Lt
+
+ fun normalizeAtom (negating, (cmp, e1, e2)) =
+ (* Restricting to Le/Lt and sorting the expressions in Eq/Ne helps with
+ simplification, where we put the triples in sets. *)
+ case (if negating then negateCmp cmp else cmp) of
+ Sql.Eq => (case AtomOptionKey.compare (e1, e2) of
+ LESS => (Sql.Eq, e2, e1)
+ | _ => (Sql.Eq, e1, e2))
+ | Sql.Ne => (case AtomOptionKey.compare (e1, e2) of
+ LESS => (Sql.Ne, e2, e1)
+ | _ => (Sql.Ne, e1, e2))
+ | Sql.Lt => (Sql.Lt, e1, e2)
+ | Sql.Le => (Sql.Le, e1, e2)
+ | Sql.Gt => (Sql.Lt, e2, e1)
+ | Sql.Ge => (Sql.Le, e2, e1)
val markQuery : (Sql.cmp * Sql.sqexp * Sql.sqexp) formula ->
(Sql.cmp * atomExp option * atomExp option) formula =
@@ -376,7 +392,7 @@ structure ConflictMaps = struct
o map (fn xs => TS.addList (TS.empty, xs))
fun dnf (fQuery, fDml) =
- normalize simplify negateCmp Disj (Combo (Conj, [markQuery fQuery, markDml fDml]))
+ normalize simplify normalizeAtom Disj (Combo (Conj, [markQuery fQuery, markDml fDml]))
val conflictMaps = List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf
@@ -435,7 +451,7 @@ val rec dmlToFormula =
in
renameTables [(table, "T")]
(Combo (Disj, [Combo (Conj, [fVals, mark fWhere]),
- Combo (Conj, [mark fVals, fWhere])]))
+ Combo (Conj, [mark fVals, fWhere])]))
end
val rec tablesQuery =