{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}

{-# OPTIONS_HADDOCK hide #-}

module Capability.Reader.Internal.Class
  ( HasReader(..)
  , ask
  , asks
  , local
  , reader
  , magnify
  , Reified(..)
  ) where

import Capability.Constraints
import Capability.Derive (derive)
import Capability.Reflection
import Capability.Source.Internal.Class
import Data.Coerce (Coercible, coerce)
import Data.Kind (Type)
import GHC.Exts (Proxy#, proxy#)

-- | Reader capability
--
-- An instance should fulfill the following laws.
-- At this point these laws are not definitive,
-- see <https://github.com/haskell/mtl/issues/5>.
--
-- prop> k <*> ask @t = ask @t <**> k
-- prop> ask @t *> m = m = m <* ask @t
-- prop> local @t f (ask @t) = fmap f (ask @t)
-- prop> local @t f . local @t g = local @t (g . f)
-- prop> local @t f (pure x) = pure x
-- prop> local @t f (m >>= \x -> k x) = local @t f m >>= \x -> local @t f (k x)
-- prop> reader @t f = f <$> ask @t
class (Monad m, HasSource tag r m)
  => HasReader (tag :: k) (r :: Type) (m :: Type -> Type) | tag m -> r
  where
    -- | For technical reasons, this method needs an extra proxy argument.
    -- You only need it if you are defining new instances of 'HasReader'.
    -- Otherwise, you will want to use 'local'.
    -- See 'local' for more documentation.
    local_ :: Proxy# tag -> (r -> r) -> m a -> m a
    -- | For technical reasons, this method needs an extra proxy argument.
    -- You only need it if you are defining new instances of 'HasReader'.
    -- Otherwise, you will want to use 'reader'.
    -- See 'reader' for more documentation.
    reader_ :: Proxy# tag -> (r -> a) -> m a

-- | @ask \@tag@
-- retrieves the environment of the reader capability @tag@.
ask :: forall tag r m. HasReader tag r m => m r
ask :: m r
ask = forall k (tag :: k) a (m :: * -> *). HasSource tag a m => m a
forall a (m :: * -> *). HasSource tag a m => m a
await @tag
{-# INLINE ask #-}

-- | @asks \@tag@
-- retrieves the image by @f@ of the environment
-- of the reader capability @tag@.
--
-- prop> asks @tag f = f <$> ask @tag
asks :: forall tag r m a. HasReader tag r m => (r -> a) -> m a
asks :: (r -> a) -> m a
asks = forall k (tag :: k) r (m :: * -> *) a.
HasSource tag r m =>
(r -> a) -> m a
forall r (m :: * -> *) a. HasSource tag r m => (r -> a) -> m a
awaits @tag
{-# INLINE asks #-}

-- | @local \@tag f m@
-- runs the monadic action @m@ in a modified environment @e' = f e@,
-- where @e@ is the environment of the reader capability @tag@.
-- Symbolically: @return e = ask \@tag@.
local :: forall tag r m a. HasReader tag r m => (r -> r) -> m a -> m a
local :: (r -> r) -> m a -> m a
local = Proxy# tag -> (r -> r) -> m a -> m a
forall k (tag :: k) r (m :: * -> *) a.
HasReader tag r m =>
Proxy# tag -> (r -> r) -> m a -> m a
local_ (Proxy# tag
forall k (a :: k). Proxy# a
proxy# @tag)
{-# INLINE local #-}

-- | @reader \@tag act@
-- lifts a purely environment-dependent action @act@ to a monadic action
-- in an arbitrary monad @m@ with capability @HasReader@.
--
-- It happens to coincide with @asks@: @reader = asks@.
reader :: forall tag r m a. HasReader tag r m => (r -> a) -> m a
reader :: (r -> a) -> m a
reader = Proxy# tag -> (r -> a) -> m a
forall k (tag :: k) r (m :: * -> *) a.
HasReader tag r m =>
Proxy# tag -> (r -> a) -> m a
reader_ (Proxy# tag
forall k (a :: k). Proxy# a
proxy# @tag)
{-# INLINE reader #-}

-- | Execute the given reader action on a sub-component of the current context
-- as defined by the given transformer @t@, retaining arbitrary capabilities
-- listed in @cs@.
--
-- See the similar 'Capability.State.zoom' function for more details and
-- examples.
--
-- This function is experimental and subject to change.
-- See <https://github.com/tweag/capability/issues/46>.
magnify :: forall innertag t (cs :: [Capability]) inner m a.
  ( forall x. Coercible (t m x) (m x)
  , HasReader innertag inner (t m)
  , All cs m)
  => (forall m'. All (HasReader innertag inner ': cs) m' => m' a) -> m a
magnify :: (forall (m' :: * -> *).
 All (HasReader innertag inner : cs) m' =>
 m' a)
-> m a
magnify =
  forall (m :: * -> *) a.
(forall x. Coercible (t m x) (m x),
 All '[HasReader innertag inner] (t m), All cs m) =>
(forall (m' :: * -> *).
 (All '[HasReader innertag inner] m', All cs m') =>
 m' a)
-> m a
forall (t :: (* -> *) -> * -> *)
       (derived :: [(* -> *) -> Constraint])
       (ambient :: [(* -> *) -> Constraint]) (m :: * -> *) a.
(forall x. Coercible (t m x) (m x), All derived (t m),
 All ambient m) =>
(forall (m' :: * -> *). (All derived m', All ambient m') => m' a)
-> m a
derive @t @'[HasReader innertag inner] @cs
{-# INLINE magnify #-}

--------------------------------------------------------------------------------

data instance Reified tag (HasReader tag r) m = ReifiedReader
  { Reified tag (HasReader tag r) m -> Reified tag (HasSource tag r) m
_readerSource :: Reified tag (HasSource tag r) m,
    Reified tag (HasReader tag r) m -> forall a. (r -> r) -> m a -> m a
_local :: forall a. (r -> r) -> m a -> m a,
    Reified tag (HasReader tag r) m -> forall a. (r -> a) -> m a
_reader :: forall a. (r -> a) -> m a
  }

instance
  ( Monad m,
    Reifies s (Reified tag (HasReader tag r) m)
  ) =>
  HasSource tag r (Reflected s (HasReader tag r) m)
  where
  await_ :: Proxy# tag -> Reflected s (HasReader tag r) m r
await_ Proxy# tag
_ = m r -> Reflected s (HasReader tag r) m r
coerce (m r -> Reflected s (HasReader tag r) m r)
-> m r -> Reflected s (HasReader tag r) m r
forall a b. (a -> b) -> a -> b
$ Reified tag (HasSource tag r) m -> m r
forall k (tag :: k) a (m :: * -> *).
Reified tag (HasSource tag a) m -> m a
_await (Reified tag (HasSource tag r) m -> m r)
-> Reified tag (HasSource tag r) m -> m r
forall a b. (a -> b) -> a -> b
$ Reified tag (HasReader tag r) m -> Reified tag (HasSource tag r) m
forall k (tag :: k) r (m :: * -> *).
Reified tag (HasReader tag r) m -> Reified tag (HasSource tag r) m
_readerSource (Reified tag (HasReader tag r) m
 -> Reified tag (HasSource tag r) m)
-> Reified tag (HasReader tag r) m
-> Reified tag (HasSource tag r) m
forall a b. (a -> b) -> a -> b
$ forall (tag :: k) (c :: (* -> *) -> Constraint) (m :: * -> *).
Reifies s (Reified tag c m) =>
Reified tag c m
forall k1 k2 (s :: k1) (tag :: k2) (c :: (* -> *) -> Constraint)
       (m :: * -> *).
Reifies s (Reified tag c m) =>
Reified tag c m
reified @s
  {-# INLINE await_ #-}

instance
  ( Monad m,
    Reifies s (Reified tag (HasReader tag r) m)
  ) =>
  HasReader tag r (Reflected s (HasReader tag r) m)
  where
  local_ :: forall a. Proxy# tag -> (r -> r) -> Reflected s (HasReader tag r) m a -> Reflected s (HasReader tag r) m a
  local_ :: Proxy# tag
-> (r -> r)
-> Reflected s (HasReader tag r) m a
-> Reflected s (HasReader tag r) m a
local_ Proxy# tag
_ = forall b.
Coercible ((r -> r) -> m a -> m a) b =>
((r -> r) -> m a -> m a) -> b
coerce @((r -> r) -> m a -> m a) (((r -> r) -> m a -> m a)
 -> (r -> r)
 -> Reflected s (HasReader tag r) m a
 -> Reflected s (HasReader tag r) m a)
-> ((r -> r) -> m a -> m a)
-> (r -> r)
-> Reflected s (HasReader tag r) m a
-> Reflected s (HasReader tag r) m a
forall a b. (a -> b) -> a -> b
$ Reified tag (HasReader tag r) m -> forall a. (r -> r) -> m a -> m a
forall k (tag :: k) r (m :: * -> *).
Reified tag (HasReader tag r) m -> forall a. (r -> r) -> m a -> m a
_local (forall (tag :: k) (c :: (* -> *) -> Constraint) (m :: * -> *).
Reifies s (Reified tag c m) =>
Reified tag c m
forall k1 k2 (s :: k1) (tag :: k2) (c :: (* -> *) -> Constraint)
       (m :: * -> *).
Reifies s (Reified tag c m) =>
Reified tag c m
reified @s)
  {-# INLINE local_ #-}
  reader_ :: forall a. Proxy# tag -> (r -> a) -> Reflected s (HasReader tag r) m a
  reader_ :: Proxy# tag -> (r -> a) -> Reflected s (HasReader tag r) m a
reader_ Proxy# tag
_ = forall b. Coercible ((r -> a) -> m a) b => ((r -> a) -> m a) -> b
coerce @((r -> a) -> m a) (((r -> a) -> m a)
 -> (r -> a) -> Reflected s (HasReader tag r) m a)
-> ((r -> a) -> m a)
-> (r -> a)
-> Reflected s (HasReader tag r) m a
forall a b. (a -> b) -> a -> b
$ Reified tag (HasReader tag r) m -> forall a. (r -> a) -> m a
forall k (tag :: k) r (m :: * -> *).
Reified tag (HasReader tag r) m -> forall a. (r -> a) -> m a
_reader (forall (tag :: k) (c :: (* -> *) -> Constraint) (m :: * -> *).
Reifies s (Reified tag c m) =>
Reified tag c m
forall k1 k2 (s :: k1) (tag :: k2) (c :: (* -> *) -> Constraint)
       (m :: * -> *).
Reifies s (Reified tag c m) =>
Reified tag c m
reified @s)
  {-# INLINE reader_ #-}