added sort_distinct;
authorwenzelm
Sat Dec 17 01:00:38 2005 +0100 (2005-12-17)
changeset 18427b7ee916ae3ec
parent 18426 d2303e8654a2
child 18428 4059413acbc1
added sort_distinct;
removed obsolete unique_strings;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Fri Dec 16 18:22:58 2005 +0100
     1.2 +++ b/src/Pure/library.ML	Sat Dec 17 01:00:38 2005 +0100
     1.3 @@ -231,9 +231,9 @@
     1.4    val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
     1.5    val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
     1.6    val sort: ('a * 'a -> order) -> 'a list -> 'a list
     1.7 +  val sort_distinct: ('a * 'a -> order) -> 'a list -> 'a list
     1.8    val sort_strings: string list -> string list
     1.9    val sort_wrt: ('a -> string) -> 'a list -> 'a list
    1.10 -  val unique_strings: string list -> string list
    1.11  
    1.12    (*random numbers*)
    1.13    exception RANDOM
    1.14 @@ -1106,31 +1106,33 @@
    1.15  
    1.16  (* sorting *)
    1.17  
    1.18 -(*quicksort (stable, i.e. does not reorder equal elements)*)
    1.19 -fun sort ord =
    1.20 +(*quicksort -- stable, i.e. does not reorder equal elements*)
    1.21 +fun quicksort unique ord =
    1.22    let
    1.23      fun qsort [] = []
    1.24        | qsort (xs as [_]) = xs
    1.25 -      | qsort (xs as [x, y]) = if ord (x, y) = GREATER then [y, x] else xs
    1.26 +      | qsort (xs as [x, y]) =
    1.27 +          (case ord (x, y) of
    1.28 +            LESS => xs
    1.29 +          | EQUAL => if unique then [x] else xs
    1.30 +          | GREATER => [y, x])
    1.31        | qsort xs =
    1.32            let val (lts, eqs, gts) = part (nth xs (length xs div 2)) xs
    1.33            in qsort lts @ eqs @ qsort gts end
    1.34      and part _ [] = ([], [], [])
    1.35        | part pivot (x :: xs) = add (ord (x, pivot)) x (part pivot xs)
    1.36      and add LESS x (lts, eqs, gts) = (x :: lts, eqs, gts)
    1.37 -      | add EQUAL x (lts, eqs, gts) = (lts, x :: eqs, gts)
    1.38 +      | add EQUAL x (lts, [], gts) = (lts, [x], gts)
    1.39 +      | add EQUAL x (res as (lts, eqs, gts)) = if unique then res else (lts, x :: eqs, gts)
    1.40        | add GREATER x (lts, eqs, gts) = (lts, eqs, x :: gts);
    1.41    in qsort end;
    1.42  
    1.43 -(*sort strings*)
    1.44 +fun sort ord = quicksort false ord;
    1.45 +fun sort_distinct ord = quicksort true ord;
    1.46 +
    1.47  val sort_strings = sort string_ord;
    1.48  fun sort_wrt sel xs = sort (string_ord o pairself sel) xs;
    1.49  
    1.50 -fun unique_strings ([]: string list) = []
    1.51 -  | unique_strings [x] = [x]
    1.52 -  | unique_strings (x :: y :: ys) =
    1.53 -      if x = y then unique_strings (y :: ys)
    1.54 -      else x :: unique_strings (y :: ys);
    1.55  
    1.56  
    1.57  (** random numbers **)