content: {-@ LIQUID "--higherorder"         @-}
  {-@ LIQUID "--totality"            @-}
  {-@ LIQUID "--exactdc"             @-}
  {-@ LIQUID "--no-measure-fields"   @-}
  
  
  module DivideAndQunquer where 
  
  import Prelude hiding (error, map, take, drop)
  import Language.Haskell.Liquid.ProofCombinators 
  
  {-@ reflect mapReduce @-}
  mapReduce :: Int -> (List a -> b) -> (b -> b -> b) -> List a -> b 
  mapReduce n f op N  = f N  
  mapReduce n f op is = reduce op (map f (chunk n is)) 
  
  chunk  :: Int -> List a -> List (List a)
  map    :: (a -> b) -> List a -> List b
  reduce :: (b -> b -> b) -> List b -> b  
  
  {-@ mapReduceTheorem :: n:Int -> f:(List a -> b) -> op:(b -> b -> b) -> is:List a
        -> distributionThm:(is1:List a -> is2:List a -> {op (f is1) (f is2) == f (append is1 is2)} ) -> 
        { f is == mapReduce n f op is } / [llen is] @-}
  mapReduceTheorem :: Int -> (List a -> b) -> (b -> b -> b) -> List a -> (List a -> List a -> Proof)  -> Proof 
  mapReduceTheorem n f op N _
    =   mapReduce n f op N 
    ==. f N 
    *** QED 
  
  mapReduceTheorem n f op is _ 
    | llen is <= n || n <= 1 
    =   mapReduce n f op is 
    ==. reduce op (map f (chunk n is))
    ==. reduce op (map f (C is N))
    ==. reduce op (f is `C` map f N)
    ==. reduce op (f is `C` N)
    ==. f is
    *** QED 
  
  mapReduceTheorem n f op is distributionThm 
    = undefined   
  {-  =   mapReduce n f op is 
    ==. reduce op (map f (chunk n is))
    ==. reduce op (map f (C (take n is) (chunk n (drop n is))))
    ==. reduce op (f (take n is) `C` map f (chunk n (drop n is)))
    ==. op (f (take n is)) (reduce op (map f (chunk n (drop n is))))
    ==. op (f (take n is)) (mapReduce n f op (drop n is))
    ==. op (f (take n is)) (f (drop n is))
          ? mapReduceTheorem n f op (drop n is) distributionThm
    ==. f (append (take n is) (drop n is))
          ? distributionThm (take n is) (drop n is)
    ==. f is 
          ? appendTakeDrop n is
    *** QED  
   -}
  -------------------------------------------------------------------------------
  -----------  List Definition --------------------------------------------------
  -------------------------------------------------------------------------------
  
  
  {-@ data List [llen] a = N | C {lhead :: a, ltail :: List a} @-}
  data List a = N | C a (List a)
  
  llen :: List a -> Int 
  {-@ measure llen @-}
  {-@ llen :: List a -> Nat @-}
  llen N        = 0 
  llen (C _ xs) = 1 + llen xs
  
  -------------------------------------------------------------------------------
  -----------  List Manipulation ------------------------------------------------
  -------------------------------------------------------------------------------
  {-@ reflect map @-}
  {-@ map :: (a -> b) -> xs:List a -> {v:List b | llen v == llen xs } @-}
  map _  N       = N
  map f (C x xs) = f x `C` map f xs 
  
  {-@ reflect append @-}
  append :: List a -> List a -> List a 
  append N        ys = ys  
  append (C x xs) ys = x `C` (append xs ys)
  
  {-@ reflect reduce @-}
  {-@ reduce :: (b -> b -> b) -> is:{List b | 1 <= llen is } -> b @-}  
  reduce _  (C x N)  = x 
  reduce op (C x xs) = op x (reduce op xs)
  
  {-@ reflect chunk @-}
  {-@ chunk :: i:Int -> xs:List a -> {v:List (List a) | (1 <= llen v) &&  (if (i <= 1 || llen xs <= i) then (llen v == 1) else (llen v < llen xs)) } / [llen xs] @-}
  chunk i xs 
    | i <= 1 
    = C xs N 
    | llen xs <= i 
    = C xs N 
    | otherwise
    = C (take i xs) (chunk i (drop i xs))
  
  {-@ reflect drop @-}
  {-@ drop :: i:Nat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == llen xs - i } @-} 
  drop :: Int -> List a -> List a 
  drop i N = N 
  drop i (C x xs)
    | i == 0 
    = C x xs  
    | otherwise 
    = drop (i-1) xs 
  
  {-@ reflect take @-}
  {-@ take :: i:Nat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == i} @-} 
  take :: Int -> List a -> List a 
  take i N = N 
  take i (C x xs)
    | i == 0 
    = N  
    | otherwise 
    = C x (take (i-1) xs)
  
  -- | Helper Theorem 
  {-@ appendTakeDrop :: i:Nat -> xs:{List a | i <= llen xs} 
    -> {xs == append (take i xs) (drop i xs) }  @-}
  
  appendTakeDrop :: Int -> List a -> Proof 
  appendTakeDrop i N 
    =   append (take i N) (drop i N)
    ==. append N N 
    ==. N 
    *** QED 
  appendTakeDrop i (C x xs)
    | i == 0 
    =   append (take 0 (C x xs)) (drop 0 (C x xs))
    ==. append N (C x xs)
    ==. C x xs 
    *** QED 
    | otherwise
    =   append (take i (C x xs)) (drop i (C x xs))
    ==. append (C x (take (i-1) xs)) (drop (i-1) xs)
    ==. C x (append (take (i-1) xs) (drop (i-1) xs))
    ==. C x xs ? appendTakeDrop (i-1) xs 
    *** QED 
  
  