01_AbstractRefinements.hs

{-@ LIQUID "--short-names"    @-}
{-@ LIQUID "--no-warnings"    @-}
{-@ LIQUID "--no-termination" @-}

module AbstractRefinements (
    listMax
  , insertSort
  , insertSort'
  , insertSort''
  , insertSort'''
  ) where

import Data.Set hiding (insert, foldr,size) 
import Prelude hiding (map, foldr)

listMax     :: [Int] -> Int

-----------------------------------------------------------------------
-- | 0. Abstract Refinements 
-----------------------------------------------------------------------

{-@ listMax :: forall <p :: Int -> Prop>. {v:[Int<p>] | len v > 0} -> Int<p> @-} 
listMax xs  = foldr1 max xs 


-- Lets define a few different subsets of Int

{-@ type Even = {v:Int | v mod 2 == 0}      @-}
{-@ type Odd  = {v:Int | v mod 2 /= 0}      @-}
{-@ type RGB  = {v:Int | 0 <= v && v < 256} @-}



{-@ xE :: Even @-}
xE = listMax [0, 200, 4000, 60] 


{-@ xO :: Odd @-}
xO = listMax [1, 21, 4001, 961] 


{-@ xR :: RGB @-}
xR = listMax [1, 21, 41, 61] 



-----------------------------------------------------------------------
-- | 1. Abstract Refinement from List's Type 
-----------------------------------------------------------------------



{-@ data List a <p :: a -> a -> Prop> 
     = N | C {x :: a, xs :: List<p> a<p x>} @-}



-----------------------------------------------------------------------
-- | 2. Instantiating Abstract Refinements 
-----------------------------------------------------------------------




{-@ type IncrList a = List <{\x y -> x <= y}> a @-} 
{-@ type DecrList a = List <{\x y -> x >= y}> a @-} 
{-@ type DiffList a = List <{\x y -> x /= y}> a @-} 

{-@ ups   :: IncrList Integer @-}
ups       = 1 `C` 2 `C` 4 `C` N

{-@ downs :: DecrList Integer @-}
downs     = 100 `C` 20 `C` 4 `C` N

{-@ diffs :: DiffList Integer @-}
diffs     = 100 `C` 1000 `C` 10 `C` 1 `C`  N



-----------------------------------------------------------------------
-- | 3. Insertion Sort: Revisited
-----------------------------------------------------------------------

{-@ insert         :: x:_ -> xs:_ -> {v:_ | AddElt v x xs && size v = 1 + size xs} @-}
insert x N         = x `C` N
insert x (C y ys)
  | x <= y         = x `C` y `C` ys
  | otherwise      = y `C` insert x ys 



{-@ insertSort      :: xs:List a -> {v:IncrList a | size v = size xs} @-}
insertSort N        = N
insertSort (C x xs) = insert x (insertSort xs)



-----------------------------------------------------------------------
-- | 3. Insertion Sort: using a `foldr` 
-----------------------------------------------------------------------



{-@ insertSort' :: xs:List a -> IncrList a @-}
insertSort' xs = foldr insert N xs




-----------------------------------------------------------------------
-- | 4. But, there are limits...
-----------------------------------------------------------------------

-- but why is this not ok?

{-@ insertSort'' :: xs:List a -> {v:IncrList a | EqSize v xs && EqElem v xs} @-}
insertSort'' xs   = foldr insert N xs


-- Hmm. Thats a bummer... How do we type `foldr` to verify the above?


-----------------------------------------------------------------------
-- | 5. Induction, as an Abstract Refinement 
-----------------------------------------------------------------------


{-@ ifoldr :: forall a b <p :: List a -> b -> Prop>. 
                 (xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)>) 
               -> b<p N> 
               -> ys:List a
               -> b<p ys>                            @-}
ifoldr :: (List a -> a -> b -> b) -> b -> List a -> b
ifoldr f b N        = b
ifoldr f b (C x xs) = f xs x (ifoldr f b xs)


{-@ insertSort''' :: xs:List a -> {v:IncrList a | EqSize v xs && EqElem v xs} @-}
insertSort''' xs = ifoldr (\_ -> insert) N xs




-----------------------------------------------------------------------
-- | Old definitions from 00_Refinements.hs
-----------------------------------------------------------------------

data List a = N | C a (List a)

infixr 9 `C`

{-@ measure size @-}
size          :: List a -> Int
size (C x xs) = 1 + size xs 
size N        = 0

foldr f acc N        = acc
foldr f acc (C x xs) = f x (foldr f acc xs)


{-@ predicate EqSize X Y = size X  = size Y @-}
{-@ predicate EqElem X Y = elems X = elems Y @-}

{-@ predicate AddElt V X Xs = elems V = Set_cup (Set_sng X) (elems Xs) @-}
 
{-@ measure elems ::List a -> (Set a)
    elems (N)      = (Set_empty 0)
    elems (C x xs) = (Set_cup (Set_sng x) (elems xs))
  @-}