replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
authorwenzelm
Mon Jul 16 15:57:21 2012 +0200 (2012-07-16)
changeset 48271b28defd0b5a5
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
     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;