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;
 src/Pure/library.ML file | annotate | diff | revisions
```     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;
```