{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Inventory.Some.State where

import Pandora.Core.Functor (type (:.), type (>>>))
import Pandora.Core.Interpreted (Interpreted (Primary, run, (<~), unite, (=#-)))
import Pandora.Pattern.Morphism.Flip (Flip)
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), identity)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
import Pandora.Pattern.Functor.Invariant (Invariant ((<!<)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Functor.Traversable (Traversable ((<-/-)))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<), (==<<)))
import Pandora.Pattern.Functor.Monad (Monad)
import Pandora.Pattern.Functor.Adjoint ((-|), (|-))
import Pandora.Paradigm.Controlflow.Effect.Adaptable (Adaptable (adapt))
import Pandora.Paradigm.Controlflow.Effect.Transformer.Monadic (Monadic (wrap), (:>) (TM))
import Pandora.Paradigm.Inventory.Ability.Gettable (Gettable (Getting, get))
import Pandora.Paradigm.Inventory.Ability.Settable (Settable (Setting, set))
import Pandora.Paradigm.Inventory.Ability.Modifiable (Modifiable (Modification, modify))
import Pandora.Paradigm.Algebraic.Exponential (type (-->))
import Pandora.Paradigm.Algebraic ((:*:) ((:*:)), delta)
import Pandora.Paradigm.Algebraic.One (One (One))
import Pandora.Paradigm.Algebraic (Pointable, point, (<-||-), (>-||-))
import Pandora.Paradigm.Schemes (Schematic, TUT (TUT), type (<:<.>:>))

-- | Effectful computation with a variable
newtype State s a = State ((->) s :. (:*:) s >>> a)

instance Covariant (->) (->) (State s) where
	a -> b
f <-|- :: (a -> b) -> State s a -> State s b
<-|- State s a
x = (((->) s :. (:*:) s) >>> b) -> State s b
forall s a. (((->) s :. (:*:) s) >>> a) -> State s a
State ((((->) s :. (:*:) s) >>> b) -> State s b)
-> (((->) s :. (:*:) s) >>> b) -> State s b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (a -> b) -> (s :*: a) -> s :*: b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) a -> b
f ((s :*: a) -> s :*: b)
-> (s -> s :*: a) -> ((->) s :. (:*:) s) >>> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. State s a -> s -> s :*: a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run State s a
x

instance Semimonoidal (-->) (:*:) (:*:) (State s) where
	mult :: (State s a :*: State s b) --> State s (a :*: b)
mult = ((State s a :*: State s b) -> State s (a :*: b))
-> (State s a :*: State s b) --> State s (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((State s a :*: State s b) -> State s (a :*: b))
 -> (State s a :*: State s b) --> State s (a :*: b))
-> ((State s a :*: State s b) -> State s (a :*: b))
-> (State s a :*: State s b) --> State s (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(State ((->) s :. (:*:) s) >>> a
g :*: State ((->) s :. (:*:) s) >>> b
h) -> (((->) s :. (:*:) s) >>> (a :*: b)) -> State s (a :*: b)
forall s a. (((->) s :. (:*:) s) >>> a) -> State s a
State ((((->) s :. (:*:) s) >>> (a :*: b)) -> State s (a :*: b))
-> (((->) s :. (:*:) s) >>> (a :*: b)) -> State s (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \s
s ->
		let s
old :*: a
x = ((->) s :. (:*:) s) >>> a
g s
s in
		let s
new :*: b
y = ((->) s :. (:*:) s) >>> b
h s
old in
		s
new s -> (a :*: b) -> s :*: (a :*: b)
forall s a. s -> a -> s :*: a
:*: a
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: b
y

instance Monoidal (-->) (-->) (:*:) (:*:) (State s) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) --> State s a
unit Proxy (:*:)
_ = (Straight (->) One a -> State s a)
-> Straight (->) (Straight (->) One a) (State s a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((Straight (->) One a -> State s a)
 -> Straight (->) (Straight (->) One a) (State s a))
-> (Straight (->) One a -> State s a)
-> Straight (->) (Straight (->) One a) (State s a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (((->) s :. (:*:) s) >>> a) -> State s a
forall s a. (((->) s :. (:*:) s) >>> a) -> State s a
State ((((->) s :. (:*:) s) >>> a) -> State s a)
-> (Straight (->) One a -> ((->) s :. (:*:) s) >>> a)
-> Straight (->) One a
-> State s a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (forall a. Category (->) => a -> a
forall (m :: * -> * -> *) a. Category m => m a a
identity @(->) ((s :*: a) -> s :*: a) -> a -> ((->) s :. (:*:) s) >>> a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
source (t a) b -> target a (u b)
-|) (a -> ((->) s :. (:*:) s) >>> a)
-> (Straight (->) One a -> a)
-> Straight (->) One a
-> ((->) s :. (:*:) s) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Straight (->) One a -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ One
One)

instance Bindable (->) (State s) where
	a -> State s b
f =<< :: (a -> State s b) -> State s a -> State s b
=<< State s a
x = (((->) s :. (:*:) s) >>> b) -> State s b
forall s a. (((->) s :. (:*:) s) >>> a) -> State s a
State ((((->) s :. (:*:) s) >>> b) -> State s b)
-> (((->) s :. (:*:) s) >>> b) -> State s b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (State s b -> ((->) s :. (:*:) s) >>> b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (State s b -> ((->) s :. (:*:) s) >>> b)
-> (a -> State s b) -> a -> ((->) s :. (:*:) s) >>> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> State s b
f (a -> ((->) s :. (:*:) s) >>> b) -> (s :*: a) -> s :*: b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
|-) ((s :*: a) -> s :*: b)
-> (s -> s :*: a) -> ((->) s :. (:*:) s) >>> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- State s a -> s -> s :*: a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run State s a
x

instance Monad (->) (State s) where

instance Invariant (Flip State r) where
	a -> b
f <!< :: (a -> b) -> (b -> a) -> Flip State r a -> Flip State r b
<!< b -> a
g = (((b -> a
g (b -> a) -> (a -> b :*: r) -> b -> b :*: r
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c.
(Contravariant m m (Flip p c), Interpreted m (Flip p c)) =>
m a b -> m (p b c) (p a c)
>-||-) ((a -> b :*: r) -> b -> b :*: r)
-> ((a -> a :*: r) -> a -> b :*: r)
-> (a -> a :*: r)
-> b
-> b :*: r
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((a -> b
f (a -> b) -> (a :*: r) -> b :*: r
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c.
(Covariant m m (Flip p c), Interpreted m (Flip p c)) =>
m a b -> m (p a c) (p b c)
<-||-) ((a :*: r) -> b :*: r) -> (a -> a :*: r) -> a -> b :*: r
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (Primary (State a) r -> Primary (State b) r)
-> ((->) < State a r) < State b r
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
=#-) (Primary (Flip State r) a -> Primary (Flip State r) b)
-> Flip State r a -> Flip State r b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
=#-)

instance Interpreted (->) (State s) where
	type Primary (State s) a = (->) s :. (:*:) s >>> a
	run :: ((->) < State s a) < Primary (State s) a
run ~(State ((->) s :. (:*:) s) >>> a
x) = Primary (State s) a
((->) s :. (:*:) s) >>> a
x
	unite :: ((->) < Primary (State s) a) < State s a
unite = ((->) < Primary (State s) a) < State s a
forall s a. (((->) s :. (:*:) s) >>> a) -> State s a
State

type instance Schematic Monad (State s) = (->) s <:<.>:> (:*:) s

instance Monadic (->) (State s) where
	wrap :: ((->) < State s a) < (:>) (State s) u a
wrap State s a
x = (<:<.>:>) ((->) s) ((:*:) s) u a -> (:>) (State s) u a
forall (t :: * -> *) (u :: * -> *) a.
Schematic Monad t u a -> (:>) t u a
TM ((<:<.>:>) ((->) s) ((:*:) s) u a -> (:>) (State s) u a)
-> ((((->) s :. (u :. (:*:) s)) >>> a)
    -> (<:<.>:>) ((->) s) ((:*:) s) u a)
-> (((->) s :. (u :. (:*:) s)) >>> a)
-> (:>) (State s) u a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (((->) s :. (u :. (:*:) s)) >>> a)
-> (<:<.>:>) ((->) s) ((:*:) s) u a
forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *)
       (t' :: k -> k) (u :: k -> k) (a :: k).
((t :. (u :. t')) >>> a) -> TUT ct ct' cu t t' u a
TUT ((((->) s :. (u :. (:*:) s)) >>> a) -> (:>) (State s) u a)
-> (((->) s :. (u :. (:*:) s)) >>> a) -> (:>) (State s) u a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (s :*: a) -> u (s :*: a)
forall (t :: * -> *) a. Pointable t => a -> t a
point ((s :*: a) -> u (s :*: a))
-> (s -> s :*: a) -> ((->) s :. (u :. (:*:) s)) >>> a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- State s a -> s -> s :*: a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run State s a
x

type Stateful s t = Adaptable t (->) (State s)

current :: Stateful s t => t s
current :: t s
current = ((->) < State s s) < t s
forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k)
       (a :: k).
Adaptable u m t =>
(m < t a) < u a
adapt (((->) < State s s) < t s) -> ((->) < State s s) < t s
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (((->) s :. (:*:) s) >>> s) -> State s s
forall s a. (((->) s :. (:*:) s) >>> a) -> State s a
State ((->) s :. (:*:) s) >>> s
forall a. a -> a :*: a
delta

-- Modify the state, state is new value, return old value
change :: Stateful s t => (s -> s) -> t s
change :: (s -> s) -> t s
change s -> s
f = ((->) < State s s) < t s
forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k)
       (a :: k).
Adaptable u m t =>
(m < t a) < u a
adapt (((->) < State s s) < t s)
-> ((s -> s :*: s) -> State s s) -> (s -> s :*: s) -> t s
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (s -> s :*: s) -> State s s
forall s a. (((->) s :. (:*:) s) >>> a) -> State s a
State ((s -> s :*: s) -> t s) -> (s -> s :*: s) -> t s
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \s
s -> s -> s
f s
s s -> s -> s :*: s
forall s a. s -> a -> s :*: a
:*: s
s

reconcile :: (Bindable (->) t, Stateful s t, Adaptable t (->) u) => (s -> u s) -> t s
reconcile :: (s -> u s) -> t s
reconcile s -> u s
f = ((->) < State s s) < t s
forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k)
       (a :: k).
Adaptable u m t =>
(m < t a) < u a
adapt (((->) < State s s) < t s) -> (s -> State s s) -> s -> t s
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall e r. Settable State => Setting State e r
forall k (i :: k) e r. Settable i => Setting i e r
set @State (s -> t s) -> t s -> t s
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
==<< ((->) < u s) < t s
forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k)
       (a :: k).
Adaptable u m t =>
(m < t a) < u a
adapt (((->) < u s) < t s) -> (s -> u s) -> s -> t s
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. s -> u s
f (s -> t s) -> t s -> t s
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
==<< ((->) < State s s) < t s
forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k)
       (a :: k).
Adaptable u m t =>
(m < t a) < u a
adapt (((->) < State s s) < t s) -> ((->) < State s s) < t s
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall e r. Gettable State => Getting State e r
forall k (i :: k) e r. Gettable i => Getting i e r
get @State

type Memorable s t = (Covariant (->) (->) t, Pointable t, Stateful s t)

-- fold :: (Traversable (->) (->) t, Memorable s u) => (a -> s -> s) -> t a -> u s
-- fold op struct = adapt <-- get @State -*- (adapt . modify @State . op <-/- struct)

instance Gettable State where
	type Getting State state ouput = State state state
	get :: Getting State e r
get = (((->) e :. (:*:) e) >>> e) -> State e e
forall s a. (((->) s :. (:*:) s) >>> a) -> State s a
State ((->) e :. (:*:) e) >>> e
forall a. a -> a :*: a
delta

instance Settable State where
	type Setting State state output = state -> State state state
	set :: Setting State e r
set e
new = (((->) e :. (:*:) e) >>> e) -> State e e
forall s a. (((->) s :. (:*:) s) >>> a) -> State s a
State ((((->) e :. (:*:) e) >>> e) -> State e e)
-> (((->) e :. (:*:) e) >>> e) -> State e e
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- \e
_ -> e
new e -> ((->) e :. (:*:) e) >>> e
forall s a. s -> a -> s :*: a
:*: e
new

instance Modifiable State where
	type Modification State state output = (state -> state) -> State state state
	modify :: Modification State e r
modify e -> e
f = (((->) e :. (:*:) e) >>> e) -> State e e
forall s a. (((->) s :. (:*:) s) >>> a) -> State s a
State ((((->) e :. (:*:) e) >>> e) -> State e e)
-> (((->) e :. (:*:) e) >>> e) -> State e e
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- \e
s -> e -> e
f e
s e -> ((->) e :. (:*:) e) >>> e
forall s a. s -> a -> s :*: a
:*: e -> e
f e
s