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 MonadTunnelIOInner 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 MonadTunnelIOInner t)
    getDiscardingUnlift = 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 (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (c :: (Type -> Type) -> Constraint) (t :: TransKind).
Unlift c t -> WUnlift c t
MkWUnlift forall a b. (a -> b) -> a -> b
$ \t m a
tma -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: Type -> Type). MonadExtract m => Extract m
mToValue forall a b. (a -> b) -> a -> b
$ 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 MonadTunnelIOInner t
du <- Unlift MonadUnliftIO t
run forall (t :: TransKind) (m :: Type -> Type).
(MonadTransUnlift t, Monad m) =>
t m (WUnlift MonadTunnelIOInner t)
getDiscardingUnlift
    Unlift MonadTunnelIOInner t
du t m a
tmr

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

composeUnliftRaised :: (MonadTransUnlift t, MonadUnliftIO m) => Unlift Functor t -> (m --> n) -> (t m --> n)
composeUnliftRaised :: forall (t :: TransKind) (m :: Type -> Type) (n :: Type -> Type).
(MonadTransUnlift t, MonadUnliftIO m) =>
Unlift Functor t -> (m --> n) -> t m --> n
composeUnliftRaised Unlift Functor t
rt m --> n
rm t m a
tma = m --> n
rm forall a b. (a -> b) -> a -> b
$ 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 = Unlift Functor t
rt 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 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 (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)
unlift -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k (p :: k -> Type) (q :: k -> Type).
(p --> q) -> WRaised p q
MkWRaised forall a b. (a -> b) -> a -> b
$ \m a
mr -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: Type -> Type). MonadExtract m => Extract m
mToValue forall a b. (a -> b) -> a -> b
$ 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 = forall k (p :: k -> Type) (q :: k -> Type).
(p -/-> q) -> WBackraised p q
MkWBackraised 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 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 = forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransUnlift t, MonadIO m) =>
(Unlift MonadTunnelIOInner t -> m r) -> t m r
liftWithUnlift forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIOInner t
tmama -> forall (m :: Type -> Type). MonadUnliftIO m => IO -/-> m
liftIOWithUnlift forall a b. (a -> b) -> a -> b
$ \m --> IO
maioa -> (t m --> IO) -> IO r
call forall a b. (a -> b) -> a -> b
$ m --> IO
maioa forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Unlift MonadTunnelIOInner 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 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 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 forall a b. (a -> b) -> a -> b
$ forall (a :: Constraint). a => Dict a
Dict

instance MonadOuter outer => MonadTransUnlift (ComposeOuter outer) where
    liftWithUnlift :: forall (m :: Type -> Type) r.
MonadIO m =>
(Unlift MonadTunnelIOInner (ComposeOuter outer) -> m r)
-> ComposeOuter outer m r
liftWithUnlift Unlift MonadTunnelIOInner (ComposeOuter outer) -> m r
call =
        forall (outer :: Type -> Type) (inner :: Type -> Type) a.
outer (inner a) -> ComposeOuter outer inner a
MkComposeOuter forall a b. (a -> b) -> a -> b
$ do
            MkWExtract Extract outer
extract <- forall (m :: Type -> Type). MonadOuter m => m (WExtract m)
getExtract
            forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Unlift MonadTunnelIOInner (ComposeOuter outer) -> m r
call forall a b. (a -> b) -> a -> b
$ Extract outer
extract forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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, MonadTunnelIOInner 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, MonadTunnelIOInner ma, MonadIO mb) =>
(ma a -> mb b) -> t ma a -> t mb b
monoHoist ma a -> mb b
f t ma a
tma = forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransUnlift t, MonadIO m) =>
(Unlift MonadTunnelIOInner t -> m r) -> t m r
liftWithUnlift forall a b. (a -> b) -> a -> b
$ \Unlift MonadTunnelIOInner t
unlift -> ma a -> mb b
f forall a b. (a -> b) -> a -> b
$ Unlift MonadTunnelIOInner t
unlift t ma a
tma