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

module Control.Effect.Interpreter.Heftia.ShiftReset where

import Control.Arrow ((>>>))
import Control.Effect (type (~>))
import Control.Effect.Hefty (
    Eff,
    injectH,
    interpretKAllH,
    interpretKH,
    interpretRecH,
    raiseH,
    runEff,
 )
import Control.Freer (Freer)
import Control.Monad ((<=<))
import Control.Monad.Freer (MonadFreer)
import Data.Effect (LiftIns)
import Data.Effect.HFunctor (HFunctor, hfmap)
import Data.Effect.Key (KeyH (KeyH))
import Data.Effect.ShiftReset (Reset (Reset), Shift, Shift' (Shift), Shift_ (Shift_))
import Data.Hefty.Union (HFunctorUnion, HFunctorUnion_ (ForallHFunctor), Union ((|+:)))

evalShift ::
    (MonadFreer c fr, Union u, c (Eff u fr '[] ef), HFunctor (u '[])) =>
    Eff u fr '[Shift r] ef r ->
    Eff u fr '[] ef r
evalShift :: forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (ef :: [(* -> *) -> * -> *]) r.
(MonadFreer c fr, Union u, c (Eff u fr '[] ef),
 HFunctor (u '[])) =>
Eff u fr '[Shift r] ef r -> Eff u fr '[] ef r
evalShift = forall r a (ef :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr '[] ef),
 HFunctor (u '[])) =>
(a -> Eff u fr '[] ef r)
-> Eff u fr '[Shift r] ef a -> Eff u fr '[] ef r
runShift forall (f :: * -> *) a. Applicative f => a -> f a
pure
{-# INLINE evalShift #-}

runShift ::
    forall r a ef fr u c.
    (MonadFreer c fr, Union u, c (Eff u fr '[] ef), HFunctor (u '[])) =>
    (a -> Eff u fr '[] ef r) ->
    Eff u fr '[Shift r] ef a ->
    Eff u fr '[] ef r
runShift :: forall r a (ef :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr '[] ef),
 HFunctor (u '[])) =>
(a -> Eff u fr '[] ef r)
-> Eff u fr '[Shift r] ef a -> Eff u fr '[] ef r
runShift a -> Eff u fr '[] ef r
f =
    forall (e :: (* -> *) -> * -> *) r (ehs :: [(* -> *) -> * -> *])
       (efs :: [(* -> *) -> * -> *]) a (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr ehs efs)) =>
(a -> Eff u fr ehs efs r)
-> (forall x.
    (x -> Eff u fr ehs efs r)
    -> e (Eff u fr '[e] efs) x -> Eff u fr ehs efs r)
-> Eff u fr '[e] efs a
-> Eff u fr ehs efs r
interpretKH a -> Eff u fr '[] ef r
f \x -> Eff u fr '[] ef r
k ->
        let k' :: x -> Eff u fr '[Shift r] ef r
k' = forall (e :: (* -> *) -> * -> *) (r :: [(* -> *) -> * -> *])
       (efs :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u r)) =>
Eff u fr r efs ~> Eff u fr (e : r) efs
raiseH forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Eff u fr '[] ef r
k
         in forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (ef :: [(* -> *) -> * -> *]) r.
(MonadFreer c fr, Union u, c (Eff u fr '[] ef),
 HFunctor (u '[])) =>
Eff u fr '[Shift r] ef r -> Eff u fr '[] ef r
evalShift forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
                KeyH (Shift (x -> Eff u fr '[Shift r] ef r) -> Eff u fr '[Shift r] ef r
g) -> (x -> Eff u fr '[Shift r] ef r) -> Eff u fr '[Shift r] ef r
g x -> Eff u fr '[Shift r] ef r
k'

withShift ::
    ( MonadFreer c fr
    , Union u
    , c (Eff u fr '[] '[LiftIns (Eff u fr eh ef)])
    , c (Eff u fr eh ef)
    , HFunctor (u '[])
    ) =>
    Eff u fr '[Shift r] '[LiftIns (Eff u fr eh ef)] r ->
    Eff u fr eh ef r
withShift :: forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (eh :: [(* -> *) -> * -> *]) (ef :: [(* -> *) -> * -> *]) r.
(MonadFreer c fr, Union u,
 c (Eff u fr '[] '[LiftIns (Eff u fr eh ef)]), c (Eff u fr eh ef),
 HFunctor (u '[])) =>
Eff u fr '[Shift r] '[LiftIns (Eff u fr eh ef)] r
-> Eff u fr eh ef r
withShift = forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (ef :: [(* -> *) -> * -> *]) r.
(MonadFreer c fr, Union u, c (Eff u fr '[] ef),
 HFunctor (u '[])) =>
Eff u fr '[Shift r] ef r -> Eff u fr '[] ef r
evalShift forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (f :: * -> *) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c f) =>
Eff u fr '[] '[LiftIns f] ~> f
runEff
{-# INLINE withShift #-}

runShift_ ::
    (MonadFreer c fr, Union u, c (Eff u fr eh ef), HFunctor (u eh)) =>
    Eff u fr (Shift_ ': eh) ef ~> Eff u fr eh ef
runShift_ :: forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (eh :: [(* -> *) -> * -> *]) (ef :: [(* -> *) -> * -> *]).
(MonadFreer c fr, Union u, c (Eff u fr eh ef), HFunctor (u eh)) =>
Eff u fr (Shift_ : eh) ef ~> Eff u fr eh ef
runShift_ =
    forall (ehs' :: [(* -> *) -> * -> *]) r a
       (ehs :: [(* -> *) -> * -> *]) (efs :: [(* -> *) -> * -> *])
       (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, c (Eff u fr ehs' efs)) =>
(a -> Eff u fr ehs' efs r)
-> (forall x.
    (x -> Eff u fr ehs' efs r)
    -> u ehs (Eff u fr ehs efs) x -> Eff u fr ehs' efs r)
-> Eff u fr ehs efs a
-> Eff u fr ehs' efs r
interpretKAllH forall (f :: * -> *) a. Applicative f => a -> f a
pure \x -> Eff u fr eh ef x
k ->
        (\(Shift_ forall r.
(x -> Eff u fr (Shift_ : eh) ef r) -> Eff u fr (Shift_ : eh) ef r
f) -> forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (eh :: [(* -> *) -> * -> *]) (ef :: [(* -> *) -> * -> *]).
(MonadFreer c fr, Union u, c (Eff u fr eh ef), HFunctor (u eh)) =>
Eff u fr (Shift_ : eh) ef ~> Eff u fr eh ef
runShift_ forall a b. (a -> b) -> a -> b
$ forall r.
(x -> Eff u fr (Shift_ : eh) ef r) -> Eff u fr (Shift_ : eh) ef r
f forall a b. (a -> b) -> a -> b
$ forall (e :: (* -> *) -> * -> *) (r :: [(* -> *) -> * -> *])
       (efs :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor (u r)) =>
Eff u fr r efs ~> Eff u fr (e : r) efs
raiseH forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Eff u fr eh ef x
k)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: (x -> Eff u fr eh ef x
k forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (c :: (* -> *) -> Constraint) (f :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (ehs :: [(* -> *) -> * -> *]) (efs :: [(* -> *) -> * -> *]).
(Freer c f, HFunctor (u ehs)) =>
u ehs (Eff u f ehs efs) ~> Eff u f ehs efs
injectH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (eh :: [(* -> *) -> * -> *]) (ef :: [(* -> *) -> * -> *]).
(MonadFreer c fr, Union u, c (Eff u fr eh ef), HFunctor (u eh)) =>
Eff u fr (Shift_ : eh) ef ~> Eff u fr eh ef
runShift_)

runReset ::
    (Freer c fr, HFunctorUnion u, ForallHFunctor u eh) =>
    Eff u fr (Reset ': eh) ef ~> Eff u fr eh ef
runReset :: forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (eh :: [(* -> *) -> * -> *]) (ef :: [(* -> *) -> * -> *]).
(Freer c fr, HFunctorUnion u, ForallHFunctor u eh) =>
Eff u fr (Reset : eh) ef ~> Eff u fr eh ef
runReset = 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 \(Reset Eff u fr eh ef x
a) -> Eff u fr eh ef x
a
{-# INLINE runReset #-}