SortedList.idr

import Data.Vect
import Data.Vect.Views

%default total

data SortedList : Nat -> Type where
    SInit : (a : Nat) -> SortedList a
    SCons : (a : Nat) -> {auto prf : LTE a b} -> SortedList b -> SortedList a

sortedToList : SortedList a -> List Nat
sortedToList (SInit a) = [a]
sortedToList (SCons a as) = a::(sortedToList as)

eitherLte : (a : Nat) -> (b : Nat) -> Either (LTE a b) (LTE b a)
eitherLte (S l) (S r) with (eitherLte l r)
    | Left  prf = Left  (LTESucc prf)
    | Right prf = Right (LTESucc prf)
eitherLte l Z = Right (LTEZero)
eitherLte Z r = Left (LTEZero)

sortedListLte : SortedList a -> SortedList b -> Either (LTE a b) (LTE b a)
sortedListLte (SInit a)   (SInit b)   = eitherLte a b
sortedListLte (SCons a _) (SCons b _) = eitherLte a b
sortedListLte (SInit a)   (SCons b _) = eitherLte a b
sortedListLte (SCons a _) (SInit b)   = eitherLte a b

insert : (a : Nat) -> SortedList b -> Either (SortedList a) (SortedList b)
insert a bl@(SInit b) =
    case eitherLte a b of
        Left  aLteB => Left  $ SCons a (SInit b) {prf=aLteB}
        Right bLteA => Right $ SCons b (SInit a) {prf=bLteA}
insert a bl@(SCons b bs) =
    case eitherLte a b of
        Left  aLteB => Left  $ SCons a bl
        Right bLteA => Right $ case insert a bs of
                                    Left  lA => SCons b lA
                                    Right lB => SCons b lB

merge : SortedList a -> SortedList b -> Either (SortedList a) (SortedList b)
merge (SInit a) b = insert a b
merge al@(SCons a as) bl@(SInit b) = mirror $ insert b al
merge al@(SCons a as) bl@(SCons b bs) =
    case sortedListLte al bl of
        Left  aLteB => Left  $ case merge as bl of
                                    Left  lA => SCons a lA
                                    Right lB => SCons a lB
        Right bLteA => Right $ case merge al bs of
                                    Left  lA => SCons b lA
                                    Right lB => SCons b lB

abstractMin : Either (SortedList a) (SortedList b) -> (c ** SortedList c)
abstractMin (Left l)  = (_ ** l)
abstractMin (Right r) = (_ ** r)

mergeSort : Vect (1 + n) Nat -> (l ** SortedList l)
mergeSort xs with (splitRec xs)
    mergeSort [x] | SplitRecOne = (_ ** SInit x)
    mergeSort ((y::ys) ++ (z::zs)) | SplitRecPair ysrec zsrec =
        let (_ ** left)  = (mergeSort (y::ys) | ysrec) in
        let (_ ** right) = (mergeSort (z::zs) | zsrec) in
        abstractMin $ merge left right