module Control.Monad.Ology.General.Trans.Tunnel where

import Control.Monad.Ology.General.Function
import Control.Monad.Ology.General.IO
import Control.Monad.Ology.General.Inner
import Control.Monad.Ology.General.Trans.Constraint
import Control.Monad.Ology.General.Trans.Hoist
import Control.Monad.Ology.Specific.ComposeInner
import Import

-- | Monad transformers that allow \"tunneling\" (working with the monad under the transformer).
type MonadTransTunnel :: TransKind -> Constraint
class (MonadTransHoist t, MonadInner (Tunnel t)) => MonadTransTunnel t where
    -- | The tunnel monad of this transformer.
    type Tunnel t :: Type -> Type
    tunnel ::
           forall m r. Monad m
        => ((forall m1 a. Monad m1 => t m1 a -> m1 (Tunnel t a)) -> m (Tunnel t r))
        -> t m r

tunnelHoist ::
       forall t m1 m2. (MonadTransTunnel t, Monad m1, Monad m2)
    => (m1 --> m2)
    -> t m1 --> t m2
tunnelHoist :: forall (t :: TransKind) (m1 :: Type -> Type) (m2 :: Type -> Type).
(MonadTransTunnel t, Monad m1, Monad m2) =>
(m1 --> m2) -> t m1 --> t m2
tunnelHoist m1 --> m2
mma t m1 a
sm1 = forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransTunnel t, Monad m) =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m (Tunnel t r))
-> t m r
tunnel forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
tun -> m1 --> m2
mma forall a b. (a -> b) -> a -> b
$ forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
tun t m1 a
sm1

backHoist :: (MonadTransTunnel t, Monad ma, Monad mb) => (ma -/-> mb) -> t ma -/-> t mb
backHoist :: forall (t :: TransKind) (ma :: Type -> Type) (mb :: Type -> Type).
(MonadTransTunnel t, Monad ma, Monad mb) =>
(ma -/-> mb) -> t ma -/-> t mb
backHoist ma -/-> mb
wt (t mb --> t ma) -> t ma r
tm = forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransTunnel t, Monad m) =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m (Tunnel t r))
-> t m r
tunnel forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift -> ma -/-> mb
wt forall a b. (a -> b) -> a -> b
$ \mb --> ma
tba -> forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift forall a b. (a -> b) -> a -> b
$ (t mb --> t ma) -> t ma r
tm forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (m1 :: Type -> Type) (m2 :: Type -> Type).
(MonadTransHoist t, Monad m1, Monad m2) =>
(m1 --> m2) -> t m1 --> t m2
hoist mb --> ma
tba

wBackHoist :: (MonadTransTunnel t, Monad ma, Monad mb) => WBackraised ma mb -> WBackraised (t ma) (t mb)
wBackHoist :: forall (t :: TransKind) (ma :: Type -> Type) (mb :: Type -> Type).
(MonadTransTunnel t, Monad ma, Monad mb) =>
WBackraised ma mb -> WBackraised (t ma) (t mb)
wBackHoist (MkWBackraised ma -/-> mb
f) = forall k (p :: k -> Type) (q :: k -> Type).
(p -/-> q) -> WBackraised p q
MkWBackraised forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (ma :: Type -> Type) (mb :: Type -> Type).
(MonadTransTunnel t, Monad ma, Monad mb) =>
(ma -/-> mb) -> t ma -/-> t mb
backHoist ma -/-> mb
f

-- | Commute two transformers in a transformer stack, by commuting their tunnel monads.
commuteTWith ::
       forall ta tb m. (MonadTransTunnel ta, MonadTransTunnel tb, Monad m)
    => (forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r))
    -> ta (tb m) --> tb (ta m)
commuteTWith :: forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
(forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r))
-> ta (tb m) --> tb (ta m)
commuteTWith forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r)
commutef ta (tb m) a
tabm =
    case forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type).
(TransConstraint c t, c m) =>
Dict (c (t m))
hasTransConstraint @Monad @ta @m of
        Dict (Monad (ta m))
Dict ->
            case forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type).
(TransConstraint c t, c m) =>
Dict (c (t m))
hasTransConstraint @Monad @tb @m of
                Dict (Monad (tb m))
Dict -> forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransTunnel t, Monad m) =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m (Tunnel t r))
-> t m r
tunnel forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
tb m1 a -> m1 (Tunnel tb a)
unliftb -> forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransTunnel t, Monad m) =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m (Tunnel t r))
-> t m r
tunnel forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
ta m1 a -> m1 (Tunnel ta a)
unlifta -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r)
commutef forall a b. (a -> b) -> a -> b
$ forall (m1 :: Type -> Type) a.
Monad m1 =>
tb m1 a -> m1 (Tunnel tb a)
unliftb forall a b. (a -> b) -> a -> b
$ forall (m1 :: Type -> Type) a.
Monad m1 =>
ta m1 a -> m1 (Tunnel ta a)
unlifta ta (tb m) a
tabm

-- | Commute two transformers in a transformer stack.
commuteT ::
       forall ta tb m. (MonadTransTunnel ta, MonadTransTunnel tb, Monad (Tunnel ta), MonadInner (Tunnel tb), Monad m)
    => ta (tb m) --> tb (ta m)
commuteT :: forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad (Tunnel ta),
 MonadInner (Tunnel tb), Monad m) =>
ta (tb m) --> tb (ta m)
commuteT = forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
(forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r))
-> ta (tb m) --> tb (ta m)
commuteTWith forall (m :: Type -> Type) (f :: Type -> Type) a.
(MonadInner m, Applicative f) =>
m (f a) -> f (m a)
commuteInner

commuteTBack ::
       forall ta tb m.
       (MonadTransTunnel ta, MonadTransTunnel tb, MonadInner (Tunnel ta), MonadInner (Tunnel tb), Monad m)
    => ta (tb m) -/-> tb (ta m)
commuteTBack :: forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, MonadInner (Tunnel ta),
 MonadInner (Tunnel tb), Monad m) =>
ta (tb m) -/-> tb (ta m)
commuteTBack (tb (ta m) --> ta (tb m)) -> ta (tb m) r
call = forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad (Tunnel ta),
 MonadInner (Tunnel tb), Monad m) =>
ta (tb m) --> tb (ta m)
commuteT forall a b. (a -> b) -> a -> b
$ (tb (ta m) --> ta (tb m)) -> ta (tb m) r
call forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad (Tunnel ta),
 MonadInner (Tunnel tb), Monad m) =>
ta (tb m) --> tb (ta m)
commuteT

instance MonadInner inner => MonadTransTunnel (ComposeInner inner) where
    type Tunnel (ComposeInner inner) = inner
    tunnel :: forall (m :: Type -> Type) r.
Monad m =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  ComposeInner inner m1 a -> m1 (Tunnel (ComposeInner inner) a))
 -> m (Tunnel (ComposeInner inner) r))
-> ComposeInner inner m r
tunnel (forall (m1 :: Type -> Type) a.
 Monad m1 =>
 ComposeInner inner m1 a -> m1 (Tunnel (ComposeInner inner) a))
-> m (Tunnel (ComposeInner inner) r)
call = forall (inner :: Type -> Type) (outer :: Type -> Type) a.
outer (inner a) -> ComposeInner inner outer a
MkComposeInner forall a b. (a -> b) -> a -> b
$ (forall (m1 :: Type -> Type) a.
 Monad m1 =>
 ComposeInner inner m1 a -> m1 (Tunnel (ComposeInner inner) a))
-> m (Tunnel (ComposeInner inner) r)
call forall (inner :: Type -> Type) (outer :: Type -> Type) a.
ComposeInner inner outer a -> outer (inner a)
unComposeInner

class (MonadHoistIO m, MonadInner (TunnelIO m)) => MonadTunnelIO m where
    type TunnelIO m :: Type -> Type
    tunnelIO :: forall r. ((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m r)) -> m r

instance MonadTunnelIO IO where
    type TunnelIO IO = Identity
    tunnelIO :: forall r.
((forall a. IO a -> IO (TunnelIO IO a)) -> IO (TunnelIO IO r))
-> IO r
tunnelIO (forall a. IO a -> IO (TunnelIO IO a)) -> IO (TunnelIO IO r)
call = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ (forall a. IO a -> IO (TunnelIO IO a)) -> IO (TunnelIO IO r)
call forall a b. (a -> b) -> a -> b
$ \IO a
ma -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Identity a
Identity forall a b. (a -> b) -> a -> b
$ IO a
ma

instance (MonadTransTunnel t, MonadInner (Tunnel t), MonadTunnelIO m, MonadIO (t m)) => MonadTunnelIO (t m) where
    type TunnelIO (t m) = ComposeInner (Tunnel t) (TunnelIO m)
    tunnelIO :: forall r.
((forall a. t m a -> IO (TunnelIO (t m) a))
 -> IO (TunnelIO (t m) r))
-> t m r
tunnelIO (forall a. t m a -> IO (TunnelIO (t m) a)) -> IO (TunnelIO (t m) r)
call =
        forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransTunnel t, Monad m) =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m (Tunnel t r))
-> t m r
tunnel forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift -> forall (m :: Type -> Type) r.
MonadTunnelIO m =>
((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m r)) -> m r
tunnelIO forall a b. (a -> b) -> a -> b
$ \forall a. m a -> IO (TunnelIO m a)
unliftIO -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (inner :: Type -> Type) (outer :: Type -> Type) a.
ComposeInner inner outer a -> outer (inner a)
unComposeInner forall a b. (a -> b) -> a -> b
$ (forall a. t m a -> IO (TunnelIO (t m) a)) -> IO (TunnelIO (t m) r)
call forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (inner :: Type -> Type) (outer :: Type -> Type) a.
outer (inner a) -> ComposeInner inner outer a
MkComposeInner forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. m a -> IO (TunnelIO m a)
unliftIO forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift

instance (MonadTransTunnel t, MonadInner (Tunnel t), TransConstraint MonadIO t) => TransConstraint MonadTunnelIO t where
    hasTransConstraint :: forall (m :: Type -> Type).
MonadTunnelIO m =>
Dict (MonadTunnelIO (t m))
hasTransConstraint = forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type) (c' :: (Type -> Type) -> Constraint).
(TransConstraint c t, c m) =>
(c (t m) => Dict (c' (t m))) -> Dict (c' (t m))
withTransConstraintDict @MonadIO forall (a :: Constraint). a => Dict a
Dict

-- | for use in 'WUnlift', etc.
class (MonadTunnelIO m, MonadInner (TunnelIO m)) => MonadTunnelIOInner m

instance (MonadTunnelIO m, MonadInner (TunnelIO m)) => MonadTunnelIOInner m

instance (MonadTransTunnel t, MonadInner (Tunnel t), TransConstraint MonadIO t) => TransConstraint MonadTunnelIOInner t where
    hasTransConstraint :: forall (m :: Type -> Type).
MonadTunnelIOInner m =>
Dict (MonadTunnelIOInner (t m))
hasTransConstraint = forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type) (c' :: (Type -> Type) -> Constraint).
(TransConstraint c t, c m) =>
(c (t m) => Dict (c' (t m))) -> Dict (c' (t m))
withTransConstraintDict @MonadIO forall (a :: Constraint). a => Dict a
Dict