{-# OPTIONS_GHC -fno-warn-orphans #-}

module Pandora.Paradigm.Inventory.State where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern.Category (identity, (.), ($))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), (<$$>)))
import Pandora.Pattern.Functor.Avoidable (Avoidable (empty))
import Pandora.Pattern.Functor.Pointable (Pointable (point))
import Pandora.Pattern.Functor.Applicative (Applicative ((<*>), (*>)))
import Pandora.Pattern.Functor.Alternative (Alternative ((<+>)))
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.Pattern.Functor.Bivariant ((<->))
import Pandora.Pattern.Functor ((<*+>))
import Pandora.Paradigm.Controlflow.Effect.Adaptable (Adaptable (adapt))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run), Schematic)
import Pandora.Paradigm.Controlflow.Effect.Transformer.Monadic (Monadic (wrap), (:>) (TM))
import Pandora.Paradigm.Schemes.TUT (TUT (TUT), type (<:<.>:>))
import Pandora.Paradigm.Primary.Functor (Product ((:*:)), type (:*:), delta)

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 a b -> m a b
$ (a -> b) -> Product s a -> Product s b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
(<$>) a -> b
f (Product s a -> Product s b)
-> (s -> Product s a) -> ((->) s :. (:*:) s) := b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. State s a -> Primary (State s) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run State s a
x

instance Applicative (State s) where
	State s (a -> b)
f <*> :: State s (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 a b -> m a b
$ (Product (s :*: a) (a -> b)
-> ((a -> b) -> (s :*: a) -> s :*: b) -> s :*: b
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
t a -> (a -> u b) -> b
|- (a -> b) -> (s :*: a) -> s :*: b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
(<$>)) (Product (s :*: a) (a -> b) -> s :*: b)
-> (s -> Product (s :*: a) (a -> b)) -> ((->) s :. (:*:) s) := b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (State s a -> Primary (State s) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run State s a
x (((->) s :. (:*:) s) := a)
-> ((a -> b) -> a -> b)
-> Product s (a -> b)
-> Product (s :*: a) (a -> b)
forall (v :: * -> * -> *) a b c d.
Bivariant v =>
(a -> b) -> (c -> d) -> v a c -> v b d
<-> (a -> b) -> a -> b
forall (m :: * -> * -> *) a. Category m => m a a
identity) (Product s (a -> b) -> Product (s :*: a) (a -> b))
-> (s -> Product s (a -> b)) -> s -> Product (s :*: a) (a -> b)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. State s (a -> b) -> Primary (State s) (a -> b)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run State s (a -> b)
f

instance Pointable (State s) where
	point :: a |-> State s
point = (((->) s :. (:*:) s) := a) -> State s a
forall s a. (((->) s :. (:*:) s) := a) -> State s a
State ((((->) s :. (:*:) s) := a) -> State s a)
-> (a -> ((->) s :. (:*:) s) := a) -> a |-> State s
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> (Product s a -> Product s a) -> ((->) s :. (:*:) s) := a
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
a -> (t a -> b) -> u b
-| Product s a -> Product s a
forall (m :: * -> * -> *) a. Category m => m a a
identity)

instance Bindable (State s) where
	State s a
x >>= :: State s a -> (a -> State s b) -> State s b
>>= a -> State s b
f = (((->) 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 a b -> m a b
$ (Product s (State s b)
-> (State s b -> ((->) s :. (:*:) s) := b) -> s :*: b
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
t a -> (a -> u b) -> b
|- State s b -> ((->) s :. (:*:) s) := b
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run) (Product s (State s b) -> s :*: b)
-> (s -> Product s (State s b)) -> ((->) s :. (:*:) s) := b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> State s b) -> Product s a -> Product s (State s b)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
(<$>) a -> State s b
f (Product s a -> Product s (State s b))
-> (s -> Product s a) -> s -> Product s (State s b)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. State s a -> Primary (State s) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run State s a
x

instance Monad (State s) where

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

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

instance Monadic (State s) where
	wrap :: State s ~> (State s :> u)
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.
Category 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 a b -> m a b
$ (s :*: a) |-> u
forall (t :: * -> *) a. Pointable t => a |-> t
point ((s :*: a) |-> u)
-> (s -> s :*: a) -> ((->) s :. (u :. (:*:) s)) := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> State s a -> Primary (State s) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run State s a
x

type Stateful s = Adaptable (State s)

instance Covariant u => Covariant ((->) s <:<.>:> (:*:) s := u) where
	a -> b
f <$> :: (a -> b)
-> (:=) ((->) s <:<.>:> (:*:) s) u a
-> (:=) ((->) s <:<.>:> (:*:) s) u b
<$> (:=) ((->) s <:<.>:> (:*:) s) u a
x = (((->) s :. (u :. (:*:) s)) := b)
-> (:=) ((->) s <:<.>:> (:*:) s) u b
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)) := b)
 -> (:=) ((->) s <:<.>:> (:*:) s) u b)
-> (((->) s :. (u :. (:*:) s)) := b)
-> (:=) ((->) s <:<.>:> (:*:) s) u b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (a -> b) -> ((u :. (:*:) s) := a) -> (u :. (:*:) s) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
(<$$>) a -> b
f (((u :. (:*:) s) := a) -> (u :. (:*:) s) := b)
-> (s -> (u :. (:*:) s) := a) -> ((->) s :. (u :. (:*:) s)) := b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (:=) ((->) s <:<.>:> (:*:) s) u a
-> Primary (((->) s <:<.>:> (:*:) s) := u) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (:=) ((->) s <:<.>:> (:*:) s) u a
x

instance Bindable u => Applicative ((->) s <:<.>:> (:*:) s := u) where
	(:=) ((->) s <:<.>:> (:*:) s) u (a -> b)
f <*> :: (:=) ((->) s <:<.>:> (:*:) s) u (a -> b)
-> (:=) ((->) s <:<.>:> (:*:) s) u a
-> (:=) ((->) s <:<.>:> (:*:) s) u b
<*> (:=) ((->) s <:<.>:> (:*:) s) u a
x = (((->) s :. (u :. (:*:) s)) := b)
-> (:=) ((->) s <:<.>:> (:*:) s) u b
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)) := b)
 -> (:=) ((->) s <:<.>:> (:*:) s) u b)
-> (((->) s :. (u :. (:*:) s)) := b)
-> (:=) ((->) s <:<.>:> (:*:) s) u b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (:=) ((->) s <:<.>:> (:*:) s) u (a -> b)
-> Primary (((->) s <:<.>:> (:*:) s) := u) (a -> b)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (:=) ((->) s <:<.>:> (:*:) s) u (a -> b)
f (((->) s :. (u :. (:*:) s)) := (a -> b))
-> (Product s (a -> b) -> u (Product s b))
-> ((->) s :. (u :. (:*:) s)) := b
forall (t :: * -> *) a b c.
Bindable t =>
(a -> t b) -> (b -> t c) -> a -> t c
>=> \ ~(s
new :*: a -> b
g) -> a -> b
g (a -> b) -> ((u :. (:*:) s) := a) -> u (Product s b)
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
<$$> (:=) ((->) s <:<.>:> (:*:) s) u a
-> ((->) s :. (u :. (:*:) s)) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (:=) ((->) s <:<.>:> (:*:) s) u a
x s
new

instance Pointable u => Pointable ((->) s <:<.>:> (:*:) s := u) where
	point :: a |-> (((->) s <:<.>:> (:*:) s) := u)
point = (((->) s :. (u :. (:*:) s)) := a)
-> TUT Covariant Covariant Covariant ((->) 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)
 -> TUT Covariant Covariant Covariant ((->) s) ((:*:) s) u a)
-> (a -> ((->) s :. (u :. (:*:) s)) := a)
-> a |-> (((->) s <:<.>:> (:*:) s) := u)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> ((s :*: a) -> u (s :*: a)) -> ((->) s :. (u :. (:*:) s)) := a
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
a -> (t a -> b) -> u b
-| (s :*: a) -> u (s :*: a)
forall (t :: * -> *) a. Pointable t => a |-> t
point)

instance Bindable u => Bindable ((->) s <:<.>:> (:*:) s := u) where
	(:=) ((->) s <:<.>:> (:*:) s) u a
x >>= :: (:=) ((->) s <:<.>:> (:*:) s) u a
-> (a -> (:=) ((->) s <:<.>:> (:*:) s) u b)
-> (:=) ((->) s <:<.>:> (:*:) s) u b
>>= a -> (:=) ((->) s <:<.>:> (:*:) s) u b
f = (((->) s :. (u :. (:*:) s)) := b)
-> (:=) ((->) s <:<.>:> (:*:) s) u b
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)) := b)
 -> (:=) ((->) s <:<.>:> (:*:) s) u b)
-> (((->) s :. (u :. (:*:) s)) := b)
-> (:=) ((->) s <:<.>:> (:*:) s) u b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (:=) ((->) s <:<.>:> (:*:) s) u a
-> Primary (((->) s <:<.>:> (:*:) s) := u) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (:=) ((->) s <:<.>:> (:*:) s) u a
x (((->) s :. (u :. (:*:) s)) := a)
-> (Product s a -> u (s :*: b)) -> ((->) s :. (u :. (:*:) s)) := b
forall (t :: * -> *) a b c.
Bindable t =>
(a -> t b) -> (b -> t c) -> a -> t c
>=> \ ~(s
new :*: a
y) -> ((((->) s :. (u :. (:*:) s)) := b)
-> ((->) s :. (u :. (:*:) s)) := b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ s
new) ((((->) s :. (u :. (:*:) s)) := b) -> u (s :*: b))
-> (a -> ((->) s :. (u :. (:*:) s)) := b) -> a -> u (s :*: b)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (:=) ((->) s <:<.>:> (:*:) s) u b
-> ((->) s :. (u :. (:*:) s)) := b
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((:=) ((->) s <:<.>:> (:*:) s) u b
 -> ((->) s :. (u :. (:*:) s)) := b)
-> (a -> (:=) ((->) s <:<.>:> (:*:) s) u b)
-> a
-> ((->) s :. (u :. (:*:) s)) := b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> (:=) ((->) s <:<.>:> (:*:) s) u b
f (a -> u (s :*: b)) -> a -> u (s :*: b)
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a
y

instance Monad u => Monad ((->) s <:<.>:> (:*:) s := u) where

instance Alternative u => Alternative ((->) s <:<.>:> (:*:) s := u) where
	(:=) ((->) s <:<.>:> (:*:) s) u a
x <+> :: (:=) ((->) s <:<.>:> (:*:) s) u a
-> (:=) ((->) s <:<.>:> (:*:) s) u a
-> (:=) ((->) s <:<.>:> (:*:) s) u a
<+> (:=) ((->) s <:<.>:> (:*:) s) u a
y = (((->) 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)
 -> (:=) ((->) s <:<.>:> (:*:) s) u a)
-> (((->) s :. (u :. (:*:) s)) := a)
-> (:=) ((->) s <:<.>:> (:*:) s) u a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (:=) ((->) s <:<.>:> (:*:) s) u a
-> Primary (((->) s <:<.>:> (:*:) s) := u) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (:=) ((->) s <:<.>:> (:*:) s) u a
x (((->) s :. (u :. (:*:) s)) := a)
-> (((->) s :. (u :. (:*:) s)) := a)
-> ((->) s :. (u :. (:*:) s)) := a
forall (t :: * -> *) (u :: * -> *) a.
(Applicative t, Alternative u) =>
((t :. u) := a) -> ((t :. u) := a) -> (t :. u) := a
<*+> (:=) ((->) s <:<.>:> (:*:) s) u a
-> Primary (((->) s <:<.>:> (:*:) s) := u) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (:=) ((->) s <:<.>:> (:*:) s) u a
y

instance Avoidable u => Avoidable ((->) s <:<.>:> (:*:) s := u) where
	empty :: (:=) ((->) s <:<.>:> (:*:) s) u a
empty = (((->) 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)
 -> (:=) ((->) s <:<.>:> (:*:) s) u a)
-> (((->) s :. (u :. (:*:) s)) := a)
-> (:=) ((->) s <:<.>:> (:*:) s) u a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ \s
_ -> u (s :*: a)
forall (t :: * -> *) a. Avoidable t => t a
empty

current :: Stateful s t => t s
current :: t s
current = State s s -> t s
forall k (t :: k -> *) (u :: k -> *). Adaptable t u => t ~> u
adapt (State s s -> t s) -> State s s -> t s
forall (m :: * -> * -> *) a b. Category 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 :: Stateful s t => (s -> s) -> t ()
modify :: (s -> s) -> t ()
modify s -> s
f = State s () -> t ()
forall k (t :: k -> *) (u :: k -> *). Adaptable t u => t ~> u
adapt (State s () -> t ())
-> ((((->) s :. (:*:) s) := ()) -> State s ())
-> (((->) s :. (:*:) s) := ())
-> t ()
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (((->) s :. (:*:) s) := ()) -> State s ()
forall s a. (((->) s :. (:*:) s) := a) -> State s a
State ((((->) s :. (:*:) s) := ()) -> t ())
-> (((->) s :. (:*:) s) := ()) -> t ()
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (s -> () -> Product s ()
forall s a. s -> a -> Product s a
:*: ()) (((->) s :. (:*:) s) := ())
-> (s -> s) -> ((->) s :. (:*:) s) := ()
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. s -> s
f

replace :: Stateful s t => s -> t ()
replace :: s -> t ()
replace s
s = State s () -> t ()
forall k (t :: k -> *) (u :: k -> *). Adaptable t u => t ~> u
adapt (State s () -> t ())
-> ((((->) s :. (:*:) s) := ()) -> State s ())
-> (((->) s :. (:*:) s) := ())
-> t ()
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (((->) s :. (:*:) s) := ()) -> State s ()
forall s a. (((->) s :. (:*:) s) := a) -> State s a
State ((((->) s :. (:*:) s) := ()) -> t ())
-> (((->) s :. (:*:) s) := ()) -> t ()
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ \s
_ -> s
s s -> () -> Product s ()
forall s a. s -> a -> Product s a
:*: ()

type Memorable s t = (Pointable t, Applicative 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 = t a
struct t a -> (a -> u ()) -> (u :. t) := ()
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> (s -> s) -> u ()
forall s (t :: * -> *). Stateful s t => (s -> s) -> t ()
modify ((s -> s) -> u ()) -> (a -> s -> s) -> a -> u ()
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> s -> s
op ((u :. t) := ()) -> u s -> u s
forall (t :: * -> *) a b. Applicative t => t a -> t b -> t b
*> u s
forall s (t :: * -> *). Stateful s t => t s
current

type Decisive t = (Pointable t, Avoidable t, Alternative t, Applicative t)