{-# LANGUAGE QuantifiedConstraints #-}

-- 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 Freer carrier transformers.
-}
module Control.Freer.Trans where

import Control.Effect.Class (type (~>))
import Control.Monad.Identity (IdentityT (IdentityT), runIdentityT)
import Data.Free.Sum (pattern L1, pattern R1, type (+))

-- | A type class to abstract away the encoding details of the Freer carrier transformers.
class (forall ins f. c f => c (fr ins f)) => TransFreer c fr | fr -> c where
    {-# MINIMAL liftInsT, liftLowerFT, (hoistFreer, runInterpretF | interpretFT) #-}

    -- | Lift a /instruction/ into a Freer carrier transformer.
    liftInsT :: ins ~> fr ins f

    liftLowerFT :: forall ins f. c f => f ~> fr ins f

    -- | Translate /instruction/s embedded in a Freer carrier transformer.
    transformT :: c f => (ins ~> ins') -> fr ins f ~> fr ins' f
    transformT ins ~> ins'
f = 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 {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
. ins ~> ins'
f)
    {-# INLINE transformT #-}

    -- | Translate an underlying carrier.
    hoistFreer :: (c f, c g) => (f ~> g) -> fr ins f ~> fr ins g
    hoistFreer f ~> g
f = 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 {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
       (f :: k -> *).
(TransFreer c fr, c f) =>
f ~> fr ins f
liftLowerFT forall b c a. (b -> c) -> (a -> b) -> a -> c
. f ~> g
f) forall {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
       (f :: k -> *).
TransFreer c fr =>
ins ~> fr ins f
liftInsT
    {-# INLINE hoistFreer #-}

    interposeLowerT :: (c f, c g) => (f ~> fr ins g) -> fr ins f ~> fr ins g
    interposeLowerT f ~> fr ins g
f = 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 f ~> fr ins g
f forall {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
       (f :: k -> *).
TransFreer c fr =>
ins ~> fr ins f
liftInsT
    {-# INLINE interposeLowerT #-}

    runInterpretF :: c f => (ins ~> f) -> fr ins f a -> f a
    default runInterpretF :: (c f, c (IdentityT f)) => (ins ~> f) -> fr ins f a -> f a
    runInterpretF ins ~> 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 {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 {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
. ins ~> f
f)
    {-# INLINE runInterpretF #-}

    interpretFT :: (c f, c g) => (f ~> g) -> (ins ~> g) -> fr ins f ~> g
    interpretFT f ~> g
f ins ~> g
i = forall {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (ins :: k -> *) (a :: k).
(TransFreer c fr, c f) =>
(ins ~> f) -> fr ins f a -> f a
runInterpretF ins ~> g
i 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 f ~> g
f
    {-# INLINE interpretFT #-}

    reinterpretFT :: c f => (ins ~> fr ins f) -> fr ins f ~> fr ins f
    reinterpretFT = 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 {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
       (f :: k -> *).
(TransFreer c fr, c f) =>
f ~> fr ins f
liftLowerFT
    {-# INLINE reinterpretFT #-}

mergeFreer ::
    forall fr m ins ins' c.
    (TransFreer c fr, c m) =>
    fr ins (fr ins' m) ~> fr (ins + ins') m
mergeFreer :: forall {k} (fr :: (k -> *) -> (k -> *) -> k -> *) (m :: k -> *)
       (ins :: k -> *) (ins' :: k -> *) (c :: (k -> *) -> Constraint).
(TransFreer c fr, c m) =>
fr ins (fr ins' m) ~> fr (ins + ins') m
mergeFreer = 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 {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (ins :: k -> *) (ins' :: k -> *).
(TransFreer c fr, c f) =>
(ins ~> ins') -> fr ins f ~> fr ins' f
transformT @c forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1) (forall {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
       (f :: k -> *).
TransFreer c fr =>
ins ~> fr ins f
liftInsT @c forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1)

splitFreer ::
    forall fr m ins ins' c.
    (TransFreer c fr, c m) =>
    fr (ins + ins') m ~> fr ins (fr ins' m)
splitFreer :: forall {k} (fr :: (k -> *) -> (k -> *) -> k -> *) (m :: k -> *)
       (ins :: k -> *) (ins' :: k -> *) (c :: (k -> *) -> Constraint).
(TransFreer c fr, c m) =>
fr (ins + ins') m ~> fr ins (fr ins' m)
splitFreer = 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 {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
       (f :: k -> *).
(TransFreer c fr, c f) =>
f ~> fr ins f
liftLowerFT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
       (f :: k -> *).
(TransFreer c fr, c f) =>
f ~> fr ins f
liftLowerFT) \case
    L1 ins x
e -> forall {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
       (f :: k -> *).
TransFreer c fr =>
ins ~> fr ins f
liftInsT ins x
e
    R1 ins' x
e -> forall {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
       (f :: k -> *).
(TransFreer c fr, c f) =>
f ~> fr ins f
liftLowerFT forall a b. (a -> b) -> a -> b
$ forall {k} (c :: (k -> *) -> Constraint)
       (fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
       (f :: k -> *).
TransFreer c fr =>
ins ~> fr ins f
liftInsT ins' x
e