{-# LANGUAGE DerivingVia #-}

-- 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 Freer transformer.
-}
module Control.Monad.Trans.Freer.Church where

import Control.Effect.Class (Instruction, LiftIns (..))
import Control.Freer.Trans (TransFreer (hoistFreer, liftInsT, liftLowerFT, runInterpretF))
import Control.Heftia.Trans (TransHeftia (..), liftSigT)
import Control.Monad.Trans (MonadTrans)
import Control.Monad.Trans.Freer (
    MonadTransFreer (interpretMK, reinterpretMK),
    ViaLiftLower (ViaLiftLower),
 )
import Control.Monad.Trans.Heftia.Church (HeftiaChurchT (HeftiaChurchT))

-- | A Church-encoded Freer transformer.
newtype FreerChurchT (ins :: Instruction) f a = FreerChurchT
    {forall {k} (ins :: * -> *) (f :: k -> *) a.
FreerChurchT ins f a -> HeftiaChurchT (LiftIns ins) f a
unFreerChurchT :: HeftiaChurchT (LiftIns ins) f a}

deriving newtype instance Functor (FreerChurchT ins m)
deriving newtype instance Applicative (FreerChurchT ins m)
deriving newtype instance Monad (FreerChurchT ins m)

instance TransFreer Monad FreerChurchT where
    liftInsT :: forall (ins :: * -> *) (f :: * -> *). ins ~> FreerChurchT ins f
liftInsT = forall {k} (ins :: * -> *) (f :: k -> *) a.
HeftiaChurchT (LiftIns ins) f a -> FreerChurchT ins f a
FreerChurchT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (sig :: (* -> *) -> * -> *) (f :: * -> *) a.
(TransHeftia c h, HFunctor sig) =>
sig (h sig f) a -> h sig f a
liftSigT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ins :: * -> *) (f :: * -> *) a. ins a -> LiftIns ins f a
LiftIns
    {-# INLINE liftInsT #-}

    liftLowerFT :: forall (ins :: * -> *) (f :: * -> *).
Monad f =>
f ~> FreerChurchT ins f
liftLowerFT = forall {k} (ins :: * -> *) (f :: k -> *) a.
HeftiaChurchT (LiftIns ins) f a -> FreerChurchT ins f a
FreerChurchT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (sig :: (* -> *) -> * -> *) (f :: * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
f ~> h sig f
liftLowerHT
    {-# INLINE liftLowerFT #-}

    runInterpretF :: forall (f :: * -> *) (ins :: * -> *) a.
Monad f =>
(ins ~> f) -> FreerChurchT ins f a -> f a
runInterpretF ins ~> f
i = forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
(sig f ~> f) -> h sig f ~> f
runElaborateH (ins ~> f
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ins :: * -> *) (f :: * -> *) a. LiftIns ins f a -> ins a
unliftIns) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (ins :: * -> *) (f :: k -> *) a.
FreerChurchT ins f a -> HeftiaChurchT (LiftIns ins) f a
unFreerChurchT
    {-# INLINE runInterpretF #-}

    hoistFreer :: forall (f :: * -> *) (g :: * -> *) (ins :: * -> *).
(Monad f, Monad g) =>
(f ~> g) -> FreerChurchT ins f ~> FreerChurchT ins g
hoistFreer f ~> g
phi = forall {k} (ins :: * -> *) (f :: k -> *) a.
HeftiaChurchT (LiftIns ins) f a -> FreerChurchT ins f a
FreerChurchT 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 f ~> g
phi forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (ins :: * -> *) (f :: k -> *) a.
FreerChurchT ins f a -> HeftiaChurchT (LiftIns ins) f a
unFreerChurchT
    {-# INLINE hoistFreer #-}

deriving via ViaLiftLower FreerChurchT ins instance MonadTrans (FreerChurchT ins)

instance MonadTransFreer FreerChurchT where
    interpretMK :: forall (m :: * -> *) (ins :: * -> *) r.
Monad m =>
(ins ~> ContT r m) -> FreerChurchT ins m ~> ContT r m
interpretMK ins ~> ContT r m
f (FreerChurchT (HeftiaChurchT forall r.
(LiftIns ins (HeftiaChurchT (LiftIns ins) m) ~> ContT r m)
-> ContT r m x
g)) = forall r.
(LiftIns ins (HeftiaChurchT (LiftIns ins) m) ~> ContT r m)
-> ContT r m x
g forall a b. (a -> b) -> a -> b
$ ins ~> ContT r m
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ins :: * -> *) (f :: * -> *) a. LiftIns ins f a -> ins a
unliftIns
    {-# INLINE interpretMK #-}

    reinterpretMK :: forall (m :: * -> *) (ins :: * -> *) r.
Monad m =>
(ins ~> ContT r (FreerChurchT ins m))
-> FreerChurchT ins m ~> ContT r (FreerChurchT ins m)
reinterpretMK ins ~> ContT r (FreerChurchT ins m)
f = forall (fr :: (* -> *) -> (* -> *) -> * -> *) (m :: * -> *)
       (ins :: * -> *) r.
(MonadTransFreer fr, Monad m) =>
(ins ~> ContT r m) -> fr ins m ~> ContT r m
interpretMK ins ~> ContT r (FreerChurchT ins m)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *)
       (ins :: k -> *).
(TransFreer c fr, c f, c g) =>
(f ~> g) -> fr ins f ~> fr ins g
hoistFreer forall {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
       (f :: k -> *).
(TransFreer c fr, c f) =>
f ~> fr ins f
liftLowerFT
    {-# INLINE reinterpretMK #-}