-- 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.Fresh where

import Control.Arrow ((>>>))
import Control.Effect (type (~>))
import Control.Effect.Hefty (Eff, interpret, raiseUnder)
import Control.Effect.Interpreter.Heftia.State (runState)
import Control.Freer (Freer)
import Control.Monad.State (StateT)
import Data.Effect.Fresh (Fresh (Fresh), LFresh)
import Data.Effect.HFunctor (HFunctor)
import Data.Effect.State (LState, State, get, modify)
import Data.Hefty.Union (Member, Union)
import Numeric.Natural (Natural)

runFreshNatural ::
    ( Freer c fr
    , Union u
    , HFunctor (u '[])
    , Member u (State Natural) (LState Natural ': r)
    , c (Eff u fr '[] r)
    , c (StateT Natural (Eff u fr '[] r))
    , Monad (Eff u fr '[] r)
    , Monad (Eff u fr '[] (LState Natural ': r))
    ) =>
    Eff u fr '[] (LFresh Natural ': r) a ->
    Eff u fr '[] r (Natural, a)
runFreshNatural :: forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (r :: [(* -> *) -> * -> *]) a.
(Freer c fr, Union u, HFunctor (u '[]),
 Member u (State Natural) (LState Natural : r), c (Eff u fr '[] r),
 c (StateT Natural (Eff u fr '[] r)), Monad (Eff u fr '[] r),
 Monad (Eff u fr '[] (LState Natural : r))) =>
Eff u fr '[] (LFresh Natural : r) a -> Eff u fr '[] r (Natural, a)
runFreshNatural =
    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 (r :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, Member u (State Natural) r,
 Monad (Eff u fr '[] r), HFunctor (u '[])) =>
Eff u fr '[] (LFresh Natural : r) ~> Eff u fr '[] r
runFreshNaturalAsState
        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 Natural
0
{-# INLINE runFreshNatural #-}

runFreshNaturalAsState ::
    forall r fr u c.
    ( Freer c fr
    , Union u
    , Member u (State Natural) r
    , Monad (Eff u fr '[] r)
    , HFunctor (u '[])
    ) =>
    Eff u fr '[] (LFresh Natural ': r) ~> Eff u fr '[] r
runFreshNaturalAsState :: forall (r :: [(* -> *) -> * -> *]) (fr :: (* -> *) -> * -> *)
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, Member u (State Natural) r,
 Monad (Eff u fr '[] r), HFunctor (u '[])) =>
Eff u fr '[] (LFresh Natural : r) ~> Eff u fr '[] r
runFreshNaturalAsState =
    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 \Fresh Natural x
UnliftIfSingle (LFresh Natural) x
Fresh -> forall s (f :: * -> *). SendIns (State s) f => f s
get @Natural forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall s (m :: * -> *). (State s <: m, Monad m) => (s -> s) -> m ()
modify @Natural (forall a. Num a => a -> a -> a
+ Natural
1)