------------------------------------------------------------------------------
-- | An implementation of Merge Sort, where LH verifies:
--   1. Termination (Totality) 
--   2. The output is indeed in non-decreasing order 
------------------------------------------------------------------------------

module MergeSort (sort) where

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

{-@ type OListN a N = {v:OList a | len v == N} @-}

-- | The top level `sort` function. Proved:
--   (a) terminating, 
--   (b) ordered, and 
--   (c) of same size as input.

{-@ sort :: (Ord a) => xs:[a] -> OListN a {len xs} @-}
sort :: Ord a => [a] -> [a]
sort []   = []
sort [x]  = [x]
sort xs   = merge (sort xs1) (sort xs2) 
  where 
    (xs1, xs2) = split xs

-- Fun fact: if you delete the singleton case above,
-- the resulting function is, in fact, non-terminating!

-- | A type describing two `Halves` of a list `Xs` 

{-@ type Halves a Xs = {v: (Half a Xs, Half a Xs) | len (fst v) + len (snd v) == len Xs} @-}

-- | Each `Half` is empty or smaller than the input:

{-@ type Half a Xs  = {v:[a] | 2 * len v < 1 + len Xs} @-}

-- | The `split` function breaks its list into two `Halves`:

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

-- | Finally, the `merge` function combines two ordered lists into a single ordered result.

{-@ merge :: Ord a => xs:OList a -> ys:OList a -> OListN a {len xs + len ys} / [(len xs + len ys)] @-}
merge :: Ord a => [a] -> [a] ->  [a]
merge xs []         = xs
merge [] ys         = ys
merge (x:xs) (y:ys)
  | x <= y          = x : merge xs (y:ys)
  | otherwise       = y : merge (x:xs) ys