{-# OPTIONS -Wno-orphans #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_HADDOCK hide #-}

module Control.Functor.Linear.Internal.Reader
  ( --  ReaderT monad transformer
    Reader,
    reader,
    runReader,
    mapReader,
    withReader,
    ReaderT (..),
    runReaderT,
    mapReaderT,
    withReaderT,
    ask,
    local,
    asks,
  )
where

import Control.Functor.Linear.Internal.Class
import Control.Functor.Linear.Internal.Instances ()
import Control.Functor.Linear.Internal.MonadTrans
import qualified Control.Monad as NonLinear ()
import qualified Control.Monad.Trans.Reader as NonLinear
import Data.Functor.Identity
import qualified Data.Functor.Linear.Internal.Applicative as Data
import qualified Data.Functor.Linear.Internal.Functor as Data
import Data.Unrestricted.Linear.Internal.Consumable
import Data.Unrestricted.Linear.Internal.Dupable
import Prelude.Linear.Internal (runIdentity', ($), (.))

-- # Linear ReaderT
-------------------------------------------------------------------------------

-- | A linear reader monad transformer.
-- This reader monad requires that use of the read-only state is explict.
--
-- The monad instance requires that @r@ be 'Dupable'.  This means that you
-- should use the linear reader monad just like the non-linear monad, except
-- that the type system ensures that you explicity use or discard the
-- read-only state (with the 'Consumable' instance).
newtype ReaderT r m a = ReaderT (r %1 -> m a)

-- XXX: Replace with a newtype deconstructor once it can be inferred as linear.

-- | Provide an intial read-only state and run the monadic computation in
-- a reader monad transformer
runReaderT :: ReaderT r m a %1 -> r %1 -> m a
runReaderT :: forall r (m :: * -> *) a. ReaderT r m a %1 -> r %1 -> m a
runReaderT (ReaderT r %1 -> m a
f) = r %1 -> m a
f

instance (Data.Functor m) => Data.Functor (ReaderT r m) where
  fmap :: forall a b. (a %1 -> b) -> ReaderT r m a %1 -> ReaderT r m b
fmap a %1 -> b
f = forall (m :: * -> *) a (n :: * -> *) b r.
(m a %1 -> n b) %1 -> ReaderT r m a %1 -> ReaderT r n b
mapReaderT (forall (f :: * -> *) a b. Functor f => (a %1 -> b) -> f a %1 -> f b
Data.fmap a %1 -> b
f)

instance (Functor m) => Functor (ReaderT r m) where
  fmap :: forall a b. (a %1 -> b) %1 -> ReaderT r m a %1 -> ReaderT r m b
fmap a %1 -> b
f = forall (m :: * -> *) a (n :: * -> *) b r.
(m a %1 -> n b) %1 -> ReaderT r m a %1 -> ReaderT r n b
mapReaderT (forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
fmap a %1 -> b
f)

instance (Data.Applicative m, Dupable r) => Data.Applicative (ReaderT r m) where
  pure :: forall a. a -> ReaderT r m a
pure a
x = forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \r
r -> forall a b. Consumable a => a %1 -> b %1 -> b
lseq r
r (forall (f :: * -> *) a. Applicative f => a -> f a
Data.pure a
x)
  ReaderT r %1 -> m (a %1 -> b)
f <*> :: forall a b.
ReaderT r m (a %1 -> b) %1 -> ReaderT r m a %1 -> ReaderT r m b
<*> ReaderT r %1 -> m a
x = forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT ((\(r
r1, r
r2) -> r %1 -> m (a %1 -> b)
f r
r1 forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
Data.<*> r %1 -> m a
x r
r2) forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall a. Dupable a => a %1 -> (a, a)
dup)

instance (Applicative m, Dupable r) => Applicative (ReaderT r m) where
  pure :: forall a. a %1 -> ReaderT r m a
pure a
x = forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \r
r -> forall a b. Consumable a => a %1 -> b %1 -> b
lseq r
r (forall (f :: * -> *) a. Applicative f => a %1 -> f a
pure a
x)
  ReaderT r %1 -> m (a %1 -> b)
f <*> :: forall a b.
ReaderT r m (a %1 -> b) %1 -> ReaderT r m a %1 -> ReaderT r m b
<*> ReaderT r %1 -> m a
x = forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT ((\(r
r1, r
r2) -> r %1 -> m (a %1 -> b)
f r
r1 forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
Data.<*> r %1 -> m a
x r
r2) forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall a. Dupable a => a %1 -> (a, a)
dup)

instance (Monad m, Dupable r) => Monad (ReaderT r m) where
  ReaderT r %1 -> m a
x >>= :: forall a b.
ReaderT r m a %1 -> (a %1 -> ReaderT r m b) %1 -> ReaderT r m b
>>= a %1 -> ReaderT r m b
f = forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT ((\(r
r1, r
r2) -> r %1 -> m a
x r
r1 forall (m :: * -> *) a b.
Monad m =>
m a %1 -> (a %1 -> m b) %1 -> m b
>>= (\a
a -> forall r (m :: * -> *) a. ReaderT r m a %1 -> r %1 -> m a
runReaderT (a %1 -> ReaderT r m b
f a
a) r
r2)) forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall a. Dupable a => a %1 -> (a, a)
dup)

type Reader r = ReaderT r Identity

ask :: (Applicative m) => ReaderT r m r
ask :: forall (m :: * -> *) r. Applicative m => ReaderT r m r
ask = forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT forall (f :: * -> *) a. Applicative f => a %1 -> f a
pure

withReaderT :: (r' %1 -> r) %1 -> ReaderT r m a %1 -> ReaderT r' m a
withReaderT :: forall r' r (m :: * -> *) a.
(r' %1 -> r) %1 -> ReaderT r m a %1 -> ReaderT r' m a
withReaderT r' %1 -> r
f ReaderT r m a
m = forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ forall r (m :: * -> *) a. ReaderT r m a %1 -> r %1 -> m a
runReaderT ReaderT r m a
m forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. r' %1 -> r
f

local :: (r %1 -> r) %1 -> ReaderT r m a %1 -> ReaderT r m a
local :: forall r (m :: * -> *) a.
(r %1 -> r) %1 -> ReaderT r m a %1 -> ReaderT r m a
local = forall r' r (m :: * -> *) a.
(r' %1 -> r) %1 -> ReaderT r m a %1 -> ReaderT r' m a
withReaderT

reader :: (Monad m) => (r %1 -> a) %1 -> ReaderT r m a
reader :: forall (m :: * -> *) r a.
Monad m =>
(r %1 -> a) %1 -> ReaderT r m a
reader r %1 -> a
f = forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT (forall (m :: * -> *) a. Monad m => a %1 -> m a
return forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. r %1 -> a
f)

runReader :: Reader r a %1 -> r %1 -> a
runReader :: forall r a. Reader r a %1 -> r %1 -> a
runReader Reader r a
m = forall a (p :: Multiplicity). Identity a %p -> a
runIdentity' forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall r (m :: * -> *) a. ReaderT r m a %1 -> r %1 -> m a
runReaderT Reader r a
m

mapReader :: (a %1 -> b) %1 -> Reader r a %1 -> Reader r b
mapReader :: forall a b r. (a %1 -> b) %1 -> Reader r a %1 -> Reader r b
mapReader a %1 -> b
f = forall (m :: * -> *) a (n :: * -> *) b r.
(m a %1 -> n b) %1 -> ReaderT r m a %1 -> ReaderT r n b
mapReaderT (forall a. a -> Identity a
Identity forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. a %1 -> b
f forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall a (p :: Multiplicity). Identity a %p -> a
runIdentity')

mapReaderT :: (m a %1 -> n b) %1 -> ReaderT r m a %1 -> ReaderT r n b
mapReaderT :: forall (m :: * -> *) a (n :: * -> *) b r.
(m a %1 -> n b) %1 -> ReaderT r m a %1 -> ReaderT r n b
mapReaderT m a %1 -> n b
f ReaderT r m a
m = forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT (m a %1 -> n b
f forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall r (m :: * -> *) a. ReaderT r m a %1 -> r %1 -> m a
runReaderT ReaderT r m a
m)

withReader :: (r' %1 -> r) %1 -> Reader r a %1 -> Reader r' a
withReader :: forall r' r a. (r' %1 -> r) %1 -> Reader r a %1 -> Reader r' a
withReader = forall r' r (m :: * -> *) a.
(r' %1 -> r) %1 -> ReaderT r m a %1 -> ReaderT r' m a
withReaderT

asks :: (Monad m) => (r %1 -> a) %1 -> ReaderT r m a
asks :: forall (m :: * -> *) r a.
Monad m =>
(r %1 -> a) %1 -> ReaderT r m a
asks r %1 -> a
f = forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT (forall (m :: * -> *) a. Monad m => a %1 -> m a
return forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. r %1 -> a
f)

instance (Dupable r) => MonadTrans (ReaderT r) where
  lift :: forall (m :: * -> *) a. Monad m => m a %1 -> ReaderT r m a
lift m a
x = forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT (forall a b. Consumable a => a %1 -> b %1 -> b
`lseq` m a
x)

-- # Instances for nonlinear ReaderT
-------------------------------------------------------------------------------

instance (Functor m) => Functor (NonLinear.ReaderT r m) where
  fmap :: forall a b. (a %1 -> b) %1 -> ReaderT r m a %1 -> ReaderT r m b
fmap a %1 -> b
f (NonLinear.ReaderT r -> m a
g) = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
NonLinear.ReaderT forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \r
r -> forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
fmap a %1 -> b
f (r -> m a
g r
r)

instance (Applicative m) => Applicative (NonLinear.ReaderT r m) where
  pure :: forall a. a %1 -> ReaderT r m a
pure a
x = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
NonLinear.ReaderT forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \r
_ -> forall (f :: * -> *) a. Applicative f => a %1 -> f a
pure a
x
  NonLinear.ReaderT r -> m (a %1 -> b)
f <*> :: forall a b.
ReaderT r m (a %1 -> b) %1 -> ReaderT r m a %1 -> ReaderT r m b
<*> NonLinear.ReaderT r -> m a
x = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
NonLinear.ReaderT forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \r
r -> r -> m (a %1 -> b)
f r
r forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
<*> r -> m a
x r
r

instance (Monad m) => Monad (NonLinear.ReaderT r m) where
  NonLinear.ReaderT r -> m a
x >>= :: forall a b.
ReaderT r m a %1 -> (a %1 -> ReaderT r m b) %1 -> ReaderT r m b
>>= a %1 -> ReaderT r m b
f = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
NonLinear.ReaderT forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \r
r -> r -> m a
x r
r forall (m :: * -> *) a b.
Monad m =>
m a %1 -> (a %1 -> m b) %1 -> m b
>>= (\a
a -> forall r (m :: * -> *) a. ReaderT r m a %1 -> r -> m a
runReaderT' (a %1 -> ReaderT r m b
f a
a) r
r)

-- XXX: Temporary, until newtype record projections are linear.
runReaderT' :: NonLinear.ReaderT r m a %1 -> r -> m a
runReaderT' :: forall r (m :: * -> *) a. ReaderT r m a %1 -> r -> m a
runReaderT' (NonLinear.ReaderT r -> m a
f) = r -> m a
f

instance MonadTrans (NonLinear.ReaderT r) where
  lift :: forall (m :: * -> *) a. Monad m => m a %1 -> ReaderT r m a
lift m a
x = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
NonLinear.ReaderT (\r
_ -> m a
x)