content: module GhcSort3 () where
  
  {-@ LIQUID "--no-termination" @-}
  
  {-@ type OList a =  [a]<{\fld v -> (v >= fld)}>  @-}
  
  {-@ assert sort3 :: (Ord a) => w:a -> [{v:a|v<=w}] -> OList a @-}
  sort3 :: (Ord a) => a -> [a] -> [a]
  sort3 w ls = qsort w ls []
  
  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 :: (Ord a) => a -> a -> [a] -> [a] -> [a] -> [a] -> [a]
  qpart w x [] rlt rge r =
      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 :: (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
  
  