@@ -718,6 +718,7 @@ isInfixOf n h = any (isPrefixOf n) (tails h)
718718-- Sorting
719719--------------------------------------------------------------------------------
720720
721+||| Check whether a list is sorted with respect to the default ordering for the type of its elements.
721722sorted : Ord a => List a -> Bool
722723sorted [] = True
723724sorted (x::xs) =
@@ -725,6 +726,9 @@ sorted (x::xs) =
725726 Nil => True
726727 (y::ys) => x <= y && sorted (y::ys)
727728
729+||| Merge two sorted lists using an arbitrary comparison
730+||| predicate. Note that the lists must have been sorted using this
731+||| predicate already.
728732mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
729733mergeBy order [] right = right
730734mergeBy order left [] = left
@@ -733,15 +737,21 @@ mergeBy order (x::xs) (y::ys) =
733737 then x :: mergeBy order xs (y::ys)
734738 else y :: mergeBy order (x::xs) ys
735739
740+||| Merge two sorted lists using the default ordering for the type of their elements.
736741merge : Ord a => List a -> List a -> List a
737742merge = mergeBy compare
738743
739−sort : Ord a => List a -> List a
740−sort [] = []
741−sort [x] = [x]
742−sort xs = let (x, y) = split xs in
743− merge (sort (assert_smaller xs x))
744− (sort (assert_smaller xs y)) -- not structurally smaller, hence assert
744+||| Sort a list using some arbitrary comparison predicate.
745+|||
746+||| @ cmp how to compare elements
747+||| @ xs the list to sort
748+sortBy : (cmp : a -> a -> Ordering) -> (xs : List a) -> List a
749+sortBy cmp [] = []
750+sortBy cmp [x] = [x]
751+sortBy cmp xs = let (x, y) = split xs in
752+ mergeBy cmp
753+ (sortBy cmp (assert_smaller xs x))
754+ (sortBy cmp (assert_smaller xs y)) -- not structurally smaller, hence assert
745755 where
746756 splitRec : List a -> List a -> (List a -> List a) -> (List a, List a)
747757 splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y))
@@ -750,6 +760,10 @@ sort xs = let (x, y) = split xs in
750760 split : List a -> (List a, List a)
751761 split xs = splitRec xs xs id
752762
763+||| Sort a list using the default ordering for the type of its elements.
764+sort : Ord a => List a -> List a
765+sort = sortBy compare
766+
753767--------------------------------------------------------------------------------
754768-- Conversions
755769--------------------------------------------------------------------------------