930 (case int_ord (length xs, length ys) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord); |
930 (case int_ord (length xs, length ys) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord); |
931 |
931 |
932 |
932 |
933 (* sorting *) |
933 (* sorting *) |
934 |
934 |
935 (*quicksort -- stable, i.e. does not reorder equal elements*) |
935 (*stable mergesort -- preserves order of equal elements*) |
936 fun quicksort unique ord = |
936 fun mergesort unique ord = |
937 let |
937 let |
938 fun qsort [] = [] |
938 fun merge (xs as x :: xs') (ys as y :: ys') = |
939 | qsort (xs as [_]) = xs |
|
940 | qsort (xs as [x, y]) = |
|
941 (case ord (x, y) of |
939 (case ord (x, y) of |
942 LESS => xs |
940 LESS => x :: merge xs' ys |
943 | EQUAL => if unique then [x] else xs |
941 | EQUAL => |
944 | GREATER => [y, x]) |
942 if unique then merge xs ys' |
945 | qsort xs = |
943 else x :: merge xs' ys |
946 let val (lts, eqs, gts) = part (nth xs (length xs div 2)) xs |
944 | GREATER => y :: merge xs ys') |
947 in qsort lts @ eqs @ qsort gts end |
945 | merge [] ys = ys |
948 and part _ [] = ([], [], []) |
946 | merge xs [] = xs; |
949 | part pivot (x :: xs) = add (ord (x, pivot)) x (part pivot xs) |
947 |
950 and add LESS x (lts, eqs, gts) = (x :: lts, eqs, gts) |
948 fun merge_all [xs] = xs |
951 | add EQUAL x (lts, [], gts) = (lts, [x], gts) |
949 | merge_all xss = merge_all (merge_pairs xss) |
952 | add EQUAL x (res as (lts, eqs, gts)) = if unique then res else (lts, x :: eqs, gts) |
950 and merge_pairs (xs :: ys :: xss) = merge xs ys :: merge_pairs xss |
953 | add GREATER x (lts, eqs, gts) = (lts, eqs, x :: gts); |
951 | merge_pairs xss = xss; |
954 in qsort end; |
952 |
955 |
953 fun runs (x :: y :: xs) = |
956 fun sort ord = quicksort false ord; |
954 (case ord (x, y) of |
957 fun sort_distinct ord = quicksort true ord; |
955 LESS => ascending y [x] xs |
|
956 | EQUAL => |
|
957 if unique then runs (x :: xs) |
|
958 else ascending y [x] xs |
|
959 | GREATER => descending y [x] xs) |
|
960 | runs xs = [xs] |
|
961 |
|
962 and ascending x xs (zs as y :: ys) = |
|
963 (case ord (x, y) of |
|
964 LESS => ascending y (x :: xs) ys |
|
965 | EQUAL => |
|
966 if unique then ascending x xs ys |
|
967 else ascending y (x :: xs) ys |
|
968 | GREATER => rev (x :: xs) :: runs zs) |
|
969 | ascending x xs [] = [rev (x :: xs)] |
|
970 |
|
971 and descending x xs (zs as y :: ys) = |
|
972 (case ord (x, y) of |
|
973 GREATER => descending y (x :: xs) ys |
|
974 | EQUAL => |
|
975 if unique then descending x xs ys |
|
976 else (x :: xs) :: runs zs |
|
977 | LESS => (x :: xs) :: runs zs) |
|
978 | descending x xs [] = [x :: xs]; |
|
979 |
|
980 in merge_all o runs end; |
|
981 |
|
982 fun sort ord = mergesort false ord; |
|
983 fun sort_distinct ord = mergesort true ord; |
958 |
984 |
959 val sort_strings = sort string_ord; |
985 val sort_strings = sort string_ord; |
960 fun sort_wrt key xs = sort (string_ord o pairself key) xs; |
986 fun sort_wrt key xs = sort (string_ord o pairself key) xs; |
961 |
987 |
962 |
988 |