Mercurial > urweb

comparison src/sqlcache.sml @ 2243:da7d026d1a94

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix possible formula simplification bug with extra formula' type.
author Ziv Scully <ziv@mit.edu>
date Mon, 20 Jul 2015 19:49:13 -0700
parents 88cc0f44c940
children e4a7e3cd6f11
comparison
equal deleted inserted replaced
2242:200a7ed4343b 2243:da7d026d1a94
143 datatype 'atom formula = 143 datatype 'atom formula =
144 Atom of 'atom 144 Atom of 'atom
145 | Negate of 'atom formula 145 | Negate of 'atom formula
146 | Combo of junctionType * 'atom formula list 146 | Combo of junctionType * 'atom formula list
147 147
148 (* Guaranteed to have all negation pushed to the atoms. *)
149 datatype 'atom formula' =
150 Atom' of 'atom
151 | Combo' of junctionType * 'atom formula' list
152
148 val flipJt = fn Conj => Disj | Disj => Conj 153 val flipJt = fn Conj => Disj | Disj => Conj
149 154
150 fun concatMap f xs = List.concat (map f xs) 155 fun concatMap f xs = List.concat (map f xs)
151 156
152 val rec cartesianProduct : 'a list list -> 'a list list = 157 val rec cartesianProduct : 'a list list -> 'a list list =
154 | (xs :: xss) => concatMap (fn ys => concatMap (fn x => [x :: ys]) xs) 159 | (xs :: xss) => concatMap (fn ys => concatMap (fn x => [x :: ys]) xs)
155 (cartesianProduct xss) 160 (cartesianProduct xss)
156 161
157 (* Pushes all negation to the atoms.*) 162 (* Pushes all negation to the atoms.*)
158 fun pushNegate (negate : 'atom -> 'atom) (negating : bool) = 163 fun pushNegate (negate : 'atom -> 'atom) (negating : bool) =
159 fn Atom x => Atom (if negating then negate x else x) 164 fn Atom x => Atom' (if negating then negate x else x)
160 | Negate f => pushNegate negate (not negating) f 165 | Negate f => pushNegate negate (not negating) f
161 | Combo (n, fs) => Combo (if negating then flipJt n else n, map (pushNegate negate negating) fs) 166 | Combo (j, fs) => Combo' (if negating then flipJt j else j, map (pushNegate negate negating) fs)
162 167
163 val rec flatten = 168 val rec flatten =
164 fn Combo (_, [f]) => flatten f 169 fn Combo' (_, [f]) => flatten f
165 | Combo (j, fs) => 170 | Combo' (j, fs) =>
166 Combo (j, List.foldr (fn (f, acc) => 171 Combo' (j, List.foldr (fn (f, acc) =>
167 case f of 172 case f of
168 Combo (j', fs') => 173 Combo' (j', fs') =>
169 if j = j' orelse length fs' = 1 174 if j = j' orelse length fs' = 1
170 then fs' @ acc 175 then fs' @ acc
171 else f :: acc 176 else f :: acc
172 | _ => f :: acc) 177 | _ => f :: acc)
173 [] 178 []
174 (map flatten fs)) 179 (map flatten fs))
175 | f => f 180 | f => f
176 181
182 (* [simplify] operates on the desired normal form. E.g., if [junc] is [Disj],
183 consider the list of lists to be a disjunction of conjunctions. *)
177 fun normalize' (simplify : 'a list list -> 'a list list) 184 fun normalize' (simplify : 'a list list -> 'a list list)
178 (negate : 'a -> 'a)
179 (junc : junctionType) = 185 (junc : junctionType) =
180 let 186 let
181 fun norm junc = 187 fun norm junc =
182 simplify 188 simplify
183 o (fn Atom x => [[x]] 189 o (fn Atom' x => [[x]]
184 | Negate f => map (map negate) (norm (flipJt junc) f) 190 | Combo' (j, fs) =>
185 | Combo (j, fs) =>
186 let 191 let
187 val fss = map (norm junc) fs 192 val fss = map (norm junc) fs
188 in 193 in
189 if j = junc 194 if j = junc
190 then List.concat fss 195 then List.concat fss
193 in 198 in
194 norm junc 199 norm junc
195 end 200 end
196 201
197 fun normalize simplify negate junc = 202 fun normalize simplify negate junc =
198 normalize' simplify negate junc 203 normalize' simplify junc
199 o flatten 204 o flatten
200 o pushNegate negate false 205 o pushNegate negate false
201 206
202 fun mapFormula mf = 207 fun mapFormula mf =
203 fn Atom x => Atom (mf x) 208 fn Atom x => Atom (mf x)
229 | (_, Sql.Gt) => GREATER 234 | (_, Sql.Gt) => GREATER
230 | (Sql.Ge, Sql.Ge) => EQUAL 235 | (Sql.Ge, Sql.Ge) => EQUAL
231 236
232 end 237 end
233 238
234 (*
235 functor ListKeyFn (K : ORD_KEY) : ORD_KEY = struct
236
237 type ord_key = K.ord_key list
238
239 val rec compare =
240 fn ([], []) => EQUAL
241 | ([], _) => LESS
242 | (_, []) => GREATER
243 | (x :: xs, y :: ys) => (case K.compare (x, y) of
244 EQUAL => compare (xs, ys)
245 | ord => ord)
246
247 end
248 *)
249
250 val rec chooseTwos : 'a list -> ('a * 'a) list = 239 val rec chooseTwos : 'a list -> ('a * 'a) list =
251 fn [] => [] 240 fn [] => []
252 | x :: ys => map (fn y => (x, y)) ys @ chooseTwos ys 241 | x :: ys => map (fn y => (x, y)) ys @ chooseTwos ys
253 242
254 fun removeRedundant madeRedundantBy zs = 243 fun removeRedundant madeRedundantBy zs =
298 287
299 structure TK = TripleKeyFn(structure I = CmpKey 288 structure TK = TripleKeyFn(structure I = CmpKey
300 structure J = OptionKeyFn(AtomExpKey) 289 structure J = OptionKeyFn(AtomExpKey)
301 structure K = OptionKeyFn(AtomExpKey)) 290 structure K = OptionKeyFn(AtomExpKey))
302 structure TS = BinarySetFn(TK) 291 structure TS = BinarySetFn(TK)
303 (* structure TLS = BinarySetFn(ListKeyFn(TK)) *)
304 292
305 val toKnownEquality = 293 val toKnownEquality =
306 (* [NONE] here means unkown. Anything that isn't a comparison between two 294 (* [NONE] here means unkown. Anything that isn't a comparison between two
307 knowns shouldn't be used, and simply dropping unused terms is okay in 295 knowns shouldn't be used, and simply dropping unused terms is okay in
308 disjunctive normal form. *) 296 disjunctive normal form. *)