1(*
2 * Extracted from Isabelle sources (src/Pure/library.ML)
3 *
4 * @TAG(OTHER_BSD)
5 *)
6
7
8signature LIBRARY =
9sig
10
11  val sort : ('a * 'a -> order) -> 'a list -> 'a list
12
13end
14
15structure Library : LIBRARY =
16struct
17
18(*stable mergesort -- preserves order of equal elements*)
19fun mergesort unique ord =
20  let
21    fun merge (xs as x :: xs') (ys as y :: ys') =
22          (case ord (x, y) of
23            LESS => x :: merge xs' ys
24          | EQUAL =>
25              if unique then merge xs ys'
26              else x :: merge xs' ys
27          | GREATER => y :: merge xs ys')
28      | merge [] ys = ys
29      | merge xs [] = xs;
30
31    fun merge_all [xs] = xs
32      | merge_all xss = merge_all (merge_pairs xss)
33    and merge_pairs (xs :: ys :: xss) = merge xs ys :: merge_pairs xss
34      | merge_pairs xss = xss;
35
36    fun runs (x :: y :: xs) =
37          (case ord (x, y) of
38             LESS => ascending y [x] xs
39           | EQUAL =>
40               if unique then runs (x :: xs)
41               else ascending y [x] xs
42           | GREATER => descending y [x] xs)
43      | runs xs = [xs]
44
45    and ascending x xs (zs as y :: ys) =
46          (case ord (x, y) of
47             LESS => ascending y (x :: xs) ys
48           | EQUAL =>
49               if unique then ascending x xs ys
50               else ascending y (x :: xs) ys
51           | GREATER => rev (x :: xs) :: runs zs)
52      | ascending x xs [] = [rev (x :: xs)]
53
54    and descending x xs (zs as y :: ys) =
55          (case ord (x, y) of
56             GREATER => descending y (x :: xs) ys
57           | EQUAL =>
58               if unique then descending x xs ys
59               else (x :: xs) :: runs zs
60           | LESS => (x :: xs) :: runs zs)
61      | descending x xs [] = [x :: xs];
62
63  in merge_all o runs end;
64
65fun sort ord = mergesort false ord;
66
67end
68