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

import Pandora.Pattern.Morphism.Flip (Flip)
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Core.Functor (type (:.), type (:=))
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.Interpreted (Interpreted (Primary, run, unite, (=#-)), Schematic)
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.Schemes.TUT (TUT (TUT), type (<:<.>:>))
import Pandora.Paradigm.Primary.Algebraic.Exponential (type (-->))
import Pandora.Paradigm.Primary.Algebraic ((:*:) ((:*:)), (.-*-), delta)
import Pandora.Paradigm.Primary.Algebraic.One (One (One))
import Pandora.Paradigm.Primary.Algebraic (Pointable, point, (<-||-), (>-||-))

-- | 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
. ((One -> a) -> One -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- One
One) ((One -> a) -> a)
-> (Straight (->) One a -> One -> a) -> Straight (->) One a -> 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)
run

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)

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 :: (a -> s -> s) -> t a -> u s
fold a -> s -> s
op t a
struct = State s s -> u 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 -> u s) -> State s s -> u 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 u s -> u (t s) -> u s
forall (t :: * -> *) b a.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t b -> t a -> t b
.-*- (State s s -> u 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 -> u s) -> (a -> State s s) -> a -> u s
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall e r. Modifiable State => Modification State e r
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @State ((s -> s) -> State s s) -> (a -> s -> s) -> a -> State s s
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> s -> s
op (a -> u s) -> t a -> u (t s)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<-- t a
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 -> let r :: e
r = e -> e
f e
s in e
r e -> ((->) e :. (:*:) e) := e
forall s a. s -> a -> s :*: a
:*: e
r