-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

{- |
Copyright   :  (c) 2023 Yamada Ryo
License     :  MPL-2.0 (see the file LICENSE)
Maintainer  :  ymdfield@outlook.jp
Stability   :  experimental
Portability :  portable

A Church-encoded Heftia transformer.
-}
module Control.Monad.Trans.Heftia.Church where

import Control.Effect.Class (type (~>))
import Control.Effect.Class.Machinery.HFunctor (hfmap)
import Control.Heftia.Trans (TransHeftia (..))
import Control.Monad (join)
import Control.Monad.Trans (MonadTrans, lift)
import Control.Monad.Trans.Cont (ContT (ContT), runContT)
import Control.Monad.Trans.Heftia (MonadTransHeftia, elaborateMK, reelaborateMK)

-- | A Church-encoded Heftia transformer.
newtype HeftiaChurchT h f a = HeftiaChurchT
    {forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
HeftiaChurchT h f a
-> forall (r :: k).
   (h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a
unHeftiaChurchT :: forall r. (h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a}
    deriving stock (forall a b. a -> HeftiaChurchT h f b -> HeftiaChurchT h f a
forall a b. (a -> b) -> HeftiaChurchT h f a -> HeftiaChurchT h f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (h :: (* -> *) -> * -> *) k (f :: k -> *) a b.
a -> HeftiaChurchT h f b -> HeftiaChurchT h f a
forall (h :: (* -> *) -> * -> *) k (f :: k -> *) a b.
(a -> b) -> HeftiaChurchT h f a -> HeftiaChurchT h f b
<$ :: forall a b. a -> HeftiaChurchT h f b -> HeftiaChurchT h f a
$c<$ :: forall (h :: (* -> *) -> * -> *) k (f :: k -> *) a b.
a -> HeftiaChurchT h f b -> HeftiaChurchT h f a
fmap :: forall a b. (a -> b) -> HeftiaChurchT h f a -> HeftiaChurchT h f b
$cfmap :: forall (h :: (* -> *) -> * -> *) k (f :: k -> *) a b.
(a -> b) -> HeftiaChurchT h f a -> HeftiaChurchT h f b
Functor)

runHeftiaChurchT :: (h (HeftiaChurchT h f) ~> ContT r f) -> HeftiaChurchT h f b -> ContT r f b
runHeftiaChurchT :: forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) (r :: k) b.
(h (HeftiaChurchT h f) ~> ContT r f)
-> HeftiaChurchT h f b -> ContT r f b
runHeftiaChurchT h (HeftiaChurchT h f) ~> ContT r f
i (HeftiaChurchT forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f b
f) = forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f b
f h (HeftiaChurchT h f) ~> ContT r f
i

instance Applicative (HeftiaChurchT h f) where
    pure :: forall a. a -> HeftiaChurchT h f a
pure a
x = forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
 (h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \h (HeftiaChurchT h f) ~> ContT r f
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
    {-# INLINE pure #-}

    HeftiaChurchT forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f (a -> b)
f <*> :: forall a b.
HeftiaChurchT h f (a -> b)
-> HeftiaChurchT h f a -> HeftiaChurchT h f b
<*> HeftiaChurchT forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a
g = forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
 (h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \h (HeftiaChurchT h f) ~> ContT r f
i -> forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f (a -> b)
f h (HeftiaChurchT h f) ~> ContT r f
i forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a
g h (HeftiaChurchT h f) ~> ContT r f
i
    {-# INLINE (<*>) #-}

instance Monad (HeftiaChurchT h f) where
    HeftiaChurchT forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a
f >>= :: forall a b.
HeftiaChurchT h f a
-> (a -> HeftiaChurchT h f b) -> HeftiaChurchT h f b
>>= a -> HeftiaChurchT h f b
k =
        forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
 (h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \h (HeftiaChurchT h f) ~> ContT r f
i -> forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a
f h (HeftiaChurchT h f) ~> ContT r f
i forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) (r :: k) b.
(h (HeftiaChurchT h f) ~> ContT r f)
-> HeftiaChurchT h f b -> ContT r f b
runHeftiaChurchT h (HeftiaChurchT h f) ~> ContT r f
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> HeftiaChurchT h f b
k
    {-# INLINE (>>=) #-}

instance TransHeftia Monad HeftiaChurchT where
    liftSigT :: forall (sig :: (* -> *) -> * -> *) (f :: * -> *) a.
HFunctor sig =>
sig (HeftiaChurchT sig f) a -> HeftiaChurchT sig f a
liftSigT sig (HeftiaChurchT sig f) a
e = forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
 (h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \sig (HeftiaChurchT sig f) ~> ContT r f
i -> sig (HeftiaChurchT sig f) ~> ContT r f
i sig (HeftiaChurchT sig f) a
e
    {-# INLINE liftSigT #-}

    translateT :: forall (f :: * -> *) (sig :: (* -> *) -> * -> *)
       (sig' :: (* -> *) -> * -> *).
(Monad f, HFunctor sig, HFunctor sig') =>
(sig (HeftiaChurchT sig' f) ~> sig' (HeftiaChurchT sig' f))
-> HeftiaChurchT sig f ~> HeftiaChurchT sig' f
translateT sig (HeftiaChurchT sig' f) ~> sig' (HeftiaChurchT sig' f)
phi (HeftiaChurchT forall r. (sig (HeftiaChurchT sig f) ~> ContT r f) -> ContT r f x
f) =
        forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
 (h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \sig' (HeftiaChurchT sig' f) ~> ContT r f
i ->
            forall r. (sig (HeftiaChurchT sig f) ~> ContT r f) -> ContT r f x
f forall a b. (a -> b) -> a -> b
$ sig' (HeftiaChurchT sig' f) ~> ContT r f
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. sig (HeftiaChurchT sig' f) ~> sig' (HeftiaChurchT sig' f)
phi forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (sig :: (* -> *) -> * -> *) (sig' :: (* -> *) -> * -> *).
(TransHeftia c h, c f, HFunctor sig, HFunctor sig') =>
(sig (h sig' f) ~> sig' (h sig' f)) -> h sig f ~> h sig' f
translateT sig (HeftiaChurchT sig' f) ~> sig' (HeftiaChurchT sig' f)
phi)

    liftLowerHT :: forall (sig :: (* -> *) -> * -> *) (f :: * -> *).
(Monad f, HFunctor sig) =>
f ~> HeftiaChurchT sig f
liftLowerHT f x
a = forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
 (h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \sig (HeftiaChurchT sig f) ~> ContT r f
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift f x
a
    {-# INLINE liftLowerHT #-}

    hoistHeftia :: forall (f :: * -> *) (g :: * -> *) (sig :: (* -> *) -> * -> *).
(Monad f, Monad g, HFunctor sig) =>
(f ~> g) -> HeftiaChurchT sig f ~> HeftiaChurchT sig g
hoistHeftia f ~> g
phi (HeftiaChurchT forall r. (sig (HeftiaChurchT sig f) ~> ContT r f) -> ContT r f x
f) =
        forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
 (h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \sig (HeftiaChurchT sig g) ~> ContT r g
i ->
            forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT \x -> g r
k ->
                forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall b c a. (b -> c) -> (a -> b) -> a -> c
. f ~> g
phi forall a b. (a -> b) -> a -> b
$
                    forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
runContT
                        ( forall r. (sig (HeftiaChurchT sig f) ~> ContT r f) -> ContT r f x
f \sig (HeftiaChurchT sig f) x
e -> forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT \x -> f (g r)
k' ->
                            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
runContT (sig (HeftiaChurchT sig g) ~> ContT r g
i forall a b. (a -> b) -> a -> b
$ forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> h sig f ~> h sig g
hoistHeftia f ~> g
phi) sig (HeftiaChurchT sig f) x
e) (forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall b c a. (b -> c) -> (a -> b) -> a -> c
. f ~> g
phi forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> f (g r)
k')
                        )
                        (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> g r
k)

    runElaborateH :: forall (f :: * -> *) (sig :: (* -> *) -> * -> *).
(Monad f, HFunctor sig) =>
(sig f ~> f) -> HeftiaChurchT sig f ~> f
runElaborateH sig f ~> f
g (HeftiaChurchT forall r. (sig (HeftiaChurchT sig f) ~> ContT r f) -> ContT r f x
f) =
        forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
runContT (forall r. (sig (HeftiaChurchT sig f) ~> ContT r f) -> ContT r f x
f forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. sig f ~> f
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
(sig f ~> f) -> h sig f ~> f
runElaborateH sig f ~> f
g)) forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance MonadTrans (HeftiaChurchT h) where
    lift :: forall (m :: * -> *) a. Monad m => m a -> HeftiaChurchT h m a
lift m a
m = forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
 (h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \h (HeftiaChurchT h m) ~> ContT r m
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
m
    {-# INLINE lift #-}

instance MonadTransHeftia HeftiaChurchT where
    elaborateMK :: forall (m :: * -> *) (sig :: (* -> *) -> * -> *) r.
(Monad m, HFunctor sig) =>
(sig (ContT r m) ~> ContT r m) -> HeftiaChurchT sig m ~> ContT r m
elaborateMK sig (ContT r m) ~> ContT r m
f (HeftiaChurchT forall r. (sig (HeftiaChurchT sig m) ~> ContT r m) -> ContT r m x
g) = forall r. (sig (HeftiaChurchT sig m) ~> ContT r m) -> ContT r m x
g forall a b. (a -> b) -> a -> b
$ sig (ContT r m) ~> ContT r m
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (m :: * -> *) (sig :: (* -> *) -> * -> *) r.
(MonadTransHeftia h, Monad m, HFunctor sig) =>
(sig (ContT r m) ~> ContT r m) -> h sig m ~> ContT r m
elaborateMK sig (ContT r m) ~> ContT r m
f)
    {-# INLINE elaborateMK #-}

    reelaborateMK :: forall (m :: * -> *) (sig :: (* -> *) -> * -> *) r.
(Monad m, HFunctor sig) =>
(sig (ContT r (HeftiaChurchT sig m))
 ~> ContT r (HeftiaChurchT sig m))
-> HeftiaChurchT sig m ~> ContT r (HeftiaChurchT sig m)
reelaborateMK sig (ContT r (HeftiaChurchT sig m))
~> ContT r (HeftiaChurchT sig m)
f = forall (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (m :: * -> *) (sig :: (* -> *) -> * -> *) r.
(MonadTransHeftia h, Monad m, HFunctor sig) =>
(sig (ContT r m) ~> ContT r m) -> h sig m ~> ContT r m
elaborateMK sig (ContT r (HeftiaChurchT sig m))
~> ContT r (HeftiaChurchT sig m)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> h sig f ~> h sig g
hoistHeftia forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (sig :: (* -> *) -> * -> *) (f :: * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
f ~> h sig f
liftLowerHT
    {-# INLINE reelaborateMK #-}