module GhcSort (qsort) where
{-@ type OList a = [a]<{\fld v -> (v >= fld)}> @-}
{-@ assert sort3 :: (Ord a) => [a] -> OList a @-}
sort3 :: (Ord a) => [a] -> [a]
sort3 = qsort
qsort:: (Ord a) => [a] -> [a]
{-@ qsort:: (Ord a) => xs:[a] -> OList a / [(len xs), 0]@-}
qsort [] = []
qsort (x:xs) = qpart x xs [] []
qpart :: (Ord a) => a -> [a] -> [a] -> [a] -> [a]
{-@ qpart :: (Ord a) => x:a -> q:[a] -> r:[{v:a | (v < x)}] -> p:[{v:a |(v >= x)}] -> OList a / [((len p) + (len r) + (len q)), ((len q) + 1)]@-}
qpart x [] rlt rge =
app x (qsort rlt) (x:qsort rge)
qpart x (y:ys) rlt rge =
case compare x y of
GT -> qpart x ys (y:rlt) rge
_ -> qpart x ys rlt (y:rge)
{-@ app :: Ord a => x:a -> (OList ({v:a | v < x})) -> (OList ({v:a| v >= x})) -> OList a @-}
app :: Ord a => a -> [a] -> [a] -> [a]
app k [] ys = ys
app k (x:xs) ys = x : (app k xs ys)