{-# 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 a b. (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 a b. (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 a. 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) -> 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 a b. 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) -> 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 a. 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) -> 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 a b. 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) -> 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 a b. 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 a. a %1 -> m a
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) -> 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) -> 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 -> 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) -> 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) -> 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) -> 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) -> 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 a b. (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) -> 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 a. 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) -> 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 a b. 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) -> 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 a b. 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) -> ReaderT r m a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
NonLinear.ReaderT (\r
_ -> m a
x)