added rev_order, make_ord;
authorwenzelm
Fri Dec 19 10:17:04 1997 +0100 (1997-12-19)
changeset 4445de74b549f976
parent 4444 fa05a79b3e97
child 4446 097004a470fb
added rev_order, make_ord;
reimplemented sort function: stable version of quicksort;
src/Pure/library.ML
     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) *)