{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Data.Functor where

import           Prelude                 hiding ( Functor(..)
                                                , Applicative(..)
                                                , Monad(..)
                                                , Foldable(..)
                                                , Maybe(..)
                                                , Monoid(..)
                                                , Semigroup(..)
                                                , Either(..)
                                                , id
                                                , flip
                                                , const
                                                , apply
                                                )
import           Liquid.ProofCombinators
import           Data.List
import Data.Function
import Data.Functor.Classes
-- TODO: Move these to a separate module. 



-- TODO: Define `Maybe a` in Data.Maybe



-- Kleisli Arrow



{-@ data Pair a b = Pair {projl :: a, projr :: b }  @-}
data Pair l r = Pair {projl :: l, projr :: r }
-- Writer Monad
instance Functor (Pair u) where
  fmap f (Pair u a) = (Pair u (f a))
  a <$ (Pair u _) = (Pair u a)

instance VFunctor (Pair u) where
  lawFunctorId (Pair _ _) = ()
  lawFunctorComposition _ _ _ = ()

-- instance Monoid u => Applicative (Pair u) where
--   pure x = Pair mempty x
--   ap (Pair u f) (Pair v x) = (Pair (u `mappend` v) (f x))
--   liftA2 f x y = pure f `ap` x `ap` y
--   a1 *> a2 = ap (id <$ a1) a2
--   a1 <* a2 = liftA2 const a1 a2

-- instance Monoid u => Monad (Pair u) where
--   bind (Pair u a) k = case k a of
--     (Pair v b) -> (Pair (mappend u v) b)
--   return = pure
--   mseq (Pair u _) (Pair v a) = (Pair (mappend u v) a)




-- instance (VMonoid u) => VApplicative (Pair u) where
--   lawApplicativeId _ = ()
--   lawApplicativeComposition (Pair _ _) (Pair _ _) (Pair _ _)  = ()
--   lawApplicativeHomomorphism f x (Pair _ _) = ()
--   lawApplicativeInterchange (Pair _ _) _ = ()



-- data Compose f g a = Compose {getCompose :: f (g a)}

-- instance (Functor f, Functor g) => Functor (Compose f g) where
--   fmap f (Compose x) = Compose $ fmap (fmap f) x
--   x <$ m = fmap (const x) m

-- instance (VFunctor f, VFunctor g) => VFunctor (Compose f g) where
-- --    {-@ lawFunctorId :: forall a . x:m a -> {fmap id x == id x} @-}
--   lawFunctorId (Compose x) =
--     (axiomExt (fmap id :: g a -> g a) id $ \x -> ()) `cast`
--     fmap id (Compose x) `cast`
--     fmap (fmap id) x `cast`
--     lawFunctorId x `cast`
--     ()
--   lawFunctorComposition f g (Compose x) =
--     fmap (fmap (compose f g)) x `cast`
--     ()

--    {-@ lawFunctorComposition :: forall a b c . f:(b -> c) -> g:(a -> b) -> x:m a -> { fmap (compose f g) x == compose (fmap f) (fmap g) x } @-}
--    lawFunctorComposition :: forall a b c. (b -> c) -> (a -> b) -> m a -> ()







-- Instantiation
-- {-@ optionCompose :: f:(a -> Optional b) -> g:(b -> Optional c) -> h:(c -> Optional d) -> x:a -> {kcompose (kcompose f g) h x == kcompose f (kcompose g h) x} @-}
-- optionCompose :: (a -> Optional b) -> (b -> Optional c) -> (c -> Optional d) -> a -> ()
-- optionCompose  = kcomposeAssoc 


-- -- TODO: Prove this
-- {-@ applicativeLemma1 :: VApplicative m => f:(a -> b) -> x:m a -> {fmap f x == ap (pure f) x} @-}
-- applicativeLemma1 :: VApplicative m => (a -> b) -> m a -> ()
-- applicativeLemma1 f x = ()

-- -- TODO: Prove this
-- {-@ applicativeLemma2 :: VApplicative m => f:(d -> c -> e) -> g:(a -> b -> c) -> p:_ -> {q:_ | p (q x y) = compose (f x) (g y)} -> {liftA2 p (liftA2 q u v) = compose (liftA2 f u) (liftA2 g v)} @-}
-- applicativeLemma2 :: VApplicative m => (d -> c -> e) -> (a -> b -> c) -> _ -> _ -> ()
-- applicativeLemma2 f g p q = undefined