module ListSort () where
{-@ type OList a = [a]<{\fld v -> v >= fld}> @-}
{-@ insertSort :: (Ord a) => xs:[a] -> {v : OList a | len(v) = len(xs)} @-}
insertSort :: (Ord a) => [a] -> [a]
insertSort [] = []
insertSort (x:xs) = insert x (insertSort xs)
{-@ insertSort' :: (Ord a) => xs:[a] -> OList a @-}
insertSort' :: (Ord a) => [a] -> [a]
insertSort' xs = foldr insert [] xs
{-@ insert :: (Ord a) => x:a -> xs: OList a -> {v: OList a | len(v) = (1 + len(xs)) } @-}
insert y [] = [y]
insert y (x : xs) | y <= x = y : x : xs
| otherwise = x : insert y xs