LiquidHaskell TreeSort example

TreeSort.hs

{-@ LIQUID "--exact-data-cons" @-}
{-@ LIQUID "--higherorder" @-}

module TreeSort where

import Prelude hiding ((.), concat, filter, foldr, map)
import Language.Haskell.Liquid.ProofCombinators


data List a = Nil | Cons a (List a)
{-@ autosize List @-}
{-@ data List a = Nil | Cons {hd :: a, tl :: List a} @-}

{-@ reflect map @-}
map :: (a -> b) -> List a -> List b
map f Nil = Nil
map f (Cons x xs) = Cons (f x) (map f xs)

{-@ reflect filter @-}
filter :: (a -> Bool) -> List a -> List a
filter f Nil = Nil
filter f (Cons x xs) = if f x then Cons x (filter f xs) else filter f xs

{-@ reflect append @-}
append :: List a -> List a -> List a
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

{-@ reflect concat @-}
concat :: List (List a) -> List a
concat Nil = Nil
concat (Cons l ls) = append l (concat ls)

{-@ reflect foldr @-}
foldr :: (a -> b -> b) -> b -> List a -> b
foldr f i Nil = i
foldr f i (Cons x xs) = f x (foldr f i xs)

{-@ reflect o @-}
o :: (b -> c) -> (a -> b) -> a -> c
f `o` g = \x -> f (g x)


ordered :: Ord b => List (a -> b) -> a -> a -> Bool
ordered Nil _ _ = True
ordered (Cons d ds) x y = d x < d y || (d x == d y) && ordered ds x y

data Tree a = Leaf a | Node (List (Tree a))

{-@ reflect mktree @-}
mktree :: (Bounded b, Enum b, Eq b) => List (a -> b) -> List a -> Tree (List a)
mktree = foldr fm Leaf
  where
    fm d g = Node `o` map g `o` ptn d

ptn :: (Bounded b, Enum b, Eq b) => (a -> b) -> List a -> List (List a)
ptn d xs = map (\m -> filter ((m ==) `o` d) xs) rng

rng :: (Bounded a, Enum a, Eq a) => List a
rng = rng1 minBound maxBound
  where
    rng1 max x | max == x = Cons x Nil
               | otherwise = Cons x (rng1 max (succ x))

{-@ reflect flatten @-}
flatten :: Tree (List a) -> List a
flatten = foldt id concat

{-@ reflect foldt @-}
foldt :: (a -> b) -> (List b -> b) -> Tree a -> b
foldt f g (Leaf x) = f x
foldt f g (Node ts) = g (map (foldt f g) ts)

{-@ reflect treesort @-}
treesort :: (Bounded b, Enum b, Eq b) => List (a -> b) -> List a -> List a
treesort = (flatten `o`) `o` mktree