-- 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'Data.Effect.Except.Throw' / t'Data.Effect.Except.Catch' effect
classes.
-}
module Control.Effect.Interpreter.Heftia.Except where

import Control.Arrow ((>>>))
import Control.Effect (type (~>))
import Control.Effect.Hefty (
    Eff,
    Elab,
    interposeK,
    interposeT,
    interpretK,
    interpretRec,
    interpretRecH,
    interpretT,
 )
import Control.Exception (Exception)
import Control.Monad.Freer (MonadFreer)
import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)
import Data.Effect.Except (Catch (Catch), LThrow, Throw (Throw))
import Data.Effect.HFunctor (HFunctor)
import Data.Effect.Unlift (UnliftIO)
import Data.Function ((&))
import Data.Hefty.Extensible (ForallHFunctor, type (<<|), type (<|))
import Data.Hefty.Extensible qualified as Ex
import Data.Hefty.Union (Member, Union)
import UnliftIO (throwIO)
import UnliftIO qualified as IO

-- | Interpret the "Data.Effect.Except" effects using the 'ExceptT' monad transformer internally.
runExcept ::
    forall e a ef fr u c.
    ( Member u (Throw e) (LThrow e ': ef)
    , MonadFreer c fr
    , Union u
    , c (Eff u fr '[] (LThrow e ': ef))
    , c (ExceptT e (Eff u fr '[] (LThrow e ': ef)))
    , HFunctor (u '[Catch e])
    , c (Eff u fr '[] ef)
    , c (ExceptT e (Eff u fr '[] ef))
    , HFunctor (u '[])
    ) =>
    Eff u fr '[Catch e] (LThrow e ': ef) a ->
    Eff u fr '[] ef (Either e a)
runExcept :: forall e a (ef :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Member u (Throw e) (LThrow e : ef), MonadFreer c fr, Union u,
 c (Eff u fr '[] (LThrow e : ef)),
 c (ExceptT e (Eff u fr '[] (LThrow e : ef))),
 HFunctor (u '[Catch e]), c (Eff u fr '[] ef),
 c (ExceptT e (Eff u fr '[] ef)), HFunctor (u '[])) =>
Eff u fr '[Catch e] (LThrow e : ef) a
-> Eff u fr '[] ef (Either e a)
runExcept = forall e (ef :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Member u (Throw e) ef, MonadFreer c fr, Union u,
 c (Eff u fr '[] ef), c (ExceptT e (Eff u fr '[] ef)),
 HFunctor (u '[Catch e]), HFunctor (u '[])) =>
Eff u fr '[Catch e] ef ~> Eff u fr '[] ef
runCatch forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall e (r :: [(* -> *) -> * -> *]) a (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr '[] r),
 c (ExceptT e (Eff u fr '[] r))) =>
Eff u fr '[] (LThrow e : r) a -> Eff u fr '[] r (Either e a)
runThrow
{-# INLINE runExcept #-}

-- | Elaborate the t'Catch' effect using the 'ExceptT' monad transformer internally.
runCatch ::
    forall e ef fr u c.
    ( Member u (Throw e) ef
    , MonadFreer c fr
    , Union u
    , c (Eff u fr '[] ef)
    , c (ExceptT e (Eff u fr '[] ef))
    , HFunctor (u '[Catch e])
    , HFunctor (u '[])
    ) =>
    Eff u fr '[Catch e] ef ~> Eff u fr '[] ef
runCatch :: forall e (ef :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Member u (Throw e) ef, MonadFreer c fr, Union u,
 c (Eff u fr '[] ef), c (ExceptT e (Eff u fr '[] ef)),
 HFunctor (u '[Catch e]), HFunctor (u '[])) =>
Eff u fr '[Catch e] ef ~> Eff u fr '[] ef
runCatch = forall (e :: (* -> *) -> * -> *) (rs :: [(* -> *) -> * -> *])
       (efs :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor e, HFunctor (u rs),
 HFunctor (u (e : rs))) =>
(e (Eff u fr rs efs) ~> Eff u fr rs efs)
-> Eff u fr (e : rs) efs ~> Eff u fr rs efs
interpretRecH forall e (ef :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Member u (Throw e) ef, MonadFreer c fr, Union u,
 c (Eff u fr '[] ef), c (ExceptT e (Eff u fr '[] ef))) =>
Elab (Catch e) (Eff u fr '[] ef)
elabCatch
{-# INLINE runCatch #-}

elabCatch ::
    forall e ef fr u c.
    ( Member u (Throw e) ef
    , MonadFreer c fr
    , Union u
    , c (Eff u fr '[] ef)
    , c (ExceptT e (Eff u fr '[] ef))
    ) =>
    Elab (Catch e) (Eff u fr '[] ef)
elabCatch :: forall e (ef :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Member u (Throw e) ef, MonadFreer c fr, Union u,
 c (Eff u fr '[] ef), c (ExceptT e (Eff u fr '[] ef))) =>
Elab (Catch e) (Eff u fr '[] ef)
elabCatch (Catch Eff u fr '[] ef x
action e -> Eff u fr '[] ef x
hdl) = do
    Either e x
r <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ Eff u fr '[] ef x
action forall a b. a -> (a -> b) -> b
& forall (e :: * -> *) (t :: (* -> *) -> * -> *)
       (efs :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, MonadTrans t, Member u e efs,
 Monad (Eff u fr '[] efs), c (t (Eff u fr '[] efs))) =>
(e ~> t (Eff u fr '[] efs))
-> Eff u fr '[] efs ~> t (Eff u fr '[] efs)
interposeT \(Throw e
e) -> forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE e
e
    case Either e x
r of
        Left e
e -> e -> Eff u fr '[] ef x
hdl e
e
        Right x
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure x
a

-- | Elaborate the 'Catch' effect using a delimited continuation.
elabCatchK ::
    forall e ef fr u c.
    (Member u (Throw e) ef, MonadFreer c fr, Union u, c (Eff u fr '[] ef)) =>
    Elab (Catch e) (Eff u fr '[] ef)
elabCatchK :: forall e (ef :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Member u (Throw e) ef, MonadFreer c fr, Union u,
 c (Eff u fr '[] ef)) =>
Elab (Catch e) (Eff u fr '[] ef)
elabCatchK (Catch Eff u fr '[] ef x
action e -> Eff u fr '[] ef x
hdl) =
    Eff u fr '[] ef x
action forall a b. a -> (a -> b) -> b
& forall (e :: * -> *) (efs :: [(* -> *) -> * -> *]) r a
       (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, Member u e efs, c (Eff u fr '[] efs)) =>
(a -> Eff u fr '[] efs r)
-> (forall x.
    (x -> Eff u fr '[] efs r) -> e x -> Eff u fr '[] efs r)
-> Eff u fr '[] efs a
-> Eff u fr '[] efs r
interposeK forall (f :: * -> *) a. Applicative f => a -> f a
pure \x -> Eff u fr '[] ef x
_ (Throw e
e) -> e -> Eff u fr '[] ef x
hdl e
e

-- | Interpret the 'Throw' effect using the 'ExceptT' monad transformer.
runThrow ::
    forall e r a fr u c.
    (MonadFreer c fr, Union u, c (Eff u fr '[] r), c (ExceptT e (Eff u fr '[] r))) =>
    Eff u fr '[] (LThrow e ': r) a ->
    Eff u fr '[] r (Either e a)
runThrow :: forall e (r :: [(* -> *) -> * -> *]) a (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr '[] r),
 c (ExceptT e (Eff u fr '[] r))) =>
Eff u fr '[] (LThrow e : r) a -> Eff u fr '[] r (Either e a)
runThrow = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (r :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr '[] r),
 c (ExceptT e (Eff u fr '[] r))) =>
Eff u fr '[] (LThrow e : r) ~> ExceptT e (Eff u fr '[] r)
runThrowT
{-# INLINE runThrow #-}

-- | Interpret the 'Throw' effect using the 'ExceptT' monad transformer.
runThrowT ::
    forall e r fr u c.
    (MonadFreer c fr, Union u, c (Eff u fr '[] r), c (ExceptT e (Eff u fr '[] r))) =>
    Eff u fr '[] (LThrow e ': r) ~> ExceptT e (Eff u fr '[] r)
runThrowT :: forall e (r :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr '[] r),
 c (ExceptT e (Eff u fr '[] r))) =>
Eff u fr '[] (LThrow e : r) ~> ExceptT e (Eff u fr '[] r)
runThrowT = forall (e :: (* -> *) -> * -> *) (r :: [(* -> *) -> * -> *])
       (t :: (* -> *) -> * -> *) (ehs :: [(* -> *) -> * -> *])
       (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, MonadTrans t, HeadIns e,
 Monad (Eff u fr ehs r), c (t (Eff u fr ehs r))) =>
(UnliftIfSingle e ~> t (Eff u fr ehs r))
-> Eff u fr '[] (e : r) ~> t (Eff u fr ehs r)
interpretT \(Throw e
e) -> forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE e
e
{-# INLINE runThrowT #-}

-- | Interpret the 'Throw' effect using a delimited continuation.
runThrowK ::
    forall e r a fr u c.
    (MonadFreer c fr, Union u, c (Eff u fr '[] r)) =>
    Eff u fr '[] (LThrow e ': r) a ->
    Eff u fr '[] r (Either e a)
runThrowK :: forall e (r :: [(* -> *) -> * -> *]) a (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr '[] r)) =>
Eff u fr '[] (LThrow e : r) a -> Eff u fr '[] r (Either e a)
runThrowK = forall (e :: (* -> *) -> * -> *) (rs :: [(* -> *) -> * -> *]) r a
       (ehs :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) =>
(a -> Eff u fr ehs rs r)
-> (forall x.
    (x -> Eff u fr ehs rs r)
    -> UnliftIfSingle e x -> Eff u fr ehs rs r)
-> Eff u fr '[] (e : rs) a
-> Eff u fr ehs rs r
interpretK (forall (f :: * -> *) 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 -> Eff u fr '[] r (Either e a)
_ (Throw e
e) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left e
e

runThrowIO ::
    forall e eh ef fr c.
    (MonadFreer c fr, IO <| ef, ForallHFunctor eh, Exception e) =>
    Ex.Eff fr eh (LThrow e ': ef) ~> Ex.Eff fr eh ef
runThrowIO :: forall e (eh :: [(* -> *) -> * -> *]) (ef :: [(* -> *) -> * -> *])
       (fr :: (* -> *) -> * -> *) (c :: (* -> *) -> Constraint).
(MonadFreer c fr, IO <| ef, ForallHFunctor eh, Exception e) =>
Eff fr eh (LThrow e : ef) ~> Eff fr eh ef
runThrowIO = forall (e :: (* -> *) -> * -> *) (rs :: [(* -> *) -> * -> *])
       (ehs :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs), HeadIns e) =>
(UnliftIfSingle e ~> Eff u fr ehs rs)
-> Eff u fr ehs (e : rs) ~> Eff u fr ehs rs
interpretRec \(Throw e
e) -> forall (m :: * -> *) e a. (MonadIO m, Exception e) => e -> m a
throwIO e
e
{-# INLINE runThrowIO #-}

runCatchIO ::
    forall e eh ef fr c.
    (MonadFreer c fr, UnliftIO <<| eh, IO <| ef, ForallHFunctor eh, Exception e) =>
    Ex.Eff fr (Catch e ': eh) ef ~> Ex.Eff fr eh ef
runCatchIO :: forall e (eh :: [(* -> *) -> * -> *]) (ef :: [(* -> *) -> * -> *])
       (fr :: (* -> *) -> * -> *) (c :: (* -> *) -> Constraint).
(MonadFreer c fr, UnliftIO <<| eh, IO <| ef, ForallHFunctor eh,
 Exception e) =>
Eff fr (Catch e : eh) ef ~> Eff fr eh ef
runCatchIO = forall (e :: (* -> *) -> * -> *) (rs :: [(* -> *) -> * -> *])
       (efs :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor e, HFunctor (u rs),
 HFunctor (u (e : rs))) =>
(e (Eff u fr rs efs) ~> Eff u fr rs efs)
-> Eff u fr (e : rs) efs ~> Eff u fr rs efs
interpretRecH \(Catch Eff ExtensibleUnion fr eh ef x
action e -> Eff ExtensibleUnion fr eh ef x
hdl) -> forall (m :: * -> *) e a.
(MonadUnliftIO m, Exception e) =>
m a -> (e -> m a) -> m a
IO.catch Eff ExtensibleUnion fr eh ef x
action e -> Eff ExtensibleUnion fr eh ef x
hdl
{-# INLINE runCatchIO #-}