-- 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

Interpreter and elaborator for the t'Control.Effect.Class.Reader.Reader' effect class.
-}
module Control.Effect.Handler.Heftia.Reader where

import Control.Effect.Class (type (~>))
import Control.Effect.Class.Reader (AskI (Ask), LocalS (Local), ask)
import Control.Effect.Freer (Fre, interpose, interpret, raise, type (<|))
import Control.Effect.Heftia (ForallHFunctor, Hef, hoistHeftiaEffects, hoistInterpose, interpretH, raiseH)
import Data.Function ((&))

interpretReader ::
    (Monad m, ForallHFunctor es) =>
    r ->
    Hef (LocalS r ': es) (Fre (AskI r ': es') m) ~> Hef es (Fre es' m)
interpretReader :: forall (m :: * -> *) (es :: [(* -> *) -> * -> *]) r
       (es' :: [* -> *]).
(Monad m, ForallHFunctor es) =>
r
-> Hef (LocalS r : es) (Fre (AskI r : es') m) ~> Hef es (Fre es' m)
interpretReader r
r = forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *) (g :: * -> *).
(TransHeftia c h, HFunctor (u es), c f, c g) =>
(f ~> g) -> HeftiaEffects h u es f ~> HeftiaEffects h u es g
hoistHeftiaEffects (forall (m :: * -> *) r (es :: [* -> *]).
Monad m =>
r -> Fre (AskI r : es) m ~> Fre es m
interpretAsk r
r) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r (es' :: [* -> *]) (es :: [(* -> *) -> * -> *])
       (m :: * -> *).
(AskI r <| es', ForallHFunctor es, Monad m) =>
Hef (LocalS r : es) (Fre es' m) ~> Hef es (Fre es' m)
interpretReaderH
{-# INLINE interpretReader #-}

interpretReaderH ::
    (AskI r <| es', ForallHFunctor es, Monad m) =>
    Hef (LocalS r ': es) (Fre es' m) ~> Hef es (Fre es' m)
interpretReaderH :: forall r (es' :: [* -> *]) (es :: [(* -> *) -> * -> *])
       (m :: * -> *).
(AskI r <| es', ForallHFunctor es, Monad m) =>
Hef (LocalS r : es) (Fre es' m) ~> Hef es (Fre es' m)
interpretReaderH =
    forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (e :: (* -> *) -> * -> *)
       (f :: * -> *).
(TransHeftia c h, UnionH u, HFunctor (u es), HFunctor (u (e : es)),
 HFunctor e, c f) =>
(e (HeftiaEffects h u es f) ~> HeftiaEffects h u es f)
-> HeftiaEffects h u (e : es) f ~> HeftiaEffects h u es f
interpretH \(Local (r -> r
f :: r -> r) HeftiaEffects HeftiaChurchT ExtensibleUnionH es (Fre es' m) x
a) ->
        HeftiaEffects HeftiaChurchT ExtensibleUnionH es (Fre es' m) x
a forall a b. a -> (a -> b) -> b
& forall (e :: * -> *)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> (* -> *) -> * -> *)
       (u' :: [* -> *] -> * -> *) (es' :: [* -> *]) (f :: * -> *)
       (c :: (* -> *) -> Constraint) (c' :: (* -> *) -> Constraint).
(TransHeftia c h, HFunctor (u es), TransFreer c' fr, Union u',
 Member u' e es', c (FreerEffects fr u' es' f), c' f) =>
(e ~> FreerEffects fr u' es' f)
-> HeftiaEffects h u es (FreerEffects fr u' es' f)
   ~> HeftiaEffects h u es (FreerEffects fr u' es' f)
hoistInterpose @(AskI r) \AskI r x
Ask -> r -> r
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (f :: * -> *). Ask r f => f r
ask

elaborateReader ::
    (AskI r <| es, Monad m) =>
    LocalS r (Fre es m) ~> Fre es m
elaborateReader :: forall r (es :: [* -> *]) (m :: * -> *).
(AskI r <| es, Monad m) =>
LocalS r (Fre es m) ~> Fre es m
elaborateReader (Local (r -> r
f :: r -> r) Fre es m x
a) =
    Fre es m x
a forall a b. a -> (a -> b) -> b
& forall (e :: * -> *) (fr :: (* -> *) -> (* -> *) -> * -> *)
       (u :: [* -> *] -> * -> *) (es :: [* -> *]) (f :: * -> *)
       (c :: (* -> *) -> Constraint).
(TransFreer c fr, Union u, Member u e es, c f) =>
(e ~> FreerEffects fr u es f)
-> FreerEffects fr u es f ~> FreerEffects fr u es f
interpose @(AskI r) \AskI r x
Ask -> r -> r
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (f :: * -> *). Ask r f => f r
ask

interpretAsk :: Monad m => r -> Fre (AskI r ': es) m ~> Fre es m
interpretAsk :: forall (m :: * -> *) r (es :: [* -> *]).
Monad m =>
r -> Fre (AskI r : es) m ~> Fre es m
interpretAsk r
r = forall (c :: (* -> *) -> Constraint)
       (fr :: (* -> *) -> (* -> *) -> * -> *) (u :: [* -> *] -> * -> *)
       (f :: * -> *) (e :: * -> *) (es :: [* -> *]).
(TransFreer c fr, Union u, c f) =>
(e ~> FreerEffects fr u es f)
-> FreerEffects fr u (e : es) f ~> FreerEffects fr u es f
interpret \AskI r x
Ask -> forall (f :: * -> *) a. Applicative f => a -> f a
pure r
r
{-# INLINE interpretAsk #-}

liftReader ::
    (ForallHFunctor es, Monad m) =>
    Hef es (Fre es' m) ~> Hef (LocalS FilePath ': es) (Fre (AskI FilePath ': es') m)
liftReader :: forall (es :: [(* -> *) -> * -> *]) (m :: * -> *)
       (es' :: [* -> *]).
(ForallHFunctor es, Monad m) =>
Hef es (Fre es' m)
~> Hef (LocalS FilePath : es) (Fre (AskI FilePath : es') m)
liftReader = forall (e :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *])
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *) (f :: * -> *)
       (c :: (* -> *) -> Constraint).
(TransHeftia c h, HFunctor (u hs), HFunctor (u (e : hs)), c f,
 UnionH u) =>
HeftiaEffects h u hs f ~> HeftiaEffects h u (e : hs) f
raiseH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint)
       (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *) (g :: * -> *).
(TransHeftia c h, HFunctor (u es), c f, c g) =>
(f ~> g) -> HeftiaEffects h u es f ~> HeftiaEffects h u es g
hoistHeftiaEffects forall (e :: * -> *) (es :: [* -> *])
       (fr :: (* -> *) -> (* -> *) -> * -> *) (u :: [* -> *] -> * -> *)
       (f :: * -> *) (c :: (* -> *) -> Constraint).
(TransFreer c fr, Union u, c f) =>
FreerEffects fr u es f ~> FreerEffects fr u (e : es) f
raise
{-# INLINE liftReader #-}