From bc38beafd07b7ae6106a2fffda82084a08af7f06 Mon Sep 17 00:00:00 2001 From: Ziv Scully Date: Sun, 19 Jul 2015 19:03:11 -0700 Subject: Rename C functions and remove functors nested inside modules. --- src/option_key_fn.sml | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 src/option_key_fn.sml (limited to 'src/option_key_fn.sml') diff --git a/src/option_key_fn.sml b/src/option_key_fn.sml new file mode 100644 index 00000000..ba636d4e --- /dev/null +++ b/src/option_key_fn.sml @@ -0,0 +1,11 @@ +functor OptionKeyFn(K : ORD_KEY) : ORD_KEY = struct + +type ord_key = K.ord_key option + +val compare = + fn (NONE, NONE) => EQUAL + | (NONE, _) => LESS + | (_, NONE) => GREATER + | (SOME x, SOME y) => K.compare (x, y) + +end -- cgit v1.2.3 From 4ff7cf9503b917dcc8db1de3ba03b513240f7dc8 Mon Sep 17 00:00:00 2001 From: Ziv Scully Date: Mon, 20 Jul 2015 23:25:44 -0700 Subject: Use uniform representation of comparisons for better simplification. --- src/option_key_fn.sml | 3 ++- src/sqlcache.sml | 56 +++++++++++++++++++++++++++++++++------------------ 2 files changed, 38 insertions(+), 21 deletions(-) (limited to 'src/option_key_fn.sml') 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 = -- cgit v1.2.3