module GhcSort () 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