Mercurial > urweb
comparison src/sqlcache.sml @ 2236:fab8c1f131a5
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 |