content: {-@ LIQUID "--higherorder"     @-}
  {-@ LIQUID "--exact-data-cons" @-}
  {-@ LIQUID "--alphaequivalence" @-}
  {-@ LIQUID "--betaequivalence"  @-}
  
  {-# LANGUAGE IncoherentInstances #-}
  {-# LANGUAGE FlexibleContexts    #-}
  module FunctorReader where
  
  import Prelude hiding (fmap, id)
  
  import Proves
  import Helper 
  
  -- | Functor Laws :
  -- | fmap-id fmap id ≡ id
  -- | fmap-distrib ∀ g h . fmap (g ◦ h) ≡ fmap g ◦ fmap h
  
  {-@ data Reader r a = Reader { runIdentity :: r -> a } @-}
  data Reader r a     = Reader { runIdentity :: r -> a }
  
  {-@ reflect fmap @-}
  fmap :: (a -> b) -> Reader r a -> Reader r b
  fmap f (Reader rd) = Reader (\r -> f (rd r))
  
  {-@ reflect id @-}
  id :: a -> a
  id x = x
  
  {-@ reflect compose @-}
  compose :: (b -> c) -> (a -> b) -> a -> c
  compose f g x = f (g x)
  
  -- | Identity 
  
  {-@ fmap_id :: xs:Reader r a -> { fmap id xs == id xs } @-}
  fmap_id :: Arg r => Reader r a  ->  Proof
  fmap_id (Reader x) 
     =   fmap id (Reader x)
     ==. Reader (\r -> id (x r))
     ==. Reader (\r -> x r)       ? fmap_id_helper x  
     ==. Reader x                 ? lambda_expand x 
     ==. id (Reader x)
     *** QED
   
  
  {-@ fmap_id_helper ::  f:(r -> a)
              -> { (\r:r -> (id (f r))) == (\r:r-> (f (r))) } @-}
  fmap_id_helper :: (Arg r) => (r -> a) ->  Proof
  fmap_id_helper f
     =    ((\r -> id (f r)) 
     =*=: (\r -> f r)) (fmap_id_helper_body f)
     *** QED 
  
  
  {-@ fmap_id_helper_body 
    :: f:(r -> a) -> r:r 
    -> {(id (f r) == f r) 
        && ((\r:r -> (id (f r))) (r) == id (f r))  
        && ((\r:r-> (f r)) (r) == f r) 
        } @-} 
  fmap_id_helper_body :: Arg r => (r -> a) -> r -> Proof 
  fmap_id_helper_body f r 
    = id (f r) ==. f r *** QED 
  
  
  
  {-@ fmap_distrib :: f:(a -> a) -> g:(a -> a) -> xs:Reader r a
                 -> { fmap  (compose f g) xs == (compose (fmap f) (fmap g)) (xs) } @-}
  fmap_distrib :: Arg r => (a -> a) -> (a -> a) -> Reader r a -> Proof
  fmap_distrib f g (Reader x)
    =   fmap (compose f g) (Reader x)
    ==. Reader (\r -> (compose f g) (x r))     
    ==. Reader (\r -> f ( g (x r)))            ? fmap_distrib_helper f g x 
    ==. Reader (\r -> f ((\w -> g (x w)) r))
    ==. fmap f (Reader (\w -> g (x w)))
    ==. fmap f (fmap g (Reader x))
    ==. (compose (fmap f) (fmap g)) (Reader x)
    *** QED
  
  
  
  
  
  fmap_distrib_helper :: Arg r => (a -> a) -> (a -> a) -> (r -> a) -> Proof 
  {-@ fmap_distrib_helper
    :: f:(a -> a) -> g:(a -> a) -> x:(r -> a) 
    -> {(\r:r -> (compose f g) (x r)) == (\r:r -> (f (g (x r))) ) } @-}
  fmap_distrib_helper f g x 
    =   ((\r -> (compose f g) (x r)) 
    =*=: (\r -> f (g (x r)))) (fmap_distrib_helper' f g x)
    *** QED 
  
  
  
  fmap_distrib_helper' :: Arg r => (a -> a) -> (a -> a) -> (r -> a) -> r -> Proof 
  {-@ fmap_distrib_helper' 
    :: f:(a -> a) -> g:(a -> a) -> x:(r -> a) -> r:r
    -> { (\r:r -> (compose f g) (x r)) (r) == (\r:r -> (f (g (x r)))) (r) } @-}
  fmap_distrib_helper' f g x r  
    =   (compose f g) (x r) 
    ==. f (g (x r))
    *** QED 
  
  
  
  {-@ qual :: f:(r -> a) -> {v:Reader r a | v == Reader f} @-}
  qual :: (r -> a) -> Reader r a 
  qual = Reader 
  