# HG changeset patch # User wenzelm # Date 882523024 -3600 # Node ID de74b549f976c066cbf74bbcd0bb7f86587c7b07 # Parent fa05a79b3e975ce903598218d9a22e312e2e48e4 added rev_order, make_ord; reimplemented sort function: stable version of quicksort; diff -r fa05a79b3e97 -r de74b549f976 src/Pure/library.ML --- a/src/Pure/library.ML Fri Dec 19 10:16:16 1997 +0100 +++ b/src/Pure/library.ML Fri Dec 19 10:17:04 1997 +0100 @@ -725,6 +725,15 @@ datatype order = LESS | EQUAL | GREATER; +fun rev_order LESS = GREATER + | rev_order EQUAL = EQUAL + | rev_order GREATER = LESS; + +fun make_ord rel (x, y) = + if rel (x, y) then LESS + else if rel (y, x) then GREATER + else EQUAL; + fun int_ord (i, j: int) = if i < j then LESS else if i = j then EQUAL @@ -887,19 +896,27 @@ (* sorting *) -(*insertion sort; stable (does not reorder equal elements) - 'less' is less-than test on type 'a*) -fun sort (less: 'a*'a -> bool) = - let fun insert (x, []) = [x] - | insert (x, y::ys) = - if less(y, x) then y :: insert (x, ys) else x::y::ys; - fun sort1 [] = [] - | sort1 (x::xs) = insert (x, sort1 xs) - in sort1 end; +(*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 + 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) + | add EQUAL x (lts, eqs, gts) = (lts, x :: eqs, gts) + | add GREATER x (lts, eqs, gts) = (lts, eqs, x :: gts); + in qsort end; (*sort strings*) -fun sort_wrt sel xs = sort (op <= o pairself (sel: 'a -> string)) xs; -val sort_strings = sort_wrt I; +val sort_strings = sort string_ord; +fun sort_wrt sel xs = sort (string_ord o pairself sel) xs; (* transitive closure (not Warshall's algorithm) *)