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

import Pandora.Core (type (:.), type (>>>), type (<:=), type (~>))
import Pandora.Core.Interpreted (Interpreted (Primary, run, unite, (=#-)))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<------), identity)
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|--), (<-|-|-)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Functor.Invariant (Invariant ((<!<)))
import Pandora.Pattern.Functor.Extendable (Extendable ((<<=)))
import Pandora.Pattern.Functor.Comonad (Comonad)
import Pandora.Pattern.Functor.Adjoint ((-|), (|-))
import Pandora.Paradigm.Algebraic.Exponential (type (<--), type (-->), (%), (.:..))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), attached)
import Pandora.Paradigm.Algebraic (extract, (<-||-), (>-||-))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Paradigm.Controlflow.Effect.Adaptable (Adaptable (adapt))
import Pandora.Paradigm.Controlflow.Effect.Transformer.Comonadic (Comonadic (bring), (:<) (TC))
import Pandora.Paradigm.Schemes (Schematic, TUT (TUT), type (<:<.>:>))

-- | Context based computation on value
newtype Store s a = Store ((:*:) s :. (->) s >>> a)

-- TODO: Try to generalize (->) here
instance Covariant (->) (->) (Store s) where
	<-|- :: (a -> b) -> Store s a -> Store s b
(<-|-) a -> b
f = (((->) < Primary (Store s) a) < Primary (Store s) b)
-> Store s a -> Store s 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
(=#-) (a -> b
f (a -> b) -> (s :*: (s -> a)) -> s :*: (s -> b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
<-|-|-)

instance Semimonoidal (<--) (:*:) (:*:) (Store s) where
	mult :: (Store s a :*: Store s b) <-- Store s (a :*: b)
mult = (Store s (a :*: b) -> Store s a :*: Store s b)
-> (Store s a :*: Store s b) <-- Store s (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Store s (a :*: b) -> Store s a :*: Store s b)
 -> (Store s a :*: Store s b) <-- Store s (a :*: b))
-> (Store s (a :*: b) -> Store s a :*: Store s b)
-> (Store s a :*: Store s b) <-- Store s (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Store (s
s :*: s -> a :*: b
f)) ->
		let (a
x :*: b
y) = s -> a :*: b
f s
s in
		(((:*:) s :. (->) s) >>> a) -> Store s a
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store (s
s s -> (s -> a) -> ((:*:) s :. (->) s) >>> a
forall s a. s -> a -> s :*: a
:*: a -> s -> a
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant a
x) Store s a -> Store s b -> Store s a :*: Store s b
forall s a. s -> a -> s :*: a
:*: (((:*:) s :. (->) s) >>> b) -> Store s b
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store (s
s s -> (s -> b) -> ((:*:) s :. (->) s) >>> b
forall s a. s -> a -> s :*: a
:*: b -> s -> b
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant b
y)

instance Monoidal (<--) (-->) (:*:) (:*:) (Store s) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) <-- Store s a
unit Proxy (:*:)
_ = (Store s a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (Store s a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Store s a -> Straight (->) One a)
 -> Flip (->) (Straight (->) One a) (Store s a))
-> (Store s a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (Store s a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (One -> a) -> Straight (->) One a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((One -> a) -> Straight (->) One a)
-> (Store s a -> One -> a) -> Store s a -> Straight (->) One a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> One -> a
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant (a -> One -> a) -> (Store s a -> a) -> Store s a -> One -> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((s -> a) -> s -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
(<--) ((s -> a) -> s -> a) -> (s :*: (s -> a)) -> a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
|-) ((s :*: (s -> a)) -> a)
-> (Store s a -> s :*: (s -> a)) -> Store s a -> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Store s a -> s :*: (s -> a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run

-- TODO: Try to generalize (->) here
instance Extendable (->) (Store s) where
	Store s a -> b
f <<= :: (Store s a -> b) -> Store s a -> Store s b
<<= Store ((:*:) s :. (->) s) >>> a
x = (((:*:) s :. (->) s) >>> b) -> Store s b
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) s :. (->) s) >>> b) -> Store s b)
-> (((:*:) s :. (->) s) >>> b) -> Store s b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<------ Store s a -> b
f (Store s a -> b)
-> (s :*: (s -> Store s a)) -> ((:*:) s :. (->) s) >>> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
<-|-|- (((((:*:) s :. (->) s) >>> a) -> Store s a
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) s :. (->) s) >>> a) -> Store s a)
-> ((s -> a) -> s -> ((:*:) s :. (->) s) >>> a)
-> (s -> a)
-> s
-> Store s a
forall (target :: * -> * -> *) (v :: * -> * -> *) a c d b.
(Covariant (->) target (v a), Semigroupoid v) =>
v c d -> target (v a (v b c)) (v a (v b d))
.:.. (forall a. Category (->) => a -> a
forall (m :: * -> * -> *) a. Category m => m a a
identity @(->) ((((:*:) s :. (->) s) >>> a) -> ((:*:) s :. (->) s) >>> a)
-> (s -> a) -> s -> ((:*:) s :. (->) s) >>> a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
source (t a) b -> target a (u b)
-|)) ((s -> a) -> s -> Store s a)
-> (((:*:) s :. (->) s) >>> a) -> s :*: (s -> Store s a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-- ((:*:) s :. (->) s) >>> a
x)

instance Comonad (->) (Store s) where

instance Invariant (Flip Store r) where
	a -> b
f <!< :: (a -> b) -> (b -> a) -> Flip Store r a -> Flip Store r b
<!< b -> a
g = (((a -> b
f (a -> b) -> (a :*: (b -> r)) -> b :*: (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 :*: (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
. ((b -> a
g (b -> a) -> (a -> r) -> 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 -> 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 (Store a) r -> Primary (Store b) r)
-> ((->) < Store a r) < Store 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 Store r) a -> Primary (Flip Store r) b)
-> Flip Store r a -> Flip Store 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 (->) (Store s) where
	type Primary (Store s) a = (:*:) s :. (->) s >>> a
	run :: ((->) < Store s a) < Primary (Store s) a
run ~(Store ((:*:) s :. (->) s) >>> a
x) = Primary (Store s) a
((:*:) s :. (->) s) >>> a
x
	unite :: ((->) < Primary (Store s) a) < Store s a
unite = ((->) < Primary (Store s) a) < Store s a
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store

type instance Schematic Comonad (Store s) = (:*:) s <:<.>:> (->) s

instance Comonadic (->) (Store s) where
	bring :: ((->) < (:<) (Store s) u a) < Store s a
bring (TC (TUT (s :*: f))) = (((:*:) s :. (->) s) >>> a) -> Store s a
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) s :. (->) s) >>> a) -> Store s a)
-> (((:*:) s :. (->) s) >>> a) -> Store s a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- s
s s -> (s -> a) -> ((:*:) s :. (->) s) >>> a
forall s a. s -> a -> s :*: a
:*: u (s -> a) -> s -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract u (s -> a)
f

type Storable s t = Adaptable (Store s) (->) t

-- | Get current index
position :: Storable s t => t a -> s
position :: t a -> s
position = (s :*: (s -> a)) -> s
forall a b. (a :*: b) -> a
attached ((s :*: (s -> a)) -> s) -> (t a -> s :*: (s -> a)) -> t a -> s
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a.
Interpreted (->) (Store s) =>
((->) < Store s a) < Primary (Store s) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run @(->) @(Store _) (Store s a -> s :*: (s -> a))
-> (t a -> Store s a) -> t a -> s :*: (s -> a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. t a -> Store s a
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

-- | Given an index return value
look :: Storable s t => s -> a <:= t
look :: s -> a <:= t
look s
s = ((s :*: (s -> a)) -> s -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((s :*: (s -> a)) -> s -> a) -> s -> (s :*: (s -> a)) -> a
forall a b c. (a -> b -> c) -> b -> a -> c
% s
s) ((s :*: (s -> a)) -> a) -> (t a -> s :*: (s -> a)) -> a <:= t
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a.
Interpreted (->) (Store s) =>
((->) < Store s a) < Primary (Store s) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run @(->) @(Store _) (Store s a -> s :*: (s -> a))
-> (t a -> Store s a) -> t a -> s :*: (s -> a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. t a -> Store s a
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

-- | Change index with function
retrofit :: (s -> s) -> Store s ~> Store s
retrofit :: (s -> s) -> Store s ~> Store s
retrofit s -> s
g (Store (s
s :*: s -> a
f)) = (s :*: (s -> a)) -> Store s a
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((s :*: (s -> a)) -> Store s a) -> (s :*: (s -> a)) -> Store s a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- s -> s
g s
s s -> (s -> a) -> s :*: (s -> a)
forall s a. s -> a -> s :*: a
:*: s -> a
f