author | wenzelm |

Mon Jul 16 15:57:21 2012 +0200 (2012-07-16) | |

changeset 48271 | b28defd0b5a5 |

parent 48270 | 9cfd3e7ad5c8 |

child 48272 | db75b4005d9a |

replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;

1.1 --- a/src/Pure/library.ML Mon Jul 16 15:55:21 2012 +0200 1.2 +++ b/src/Pure/library.ML Mon Jul 16 15:57:21 2012 +0200 1.3 @@ -932,29 +932,55 @@ 1.4 1.5 (* sorting *) 1.6 1.7 -(*quicksort -- stable, i.e. does not reorder equal elements*) 1.8 -fun quicksort unique ord = 1.9 +(*stable mergesort -- preserves order of equal elements*) 1.10 +fun mergesort unique ord = 1.11 let 1.12 - fun qsort [] = [] 1.13 - | qsort (xs as [_]) = xs 1.14 - | qsort (xs as [x, y]) = 1.15 + fun merge (xs as x :: xs') (ys as y :: ys') = 1.16 + (case ord (x, y) of 1.17 + LESS => x :: merge xs' ys 1.18 + | EQUAL => 1.19 + if unique then merge xs ys' 1.20 + else x :: merge xs' ys 1.21 + | GREATER => y :: merge xs ys') 1.22 + | merge [] ys = ys 1.23 + | merge xs [] = xs; 1.24 + 1.25 + fun merge_all [xs] = xs 1.26 + | merge_all xss = merge_all (merge_pairs xss) 1.27 + and merge_pairs (xs :: ys :: xss) = merge xs ys :: merge_pairs xss 1.28 + | merge_pairs xss = xss; 1.29 + 1.30 + fun runs (x :: y :: xs) = 1.31 (case ord (x, y) of 1.32 - LESS => xs 1.33 - | EQUAL => if unique then [x] else xs 1.34 - | GREATER => [y, x]) 1.35 - | qsort xs = 1.36 - let val (lts, eqs, gts) = part (nth xs (length xs div 2)) xs 1.37 - in qsort lts @ eqs @ qsort gts end 1.38 - and part _ [] = ([], [], []) 1.39 - | part pivot (x :: xs) = add (ord (x, pivot)) x (part pivot xs) 1.40 - and add LESS x (lts, eqs, gts) = (x :: lts, eqs, gts) 1.41 - | add EQUAL x (lts, [], gts) = (lts, [x], gts) 1.42 - | add EQUAL x (res as (lts, eqs, gts)) = if unique then res else (lts, x :: eqs, gts) 1.43 - | add GREATER x (lts, eqs, gts) = (lts, eqs, x :: gts); 1.44 - in qsort end; 1.45 + LESS => ascending y [x] xs 1.46 + | EQUAL => 1.47 + if unique then runs (x :: xs) 1.48 + else ascending y [x] xs 1.49 + | GREATER => descending y [x] xs) 1.50 + | runs xs = [xs] 1.51 1.52 -fun sort ord = quicksort false ord; 1.53 -fun sort_distinct ord = quicksort true ord; 1.54 + and ascending x xs (zs as y :: ys) = 1.55 + (case ord (x, y) of 1.56 + LESS => ascending y (x :: xs) ys 1.57 + | EQUAL => 1.58 + if unique then ascending x xs ys 1.59 + else ascending y (x :: xs) ys 1.60 + | GREATER => rev (x :: xs) :: runs zs) 1.61 + | ascending x xs [] = [rev (x :: xs)] 1.62 + 1.63 + and descending x xs (zs as y :: ys) = 1.64 + (case ord (x, y) of 1.65 + GREATER => descending y (x :: xs) ys 1.66 + | EQUAL => 1.67 + if unique then descending x xs ys 1.68 + else (x :: xs) :: runs zs 1.69 + | LESS => (x :: xs) :: runs zs) 1.70 + | descending x xs [] = [x :: xs]; 1.71 + 1.72 + in merge_all o runs end; 1.73 + 1.74 +fun sort ord = mergesort false ord; 1.75 +fun sort_distinct ord = mergesort true ord; 1.76 1.77 val sort_strings = sort string_ord; 1.78 fun sort_wrt key xs = sort (string_ord o pairself key) xs;