{-# LANGUAGE QuantifiedConstraints #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Eta reduce" #-}

-- 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 type class to abstract away the encoding details of the Heftia carrier transformers.
-}
module Control.Heftia.Trans where

import Control.Effect.Class (LiftIns (LiftIns), unliftIns, type (~>))
import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap, (:+:) (Inl, Inr))
import Control.Freer.Trans (TransFreer, interpretFT, liftInsT, liftLowerFT)
import Control.Monad.Identity (IdentityT (IdentityT), runIdentityT)

-- | A type class to abstract away the encoding details of the Heftia carrier transformers.
class (forall sig f. c f => c (h sig f)) => TransHeftia c h | h -> c where
    {-# MINIMAL liftSigT, liftLowerHT, (hoistHeftia, runElaborateH | elaborateHT) #-}

    -- | Lift a /signature/ into a Heftia carrier transformer.
    liftSigT :: HFunctor sig => sig (h sig f) a -> h sig f a

    transformHT ::
        (c f, HFunctor sig, HFunctor sig') =>
        (forall g. sig g ~> sig' g) ->
        h sig f ~> h sig' f
    transformHT forall (g :: * -> *). sig g ~> sig' g
f = 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 forall (g :: * -> *). sig g ~> sig' g
f
    {-# INLINE transformHT #-}

    -- | Translate /signature/s embedded in a Heftia carrier transformer.
    translateT ::
        (c f, HFunctor sig, HFunctor sig') =>
        (sig (h sig' f) ~> sig' (h sig' f)) ->
        h sig f ~> h sig' f
    translateT sig (h sig' f) ~> sig' (h sig' f)
f = forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> (sig g ~> g) -> h sig f ~> g
elaborateHT forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (sig :: (* -> *) -> * -> *) (f :: * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
f ~> h sig f
liftLowerHT (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
. sig (h sig' f) ~> sig' (h sig' f)
f)
    {-# INLINE translateT #-}

    liftLowerHT :: forall sig f. (c f, HFunctor sig) => f ~> h sig f

    -- | Translate an underlying monad.
    hoistHeftia :: (c f, c g, HFunctor sig) => (f ~> g) -> h sig f ~> h sig g
    hoistHeftia f ~> g
phi = forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> (sig g ~> g) -> h sig f ~> g
elaborateHT (forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (sig :: (* -> *) -> * -> *) (f :: * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
f ~> h sig f
liftLowerHT forall b c a. (b -> c) -> (a -> b) -> a -> c
. f ~> g
phi) forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (sig :: (* -> *) -> * -> *) (f :: * -> *) a.
(TransHeftia c h, HFunctor sig) =>
sig (h sig f) a -> h sig f a
liftSigT
    {-# INLINE hoistHeftia #-}

    interpretLowerHT :: (HFunctor sig, c f, c g) => (f ~> h sig g) -> h sig f ~> h sig g
    interpretLowerHT f ~> h sig g
f = forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> (sig g ~> g) -> h sig f ~> g
elaborateHT f ~> h sig g
f forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (sig :: (* -> *) -> * -> *) (f :: * -> *) a.
(TransHeftia c h, HFunctor sig) =>
sig (h sig f) a -> h sig f a
liftSigT
    {-# INLINE interpretLowerHT #-}

    runElaborateH :: (c f, HFunctor sig) => (sig f ~> f) -> h sig f ~> f
    default runElaborateH :: (c f, c (IdentityT f), HFunctor sig) => (sig f ~> f) -> h sig f ~> f
    runElaborateH sig f ~> f
f = forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT 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) -> (sig g ~> g) -> h sig f ~> g
elaborateHT forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT (forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT forall b c a. (b -> c) -> (a -> b) -> a -> c
. sig f ~> f
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 {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT)
    {-# INLINE runElaborateH #-}

    elaborateHT :: (c f, c g, HFunctor sig) => (f ~> g) -> (sig g ~> g) -> h sig f ~> g
    elaborateHT f ~> g
f sig g ~> g
i = forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
(sig f ~> f) -> h sig f ~> f
runElaborateH sig g ~> g
i 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
f
    {-# INLINE elaborateHT #-}

    reelaborateHT :: (c f, HFunctor sig) => (sig (h sig f) ~> h sig f) -> h sig f ~> h sig f
    reelaborateHT = forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> (sig g ~> g) -> h sig f ~> g
elaborateHT forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (sig :: (* -> *) -> * -> *) (f :: * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
f ~> h sig f
liftLowerHT
    {-# INLINE reelaborateHT #-}

heftiaToFreer ::
    (TransHeftia c h, TransFreer c' fr, c f, c (fr ins f), c' f) =>
    h (LiftIns ins) f ~> fr ins f
heftiaToFreer :: forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (c' :: (* -> *) -> Constraint)
       (fr :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (ins :: * -> *).
(TransHeftia c h, TransFreer c' fr, c f, c (fr ins f), c' f) =>
h (LiftIns ins) f ~> fr ins f
heftiaToFreer = forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> (sig g ~> g) -> h sig f ~> g
elaborateHT forall {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
       (f :: k -> *).
(TransFreer c fr, c f) =>
f ~> fr ins f
liftLowerFT (forall {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
       (f :: k -> *).
TransFreer c fr =>
ins ~> fr ins f
liftInsT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ins :: * -> *) (f :: * -> *) a. LiftIns ins f a -> ins a
unliftIns)
{-# INLINE heftiaToFreer #-}

freerToHeftia ::
    (TransHeftia c h, TransFreer c' fr, c' f, c' (fr ins f), c' (h (LiftIns ins) f), c f) =>
    fr ins f ~> h (LiftIns ins) f
freerToHeftia :: forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (c' :: (* -> *) -> Constraint)
       (fr :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (ins :: * -> *).
(TransHeftia c h, TransFreer c' fr, c' f, c' (fr ins f),
 c' (h (LiftIns ins) f), c f) =>
fr ins f ~> h (LiftIns ins) f
freerToHeftia = forall {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *)
       (ins :: k -> *).
(TransFreer c fr, c f, c g) =>
(f ~> g) -> (ins ~> g) -> fr ins f ~> g
interpretFT forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (sig :: (* -> *) -> * -> *) (f :: * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
f ~> h sig f
liftLowerHT (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 freerToHeftia #-}

mergeHeftia ::
    forall h m sig sig' a c.
    (HFunctor sig, HFunctor sig', TransHeftia c h, c m) =>
    h sig (h sig' m) a ->
    h (sig :+: sig') m a
mergeHeftia :: forall (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (m :: * -> *) (sig :: (* -> *) -> * -> *)
       (sig' :: (* -> *) -> * -> *) a (c :: (* -> *) -> Constraint).
(HFunctor sig, HFunctor sig', TransHeftia c h, c m) =>
h sig (h sig' m) a -> h (sig :+: sig') m a
mergeHeftia = forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> (sig g ~> g) -> h sig f ~> g
elaborateHT (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 @c forall {k} (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
g h e -> (:+:) f g h e
Inr) (forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (sig :: (* -> *) -> * -> *) (f :: * -> *) a.
(TransHeftia c h, HFunctor sig) =>
sig (h sig f) a -> h sig f a
liftSigT @c forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
f h e -> (:+:) f g h e
Inl)