content: {-@ LIQUID "--short-names"    @-}
  {-@ LIQUID "--no-warnings"    @-}
  {-@ LIQUID "--no-termination" @-}
  
  module AbstractRefinements (
      listMax
    , insertSort
    , insertSort'
    ) where
  
  
  import Data.Set hiding (insert, foldr,size) 
  import Prelude hiding (map, foldr)
  
  
  
  -----------------------------------------------------------------------
  -- | 0. Abstract Refinements 
  -----------------------------------------------------------------------
  
  
  -- Warmup: How shall we type listMax?
  
  {-@ listMax  :: forall <p :: Int -> Prop>. {v:[Int<p>] | len v > 0}
               -> Int<p> @-}
  listMax     :: [Int] -> Int
  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 <= 255}  @-}
  
  
  -- compute the largest of some lists
  
  {-@ xE :: Even @-}
  xE = listMax [0, 1] 
  
  
  
  {-@ xO :: Odd @-}
  xO = listMax [1, 21, 4001, 961] 
  
  
  
  {-@ xR :: RGB @-}
  xR = listMax [1, 21, 41, 61] 
  
  
  -- Why do we get the errors? How do we fix it?
  
  
  
  
  
  
  
  
  
  -----------------------------------------------------------------------
  -- | 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 <{\x1 x2 -> x1 <= x2}> a@-} 
  {-@ type DecrList a = List <{\x1 x2 -> x1 >= x2}> a@-} 
  {-@ type DiffList a = List <{\x1 x2 -> x1 /= x2}> a@-} 
  
  ups, downs  :: List Int
  
  {-@ ups :: IncrList Int @-}
  ups   = 1 `C` 2 `C` 3 `C` N
  
  {-@ downs :: DecrList Int @-}
  downs = 10 `C` 8 `C` 6 `C` N
  
  
  
  
  -----------------------------------------------------------------------
  -- | 3. Insertion Sort: Revisited
  -----------------------------------------------------------------------
  
  {-@ insert         :: _ -> xs:_ -> {v:_ | 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 | EqSize v xs} @-}
  insertSort N        = N
  insertSort (C x xs) = insert x (insertSort xs)
  
  
  
  
  
  
  
  
  
  
  
  -----------------------------------------------------------------------
  -- | 3. Insertion Sort: using a `foldr` 
  -----------------------------------------------------------------------
  
  
  {-@ insertSort' :: xs:List a -> {v:IncrList a | true } @-}
  insertSort' xs = foldr insert N xs 
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  -----------------------------------------------------------------------
  -- | 4. But, there are limits...
  -----------------------------------------------------------------------
  
  -- how big is the list returned by insertSort' ?
  
  
  -- Hmm. Thats a bummer... How do we type `foldr` to verify the above?
  
  
  
  
  
  
  
  
  
  
  
  -----------------------------------------------------------------------
  -- | 5. Induction, as an Abstract Refinement 
  -----------------------------------------------------------------------
  
  
  ifoldr = undefined
  
  {- insertSort' :: xs:List a -> {v:IncrList a | size v = size xs} -}
  
  
  
  
  
  
  
  -----------------------------------------------------------------------
  -- | 6. But can you prove that you've permuted the input?
  -----------------------------------------------------------------------
  
  
  -- Lets reason about the set of elements in a container
  
  -- measure elems
  
  {-@ predicate EqSize X Y = size X = size Y @-}
  
  -- predicate EqElems
  
  
  -----------------------------------------------------------------------
  -- | 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)
   
  