module ListSort () where {-@ LIQUID "--no-termination" @-} import Language.Haskell.Liquid.Prelude {-@ type OList a = [a]<{\x v -> v >= x}> @-} {-@ assume (++) :: forall

Bool, q :: a -> Bool, r :: a -> Bool>. {x::a

|- a <: {v:a| x <= v}} {a

<: a} {a <: a} Ord a => OList (a

) -> OList (a) -> OList a @-} {-@ app :: forall

Bool, q :: a -> Bool, r :: a -> Bool>. {x::a

|- a <: {v:a| x <= v}} {a

<: a} {a <: a} Ord a => OList (a

) -> OList (a) -> OList a @-} app :: Ord a => [a] -> [a] -> [a] app [] ys = ys app (x:xs) ys = x:(app xs ys) takeL :: Ord a => a -> [a] -> [a] {-@ takeL :: Ord a => x:a -> [a] -> [{v:a|v<=x}] @-} takeL x [] = [] takeL x (y:ys) = if (y a -> [a] -> [a] {-@ takeGE :: Ord a => x:a -> [a] -> [{v:a|v>=x}] @-} takeGE x [] = [] takeGE x (y:ys) = if (y>=x) then y:(takeGE x ys) else takeGE x ys {-@ quicksort :: (Ord a) => xs:[a] -> [a]<{\fld v -> (v >= fld)}> @-} quicksort [] = [] quicksort (x:xs) = xsle ++ (x:xsge) where xsle = quicksort (takeL x xs) xsge = quicksort (takeGE x xs) {-@ qsort :: (Ord a) => xs:[a] -> [a]<{\fld v -> (v >= fld)}> @-} qsort [] = [] qsort (x:xs) = (qsort [y | y <- xs, y < x]) ++ (x:(qsort [z | z <- xs, z >= x]))