{-# 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 = (m a %1 -> m b) %1 -> ReaderT r m a %1 -> ReaderT r m b
forall (m :: * -> *) a (n :: * -> *) b r.
(m a %1 -> n b) %1 -> ReaderT r m a %1 -> ReaderT r n b
mapReaderT ((a %1 -> b) -> m a %1 -> m b
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 = (m a %1 -> m b) %1 -> ReaderT r m a %1 -> ReaderT r m b
forall (m :: * -> *) a (n :: * -> *) b r.
(m a %1 -> n b) %1 -> ReaderT r m a %1 -> ReaderT r n b
mapReaderT ((a %1 -> b) %1 -> m a %1 -> m b
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 = (r %1 -> m a) -> ReaderT r m a
forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT ((r %1 -> m a) -> ReaderT r m a) -> (r %1 -> m a) -> ReaderT r m a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \r
r -> r %1 -> m a %1 -> m a
forall a b. Consumable a => a %1 -> b %1 -> b
lseq r
r (a -> m a
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 = (r %1 -> m b) %1 -> ReaderT r m b
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 m (a %1 -> b) %1 -> m a %1 -> m b
forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
Data.<*> r %1 -> m a
x r
r2) ((r, r) %1 -> m b) %1 -> (r %1 -> (r, r)) -> r %1 -> m b
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. r %1 -> (r, r)
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 = (r %1 -> m a) %1 -> ReaderT r m a
forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT ((r %1 -> m a) %1 -> ReaderT r m a)
-> (r %1 -> m a) %1 -> ReaderT r m a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \r
r -> r %1 -> m a %1 -> m a
forall a b. Consumable a => a %1 -> b %1 -> b
lseq r
r (a %1 -> m a
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 = (r %1 -> m b) %1 -> ReaderT r m b
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 m (a %1 -> b) %1 -> m a %1 -> m b
forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
Data.<*> r %1 -> m a
x r
r2) ((r, r) %1 -> m b) %1 -> (r %1 -> (r, r)) -> r %1 -> m b
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. r %1 -> (r, r)
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 = (r %1 -> m b) %1 -> ReaderT r m b
forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT ((\(r
r1, r
r2) -> r %1 -> m a
x r
r1 m a %1 -> (a %1 -> m b) %1 -> m b
forall (m :: * -> *) a b.
Monad m =>
m a %1 -> (a %1 -> m b) %1 -> m b
>>= (\a
a -> ReaderT r m b %1 -> r %1 -> m b
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)) ((r, r) %1 -> m b) %1 -> (r %1 -> (r, r)) -> r %1 -> m b
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. r %1 -> (r, r)
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 = (r %1 -> m r) -> ReaderT r m r
forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT r %1 -> m r
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 = (r' %1 -> m a) %1 -> ReaderT r' m a
forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT ((r' %1 -> m a) %1 -> ReaderT r' m a)
-> (r' %1 -> m a) %1 -> ReaderT r' m a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ ReaderT r m a %1 -> r %1 -> m a
forall r (m :: * -> *) a. ReaderT r m a %1 -> r %1 -> m a
runReaderT ReaderT r m a
m (r %1 -> m a) %1 -> (r' %1 -> r) %1 -> r' %1 -> m a
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 = (r %1 -> r) %1 -> ReaderT r m a %1 -> ReaderT r m a
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 = (r %1 -> m a) %1 -> ReaderT r m a
forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT (a %1 -> m a
forall (m :: * -> *) a. Monad m => a %1 -> m a
return (a %1 -> m a) -> (r %1 -> a) %1 -> r %1 -> m a
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 = Identity a %1 -> a
forall a (p :: Multiplicity). Identity a %p -> a
runIdentity' (Identity a %1 -> a) -> (r %1 -> Identity a) %1 -> r %1 -> a
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. Reader r a %1 -> r %1 -> Identity a
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 = (Identity a %1 -> Identity b)
%1 -> ReaderT r Identity a %1 -> ReaderT r Identity b
forall (m :: * -> *) a (n :: * -> *) b r.
(m a %1 -> n b) %1 -> ReaderT r m a %1 -> ReaderT r n b
mapReaderT (b %1 -> Identity b
forall a. a -> Identity a
Identity (b %1 -> Identity b)
-> (Identity a %1 -> b) %1 -> Identity a %1 -> Identity b
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 (a %1 -> b) %1 -> (Identity a %1 -> a) -> Identity a %1 -> b
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. Identity a %1 -> a
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 = (r %1 -> n b) %1 -> ReaderT r n b
forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT (m a %1 -> n b
f (m a %1 -> n b) %1 -> (r %1 -> m a) %1 -> r %1 -> n b
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. ReaderT r m a %1 -> r %1 -> m a
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 = (r' %1 -> r) %1 -> ReaderT r Identity a %1 -> ReaderT r' Identity a
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 = (r %1 -> m a) %1 -> ReaderT r m a
forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT (a %1 -> m a
forall (m :: * -> *) a. Monad m => a %1 -> m a
return (a %1 -> m a) -> (r %1 -> a) %1 -> r %1 -> m a
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 = (r %1 -> m a) %1 -> ReaderT r m a
forall r (m :: * -> *) a. (r %1 -> m a) -> ReaderT r m a
ReaderT (r %1 -> m a %1 -> m a
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) = (r -> m b) %1 -> ReaderT r m b
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
NonLinear.ReaderT ((r -> m b) %1 -> ReaderT r m b) -> (r -> m b) %1 -> ReaderT r m b
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \r
r -> (a %1 -> b) %1 -> m a %1 -> m b
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 = (r -> m a) %1 -> ReaderT r m a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
NonLinear.ReaderT ((r -> m a) %1 -> ReaderT r m a) -> (r -> m a) %1 -> ReaderT r m a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \r
_ -> a %1 -> m a
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 = (r -> m b) %1 -> ReaderT r m b
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
NonLinear.ReaderT ((r -> m b) %1 -> ReaderT r m b) -> (r -> m b) %1 -> ReaderT r m b
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \r
r -> r -> m (a %1 -> b)
f r
r m (a %1 -> b) %1 -> m a %1 -> m b
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 = (r -> m b) %1 -> ReaderT r m b
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
NonLinear.ReaderT ((r -> m b) %1 -> ReaderT r m b) -> (r -> m b) %1 -> ReaderT r m b
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \r
r -> r -> m a
x r
r m a %1 -> (a %1 -> m b) %1 -> m b
forall (m :: * -> *) a b.
Monad m =>
m a %1 -> (a %1 -> m b) %1 -> m b
>>= (\a
a -> ReaderT r m b %1 -> r -> m b
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 = (r -> m a) %1 -> ReaderT r m a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
NonLinear.ReaderT (\r
_ -> m a
x)