content: {-@ LIQUID "--short-names"    @-}
  {-@ LIQUID "--no-warnings"    @-}
  {-@ LIQUID "--no-termination" @-}
  
  module AbstractRefinements (
      listMax
    , insertSort
    , insertSort'
    , insertSort''
    ) where
  
  import Data.Set hiding (insert, foldr,size,filter, append) 
  import Prelude hiding (map, foldr, filter, append)
  
  listMax     :: [Int] -> Int
  
  
  
  -----------------------------------------------------------------------
  -- | #1. 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] 
  
  
  
  
  
  
  
  -- > RJ: Return to slides for 06_Inductive
  
  
  
  
  
  
  
  
  
  -----------------------------------------------------------------------
  -- | #2. 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)
  
  
  
  
  
  
  
  
  {-@ append :: xs:List a -> ys:List a -> {v:List a | UnElems v xs ys} @-} 
  append xs ys = ifoldr (\_ -> C) ys xs 
  
  
  
  
  
  
  
  {-@ filter :: (a -> Bool) -> xs:List a -> {v:List a | SubElems v xs } @-} 
  filter f xs = ifoldr (id (\_ x ys -> if f x then C x ys else ys)) N xs
  
  
  
  
  
  
  -- > RJ: Return to slides for 08_Recursive
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  -----------------------------------------------------------------------
  -- | #3. Abstract Refinement from List's Type 
  -----------------------------------------------------------------------
  
  
  {-@ data List a <p :: a -> a -> Prop> 
       = N | C {hd :: a, tl :: List<p> (a<p hd>) } @-}
  
  
  
  
  
  
  
  
  -----------------------------------------------------------------------
  -- | #4. Instantiating Abstract Refinements on Lists 
  -----------------------------------------------------------------------
  
  
  {-@ 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
  
  -----------------------------------------------------------------------
  -- | 5. Insertion Sort
  -----------------------------------------------------------------------
  
  {-@ insert         :: x:a -> xs:IncrList a -> {v:IncrList a | 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 -> IncrList a @-}
  insertSort N        = N
  insertSort (C x xs) = insert x (insertSort xs)
  
  -----------------------------------------------------------------------
  -- | 6. Insertion Sort: using a `foldr` 
  -----------------------------------------------------------------------
  
  {-@ insertSort' :: xs:List a -> IncrList a @-}
  insertSort' xs = foldr insert N xs
  
  
  
  
  
  
  
  -- Or even better... we can use `ifoldr`
  
  {-@ insertSort'' :: xs:List a -> {v:IncrList a | EqSize v xs && EqElem v xs} @-}
  insertSort'' xs = ifoldr (\_ -> insert) N xs
  
  
  
  
  
  
  
  
  -- > RJ: Return to slides for "07_Array"
  
  
  
  
  
  
                
  -----------------------------------------------------------------------
  -- | Boilerplate 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 UnElems X Y Z = elems X = Set_cup (elems Y) (elems Z)    @-}
  {-@ predicate SubElems X Y  = Set_sub (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))
    @-}
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  {-@ predicate SubConsElems X Y Ys = Set_sub (elems X) (Set_cup (Set_sng Y) (elems Ys)) @-}
  
  {-@ qual1  :: y:_ -> ys:_ -> {v:_ | SubConsElems v y ys} @-}
  qual1 :: a -> List a -> List a 
  qual1 y ys = undefined 
  
  {-@ qual2  :: y:_ -> ys:_ -> {v:_ | size v <= 1 + size ys} @-}
  qual2 :: a -> List a -> List a 
  qual2 y ys = undefined 
  
  
  
  