src/Pure/library.ML
changeset 16878 07213f0e291f
parent 16869 bc98da5727be
child 16984 abc48b981e60
     1.1 --- a/src/Pure/library.ML	Tue Jul 19 17:21:49 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Jul 19 17:21:50 2005 +0200
     1.3 @@ -209,6 +209,7 @@
     1.4    val findrep: ''a list -> ''a list
     1.5    val gen_duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
     1.6    val duplicates: ''a list -> ''a list
     1.7 +  val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
     1.8  
     1.9    (*association lists*)
    1.10    val assoc: (''a * 'b) list * ''a -> 'b option
    1.11 @@ -638,7 +639,7 @@
    1.12  exception UnequalLengths;
    1.13  
    1.14  fun map2 _ ([], []) = []
    1.15 -  | map2 f (x :: xs, y :: ys) = (f (x, y) :: map2 f (xs, ys))
    1.16 +  | map2 f (x :: xs, y :: ys) = f (x, y) :: map2 f (xs, ys)
    1.17    | map2 _ _ = raise UnequalLengths;
    1.18  
    1.19  fun exists2 _ ([], []) = false
    1.20 @@ -983,7 +984,6 @@
    1.21  
    1.22  fun distinct l = gen_distinct (op =) l;
    1.23  
    1.24 -
    1.25  (*returns the tail beginning with the first repeated element, or []*)
    1.26  fun findrep [] = []
    1.27    | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
    1.28 @@ -1006,6 +1006,12 @@
    1.29  
    1.30  fun duplicates l = gen_duplicates (op =) l;
    1.31  
    1.32 +fun has_duplicates eq =
    1.33 +  let
    1.34 +    fun dups [] = false
    1.35 +      | dups (x :: xs) = member eq xs x orelse dups xs;
    1.36 +  in dups end;
    1.37 +
    1.38  
    1.39  
    1.40  (** association lists **)
    1.41 @@ -1154,14 +1160,12 @@
    1.42  (*quicksort (stable, i.e. does not reorder equal elements)*)
    1.43  fun sort ord =
    1.44    let
    1.45 -    fun qsort xs =
    1.46 -      let val len = length xs in
    1.47 -        if len <= 1 then xs
    1.48 -        else
    1.49 -          let val (lts, eqs, gts) = part (nth_elem (len div 2, xs)) xs in
    1.50 -            qsort lts @ eqs @ qsort gts
    1.51 -          end
    1.52 -      end
    1.53 +    fun qsort [] = []
    1.54 +      | qsort (xs as [_]) = xs
    1.55 +      | qsort (xs as [x, y]) = if ord (x, y) = GREATER then [y, x] else xs
    1.56 +      | qsort xs =
    1.57 +          let val (lts, eqs, gts) = part (nth_elem (length xs div 2, xs)) xs
    1.58 +          in qsort lts @ eqs @ qsort gts end
    1.59      and part _ [] = ([], [], [])
    1.60        | part pivot (x :: xs) = add (ord (x, pivot)) x (part pivot xs)
    1.61      and add LESS x (lts, eqs, gts) = (x :: lts, eqs, gts)