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

import Control.Arrow ((>>>))
import Control.Effect (type (~>))
import Control.Effect.Hefty (Eff, interpret, interpretRec, raiseUnder)
import Control.Effect.Interpreter.Heftia.State (evalState)
import Control.Freer (Freer)
import Control.Monad.State (StateT)
import Data.Effect.HFunctor (HFunctor)
import Data.Effect.Input (Input (Input), LInput)
import Data.Effect.State (LState, State, gets, put)
import Data.Hefty.Union (Member, Union)
import Data.List (uncons)

runInputEff ::
    forall i r eh fr u c.
    (Freer c fr, Union u, Applicative (Eff u fr eh r), HFunctor (u eh)) =>
    Eff u fr eh r i ->
    Eff u fr eh (LInput i ': r) ~> Eff u fr eh r
runInputEff :: forall i (r :: [SigClass]) (eh :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, Applicative (Eff u fr eh r),
 HFunctor (u eh)) =>
Eff u fr eh r i -> Eff u fr eh (LInput i : r) ~> Eff u fr eh r
runInputEff Eff u fr eh r i
a = forall (e :: SigClass) (rs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (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 \Input i x
UnliftIfSingle (LInput i) x
Input -> Eff u fr eh r i
a
{-# INLINE runInputEff #-}

runInputConst ::
    forall i r eh fr u c.
    (Freer c fr, Union u, Applicative (Eff u fr eh r), HFunctor (u eh)) =>
    i ->
    Eff u fr eh (LInput i ': r) ~> Eff u fr eh r
runInputConst :: forall i (r :: [SigClass]) (eh :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, Applicative (Eff u fr eh r),
 HFunctor (u eh)) =>
i -> Eff u fr eh (LInput i : r) ~> Eff u fr eh r
runInputConst i
i = forall (e :: SigClass) (rs :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (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 \Input i x
UnliftIfSingle (LInput i) x
Input -> forall (f :: * -> *) a. Applicative f => a -> f a
pure i
i
{-# INLINE runInputConst #-}

runInputList ::
    forall i r fr u c.
    ( Freer c fr
    , Union u
    , Applicative (Eff u fr '[] r)
    , Monad (Eff u fr '[] (LState [i] ': r))
    , c (Eff u fr '[] r)
    , c (StateT [i] (Eff u fr '[] r))
    , Member u (State [i]) (LState [i] ': r)
    , HFunctor (u '[])
    ) =>
    [i] ->
    Eff u fr '[] (LInput (Maybe i) ': r) ~> Eff u fr '[] r
runInputList :: forall i (r :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, Applicative (Eff u fr '[] r),
 Monad (Eff u fr '[] (LState [i] : r)), c (Eff u fr '[] r),
 c (StateT [i] (Eff u fr '[] r)),
 Member u (State [i]) (LState [i] : r), HFunctor (u '[])) =>
[i] -> Eff u fr '[] (LInput (Maybe i) : r) ~> Eff u fr '[] r
runInputList [i]
is =
    forall (e1 :: SigClass) (e2 :: SigClass) (r :: [SigClass])
       (ehs :: [SigClass]) (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (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 :: SigClass) (r :: [SigClass]) (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (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 \Input (Maybe i) x
UnliftIfSingle (LInput (Maybe i)) x
Input -> do
                Maybe (i, [i])
is' <- forall s (f :: * -> *) a.
(State s <: f, Functor f) =>
(s -> a) -> f a
gets @[i] forall a. [a] -> Maybe (a, [a])
uncons
                forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall s (f :: * -> *). SendIns (State s) f => s -> f ()
put forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Maybe (i, [i])
is'
                forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (i, [i])
is'
            )
        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 :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (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) ~> Eff u fr '[] r
evalState [i]
is