src/Pure/library.ML
 changeset 4445 de74b549f976 parent 4363 b449831f03f4 child 4479 708d7c26db5b
```     1.1 --- a/src/Pure/library.ML	Fri Dec 19 10:16:16 1997 +0100
1.2 +++ b/src/Pure/library.ML	Fri Dec 19 10:17:04 1997 +0100
1.3 @@ -725,6 +725,15 @@
1.4
1.5  datatype order = LESS | EQUAL | GREATER;
1.6
1.7 +fun rev_order LESS = GREATER
1.8 +  | rev_order EQUAL = EQUAL
1.9 +  | rev_order GREATER = LESS;
1.10 +
1.11 +fun make_ord rel (x, y) =
1.12 +  if rel (x, y) then LESS
1.13 +  else if rel (y, x) then GREATER
1.14 +  else EQUAL;
1.15 +
1.16  fun int_ord (i, j: int) =
1.17    if i < j then LESS
1.18    else if i = j then EQUAL
1.19 @@ -887,19 +896,27 @@
1.20
1.21  (* sorting *)
1.22
1.23 -(*insertion sort; stable (does not reorder equal elements)
1.24 -  'less' is less-than test on type 'a*)
1.25 -fun sort (less: 'a*'a -> bool) =
1.26 -  let fun insert (x, []) = [x]
1.27 -        | insert (x, y::ys) =
1.28 -              if less(y, x) then y :: insert (x, ys) else x::y::ys;
1.29 -      fun sort1 [] = []
1.30 -        | sort1 (x::xs) = insert (x, sort1 xs)
1.31 -  in  sort1  end;
1.32 +(*quicksort (stable, i.e. does not reorder equal elements)*)
1.33 +fun sort ord =
1.34 +  let
1.35 +    fun qsort xs =
1.36 +      let val len = length xs in
1.37 +        if len <= 1 then xs
1.38 +        else
1.39 +          let val (lts, eqs, gts) = part (nth_elem (len div 2, xs)) xs in
1.40 +            qsort lts @ eqs @ qsort gts
1.41 +          end
1.42 +      end
1.43 +    and part _ [] = ([], [], [])
1.44 +      | part pivot (x :: xs) = add (ord (x, pivot)) x (part pivot xs)
1.45 +    and add LESS x (lts, eqs, gts) = (x :: lts, eqs, gts)
1.46 +      | add EQUAL x (lts, eqs, gts) = (lts, x :: eqs, gts)
1.47 +      | add GREATER x (lts, eqs, gts) = (lts, eqs, x :: gts);
1.48 +  in qsort end;
1.49
1.50  (*sort strings*)
1.51 -fun sort_wrt sel xs = sort (op <= o pairself (sel: 'a -> string)) xs;
1.52 -val sort_strings = sort_wrt I;
1.53 +val sort_strings = sort string_ord;
1.54 +fun sort_wrt sel xs = sort (string_ord o pairself sel) xs;
1.55
1.56
1.57  (* transitive closure (not Warshall's algorithm) *)
```