-- 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.Except.Except' effect class.
-}
module Control.Effect.Handler.Heftia.Except where

import Control.Effect.Class (type (~>))
import Control.Effect.Class.Except (CatchS (Catch), ThrowI (Throw))
import Control.Effect.Freer (Fre, interposeK, interposeT, interpretK, interpretT, type (<|))
import Control.Monad.Trans.Except (ExceptT (ExceptT), runExceptT, throwE)
import Data.Function ((&))

-- | Elaborate the 'Catch' effect using the 'ExceptT' monad transformer.
elaborateExceptT ::
    (ThrowI e <| es, Monad m) =>
    CatchS e (Fre es m) ~> Fre es m
elaborateExceptT :: forall e (es :: [Instruction]) (m :: Instruction).
(ThrowI e <| es, Monad m) =>
CatchS e (Fre es m) ~> Fre es m
elaborateExceptT (Catch Fre es m x
action (e -> Fre es m x
hdl :: e -> Fre es m a)) = do
    Either e x
r <- forall e (m :: Instruction) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ Fre es m x
action forall a b. a -> (a -> b) -> b
& forall (e :: Instruction) (t :: Instruction -> Instruction)
       (fr :: Instruction -> Instruction -> Instruction)
       (u :: [Instruction] -> Instruction) (es :: [Instruction])
       (m :: Instruction).
(MonadTransFreer fr, Union u, Member u e es, Monad m, MonadTrans t,
 forall (m1 :: Instruction) (m2 :: Instruction) x.
 Coercible m1 m2 =>
 Coercible (t m1 x) (t m2 x),
 Monad (t (fr (u es) m))) =>
(e ~> t (FreerEffects fr u es m))
-> FreerEffects fr u es m ~> t (FreerEffects fr u es m)
interposeT \(Throw (e
e :: e)) -> forall (m :: Instruction) e a. Monad m => e -> ExceptT e m a
throwE e
e
    case Either e x
r of
        Left e
e -> e -> Fre es m x
hdl e
e
        Right x
a -> forall (f :: Instruction) a. Applicative f => a -> f a
pure x
a

{- |
Elaborate the 'Catch' effect using the t'Control.Monad.Trans.Cont.ContT' continuation monad
transformer.
-}
elaborateExceptK ::
    (ThrowI e <| es, Monad m) =>
    CatchS e (Fre es m) ~> Fre es m
elaborateExceptK :: forall e (es :: [Instruction]) (m :: Instruction).
(ThrowI e <| es, Monad m) =>
CatchS e (Fre es m) ~> Fre es m
elaborateExceptK (Catch Fre es m x
action (e -> Fre es m x
hdl :: e -> Fre es m a)) =
    Fre es m x
action forall a b. a -> (a -> b) -> b
& forall (fr :: Instruction -> Instruction -> Instruction)
       (u :: [Instruction] -> Instruction) (e :: Instruction)
       (es :: [Instruction]) (m :: Instruction) a r.
(MonadTransFreer fr, Union u, Member u e es, Monad m) =>
(a -> FreerEffects fr u es m r)
-> (forall x.
    (x -> FreerEffects fr u es m r) -> e x -> FreerEffects fr u es m r)
-> FreerEffects fr u es m a
-> FreerEffects fr u es m r
interposeK forall (f :: Instruction) a. Applicative f => a -> f a
pure \x -> Fre es m x
_ (Throw (e
e :: e)) -> e -> Fre es m x
hdl e
e

-- | Interpret the 'Throw' effect using the 'ExceptT' monad transformer.
interpretThrowT :: Monad m => Fre (ThrowI e ': es) m ~> ExceptT e (Fre es m)
interpretThrowT :: forall (m :: Instruction) e (es :: [Instruction]).
Monad m =>
Fre (ThrowI e : es) m ~> ExceptT e (Fre es m)
interpretThrowT = forall (t :: Instruction -> Instruction)
       (fr :: Instruction -> Instruction -> Instruction)
       (u :: [Instruction] -> Instruction) (e :: Instruction)
       (es :: [Instruction]) (f :: Instruction).
(MonadTransFreer fr, Union u, MonadTrans t, Monad f,
 Monad (t (FreerEffects fr u es f))) =>
(e ~> t (FreerEffects fr u es f))
-> FreerEffects fr u (e : es) f ~> t (FreerEffects fr u es f)
interpretT \(Throw e
e) -> forall (m :: Instruction) e a. Monad m => e -> ExceptT e m a
throwE e
e
{-# INLINE interpretThrowT #-}

{- |
Interpret the 'Throw' effect using the t'Control.Monad.Trans.Cont.ContT' continuation monad
transformer.
-}
interpretThrowK :: Monad m => Fre (ThrowI e ': es) m a -> Fre es m (Either e a)
interpretThrowK :: forall (m :: Instruction) e (es :: [Instruction]) a.
Monad m =>
Fre (ThrowI e : es) m a -> Fre es m (Either e a)
interpretThrowK = forall (fr :: Instruction -> Instruction -> Instruction)
       (u :: [Instruction] -> Instruction) (f :: Instruction) a
       (es :: [Instruction]) r (e :: Instruction).
(MonadTransFreer fr, Union u, Monad f) =>
(a -> FreerEffects fr u es f r)
-> (forall x.
    (x -> FreerEffects fr u es f r) -> e x -> FreerEffects fr u es f r)
-> FreerEffects fr u (e : es) f a
-> FreerEffects fr u es f r
interpretK (forall (f :: Instruction) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right) \x -> FreerEffects FreerChurchT ExtensibleUnion es m (Either e a)
_ (Throw e
e) -> forall (f :: Instruction) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left e
e