0 | module Data.Vect.Sort
 1 |
 2 | import Data.Vect
 3 | import Data.Nat.Views
 4 |
 5 | %default total
 6 |
 7 | mutual
 8 |   sortBySplit : (n : Nat) -> (a -> a -> Ordering) -> Vect n a -> Vect n a
 9 |   sortBySplit Z cmp [] = []
10 |   sortBySplit (S Z) cmp [x] = [x]
11 |   sortBySplit n cmp xs with (half n)
12 |     sortBySplit (k + k) cmp xs     | HalfEven k = sortByMerge k k cmp xs
13 |     sortBySplit (S (k + k)) cmp xs | HalfOdd k = sortByMerge (S k) k cmp xs
14 |
15 |   sortByMerge : (n : Nat) -> (m : Nat) -> (a -> a -> Ordering) -> Vect (n + m) a -> Vect (n + m) a
16 |   sortByMerge n m cmp xs =
17 |     let (left, right) = splitAt n xs in
18 |       mergeBy cmp
19 |         (sortBySplit n cmp (assert_smaller xs left))
20 |         (sortBySplit m cmp (assert_smaller xs right))
21 |
22 | ||| Merge sort implementation for Vect n a
23 | export
24 | sortBy : {n : Nat} -> (cmp : a -> a -> Ordering) -> (xs : Vect n a) -> Vect n a
25 | sortBy cmp xs = sortBySplit n cmp xs
26 |
27 | export
28 | sort : Ord a => {n : Nat} -> Vect n a -> Vect n a
29 | sort = sortBy compare
30 |