-- SPDX-License-Identifier: MPL-2.0

{- |
Copyright   :  (c) 2024-2025 Sayo contributors
License     :  MPL-2.0 (see the LICENSE file)
Maintainer  :  ymdfield@outlook.jp
-}
module Control.Monad.Hefty.Fresh (
    module Control.Monad.Hefty.Fresh,
    module Data.Effect.Fresh,
) where

import Control.Arrow ((>>>))
import Control.Monad.Hefty (Eff, FOEs, interpret, raiseUnder, (:>))
import Control.Monad.Hefty.State (runState)
import Data.Effect.Fresh
import Data.Effect.State (State, get, modify)
import Numeric.Natural (Natural)

runFreshNatural :: (FOEs es) => Eff (Fresh Natural ': es) a -> Eff es (Natural, a)
runFreshNatural :: forall (es :: [Effect]) a.
FOEs es =>
Eff (Fresh Natural : es) a -> Eff es (Natural, a)
runFreshNatural =
    Eff (Fresh Natural : es) a
-> Eff Freer (Fresh Natural : State Natural : es) a
forall (e0 :: Effect) (e1 :: Effect) (es :: [Effect]) a
       (ff :: Effect) (c :: (* -> *) -> Constraint).
Free c ff =>
Eff ff (e0 : es) a -> Eff ff (e0 : e1 : es) a
raiseUnder (Eff (Fresh Natural : es) a
 -> Eff Freer (Fresh Natural : State Natural : es) a)
-> (Eff Freer (Fresh Natural : State Natural : es) a
    -> Eff es (Natural, a))
-> Eff (Fresh Natural : es) a
-> Eff es (Natural, a)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Eff Freer (Fresh Natural : State Natural : es) a
-> Eff (State Natural : es) a
forall (es :: [Effect]) a.
(State Natural :> es) =>
Eff (Fresh Natural : es) a -> Eff es a
runFreshNaturalAsState (Eff Freer (Fresh Natural : State Natural : es) a
 -> Eff (State Natural : es) a)
-> (Eff (State Natural : es) a -> Eff es (Natural, a))
-> Eff Freer (Fresh Natural : State Natural : es) a
-> Eff es (Natural, a)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Natural -> Eff (State Natural : es) a -> Eff es (Natural, a)
forall s (es :: [Effect]) a.
FOEs es =>
s -> Eff (State s : es) a -> Eff es (s, a)
runState Natural
0
{-# INLINE runFreshNatural #-}

runFreshNaturalAsState
    :: (State Natural :> es)
    => Eff (Fresh Natural ': es) a
    -> Eff es a
runFreshNaturalAsState :: forall (es :: [Effect]) a.
(State Natural :> es) =>
Eff (Fresh Natural : es) a -> Eff es a
runFreshNaturalAsState =
    (Fresh Natural ~~> Eff Freer es)
-> Eff Freer (Fresh Natural : es) a -> Eff Freer es a
forall (e :: Effect) (es :: [Effect]) (ff :: Effect) a
       (c :: (* -> *) -> Constraint).
(KnownOrder e, Free c ff) =>
(e ~~> Eff ff es) -> Eff ff (e : es) a -> Eff ff es a
interpret \Fresh Natural (Eff Freer es) x
Fresh -> Eff Freer es x
forall s (a :: * -> *) (es :: [Effect]) (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(Free c ff, a ~ Eff ff es, State s :> es) =>
a s
get Eff Freer es x -> Eff Freer es () -> Eff Freer es x
forall a b. Eff Freer es a -> Eff Freer es b -> Eff Freer es a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* (Natural -> Natural) -> Eff Freer es ()
forall s (es :: [Effect]) (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(State s :> es, Monad (Eff ff es), Free c ff) =>
(s -> s) -> Eff ff es ()
modify (Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1)
{-# INLINE runFreshNaturalAsState #-}