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

module FMonad.State.Simple.Inner
  (StateT(..),
   flift,
   toAdjointT,
   fromAdjointT,
   
   State,
   state,
   runState
) where

import Control.Monad.Trans.Identity ( IdentityT(..) )
import Control.Comonad.Trans.Traced ( TracedT(..) )
import Control.Monad.Trans.Writer ( WriterT(..) )
import Data.Functor.Day (Day(..), swapped)
import Data.Functor.Day.Extra (dayToTraced)
import Data.Coerce (coerce)

import FMonad
import FMonad.Adjoint
import FStrong

newtype StateT s1 mm x a = StateT { forall s1 (mm :: (* -> *) -> * -> *) (x :: * -> *) a.
StateT s1 mm x a -> mm (TracedT s1 x) (a, s1)
runStateT :: mm (TracedT s1 x) (a, s1) }
   deriving ((forall (g :: * -> *). Functor g => Functor (StateT s1 mm g)) =>
(forall (g :: * -> *) (h :: * -> *) x.
 (Functor g, Functor h) =>
 (g ~> h) -> StateT s1 mm g x -> StateT s1 mm h x)
-> FFunctor (StateT s1 mm)
forall s1 (mm :: (* -> *) -> * -> *) (g :: * -> *).
(FFunctor mm, Functor g) =>
Functor (StateT s1 mm g)
forall s1 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) x.
(FFunctor mm, Functor g, Functor h) =>
(g ~> h) -> StateT s1 mm g x -> StateT s1 mm h x
forall (g :: * -> *). Functor g => Functor (StateT s1 mm g)
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> StateT s1 mm g x -> StateT s1 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 s1 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) x.
(FFunctor mm, Functor g, Functor h) =>
(g ~> h) -> StateT s1 mm g x -> StateT s1 mm h x
ffmap :: forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> StateT s1 mm g x -> StateT s1 mm h x
FFunctor, FFunctor (StateT s1 mm)
FFunctor (StateT s1 mm) =>
(forall (g :: * -> *). Functor g => g ~> StateT s1 mm g)
-> (forall (g :: * -> *) (h :: * -> *) a.
    (Functor g, Functor h) =>
    (g ~> StateT s1 mm h) -> StateT s1 mm g a -> StateT s1 mm h a)
-> FMonad (StateT s1 mm)
forall s1 (mm :: (* -> *) -> * -> *).
FMonad mm =>
FFunctor (StateT s1 mm)
forall s1 (mm :: (* -> *) -> * -> *) (g :: * -> *).
(FMonad mm, Functor g) =>
g ~> StateT s1 mm g
forall s1 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) a.
(FMonad mm, Functor g, Functor h) =>
(g ~> StateT s1 mm h) -> StateT s1 mm g a -> StateT s1 mm h a
forall (g :: * -> *). Functor g => g ~> StateT s1 mm g
forall (g :: * -> *) (h :: * -> *) a.
(Functor g, Functor h) =>
(g ~> StateT s1 mm h) -> StateT s1 mm g a -> StateT s1 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 s1 (mm :: (* -> *) -> * -> *) (g :: * -> *).
(FMonad mm, Functor g) =>
g ~> StateT s1 mm g
fpure :: forall (g :: * -> *). Functor g => g ~> StateT s1 mm g
$cfbind :: forall s1 (mm :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *) a.
(FMonad mm, Functor g, Functor h) =>
(g ~> StateT s1 mm h) -> StateT s1 mm g a -> StateT s1 mm h a
fbind :: forall (g :: * -> *) (h :: * -> *) a.
(Functor g, Functor h) =>
(g ~> StateT s1 mm h) -> StateT s1 mm g a -> StateT s1 mm h a
FMonad) via (AdjointT (TracedT s1) (WriterT s1) mm)
type State s1 = StateT s1 IdentityT

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

toAdjointT :: StateT s1 mm x ~> AdjointT (TracedT s1) (WriterT s1) mm x
toAdjointT :: forall s1 (mm :: (* -> *) -> * -> *) (x :: * -> *) x.
StateT s1 mm x x -> AdjointT (TracedT s1) (WriterT s1) mm x x
toAdjointT = StateT s1 mm x x -> AdjointT (TracedT s1) (WriterT s1) mm x x
forall a b. Coercible a b => a -> b
coerce

fromAdjointT :: AdjointT (TracedT s1) (WriterT s1) mm x ~> StateT s1 mm x
fromAdjointT :: forall s1 (mm :: (* -> *) -> * -> *) (x :: * -> *) x.
AdjointT (TracedT s1) (WriterT s1) mm x x -> StateT s1 mm x x
fromAdjointT = AdjointT (TracedT s1) (WriterT s1) mm x x -> StateT s1 mm x x
forall a b. Coercible a b => a -> b
coerce

flift :: (FStrong mm, Functor x)
  => mm x ~> StateT s1 mm x
flift :: forall (mm :: (* -> *) -> * -> *) (x :: * -> *) s1.
(FStrong mm, Functor x) =>
mm x ~> StateT s1 mm x
flift mm x x
mm = AdjointT (TracedT s1) (WriterT s1) mm x x -> StateT s1 mm x x
forall s1 (mm :: (* -> *) -> * -> *) (x :: * -> *) x.
AdjointT (TracedT s1) (WriterT s1) mm x x -> StateT s1 mm x x
fromAdjointT (AdjointT (TracedT s1) (WriterT s1) mm x x -> StateT s1 mm x x)
-> AdjointT (TracedT s1) (WriterT s1) mm x x -> StateT s1 mm x x
forall a b. (a -> b) -> a -> b
$ WriterT s1 (mm (TracedT s1 x)) x
-> AdjointT (TracedT s1) (WriterT s1) mm x x
forall {k} {k1} {k2} {k3} (ff :: k -> k1) (uu :: k2 -> k3 -> *)
       (mm :: k1 -> k2) (g :: k) (x :: k3).
uu (mm (ff g)) x -> AdjointT ff uu mm g x
AdjointT (WriterT s1 (mm (TracedT s1 x)) x
 -> AdjointT (TracedT s1) (WriterT s1) mm x x)
-> WriterT s1 (mm (TracedT s1 x)) x
-> AdjointT (TracedT s1) (WriterT s1) mm x x
forall a b. (a -> b) -> a -> b
$ mm (TracedT s1 x) (x, s1) -> WriterT s1 (mm (TracedT s1 x)) x
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (mm (TracedT s1 x) (x, s1) -> WriterT s1 (mm (TracedT s1 x)) x)
-> mm (TracedT s1 x) (x, s1) -> WriterT s1 (mm (TracedT s1 x)) x
forall a b. (a -> b) -> a -> b
$ (Day x ((->) s1) ~> TracedT s1 x)
-> mm (Day x ((->) s1)) (x, s1) -> mm (TracedT s1 x) (x, s1)
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 (Day ((->) s1) x x -> TracedT s1 x x
Day ((->) s1) x ~> TracedT s1 x
forall (f :: * -> *) s1.
Functor f =>
Day ((->) s1) f ~> TracedT s1 f
dayToTraced (Day ((->) s1) x x -> TracedT s1 x x)
-> (Day x ((->) s1) x -> Day ((->) s1) x x)
-> Day x ((->) s1) x
-> TracedT s1 x x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Day x ((->) s1) x -> Day ((->) s1) x x
forall (f :: * -> *) (g :: * -> *) a. Day f g a -> Day g f a
swapped) (Day (mm x) ((->) s1) (x, s1) -> mm (Day x ((->) s1)) (x, s1)
Day (mm x) ((->) s1) ~> mm (Day x ((->) s1))
forall (g :: * -> *) (h :: * -> *).
Functor g =>
Day (mm g) h ~> mm (Day g h)
forall (ff :: (* -> *) -> * -> *) (g :: * -> *) (h :: * -> *).
(FStrong ff, Functor g) =>
Day (ff g) h ~> ff (Day g h)
fstrength (mm x x
-> (s1 -> s1)
-> (x -> s1 -> (x, s1))
-> Day (mm x) ((->) s1) (x, s1)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day mm x x
mm s1 -> s1
forall a. a -> a
id (,)))

state :: forall s1 x mm a. (Functor x, FMonad mm) => x (s1 -> (a, s1)) -> StateT s1 mm x a
state :: forall s1 (x :: * -> *) (mm :: (* -> *) -> * -> *) a.
(Functor x, FMonad mm) =>
x (s1 -> (a, s1)) -> StateT s1 mm x a
state = mm (TracedT s1 x) (a, s1) -> StateT s1 mm x a
forall s1 (mm :: (* -> *) -> * -> *) (x :: * -> *) a.
mm (TracedT s1 x) (a, s1) -> StateT s1 mm x a
StateT (mm (TracedT s1 x) (a, s1) -> StateT s1 mm x a)
-> (x (s1 -> (a, s1)) -> mm (TracedT s1 x) (a, s1))
-> x (s1 -> (a, s1))
-> StateT s1 mm x a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TracedT s1 x (a, s1) -> mm (TracedT s1 x) (a, s1)
TracedT s1 x ~> mm (TracedT s1 x)
forall (g :: * -> *). Functor g => g ~> mm g
forall (ff :: (* -> *) -> * -> *) (g :: * -> *).
(FMonad ff, Functor g) =>
g ~> ff g
fpure (TracedT s1 x (a, s1) -> mm (TracedT s1 x) (a, s1))
-> (x (s1 -> (a, s1)) -> TracedT s1 x (a, s1))
-> x (s1 -> (a, s1))
-> mm (TracedT s1 x) (a, s1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x (s1 -> (a, s1)) -> TracedT s1 x (a, s1)
forall m (w :: * -> *) a. w (m -> a) -> TracedT m w a
TracedT

runState :: State s1 x a -> x (s1 -> (a, s1))
runState :: forall s1 (x :: * -> *) a. State s1 x a -> x (s1 -> (a, s1))
runState = State s1 x a -> x (s1 -> (a, s1))
forall a b. Coercible a b => a -> b
coerce