module ListSort () where

import Language.Haskell.Liquid.Prelude

{-@ type OList a = [a]<{\fld v -> (v >= fld)}>  @-}

{-@ predicate Pr X Y = (((len Y) > 1) => ((len Y) < (len X))) @-}

{-@ split :: xs:[a] 
          -> ({v:[a] | (Pr xs v)}, {v:[a]|(Pr xs v)})
                 <{\x y -> ((len x) + (len y) = (len xs))}> 
  @-}

split :: [a] -> ([a], [a])
split (x:(y:zs)) = (x:xs, y:ys) where (xs, ys) = split zs
split xs                   = (xs, [])


{-@ decrease merge 4 @-}
{-@ merge :: Ord a => xs:(OList a) -> ys:(OList a) -> d:{v:Int| v = (len xs) + (len ys)} -> {v:(OList a) | (len v) = d} @-}
merge :: Ord a => [a] -> [a] -> Int -> [a]
merge xs [] _ = xs
merge [] ys _ = ys
merge (x:xs) (y:ys) d
  | x <= y
  = x:(merge xs (y:ys) (d-1))
  | otherwise 
  = y:(merge (x:xs) ys (d-1))

{-@ mergesort :: (Ord a) => xs:[a] -> {v:(OList a) | (len v) = (len xs)}  @-}
mergesort :: Ord a => [a] -> [a]
mergesort []  = []
mergesort [x] = [x]
mergesort xs  = merge (mergesort xs1) (mergesort xs2) d 
  where (xs1, xs2) = split xs
        d          = length xs