{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE StandaloneDeriving #-}

module FMonad.State.Simple.Outer
  (StateT(..), flift, 
   fromAdjointT, toAdjointT,

   State,
   state, runState, 
  ) where

import Control.Monad.Trans.Identity ( IdentityT(..) )
import Control.Comonad.Trans.Env
import Control.Monad.Trans.Reader
import Data.Tuple (swap)
import Data.Coerce (coerce)

import FMonad
import FMonad.Adjoint

newtype StateT s0 mm x a = StateT { forall s0 (mm :: (* -> *) -> * -> *) (x :: * -> *) a.
StateT s0 mm x a -> s0 -> mm (EnvT s0 x) a
runStateT :: s0 -> mm (EnvT s0 x) a }
   deriving ((forall (g :: * -> *). Functor g => Functor (StateT s0 mm g)) =>
(forall (g :: * -> *) (h :: * -> *) x.
 (Functor g, Functor h) =>
 (g ~> h) -> StateT s0 mm g x -> StateT s0 mm h x)
-> FFunctor (StateT s0 mm)
forall s0 (mm :: (* -> *) -> * -> *) (g :: * -> *).
(FFunctor mm, Functor g) =>
Functor (StateT s0 mm g)
forall s0 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) x.
(FFunctor mm, Functor g, Functor h) =>
(g ~> h) -> StateT s0 mm g x -> StateT s0 mm h x
forall (g :: * -> *). Functor g => Functor (StateT s0 mm g)
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> StateT s0 mm g x -> StateT s0 mm h x
forall (ff :: (* -> *) -> * -> *).
(forall (g :: * -> *). Functor g => Functor (ff g)) =>
(forall (g :: * -> *) (h :: * -> *) x.
 (Functor g, Functor h) =>
 (g ~> h) -> ff g x -> ff h x)
-> FFunctor ff
$cffmap :: forall s0 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) x.
(FFunctor mm, Functor g, Functor h) =>
(g ~> h) -> StateT s0 mm g x -> StateT s0 mm h x
ffmap :: forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> StateT s0 mm g x -> StateT s0 mm h x
FFunctor, FFunctor (StateT s0 mm)
FFunctor (StateT s0 mm) =>
(forall (g :: * -> *). Functor g => g ~> StateT s0 mm g)
-> (forall (g :: * -> *) (h :: * -> *) a.
    (Functor g, Functor h) =>
    (g ~> StateT s0 mm h) -> StateT s0 mm g a -> StateT s0 mm h a)
-> FMonad (StateT s0 mm)
forall s0 (mm :: (* -> *) -> * -> *).
FMonad mm =>
FFunctor (StateT s0 mm)
forall s0 (mm :: (* -> *) -> * -> *) (g :: * -> *).
(FMonad mm, Functor g) =>
g ~> StateT s0 mm g
forall s0 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) a.
(FMonad mm, Functor g, Functor h) =>
(g ~> StateT s0 mm h) -> StateT s0 mm g a -> StateT s0 mm h a
forall (g :: * -> *). Functor g => g ~> StateT s0 mm g
forall (g :: * -> *) (h :: * -> *) a.
(Functor g, Functor h) =>
(g ~> StateT s0 mm h) -> StateT s0 mm g a -> StateT s0 mm h a
forall (ff :: (* -> *) -> * -> *).
FFunctor ff =>
(forall (g :: * -> *). Functor g => g ~> ff g)
-> (forall (g :: * -> *) (h :: * -> *) a.
    (Functor g, Functor h) =>
    (g ~> ff h) -> ff g a -> ff h a)
-> FMonad ff
$cfpure :: forall s0 (mm :: (* -> *) -> * -> *) (g :: * -> *).
(FMonad mm, Functor g) =>
g ~> StateT s0 mm g
fpure :: forall (g :: * -> *). Functor g => g ~> StateT s0 mm g
$cfbind :: forall s0 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) a.
(FMonad mm, Functor g, Functor h) =>
(g ~> StateT s0 mm h) -> StateT s0 mm g a -> StateT s0 mm h a
fbind :: forall (g :: * -> *) (h :: * -> *) a.
(Functor g, Functor h) =>
(g ~> StateT s0 mm h) -> StateT s0 mm g a -> StateT s0 mm h a
FMonad) via (AdjointT (EnvT s0) (ReaderT s0) mm)
type State s0 = StateT s0 IdentityT

deriving
  stock instance (FFunctor mm, Functor x) => Functor (StateT s0 mm x)

fromAdjointT :: AdjointT (EnvT s0) (ReaderT s0) mm x ~> StateT s0 mm x
fromAdjointT :: forall s0 (mm :: (* -> *) -> * -> *) (x :: * -> *) x.
AdjointT (EnvT s0) (ReaderT s0) mm x x -> StateT s0 mm x x
fromAdjointT =  AdjointT (EnvT s0) (ReaderT s0) mm x x -> StateT s0 mm x x
forall a b. Coercible a b => a -> b
coerce

toAdjointT :: StateT s0 mm x ~> AdjointT (EnvT s0) (ReaderT s0) mm x
toAdjointT :: forall s0 (mm :: (* -> *) -> * -> *) (x :: * -> *) x.
StateT s0 mm x x -> AdjointT (EnvT s0) (ReaderT s0) mm x x
toAdjointT = StateT s0 mm x x -> AdjointT (EnvT s0) (ReaderT s0) mm x x
forall a b. Coercible a b => a -> b
coerce

flift :: (FFunctor mm, Functor x)
  => mm x ~> StateT s0 mm x
flift :: forall (mm :: (* -> *) -> * -> *) (x :: * -> *) s0.
(FFunctor mm, Functor x) =>
mm x ~> StateT s0 mm x
flift mm x x
mm = (s0 -> mm (EnvT s0 x) x) -> StateT s0 mm x x
forall s0 (mm :: (* -> *) -> * -> *) (x :: * -> *) a.
(s0 -> mm (EnvT s0 x) a) -> StateT s0 mm x a
StateT ((s0 -> mm (EnvT s0 x) x) -> StateT s0 mm x x)
-> (s0 -> mm (EnvT s0 x) x) -> StateT s0 mm x x
forall a b. (a -> b) -> a -> b
$ \s0
s0 -> (x ~> EnvT s0 x) -> mm x x -> mm (EnvT s0 x) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> mm g x -> mm h x
forall (ff :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap (s0 -> x x -> EnvT s0 x x
forall e (w :: * -> *) a. e -> w a -> EnvT e w a
EnvT s0
s0) mm x x
mm

state :: forall s0 x mm a. (FMonad mm, Functor x) => (s0 -> (x a, s0)) -> StateT s0 mm x a
state :: forall s0 (x :: * -> *) (mm :: (* -> *) -> * -> *) a.
(FMonad mm, Functor x) =>
(s0 -> (x a, s0)) -> StateT s0 mm x a
state s0 -> (x a, s0)
stateX = (s0 -> mm (EnvT s0 x) a) -> StateT s0 mm x a
forall s0 (mm :: (* -> *) -> * -> *) (x :: * -> *) a.
(s0 -> mm (EnvT s0 x) a) -> StateT s0 mm x a
StateT \s0
s0 ->
    let (x a
x, s0
s0') = s0 -> (x a, s0)
stateX s0
s0
     in EnvT s0 x a -> mm (EnvT s0 x) a
EnvT s0 x ~> mm (EnvT s0 x)
forall (g :: * -> *). Functor g => g ~> mm g
forall (ff :: (* -> *) -> * -> *) (g :: * -> *).
(FMonad ff, Functor g) =>
g ~> ff g
fpure (s0 -> x a -> EnvT s0 x a
forall e (w :: * -> *) a. e -> w a -> EnvT e w a
EnvT s0
s0' x a
x)

runState :: forall s0 x a. State s0 x a -> s0 -> (x a, s0)
runState :: forall s0 (x :: * -> *) a. State s0 x a -> s0 -> (x a, s0)
runState State s0 x a
stateX = (s0, x a) -> (x a, s0)
forall a b. (a, b) -> (b, a)
swap ((s0, x a) -> (x a, s0)) -> (s0 -> (s0, x a)) -> s0 -> (x a, s0)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EnvT s0 x a -> (s0, x a)
forall e (w :: * -> *) a. EnvT e w a -> (e, w a)
runEnvT (EnvT s0 x a -> (s0, x a))
-> (s0 -> EnvT s0 x a) -> s0 -> (s0, x a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdentityT (EnvT s0 x) a -> EnvT s0 x a
forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT (IdentityT (EnvT s0 x) a -> EnvT s0 x a)
-> (s0 -> IdentityT (EnvT s0 x) a) -> s0 -> EnvT s0 x a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State s0 x a -> s0 -> IdentityT (EnvT s0 x) a
forall s0 (mm :: (* -> *) -> * -> *) (x :: * -> *) a.
StateT s0 mm x a -> s0 -> mm (EnvT s0 x) a
runStateT State s0 x a
stateX