Add Vect merge sort

[shmish111]

No description provided.

[gallais]

This looks like insertion sort to me.

[rgrover]

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}

[shmish111]

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.

[edwinb]

This would be good to have, but it is indeed insertion sort. I'll merge once it's updated.

[shmish111]

@edwinb updated in what way? You mean you would prefer a merge sort rather than an insertion sort?

[edwinb]

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?

[shmish111]

No, I just needed a sort on Vect but I can have a go at merge sort if I have time, good learning.

[shmish111]

I've added a merge sort and left the insertion sort but changed the default to merge sort.