content: {-@ LIQUID "--pruneunsorted" @-}
  
  {-@ LIQUID "--no-termination" @-}
  {-@ LIQUID "--no-totality" @-}
  
  module Toy (sizeOf) where
  
  import Language.Haskell.Liquid.Prelude (isEven)
  
  -------------------------------------------------------------------------
  -- | Parametric Invariants over Base Types ------------------------------
  -------------------------------------------------------------------------
  
  maxInt     :: Int -> Int -> Int 
  maxInt x y = if x <= y then y else x 
  
  maximumInt ::  [Int] -> Int 
  maximumInt (x:xs) = foldr maxInt x xs
  
  {-@ maxEvens1 :: [Int] -> {v:Int | v mod 2 = 0 } @-}
  maxEvens1 xs = maximumInt (0 : xs') 
    where xs' = [ x | x <- xs, isEven x]
  
  -------------------------------------------------------------------------
  -- | Parametric Invariants over Class-Predicated Tyvars -----------------
  -------------------------------------------------------------------------
  
  maxPoly     :: (Ord a) => a -> a -> a 
  maxPoly x y = if x <= y then y else x
  
  maximumPoly :: (Ord a) => [a] -> a
  maximumPoly (x:xs) = foldr maxPoly x xs
  
  {-@ maxEvens2 :: [Int] -> {v:Int | v mod 2 = 0 } @-}
  maxEvens2 xs = maximumPoly (0 : xs') 
    where xs' = [ x | x <- xs, isEven x]
  
  -------------------------------------------------------------------------
  -- | Induction over Int Ranges ------------------------------------------
  -------------------------------------------------------------------------
  
  {-@ foldN :: forall a <p :: x0:Int -> x1:a -> Bool>. 
                  (i:Int -> a<p i> -> a<p (i+1)>) 
                -> n:{v: Int | v >= 0}
                -> a <p 0> 
                -> a <p n>
    @-}
  
  foldN :: (Int -> a -> a) -> Int -> a -> a
  foldN f n = go 0 
    where go i x | i < n     = go (i+1) (f i x)
                 | otherwise = x
  
  {-@ count :: m: {v: Int | v > 0 } -> {v: Int | v = m} @-}
  count :: Int -> Int
  count m = foldN (\_ n -> n + 1) m 0
  
  -------------------------------------------------------------------------
  -- | Induction over Data types ------------------------------------------
  -------------------------------------------------------------------------
  
  data Vec a = Nil | Cons a (Vec a)
  
  {-@ data Vec [sizeOf] @-} -- a = Nil | Cons (x::a) (xs::Vec a) 
  
  -- | As a warmup, lets check that a /real/ length function indeed computes
  -- the length of the list.
  
  {-@ measure sizeOf @-}
  {-@ sizeOf :: xs:Vec a -> {v: Int | v = sizeOf xs} @-}
  sizeOf             :: Vec a -> Int
  sizeOf Nil         = 0
  sizeOf (Cons _ xs) = 1 + sizeOf xs
  
  -------------------------------------------------------------------------
  -- | Higher-order fold -------------------------------------------------- 
  -------------------------------------------------------------------------
  
  -- | Time to roll up the sleeves. Here's a a higher-order @foldr@ function
  -- for our `Vec` type. Note that the `op` argument takes an extra /ghost/
  -- parameter that will let us properly describe the type of `efoldr` 
  
  {-@ efoldr :: forall a b <p :: x0:Vec a -> x1:b -> Bool>. 
                  (xs:Vec a -> x:a -> b <p xs> -> b <p (Toy.Cons x xs)>) 
                -> b <p Toy.Nil> 
                -> ys: Vec a
                -> b <p ys>
    @-}
  efoldr :: (Vec a -> a -> b -> b) -> b -> Vec a -> b
  efoldr op b Nil         = b
  efoldr op b (Cons x xs) = op xs x (efoldr op b xs) 
  
  -------------------------------------------------------------------------
  -- | Clients of `efold` ------------------------------------------------- 
  -------------------------------------------------------------------------
  
  -- | Finally, lets write a few /client/ functions that use `efoldr` to 
  -- operate on the `Vec`s. 
  
  -- | First: Computing the length using `efoldr`
  {-@ size :: xs:Vec a -> {v: Int | v = sizeOf(xs)} @-}
  size :: Vec a -> Int
  size = efoldr (\_ _ n -> n + 1) 0
  
  -- | The above uses a helper that counts up the size. (Pesky hack to avoid writing qualifier v = ~A + 1)
  {-@ suc :: x:Int -> {v: Int | v = x + 1} @-}
  suc :: Int -> Int
  suc x = x + 1 
  
  -- | Second: Appending two lists using `efoldr`
  {-@ app  :: xs: Vec a -> ys: Vec a -> {v: Vec a | sizeOf(v) = sizeOf(xs) + sizeOf(ys) } @-} 
  app xs ys = efoldr (\_ z zs -> Cons z zs) ys xs 
  
  