Open shmish111 opened 4 years ago
The following works:
export
sortBy : {n : Nat} -> (elem -> elem -> Ordering) -> Vect n elem -> Vect n elem
sortBy _ [] = []
sortBy _ [x] = [x]
sortBy order xs with (parity n)
sortBy {n = j + j} order xs | Even =
let (left, right) = splitAt j xs in
mergeBy order (sortBy order left) (sortBy order right)
sortBy {n = S (j + j)} order xs | Odd =
let (left, right) = splitAt (S j) xs in
mergeBy order (sortBy order left) (sortBy order right)
where
data Parity : Nat -> Type where
Even : {n : _} -> Parity (n + n)
Odd : {n : _} -> Parity (S (n + n))
parity : (n:Nat) -> Parity n
parity 0 = Even {n = Z}
parity (S k) with (parity k)
parity (S (j + j)) | Even {n = j} = Odd
parity (S (S (j + j))) | Odd {n = j} =
rewrite (plusSuccRightSucc j j) in Even {n = S j}
Sorry I got confused because this uses the existing mergeBy
function. I would like a sort function in Vect
and I felt like this was the most sensible way to do it given that someone has written mergeBy
already.
This would be good to have, but it is indeed insertion sort. I'll merge once it's updated.
@edwinb updated in what way? You mean you would prefer a merge sort rather than an insertion sort?
I think merge sort would be better, yes, just for the generally better performance - I think that is what you intended though isn't it?
No, I just needed a sort on Vect but I can have a go at merge sort if I have time, good learning.
I've added a merge sort and left the insertion sort but changed the default to merge sort.
This looks like insertion sort to me.