content: module ListMSort () 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, [])
  
  
  {-@ merge :: Ord a => xs:(OList a) -> ys:(OList a) -> d:{v:Int| v = len xs + len ys} -> {v:OList a | len v = d} / [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
  