author wenzelm Tue, 19 Jul 2005 17:21:50 +0200 changeset 16878 07213f0e291f parent 16877 e92cba1d4842 child 16879 b81d3f2ee565
added has_duplicates; tuned qsort;
 src/Pure/library.ML file | annotate | diff | comparison | revisions
```--- a/src/Pure/library.ML	Tue Jul 19 17:21:49 2005 +0200
+++ b/src/Pure/library.ML	Tue Jul 19 17:21:50 2005 +0200
@@ -209,6 +209,7 @@
val findrep: ''a list -> ''a list
val gen_duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
val duplicates: ''a list -> ''a list
+  val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool

(*association lists*)
val assoc: (''a * 'b) list * ''a -> 'b option
@@ -638,7 +639,7 @@
exception UnequalLengths;

fun map2 _ ([], []) = []
-  | map2 f (x :: xs, y :: ys) = (f (x, y) :: map2 f (xs, ys))
+  | map2 f (x :: xs, y :: ys) = f (x, y) :: map2 f (xs, ys)
| map2 _ _ = raise UnequalLengths;

fun exists2 _ ([], []) = false
@@ -983,7 +984,6 @@

fun distinct l = gen_distinct (op =) l;

-
(*returns the tail beginning with the first repeated element, or []*)
fun findrep [] = []
| findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
@@ -1006,6 +1006,12 @@

fun duplicates l = gen_duplicates (op =) l;

+fun has_duplicates eq =
+  let
+    fun dups [] = false
+      | dups (x :: xs) = member eq xs x orelse dups xs;
+  in dups end;
+

(** association lists **)
@@ -1154,14 +1160,12 @@
(*quicksort (stable, i.e. does not reorder equal elements)*)
fun sort ord =
let
-    fun qsort xs =
-      let val len = length xs in
-        if len <= 1 then xs
-        else
-          let val (lts, eqs, gts) = part (nth_elem (len div 2, xs)) xs in
-            qsort lts @ eqs @ qsort gts
-          end
-      end
+    fun qsort [] = []
+      | qsort (xs as [_]) = xs
+      | qsort (xs as [x, y]) = if ord (x, y) = GREATER then [y, x] else xs
+      | qsort xs =
+          let val (lts, eqs, gts) = part (nth_elem (length xs div 2, xs)) xs
+          in qsort lts @ eqs @ qsort gts end
and part _ [] = ([], [], [])
| part pivot (x :: xs) = add (ord (x, pivot)) x (part pivot xs)
and add LESS x (lts, eqs, gts) = (x :: lts, eqs, gts)```