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

module Pandora.Paradigm.Inventory.Store where

import Pandora.Core (type (:.), type (:=), 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.Extractable (Extractable (extract))
import Pandora.Pattern.Functor.Extendable (Extendable ((<<=)))
import Pandora.Pattern.Functor.Comonad (Comonad)
import Pandora.Pattern.Functor.Bivariant ((<->))
import Pandora.Pattern.Functor.Divariant ((>->))
import Pandora.Pattern.Functor.Adjoint ((-|), (|-))
import Pandora.Paradigm.Primary.Algebraic.Exponential ((%), (-.#..-))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), attached)
import Pandora.Paradigm.Primary.Algebraic ()
import Pandora.Paradigm.Primary.Transformer.Flip (Flip (Flip))
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.Comonadic (Comonadic (bring), (:<) (TC))
import Pandora.Paradigm.Schemes.TUT (TUT (TUT), type (<:<.>:>))

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

instance Covariant (Store s) (->) (->) where
	a -> b
f -<$>- :: (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)
$ a -> b
f (a -> b) -> (((:*:) s :. (->) s) := a) -> ((:*:) s :. (->) s) := b
forall (t :: * -> *) (u :: * -> *) (category :: * -> * -> *) a b.
(Covariant u category category, Covariant t category category) =>
category a b -> category (t (u a)) (t (u b))
-<$$>- ((:*:) s :. (->) s) := a
x

instance Extractable (Store s) (->) where
	extract :: Store s a -> a
extract = ((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 (t :: * -> *) (u :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Adjoint t u source target =>
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 (t :: * -> *) a. Interpreted t => t a -> Primary t a
run

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 (t :: * -> *) (u :: * -> *) (category :: * -> * -> *) a b.
(Covariant u category category, Covariant t category category) =>
category a b -> category (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 (v :: * -> * -> *) a (target :: * -> * -> *) c d b.
(Covariant (v a) (->) target, 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 (t :: * -> *) (u :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Adjoint t u source target =>
source (t a) b -> target a (u b)
-|) ((s -> a) -> s -> Store s a)
-> (((:*:) s :. (->) s) := a) -> s :*: (s -> Store s a)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
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 = \(Flip Store a r
x) -> Store b r -> Flip Store r b
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (Store b r -> Flip Store r b) -> Store b r -> Flip Store r b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (a -> b)
-> ((a -> r) -> b -> r) -> (a :*: (a -> r)) -> b :*: (b -> r)
forall (v :: * -> * -> *) (left :: * -> * -> *)
       (right :: * -> * -> *) (target :: * -> * -> *) a b c d.
Bivariant v left right target =>
left a b -> right c d -> target (v a c) (v b d)
(<->) @_ @_ @(->) a -> b
f (b -> a
g (b -> a) -> (r -> r) -> (a -> r) -> b -> r
forall (v :: * -> * -> *) (left :: * -> * -> *)
       (right :: * -> * -> *) (target :: * -> * -> *) a b c d.
Divariant v left right target =>
left a b -> right c d -> target (v b c) (v a d)
>-> forall a. Category (->) => a -> a
forall (m :: * -> * -> *) a. Category m => m a a
identity @(->)) (Primary (Store a) r -> Primary (Store b) r)
-> Store a r -> Store b r
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||= Store a r
x

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) ~> Store s
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 :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract u (s -> a)
f

type Storable s x = Adaptable x (Store s)

-- | 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 (t :: * -> *) a. Interpreted t => 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 (t :: k -> *) (u :: k -> *). Adaptable t u => t ~> u
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 :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (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 (t :: * -> *) a. Interpreted t => 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 (t :: k -> *) (u :: k -> *). Adaptable t u => t ~> u
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