Ur/Web: src/sqlcache.sml comparison

comparison src/sqlcache.sml @ 2244:e4a7e3cd6f11

Use uniform representation of comparisons for better simplification.

author	Ziv Scully <ziv@mit.edu>
date	Mon, 20 Jul 2015 23:25:44 -0700
parents	da7d026d1a94
children	e09c3dc102ef

comparison

equal deleted inserted replaced

-:da7d026d1a94
+:e4a7e3cd6f11
 fn [] => [[]]
 | (xs :: xss) => concatMap (fn ys => concatMap (fn x => [x :: ys]) xs)
 (cartesianProduct xss)
 (* Pushes all negation to the atoms.*)
-fun pushNegate (negate : 'atom -> 'atom) (negating : bool) =
+fun pushNegate (normalizeAtom : bool * 'atom -> 'atom) (negating : bool) =
-fn Atom x => Atom' (if negating then negate x else x)
+fn Atom x => Atom' (normalizeAtom (negating, x))
-| Negate f => pushNegate negate (not negating) f
+| Negate f => pushNegate normalizeAtom (not negating) f
-| Combo (j, fs) => Combo' (if negating then flipJt j else j, map (pushNegate negate negating) fs)
+| Combo (j, fs) => Combo' (if negating then flipJt j else j,
+map (pushNegate normalizeAtom negating) fs)
 val rec flatten =
 fn Combo' (_, [f]) => flatten f
 | Combo' (j, fs) =>
 Combo' (j, List.foldr (fn (f, acc) =>
 end)
 in
 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)
 | Negate f => Negate (mapFormula mf f)
 | Combo (j, fs) => Combo (j, map (mapFormula mf) fs)
 EQUAL => String.compare (f1, f2)
 | ord => ord
 end
+structure AtomOptionKey = OptionKeyFn(AtomExpKey)
 structure UF = UnionFindFn(AtomExpKey)
 structure ConflictMaps = struct
 structure TK = TripleKeyFn(structure I = CmpKey
-structure J = OptionKeyFn(AtomExpKey)
+structure J = AtomOptionKey
-structure K = OptionKeyFn(AtomExpKey))
+structure K = AtomOptionKey)
-structure TS = BinarySetFn(TK)
+structure TS : ORD_SET = BinarySetFn(TK)
 val toKnownEquality =
 (* [NONE] here means unkown. Anything that isn't a comparison between two
 knowns shouldn't be used, and simply dropping unused terms is okay in
 disjunctive normal form. *)
 | _ => NONE
 in
 (cmp, qa e1, qa e2)
 end
-fun negateCmp (cmp, e1, e2) =
+val negateCmp =
-(case cmp of
+fn Sql.Eq => Sql.Ne
-Sql.Eq => Sql.Ne
+| Sql.Ne => Sql.Eq
-| Sql.Ne => Sql.Eq
+| Sql.Lt => Sql.Ge
-| Sql.Lt => Sql.Ge
+| Sql.Le => Sql.Gt
-| Sql.Le => Sql.Gt
+| Sql.Gt => Sql.Le
-| Sql.Gt => Sql.Le
+| Sql.Ge => Sql.Lt
-| Sql.Ge => Sql.Lt,
-e1, e2)
+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 =
 mapFormula (toAtomExps QueryArg)
 map TS.listItems
 o removeRedundant (fn (x, y) => TS.isSubset (y, x))
 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
 end
 | e => e
 val mark = mapFormula (fn (cmp, e1, e2) => (cmp, markField e1, markField e2))
 in
 renameTables [(table, "T")]
 (Combo (Disj, [Combo (Conj, [fVals, mark fWhere]),
 Combo (Conj, [mark fVals, fWhere])]))
 end
 val rec tablesQuery =
 fn Sql.Query1 {From = tablePairs, ...} => SS.fromList (map #1 tablePairs)
 | Sql.Union (q1, q2) => SS.union (tablesQuery q1, tablesQuery q2)

Mercurial > urweb

comparison src/sqlcache.sml @ 2244:e4a7e3cd6f11