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

import Control.Monad.Ology.General.Extract
import Control.Monad.Ology.General.Function
import Control.Monad.Ology.General.IO
import Control.Monad.Ology.General.Outer
import Control.Monad.Ology.General.Trans.Constraint
import Control.Monad.Ology.General.Trans.Hoist
import Control.Monad.Ology.General.Trans.Tunnel
import Control.Monad.Ology.Specific.ComposeOuter
import Import

class ( MonadTransTunnel t
      , TransConstraint MonadFail t
      , TransConstraint MonadIO t
      , TransConstraint MonadFix t
      , TransConstraint Monad t
      , MonadExtract (Tunnel t)
      ) => MonadTransUnlift t where
    -- | Lift with an unlifting function that accounts for the transformer's effects (using MVars where necessary).
    liftWithUnlift ::
           forall m r. MonadIO m
        => (Unlift MonadTunnelIO t -> m r)
        -> t m r
    -- | Return an unlifting function that discards the transformer's effects (such as state change or output).
    getDiscardingUnlift ::
           forall m. Monad m
        => t m (WUnlift MonadTunnelIO t)
    getDiscardingUnlift = ((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m (Tunnel t (WUnlift MonadTunnelIO t)))
-> t m (WUnlift MonadTunnelIO t)
forall (m :: Type -> Type) r.
Monad m =>
((forall (m1 :: Type -> Type) a.
  Monad m1 =>
  t m1 a -> m1 (Tunnel t a))
 -> m (Tunnel t r))
-> t m r
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 (m1 :: Type -> Type) a.
   Monad m1 =>
   t m1 a -> m1 (Tunnel t a))
  -> m (Tunnel t (WUnlift MonadTunnelIO t)))
 -> t m (WUnlift MonadTunnelIO t))
-> ((forall (m1 :: Type -> Type) a.
     Monad m1 =>
     t m1 a -> m1 (Tunnel t a))
    -> m (Tunnel t (WUnlift MonadTunnelIO t)))
-> t m (WUnlift MonadTunnelIO t)
forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift -> Tunnel t (WUnlift MonadTunnelIO t)
-> m (Tunnel t (WUnlift MonadTunnelIO t))
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Tunnel t (WUnlift MonadTunnelIO t)
 -> m (Tunnel t (WUnlift MonadTunnelIO t)))
-> Tunnel t (WUnlift MonadTunnelIO t)
-> m (Tunnel t (WUnlift MonadTunnelIO t))
forall a b. (a -> b) -> a -> b
$ WUnlift MonadTunnelIO t -> Tunnel t (WUnlift MonadTunnelIO t)
forall a. a -> Tunnel t a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (WUnlift MonadTunnelIO t -> Tunnel t (WUnlift MonadTunnelIO t))
-> WUnlift MonadTunnelIO t -> Tunnel t (WUnlift MonadTunnelIO t)
forall a b. (a -> b) -> a -> b
$ Unlift MonadTunnelIO t -> WUnlift MonadTunnelIO t
forall (c :: (Type -> Type) -> Constraint) (t :: TransKind).
Unlift c t -> WUnlift c t
MkWUnlift (Unlift MonadTunnelIO t -> WUnlift MonadTunnelIO t)
-> Unlift MonadTunnelIO t -> WUnlift MonadTunnelIO t
forall a b. (a -> b) -> a -> b
$ \t m a
tma -> (Tunnel t a -> a) -> m (Tunnel t a) -> m a
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Tunnel t a -> a
Extract (Tunnel t)
forall (m :: Type -> Type). MonadExtract m => Extract m
mToValue (m (Tunnel t a) -> m a) -> m (Tunnel t a) -> m a
forall a b. (a -> b) -> a -> b
$ t m a -> m (Tunnel t a)
forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift t m a
tma

toDiscardingUnlift ::
       forall t. MonadTransUnlift t
    => Unlift MonadUnliftIO t
    -> Unlift MonadUnliftIO t
toDiscardingUnlift :: forall (t :: TransKind).
MonadTransUnlift t =>
Unlift MonadUnliftIO t -> Unlift MonadUnliftIO t
toDiscardingUnlift Unlift MonadUnliftIO t
run t m a
tmr = do
    MkWUnlift Unlift MonadTunnelIO t
du <- t m (WUnlift MonadTunnelIO t) -> m (WUnlift MonadTunnelIO t)
t m --> m
Unlift MonadUnliftIO t
run t m (WUnlift MonadTunnelIO t)
forall (m :: Type -> Type).
Monad m =>
t m (WUnlift MonadTunnelIO t)
forall (t :: TransKind) (m :: Type -> Type).
(MonadTransUnlift t, Monad m) =>
t m (WUnlift MonadTunnelIO t)
getDiscardingUnlift
    t m a -> m a
t m --> m
Unlift MonadTunnelIO t
du t m a
tmr

wLiftWithUnlift ::
       forall t m. (MonadTransUnlift t, MonadTunnelIO m)
    => WBackraised m (t m)
wLiftWithUnlift :: forall (t :: TransKind) (m :: Type -> Type).
(MonadTransUnlift t, MonadTunnelIO m) =>
WBackraised m (t m)
wLiftWithUnlift = (m -/-> t m) -> WBackraised m (t m)
forall k (p :: k -> Type) (q :: k -> Type).
(p -/-> q) -> WBackraised p q
MkWBackraised ((m -/-> t m) -> WBackraised m (t m))
-> (m -/-> t m) -> WBackraised m (t m)
forall a b. (a -> b) -> a -> b
$ \(t m --> m) -> m r
call -> (Unlift MonadTunnelIO t -> m r) -> t m r
forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIO t -> m r) -> t m r
forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransUnlift t, MonadIO m) =>
(Unlift MonadTunnelIO t -> m r) -> t m r
liftWithUnlift ((Unlift MonadTunnelIO t -> m r) -> t m r)
-> (Unlift MonadTunnelIO t -> m r) -> t m r
forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIO t
unlift -> (t m --> m) -> m r
call t m a -> m a
t m --> m
Unlift MonadTunnelIO t
unlift

composeUnliftRaised :: MonadUnliftIO m => Unlift Functor t -> (m --> n) -> (t m --> n)
composeUnliftRaised :: forall (m :: Type -> Type) (t :: TransKind) (n :: Type -> Type).
MonadUnliftIO m =>
Unlift Functor t -> (m --> n) -> t m --> n
composeUnliftRaised Unlift Functor t
rt m --> n
rm t m a
tma = m a -> n a
m --> n
rm (m a -> n a) -> m a -> n a
forall a b. (a -> b) -> a -> b
$ t m a -> m a
t m --> m
Unlift Functor t
rt t m a
tma

composeUnliftRaisedCommute ::
       (MonadTransUnlift t, MonadUnliftIO m, MonadUnliftIO n) => Unlift Functor t -> (m --> n) -> (t m --> n)
composeUnliftRaisedCommute :: forall (t :: TransKind) (m :: Type -> Type) (n :: Type -> Type).
(MonadTransUnlift t, MonadUnliftIO m, MonadUnliftIO n) =>
Unlift Functor t -> (m --> n) -> t m --> n
composeUnliftRaisedCommute Unlift Functor t
rt m --> n
rm t m a
tma = t n a -> n a
t n --> n
Unlift Functor t
rt (t n a -> n a) -> t n a -> n a
forall a b. (a -> b) -> a -> b
$ (m --> n) -> t m --> t n
forall (m1 :: Type -> Type) (m2 :: Type -> Type).
(Monad m1, Monad m2) =>
(m1 --> m2) -> t m1 --> t m2
forall (t :: TransKind) (m1 :: Type -> Type) (m2 :: Type -> Type).
(MonadTransHoist t, Monad m1, Monad m2) =>
(m1 --> m2) -> t m1 --> t m2
hoist m a -> n a
m --> n
rm t m a
tma

class (MonadFail m, MonadIO m, MonadFix m, MonadTunnelIO m, MonadExtract (TunnelIO m)) => MonadUnliftIO m where
    -- | Lift with an unlifting function that accounts for the effects over 'IO'.
    liftIOWithUnlift :: IO -/-> m
    -- | Return an unlifting function that discards the effects over 'IO'.
    getDiscardingIOUnlift :: m (WRaised m IO)
    getDiscardingIOUnlift = ((forall a. m a -> IO (TunnelIO m a))
 -> IO (TunnelIO m (WRaised m IO)))
-> m (WRaised m IO)
forall r.
((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m r)) -> m r
forall (m :: Type -> Type) r.
MonadTunnelIO m =>
((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m r)) -> m r
tunnelIO (((forall a. m a -> IO (TunnelIO m a))
  -> IO (TunnelIO m (WRaised m IO)))
 -> m (WRaised m IO))
-> ((forall a. m a -> IO (TunnelIO m a))
    -> IO (TunnelIO m (WRaised m IO)))
-> m (WRaised m IO)
forall a b. (a -> b) -> a -> b
$ \forall a. m a -> IO (TunnelIO m a)
unlift -> TunnelIO m (WRaised m IO) -> IO (TunnelIO m (WRaised m IO))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TunnelIO m (WRaised m IO) -> IO (TunnelIO m (WRaised m IO)))
-> TunnelIO m (WRaised m IO) -> IO (TunnelIO m (WRaised m IO))
forall a b. (a -> b) -> a -> b
$ WRaised m IO -> TunnelIO m (WRaised m IO)
forall a. a -> TunnelIO m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (WRaised m IO -> TunnelIO m (WRaised m IO))
-> WRaised m IO -> TunnelIO m (WRaised m IO)
forall a b. (a -> b) -> a -> b
$ (m --> IO) -> WRaised m IO
forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised ((m --> IO) -> WRaised m IO) -> (m --> IO) -> WRaised m IO
forall a b. (a -> b) -> a -> b
$ \m a
mr -> (TunnelIO m a -> a) -> IO (TunnelIO m a) -> IO a
forall a b. (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap TunnelIO m a -> a
Extract (TunnelIO m)
forall (m :: Type -> Type). MonadExtract m => Extract m
mToValue (IO (TunnelIO m a) -> IO a) -> IO (TunnelIO m a) -> IO a
forall a b. (a -> b) -> a -> b
$ m a -> IO (TunnelIO m a)
forall a. m a -> IO (TunnelIO m a)
unlift m a
mr

wLiftIOWithUnlift :: MonadUnliftIO m => WBackraised IO m
wLiftIOWithUnlift :: forall (m :: Type -> Type). MonadUnliftIO m => WBackraised IO m
wLiftIOWithUnlift = (IO -/-> m) -> WBackraised IO m
forall k (p :: k -> Type) (q :: k -> Type).
(p -/-> q) -> WBackraised p q
MkWBackraised ((m --> IO) -> IO r) -> m r
IO -/-> m
forall (m :: Type -> Type). MonadUnliftIO m => IO -/-> m
liftIOWithUnlift

instance MonadUnliftIO IO where
    liftIOWithUnlift :: IO -/-> IO
liftIOWithUnlift (IO --> IO) -> IO r
call = (IO --> IO) -> IO r
call IO a -> IO a
forall a. a -> a
IO --> IO
forall {k} (cat :: k -> k -> Type) (a :: k).
Category cat =>
cat a a
id

instance (MonadTransUnlift t, MonadUnliftIO m, MonadFail (t m), MonadIO (t m), MonadFix (t m)) => MonadUnliftIO (t m) where
    liftIOWithUnlift :: IO -/-> t m
liftIOWithUnlift (t m --> IO) -> IO r
call = (Unlift MonadTunnelIO t -> m r) -> t m r
forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIO t -> m r) -> t m r
forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransUnlift t, MonadIO m) =>
(Unlift MonadTunnelIO t -> m r) -> t m r
liftWithUnlift ((Unlift MonadTunnelIO t -> m r) -> t m r)
-> (Unlift MonadTunnelIO t -> m r) -> t m r
forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIO t
tmama -> ((m --> IO) -> IO r) -> m r
IO -/-> m
forall (m :: Type -> Type). MonadUnliftIO m => IO -/-> m
liftIOWithUnlift (((m --> IO) -> IO r) -> m r) -> ((m --> IO) -> IO r) -> m r
forall a b. (a -> b) -> a -> b
$ \m --> IO
maioa -> (t m --> IO) -> IO r
call ((t m --> IO) -> IO r) -> (t m --> IO) -> IO r
forall a b. (a -> b) -> a -> b
$ m a -> IO a
m --> IO
maioa (m a -> IO a) -> (t m a -> m a) -> t m a -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. t m a -> m a
t m --> m
Unlift MonadTunnelIO t
tmama

instance MonadTransUnlift t => TransConstraint MonadUnliftIO t where
    hasTransConstraint :: forall (m :: Type -> Type).
MonadUnliftIO m =>
Dict (MonadUnliftIO (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 @MonadFail ((MonadFail (t m) => Dict (MonadUnliftIO (t m)))
 -> Dict (MonadUnliftIO (t m)))
-> (MonadFail (t m) => Dict (MonadUnliftIO (t m)))
-> Dict (MonadUnliftIO (t m))
forall a b. (a -> b) -> a -> b
$ 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 ((MonadIO (t m) => Dict (MonadUnliftIO (t m)))
 -> Dict (MonadUnliftIO (t m)))
-> (MonadIO (t m) => Dict (MonadUnliftIO (t m)))
-> Dict (MonadUnliftIO (t m))
forall a b. (a -> b) -> a -> b
$ 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 @MonadFix ((MonadFix (t m) => Dict (MonadUnliftIO (t m)))
 -> Dict (MonadUnliftIO (t m)))
-> (MonadFix (t m) => Dict (MonadUnliftIO (t m)))
-> Dict (MonadUnliftIO (t m))
forall a b. (a -> b) -> a -> b
$ Dict (MonadUnliftIO (t m))
MonadFix (t m) => Dict (MonadUnliftIO (t m))
forall (a :: Constraint). a => Dict a
Dict

instance forall outer. MonadOuter outer => MonadTransUnlift (ComposeOuter outer) where
    liftWithUnlift :: forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIO (ComposeOuter outer) -> m r)
-> ComposeOuter outer m r
liftWithUnlift Unlift MonadTunnelIO (ComposeOuter outer) -> m r
call =
        outer (m r) -> ComposeOuter outer m r
forall (outer :: Type -> Type) (inner :: Type -> Type) a.
outer (inner a) -> ComposeOuter outer inner a
MkComposeOuter (outer (m r) -> ComposeOuter outer m r)
-> outer (m r) -> ComposeOuter outer m r
forall a b. (a -> b) -> a -> b
$ do
            MkWExtract Extract outer
extract <- outer (WExtract outer)
forall (m :: Type -> Type). MonadOuter m => m (WExtract m)
getExtract
            m r -> outer (m r)
forall a. a -> outer a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (m r -> outer (m r)) -> m r -> outer (m r)
forall a b. (a -> b) -> a -> b
$ Unlift MonadTunnelIO (ComposeOuter outer) -> m r
call (Unlift MonadTunnelIO (ComposeOuter outer) -> m r)
-> Unlift MonadTunnelIO (ComposeOuter outer) -> m r
forall a b. (a -> b) -> a -> b
$ outer (m a) -> m a
Extract outer
extract (outer (m a) -> m a)
-> (ComposeOuter outer m a -> outer (m a))
-> ComposeOuter outer m a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ComposeOuter outer m a -> outer (m a)
forall (outer :: Type -> Type) (inner :: Type -> Type) a.
ComposeOuter outer inner a -> outer (inner a)
unComposeOuter

monoHoist ::
       forall (t :: TransKind) ma mb a b. (MonadTransUnlift t, MonadTunnelIO ma, MonadIO mb)
    => (ma a -> mb b)
    -> (t ma a -> t mb b)
monoHoist :: forall (t :: TransKind) (ma :: Type -> Type) (mb :: Type -> Type) a
       b.
(MonadTransUnlift t, MonadTunnelIO ma, MonadIO mb) =>
(ma a -> mb b) -> t ma a -> t mb b
monoHoist ma a -> mb b
f t ma a
tma = (Unlift MonadTunnelIO t -> mb b) -> t mb b
forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIO t -> m r) -> t m r
forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransUnlift t, MonadIO m) =>
(Unlift MonadTunnelIO t -> m r) -> t m r
liftWithUnlift ((Unlift MonadTunnelIO t -> mb b) -> t mb b)
-> (Unlift MonadTunnelIO t -> mb b) -> t mb b
forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIO t
unlift -> ma a -> mb b
f (ma a -> mb b) -> ma a -> mb b
forall a b. (a -> b) -> a -> b
$ t ma a -> ma a
t ma --> ma
Unlift MonadTunnelIO t
unlift t ma a
tma