-- 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 Sayo Koyoneda
License     :  MPL-2.0 (see the LICENSE file)
Maintainer  :  ymdfield@outlook.jp
Portability :  portable
-}
module Control.Monad.Hefty.Fresh where

import Control.Arrow ((>>>))
import Control.Monad.Hefty (Eff, interpret, raiseUnder, type (<|), type (~>))
import Control.Monad.Hefty.State (runState)
import Data.Effect.Fresh (Fresh (Fresh))
import Data.Effect.State (State, get, modify)
import Numeric.Natural (Natural)

runFreshNatural :: Eff '[] (Fresh Natural ': r) a -> Eff '[] r (Natural, a)
runFreshNatural :: forall (r :: [* -> *]) a.
Eff '[] (Fresh Natural : r) a -> Eff '[] r (Natural, a)
runFreshNatural =
    Eff '[] (Fresh Natural : r) a
-> Eff '[] (Fresh Natural : State Natural : r) a
forall (e1 :: * -> *) (e2 :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]) x.
Eff eh (e1 : ef) x -> Eff eh (e1 : e2 : ef) x
raiseUnder (Eff '[] (Fresh Natural : r) a
 -> Eff '[] (Fresh Natural : State Natural : r) a)
-> (Eff '[] (Fresh Natural : State Natural : r) a
    -> Eff '[] r (Natural, a))
-> Eff '[] (Fresh Natural : r) a
-> Eff '[] r (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 '[] (Fresh Natural : State Natural : r) a
-> Eff '[] (State Natural : r) a
forall (r :: [* -> *]) (eh :: [EffectH]).
(State Natural <| r) =>
Eff eh (Fresh Natural : r) ~> Eff eh r
Eff '[] (Fresh Natural : State Natural : r)
~> Eff '[] (State Natural : r)
runFreshNaturalAsState (Eff '[] (Fresh Natural : State Natural : r) a
 -> Eff '[] (State Natural : r) a)
-> (Eff '[] (State Natural : r) a -> Eff '[] r (Natural, a))
-> Eff '[] (Fresh Natural : State Natural : r) a
-> Eff '[] r (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 : r) a -> Eff '[] r (Natural, a)
forall s (ef :: [* -> *]) a.
s -> Eff '[] (State s : ef) a -> Eff '[] ef (s, a)
runState Natural
0

runFreshNaturalAsState
    :: (State Natural <| r)
    => Eff eh (Fresh Natural ': r) ~> Eff eh r
runFreshNaturalAsState :: forall (r :: [* -> *]) (eh :: [EffectH]).
(State Natural <| r) =>
Eff eh (Fresh Natural : r) ~> Eff eh r
runFreshNaturalAsState =
    (Fresh Natural ~> Eff eh r)
-> Eff eh (Fresh Natural : r) ~> Eff eh r
forall (e :: * -> *) (ef :: [* -> *]) (eh :: [EffectH]).
(e ~> Eff eh ef) -> Eff eh (e : ef) ~> Eff eh ef
interpret \Fresh Natural x
Fresh -> forall s (f :: * -> *). SendFOE (State s) f => f s
get @Natural Eff eh r x -> Eff eh r () -> Eff eh r x
forall a b. Eff eh r a -> Eff eh r b -> Eff eh r a
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 (Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1)