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)
```