-- 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) 2024 Yamada Ryo
License     :  MPL-2.0 (see the file LICENSE)
Maintainer  :  ymdfield@outlook.jp
Stability   :  experimental
Portability :  portable
-}
module Control.Effect.Interpreter.Heftia.Output where

import Control.Arrow ((>>>))
import Control.Effect (type (~>))
import Control.Effect.Hefty (Eff, interpret, interpretRec, raiseUnder, send0)
import Control.Effect.Interpreter.Heftia.State (runState)
import Control.Effect.Interpreter.Heftia.Writer (runTell, runTellA)
import Control.Freer (Freer)
import Control.Monad.Trans.State (StateT)
import Control.Monad.Trans.Writer.CPS qualified as CPS
import Control.Monad.Trans.Writer.Strict qualified as Strict
import Data.Effect.HFunctor (HFunctor)
import Data.Effect.Output (LOutput, Output (Output))
import Data.Effect.State (LState, State, modify)
import Data.Effect.Writer (Tell (Tell))
import Data.Hefty.Union (Member, Union)

runOutputEff ::
    (Freer c fr, Union u, HFunctor (u eh)) =>
    (o -> Eff u fr eh r ()) ->
    Eff u fr eh (LOutput o ': r) ~> Eff u fr eh r
runOutputEff :: forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (eh :: [(* -> *) -> * -> *]) o (r :: [(* -> *) -> * -> *]).
(Freer c fr, Union u, HFunctor (u eh)) =>
(o -> Eff u fr eh r ())
-> Eff u fr eh (LOutput o : r) ~> Eff u fr eh r
runOutputEff o -> Eff u fr eh r ()
f = 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 \(Output o
o) -> o -> Eff u fr eh r ()
f o
o
{-# INLINE runOutputEff #-}

ignoreOutput ::
    (Freer c fr, Union u, HFunctor (u eh), Applicative (Eff u fr eh r)) =>
    Eff u fr eh (LOutput o ': r) ~> Eff u fr eh r
ignoreOutput :: forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (eh :: [(* -> *) -> * -> *]) (r :: [(* -> *) -> * -> *]) o.
(Freer c fr, Union u, HFunctor (u eh),
 Applicative (Eff u fr eh r)) =>
Eff u fr eh (LOutput o : r) ~> Eff u fr eh r
ignoreOutput = forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (eh :: [(* -> *) -> * -> *]) o (r :: [(* -> *) -> * -> *]).
(Freer c fr, Union u, HFunctor (u eh)) =>
(o -> Eff u fr eh r ())
-> Eff u fr eh (LOutput o : r) ~> Eff u fr eh r
runOutputEff forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
{-# INLINE ignoreOutput #-}

runOutputList ::
    forall o a r fr u c.
    ( Freer c fr
    , Union u
    , c (Eff u fr '[] r)
    , c (StateT [o] (Eff u fr '[] r))
    , Applicative (Eff u fr '[] r)
    , Monad (Eff u fr '[] (LState [o] ': r))
    , Member u (State [o]) (LState [o] ': r)
    , HFunctor (u '[])
    ) =>
    Eff u fr '[] (LOutput o ': r) a ->
    Eff u fr '[] r ([o], a)
runOutputList :: forall o a (r :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c (Eff u fr '[] r),
 c (StateT [o] (Eff u fr '[] r)), Applicative (Eff u fr '[] r),
 Monad (Eff u fr '[] (LState [o] : r)),
 Member u (State [o]) (LState [o] : r), HFunctor (u '[])) =>
Eff u fr '[] (LOutput o : r) a -> Eff u fr '[] r ([o], a)
runOutputList =
    forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) (ehs :: [(* -> *) -> * -> *])
       (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e2 : r) ~> Eff u fr ehs (e2 : e1 : r)
raiseUnder
        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 :: [(* -> *) -> * -> *])
       (ehs :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HeadIns e) =>
(UnliftIfSingle e ~> Eff u fr ehs r)
-> Eff u fr '[] (e : r) ~> Eff u fr ehs r
interpret (\(Output o
o) -> forall s (m :: * -> *). (State s <: m, Monad m) => (s -> s) -> m ()
modify (o
o :))
        forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall s (r :: [(* -> *) -> * -> *]) a (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c (Eff u fr '[] r),
 c (StateT s (Eff u fr '[] r)), Applicative (Eff u fr '[] r)) =>
s -> Eff u fr '[] (LState s : r) a -> Eff u fr '[] r (s, a)
runState []

{- | Run an `Output` effect by transforming into a monoid.
     The carrier is required to be a monad.
-}
runOutputMonoid ::
    forall o m a r fr u c.
    ( Monoid m
    , Freer c fr
    , Union u
    , Monad (Eff u fr '[] r)
    , c (CPS.WriterT m (Eff u fr '[] r))
    , HFunctor (u '[])
    ) =>
    (o -> m) ->
    Eff u fr '[] (LOutput o ': r) a ->
    Eff u fr '[] r (m, a)
runOutputMonoid :: forall o m a (r :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Monoid m, Freer c fr, Union u, Monad (Eff u fr '[] r),
 c (WriterT m (Eff u fr '[] r)), HFunctor (u '[])) =>
(o -> m) -> Eff u fr '[] (LOutput o : r) a -> Eff u fr '[] r (m, a)
runOutputMonoid o -> m
f =
    forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) (ehs :: [(* -> *) -> * -> *])
       (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e2 : r) ~> Eff u fr ehs (e2 : e1 : r)
raiseUnder
        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 :: [(* -> *) -> * -> *])
       (ehs :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HeadIns e) =>
(UnliftIfSingle e ~> Eff u fr ehs r)
-> Eff u fr '[] (e : r) ~> Eff u fr ehs r
interpret (\(Output o
o) -> forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (eh :: [(* -> *) -> * -> *])
       (r :: [(* -> *) -> * -> *]).
(Freer c fr, Union u, HeadIns e) =>
UnliftIfSingle e ~> Eff u fr eh (e : r)
send0 forall a b. (a -> b) -> a -> b
$ forall w. w -> Tell w ()
Tell forall a b. (a -> b) -> a -> b
$ o -> m
f o
o)
        forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall w (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) a.
(Monoid w, Freer c fr, Union u, Monad (Eff u fr '[] r),
 c (WriterT w (Eff u fr '[] r))) =>
Eff u fr '[] (LTell w : r) a -> Eff u fr '[] r (w, a)
runTell

{- | Strict version of `runOutputMonoid`.
     The constraint on the carrier has been weakened to applicative.
-}
runOutputMonoidA ::
    forall o m a r fr u c.
    ( Monoid m
    , Freer c fr
    , Union u
    , Applicative (Eff u fr '[] r)
    , c (Strict.WriterT m (Eff u fr '[] r))
    , HFunctor (u '[])
    ) =>
    (o -> m) ->
    Eff u fr '[] (LOutput o ': r) a ->
    Eff u fr '[] r (m, a)
runOutputMonoidA :: forall o m a (r :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Monoid m, Freer c fr, Union u, Applicative (Eff u fr '[] r),
 c (WriterT m (Eff u fr '[] r)), HFunctor (u '[])) =>
(o -> m) -> Eff u fr '[] (LOutput o : r) a -> Eff u fr '[] r (m, a)
runOutputMonoidA o -> m
f =
    forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) (ehs :: [(* -> *) -> * -> *])
       (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u ehs)) =>
Eff u fr ehs (e2 : r) ~> Eff u fr ehs (e2 : e1 : r)
raiseUnder
        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 :: [(* -> *) -> * -> *])
       (ehs :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HeadIns e) =>
(UnliftIfSingle e ~> Eff u fr ehs r)
-> Eff u fr '[] (e : r) ~> Eff u fr ehs r
interpret (\(Output o
o) -> forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (eh :: [(* -> *) -> * -> *])
       (r :: [(* -> *) -> * -> *]).
(Freer c fr, Union u, HeadIns e) =>
UnliftIfSingle e ~> Eff u fr eh (e : r)
send0 forall a b. (a -> b) -> a -> b
$ forall w. w -> Tell w ()
Tell forall a b. (a -> b) -> a -> b
$ o -> m
f o
o)
        forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall w (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) a.
(Monoid w, Freer c fr, Union u, Applicative (Eff u fr '[] r),
 c (WriterT w (Eff u fr '[] r))) =>
Eff u fr '[] (LTell w : r) a -> Eff u fr '[] r (w, a)
runTellA