content: {-@ LIQUID "--higherorder"     @-}
  {-@ LIQUID "--exact-data-cons" @-}
  {-@ LIQUID "--alphaequivalence" @-}
  {-@ LIQUID "--betaequivalence" @-}
  
  {-# LANGUAGE IncoherentInstances   #-}
  {-# LANGUAGE FlexibleContexts #-}
  module ApplicativeReader where
  
  import Prelude hiding (fmap, id, seq, pure)
  
  import Proves
  import Helper (lambda_expand)
  
  -- | Applicative Laws :
  -- | identity      pure id <*> v = v
  -- | composition   pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
  -- | homomorphism  pure f <*> pure x = pure (f x)
  -- | interchange   u <*> pure y = pure ($ y) <*> u
  
  {-@ data Reader r a = Reader { runIdentity :: r -> a } @-}
  data Reader r a     = Reader { runIdentity :: r -> a }
  
  {-@ measure fromReader @-}
  fromReader :: Reader r a -> (r -> a)
  fromReader (Reader f) = f 
  
  
  {-@ axiomatize pure @-}
  pure :: a -> Reader r a
  pure x = Reader (\r -> x)
  
  {-@ axiomatize seq @-}
  seq :: Reader r (a -> b) -> Reader r a -> Reader r b
  seq (Reader f) (Reader x) = Reader (\r -> (f r) (x r))
  
  {-@ axiomatize idollar @-}
  idollar :: a -> (a -> b) -> b
  idollar x f = f x
  
  {-@ axiomatize compose @-}
  compose :: (b -> c) -> (a -> b) -> a -> c
  compose f g x = f (g x)
  
  {-@ axiomatize id @-}
  id :: a -> a
  id x = x
  
  -- | Identity
  
  {-@ identity :: x:Reader r a 
    -> { seq (pure id) x == x } @-}
  identity :: Arg r => Reader r a -> Proof
  identity (Reader r)
    =   seq (pure id) (Reader r)
    ==. seq (Reader (\w -> id)) (Reader r)
    ==. Reader (\q -> ((\w -> id) (q)) (r q))   
    ==. Reader (\q -> (id) (r q))            ? id_helper1 r
    ==. Reader (\q -> r q)                   ? id_helper2 r 
    ==. Reader r                             ? lambda_expand r 
    *** QED 
  
  
  -- NV: The following are the required helper functions as 
  -- we have no other way to prove equalities burried in lambdas. 
  -- This should be simplified
  
   
  
  id_helper2 :: Arg r => (r -> a) -> Proof 
  {-@ id_helper2 :: r:(r -> a) 
    -> { (\q:r -> r q) == (\q:r -> (id) (r q)) } @-}
  id_helper2 r 
    = ((\q -> r q) =*=: (\q -> (id) (r q))) (id_helper2_body r)
    *** QED 
  
  
  id_helper2_body :: Arg r => (r -> a) -> r ->  Proof 
  {-@ id_helper2_body :: r:(r -> a) -> q:r
    -> { (r q == (id) (r q)) 
      && (( (\q:r -> r q) (q)) == r q)
      && (((\q:r -> (id) (r q)) (q)) == id (r q))
       } @-}
  id_helper2_body r q
    = r q ==. id (r q) *** QED 
  
  
  id_helper1 :: Arg r => (r -> a) -> Proof 
  {-@ id_helper1 :: r:(r -> a) 
    -> { (\q:r -> (((\w:r -> id) (q)) (r q))) == (\q:r -> (id) (r q)) } @-}
  id_helper1 r 
    = ((\q -> (((\w -> id) q) (r q))) =*=: (\q -> id (r q))) (id_helper1_body r)
    *** QED 
  {-@ id_helper1_body :: r:(r -> a) -> q:r
    -> {(((\w:r -> id) (q)) (r q)) == (id) (r q) } @-}
  id_helper1_body :: Arg r => (r -> a) -> r -> Proof 
  id_helper1_body r q 
    =   ((\w -> id) q) (r q)
    ==. id (r q)
    *** QED   
  
  
  
  -- | Composition
  
  {-@ composition :: x:Reader r (a -> a)
                  -> y:Reader r (a -> a)
                  -> z:Reader r a
                  -> { seq (seq (seq (pure compose) x) y) z == seq x (seq y z) } @-}
  composition :: Arg r => Reader r (a -> a) -> Reader r (a -> a) -> Reader r a -> Proof
  composition (Reader x) (Reader y) (Reader z)
    =   seq (seq (seq (pure compose)            (Reader x))     (Reader y)) (Reader z) 
    ==. seq (seq (seq (Reader (\r1 -> compose)) (Reader x))     (Reader y)) (Reader z)
    ==. seq (seq (Reader (\r2 -> ((\r1 -> compose) r2) (x r2))) (Reader y)) (Reader z)
    ==. seq (seq (Reader (\r2 -> compose (x r2)))               (Reader y)) (Reader z)
    ==. seq (Reader (\r3 -> ((\r2 -> compose (x r2)) (r3)) (y r3)))         (Reader z) 
    ==. seq (Reader (\r3 -> (compose (x r3))               (y r3)))         (Reader z)
    ==. Reader (\r4 -> ((\r3 -> (compose (x r3)) (y r3)) r4) (z r4)) 
    ==. Reader (\r4 -> (compose (x r4) (y r4)) (z r4)) 
        ? composition_helper1 x y z 
    ==. Reader (\r4 -> (x r4) ((y r4) (z r4)))
    ==. Reader (\r4 -> (x r4) ((\r5 -> (y r5) (z r5)) (r4)))
    ==. seq (Reader x) (Reader (\r5 -> (y r5) (z r5)))
    ==. seq (Reader x) (seq (Reader y) (Reader z))
    *** QED 
  
  composition_helper1 :: Arg r => (r -> (a -> a)) -> (r -> (a -> a)) -> (r -> a) -> Proof 
  {-@ composition_helper1 
      :: x:(r -> (a -> a)) -> y:(r -> (a -> a)) -> z:(r -> a) 
      -> {(\r4:r -> (compose (x r4) (y r4)) (z r4))  == (\r4:r -> (x r4) ((y r4) (z r4))) }
    @-}
  composition_helper1 x y z = undefined  
  
  -- | homomorphism  pure f <*> pure x = pure (f x)
  
  {-@ homomorphism :: f:(a -> a) -> x:a
                   -> { seq (pure f) (pure x) == pure (f x) } @-}
  homomorphism :: (a -> a) -> a -> Proof
  homomorphism f x
    =   seq (pure f) (pure x)
    ==. seq (Reader (\r2 -> f)) (Reader (\r2 -> x))
    ==. Reader (\r -> ((\r2 -> f) r ) ((\r2 -> x) r))
    ==. Reader (\r -> f x)
    ==. pure (f x)
    *** QED 
  
  -- | interchange
  
  interchange :: Arg r => Reader r (a -> a) -> a -> Proof
  {-@ interchange :: u:(Reader r (a -> a)) -> y:a
       -> { seq u (pure y) == seq (pure (idollar y)) u }
    @-}
  interchange (Reader f) x
    =   seq (Reader f) (pure x)
    ==. seq (Reader f) (Reader (\r -> x))
    ==. Reader (\r' -> (f r') ((\r -> x) r'))
    ==. Reader (\r' -> (f r') x)                           ? interchange_helper_0 f x -- this is not required
    ==. Reader (\r' -> (idollar x) (f r'))                 ? interchange_helper_1 f x 
    ==. Reader (\r' -> ((\r'' -> (idollar x)) r') (f r'))  ? interchange_helper_2 f x 
    ==. seq (Reader (\r'' ->  (idollar x))) (Reader f)
    ==. seq (pure (idollar x)) (Reader f)
    *** QED 
  
  
  {-@ interchange_helper_0
    :: f:(r -> (a -> a)) -> x:a 
    -> {(\r':r -> (f r') (x)) == (\r':r -> (f r') ((\r:r -> x) (r')) )}
    @-} 
  interchange_helper_0 :: Arg r => (r -> (a -> a)) -> a -> Proof 
  interchange_helper_0 f x
    = (((\r -> (f r) x) =*=: (\r -> (f r) ((\r' -> x) r))) 
      (\_ -> simpleProof)) *** QED  
  
  
  {-@ interchange_helper_1 
    :: f:(r -> (a -> a)) -> x:a 
    -> {(\r':r -> (f r') (x)) == (\r':r -> (idollar x) (f r'))}
    @-} 
  interchange_helper_1 :: Arg r => (r -> (a -> a)) -> a -> Proof 
  interchange_helper_1 f x 
    =  (((\r -> (f r) x) =*=: (\r -> (idollar x) (f r))) (interchange_helper_1_body f x)) *** QED 
  
  {-@ interchange_helper_1_body 
    :: f:(r -> (a -> a)) -> x:a -> r':r
    -> {((f r') (x) == (idollar x) (f r'))
       && ((\r':r -> (f r') (x)) (r')  ==  (f r') (x))
       && ((\r':r -> (idollar x) (f r')) (r') == (idollar x) (f r'))
       }
    @-} 
  interchange_helper_1_body :: Arg r => (r -> (a -> a)) -> a -> r -> Proof 
  interchange_helper_1_body f x r 
    = f r x ==. (idollar x) (f r) *** QED 
  
  
  {-@ interchange_helper_2 
    :: f:(r -> (a -> a)) -> x:a 
    -> {(\r':r -> ((\r'':r -> (idollar x)) (r')) (f r')) == (\r':r -> (idollar x) (f r'))}
    @-} 
  interchange_helper_2 :: Arg r => (r -> (a -> a)) -> a -> Proof 
  interchange_helper_2 f x 
    =    (((\r' -> ((\r'' -> (idollar x)) (r')) (f r')) ) 
    =*=: (\r' -> (idollar x) (f r'))
         ) (interchange_helper_2_body f x) *** QED 
  
  {-@ interchange_helper_2_body 
    :: f:(r -> (a -> a)) -> x:a -> r':r
    -> {(\r':r -> ((\r'':r -> (idollar x)) (r')) (f r')) == (\r':r -> (idollar x) (f r'))}
    @-} 
  interchange_helper_2_body :: Arg r => (r -> (a -> a)) -> a -> r -> Proof 
  interchange_helper_2_body f x r'
    =    ((\r'' -> (idollar x)) (r')) (f r')
    ==.  (idollar x) (f r')
    *** QED 
  
  
  
  
  
  {-@ qual :: f:(r -> a) -> {v:Reader r a | v == Reader f} @-}
  qual :: (r -> a) -> Reader r a 
  qual = Reader 
   
  