diff options
author | Ziv Scully <ziv@mit.edu> | 2015-07-20 23:25:44 -0700 |
---|---|---|
committer | Ziv Scully <ziv@mit.edu> | 2015-07-20 23:25:44 -0700 |
commit | 4ff7cf9503b917dcc8db1de3ba03b513240f7dc8 (patch) | |
tree | 21db757c04d6064aee147c73a73f624753871ac1 | |
parent | 0cfbe4639f076d50f2a3bbc9e6f566a452a43167 (diff) |
Use uniform representation of comparisons for better simplification.
-rw-r--r-- | src/option_key_fn.sml | 3 | ||||
-rw-r--r-- | src/sqlcache.sml | 56 |
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 = |