content: module ListMSort_LType () where
  {-@ LIQUID "--no-termination" @-}
  
  import Language.Haskell.Liquid.Prelude
  
  {-@
  data List a <p :: x0:a -> x1:a -> Bool>
    = Nil
    | Cons (h :: a) (t :: List <p> (a <p h>))
  @-}
  data List a = Nil | Cons a (List a)
  
  
  -- This is needed to conclude that
  -- xs = Nil /\ xs = Cons _ _ <=> false
  
  {-@ measure llen @-}
  llen :: (List a) -> Int
  llen Nil       = 0
  llen (Cons x xs) = 1 + llen xs
  
  {-@ invariant {v:List a | (llen v) >= 0} @-}
  
  split :: List a -> (List a, List a)
  split (Cons x (Cons y zs)) = (Cons x xs, Cons y ys) where (xs, ys) = split zs
  split xs                   = (xs, Nil)
  
  
  {-@ lazy merge @-}
  merge :: Ord a => List a -> List a -> List a
  merge xs Nil = xs
  merge Nil ys = ys
  merge (Cons x xs) (Cons y ys)
    | x <= y
    = Cons x (merge xs (Cons y ys))
    | otherwise
    = Cons y (merge (Cons x xs) ys)
  
  mergesort :: Ord a => List a -> List a
  mergesort Nil = Nil
  mergesort (Cons x Nil) = Cons x Nil
  mergesort xs = merge (mergesort xs1) (mergesort xs2) where (xs1, xs2) = split xs
  
  chk y =
    case y of
     Nil -> True
     Cons x1 xs -> case xs of
                    Nil -> True
                    Cons x2 xs2 -> liquidAssertB (x1 <= x2) && chk xs2
  
  bar = mergesort $ mkList [1 .. 100]
  
  barI :: List Int
  barI = Cons 1 $ Cons 2 $ Cons 3 Nil
  
  mkList :: Ord a => [a] -> List a
  mkList = foldr Cons Nil
  
  prop0 = chk bar
  prop1 = chk barI
  