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