content: {-@ LIQUID "--no-termination"    @-}
  
  module GhcListSort () where
  
  import Language.Haskell.Liquid.Prelude
  
  {-@ type OList a =  [a]<{\fld v -> (v >= fld)}>  @-}
  {-@ type DList a =  [a]<{\fld v -> (fld >= v)}>  @-}
  
  ---------------------------------------------------------------------------
  ---------------------------  Official GHC Sort ----------------------------
  ---------------------------------------------------------------------------
  
  {-@ sort1 :: (Ord a) => [a] -> OList a  @-}
  sort1 :: (Ord a) => [a] -> [a]
  sort1 = mergeAll . sequences
    where
      sequences (a:b:xs)
        | a > b     = descending b [a]  xs
        | otherwise = ascending  b (a:) xs -- a >= b => (a:) ->   
      sequences [x] = [[x]]
      sequences []  = [[]]
      {- descending :: x:a -> OList {v:a | x < v} -> [a] -> [OList a] @-}
      descending a as (b:bs)
        | a > b     = descending b (a:as) bs
      descending a as bs      = (a:as): sequences bs
  
      {- ascending :: x:a -> (OList {v:a|v>=x} -> OList a) -> [a] -> [OList a] @-}
      ascending a as (b:bs)
        | a <= b = ascending b (\ys -> as (a:ys)) bs -- a <= b
      ascending a as bs       = as [a]: sequences bs
  
      mergeAll [x] = x
      mergeAll xs  = mergeAll (mergePairs xs)
  
      mergePairs (a:b:xs) = merge1 a b: mergePairs xs
      mergePairs [x]      = [x]
      mergePairs []       = []
  
  -- merge1 needs to be toplevel,
  -- to get applied transformRec tx
  merge1 (a:as') (b:bs')
    | a > b               = b:merge1 (a:as')  bs'
    | otherwise           = a:merge1 as' (b:bs')
  merge1 [] bs            = bs
  merge1 as []            = as
  
  ---------------------------------------------------------------------------
  ------------------- Mergesort ---------------------------------------------
  ---------------------------------------------------------------------------
  
  {-@ sort2 :: (Ord a) => [a] -> OList a  @-}
  sort2 :: (Ord a) => [a] -> [a]
  sort2 = mergesort
  
  mergesort :: (Ord a) => [a] -> [a]
  mergesort = mergesort' . map wrap
  
  mergesort' :: (Ord a) => [[a]] -> [a]
  mergesort' [] = []
  mergesort' [xs] = xs
  mergesort' xss = mergesort' (merge_pairs xss)
  
  merge_pairs :: (Ord a) => [[a]] -> [[a]]
  merge_pairs [] = []
  merge_pairs [xs] = [xs]
  merge_pairs (xs:ys:xss) = merge xs ys : merge_pairs xss
  
  merge :: (Ord a) => [a] -> [a] -> [a]
  merge [] ys = ys
  merge xs [] = xs
  merge (x:xs) (y:ys)
    | x > y     = y : merge (x:xs)   ys
    | otherwise = x : merge    xs (y:ys)
  
  wrap :: a -> [a]
  wrap x = [x]
  
  ----------------------------------------------------------------------
  -------------------- QuickSort ---------------------------------------
  ----------------------------------------------------------------------
  
  {-@ sort3 :: (Ord a) => w:a -> [{v:a|v<=w}] -> OList a @-}
  sort3 :: (Ord a) => a -> [a] -> [a]
  sort3 w ls = qsort w ls []
  
  -- qsort is stable and does not concatenate.
  qsort :: (Ord a) =>  a -> [a] -> [a] -> [a]
  qsort _ []     r = r
  qsort _ [x]    r = x:r
  qsort w (x:xs) r = qpart w x xs [] [] r
  
  -- qpart partitions and sorts the sublists
  qpart :: (Ord a) => a -> a -> [a] -> [a] -> [a] -> [a] -> [a]
  qpart w x [] rlt rge r =
      -- rlt and rge are in reverse order and must be sorted with an
      -- anti-stable sorting
      rqsort x rlt (x:rqsort w rge r)
  qpart w x (y:ys) rlt rge r =
      case compare x y of
          GT -> qpart w x ys (y:rlt) rge r
          _  -> qpart w x ys rlt (y:rge) r
  
  -- rqsort is as qsort but anti-stable, i.e. reverses equal elements
  rqsort :: (Ord a) => a -> [a] -> [a] -> [a]
  rqsort _ []     r = r
  rqsort _ [x]    r = x:r
  rqsort w (x:xs) r = rqpart w x xs [] [] r
  
  rqpart :: (Ord a) => a -> a -> [a] -> [a] -> [a] -> [a] -> [a]
  rqpart w x [] rle rgt r =
      qsort x rle (x:qsort w rgt r)
  rqpart w x (y:ys) rle rgt r =
      case compare y x of
          GT -> rqpart w x ys rle (y:rgt) r
          _  -> rqpart w x ys (y:rle) rgt r
  
  
  
  
  
  
  
  
  
  
  
  
  
  