Mercurial > urweb

comparison src/sqlcache.sml @ 2236:fab8c1f131a5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Major DNF-calculation performance decrapification.
author Ziv Scully <ziv@mit.edu>
date Tue, 30 Jun 2015 01:56:22 -0700
parents 0aae15c2a05a
children e79ef5792c8b
comparison
equal deleted inserted replaced
2235:0aae15c2a05a 2236:fab8c1f131a5
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 val flipJt = fn Conj => Disj | Disj => Conj 148 val flipJt = fn Conj => Disj | Disj => Conj
149 149
150 fun listBind xs f = List.concat (map f xs) 150 fun concatMap f xs = List.concat (map f xs)
151 151
152 val rec cartesianProduct : 'a list list -> 'a list list = 152 val rec cartesianProduct : 'a list list -> 'a list list =
153 fn [] => [[]] 153 fn [] => [[]]
154 | (xs :: xss) => listBind (cartesianProduct xss) 154 | (xs :: xss) => concatMap (fn ys => concatMap (fn x => [x :: ys]) xs)
155 (fn ys => listBind xs (fn x => [x :: ys])) 155 (cartesianProduct xss)
156 156
157 (* Pushes all negation to the atoms.*) 157 (* Pushes all negation to the atoms.*)
158 fun pushNegate (negate : 'atom -> 'atom) (negating : bool) = 158 fun pushNegate (negate : 'atom -> 'atom) (negating : bool) =
159 fn Atom x => Atom (if negating then negate x else x) 159 fn Atom x => Atom (if negating then negate x else x)
160 | Negate f => pushNegate negate (not negating) f 160 | Negate f => pushNegate negate (not negating) f
172 | _ => f :: acc) 172 | _ => f :: acc)
173 [] 173 []
174 (map flatten fs)) 174 (map flatten fs))
175 | f => f 175 | f => f
176 176
177 fun normalize' ((simplifyLists, simplifyAtomsConj, simplifyAtomsDisj, negate) 177 fun normPlz (junc : junctionType) =
178 fn Atom x => [[x]]
179 | Combo (j, fs) =>
180 let
181 val fss = map (normPlz junc) fs
182 in
183 if j = junc
184 then List.concat fss
185 else map List.concat (cartesianProduct fss)
186 end
187 (* Excluded by pushNegate. *)
188 | Negate _ => raise Match
189
190 fun normalize' ((simplifyLists, simplifyAtoms, negate)
178 : ('a list list -> 'a list list) 191 : ('a list list -> 'a list list)
179 * ('a list -> 'a list)
180 * ('a list -> 'a list) 192 * ('a list -> 'a list)
181 * ('a -> 'a)) 193 * ('a -> 'a))
182 (junc : junctionType) = 194 (junc : junctionType) =
183 let 195 let
184 fun simplify junc = simplifyLists o map (case junc of 196 fun simplify junc = simplifyLists o map simplifyAtoms
185 Conj => simplifyAtomsConj
186 | Disj => simplifyAtomsDisj)
187 fun norm junc = 197 fun norm junc =
188 simplify junc 198 simplify junc
189 o (fn Atom x => [[x]] 199 o (fn Atom x => [[x]]
190 | Negate f => map (map negate) (norm (flipJt junc) f) 200 | Negate f => map (map negate) (norm (flipJt junc) f)
191 | Combo (j, fs) => 201 | Combo (j, fs) =>
192 let 202 let
193 val fss = listBind fs (norm j) 203 val fss = map (norm junc) fs
194 in 204 in
195 if j = junc then fss else cartesianProduct fss 205 if j = junc
206 then List.concat fss
207 else map List.concat (cartesianProduct fss)
196 end) 208 end)
197 in 209 in
198 norm junc 210 norm junc
199 end 211 end
200 212
201 fun normalize (simplifyLists, simplifyAtomsConj, simplifyAtomsDisj, negate, junc) = 213 fun normalize (simplifyLists, simplifyAtoms, negate, junc) =
202 (normalize' (simplifyLists, simplifyAtomsConj, simplifyAtomsDisj, negate) junc) 214 (normalize' (simplifyLists, simplifyAtoms, negate) junc)
203 o flatten 215 o flatten
204 o pushNegate negate false 216 o pushNegate negate false
205 217
206 fun mapFormula mf = 218 fun mapFormula mf =
207 fn Atom x => Atom (mf x) 219 fn Atom x => Atom (mf x)
412 implementation for finding an extra equality. *) 424 implementation for finding an extra equality. *)
413 fn SOME (Field (_, field)) => String.isSuffix "*" field 425 fn SOME (Field (_, field)) => String.isSuffix "*" field
414 | _ => false 426 | _ => false
415 fun canIgnore (_, a1, a2) = isStar a1 orelse isStar a2 427 fun canIgnore (_, a1, a2) = isStar a1 orelse isStar a2
416 fun simplifyLists xs = TLS.listItems (TLS.addList (TLS.empty, xs)) 428 fun simplifyLists xs = TLS.listItems (TLS.addList (TLS.empty, xs))
417 fun simplifyAtomsConj xs = TS.listItems (TS.addList (TS.empty, xs)) 429 fun simplifyAtoms xs = TS.listItems (TS.addList (TS.empty, xs))
418 val simplifyAtomsDisj = simplifyAtomsConj o List.filter canIgnore
419 in 430 in
420 normalize (simplifyLists, simplifyAtomsConj, simplifyAtomsDisj, negateCmp, Disj) 431 normalize (simplifyLists, simplifyAtoms, negateCmp, Disj)
421 (Combo (Conj, [markQuery fQuery, markDml fDml])) 432 (Combo (Conj, [markQuery fQuery, markDml fDml]))
422 end 433 end
423 434
424 val conflictMaps = List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf 435 val conflictMaps = List.mapPartial (mergeEqs o map eqsOfClass o equivClasses) o dnf
425 436