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

module Pandora.Paradigm.Inventory.Store where

import Pandora.Core (type (:.), type (:=), type (<-|), type (~>), (%))
import Pandora.Pattern ((.|..))
import Pandora.Pattern.Category (identity, (.), ($))
import Pandora.Pattern.Functor (Covariant ((<$>), (<$$>), (<$$$>)), Extractable (extract), Extendable ((=>>), (<<=$)), Comonad, (-|), (|-))
import Pandora.Paradigm.Primary.Functor (Product ((:*:)), type (:*:), attached)
import Pandora.Paradigm.Controlflow (Adaptable (adapt), Interpreted (Primary, run), Schematic, Comonadic (bring), (:<) (TC))
import Pandora.Paradigm.Schemes.TUT (TUT (TUT), type (<:<.>:>))

newtype Store p a = Store ((:*:) p :. (->) p := a)

instance Covariant (Store p) where
	a -> b
f <$> :: (a -> b) -> Store p a -> Store p b
<$> Store ((:*:) p :. (->) p) := a
x = (((:*:) p :. (->) p) := b) -> Store p b
forall p a. (((:*:) p :. (->) p) := a) -> Store p a
Store ((((:*:) p :. (->) p) := b) -> Store p b)
-> (((:*:) p :. (->) p) := b) -> Store p b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a -> b
f (a -> b) -> (((:*:) p :. (->) p) := a) -> ((:*:) p :. (->) p) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
<$$> ((:*:) p :. (->) p) := a
x

instance Extractable (Store p) where
	extract :: a <-| Store p
extract = (Product p (p -> a) -> ((p -> a) -> p -> a) -> a
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
t a -> (a -> u b) -> b
|- (p -> a) -> p -> a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
($)) (Product p (p -> a) -> a)
-> (Store p a -> Product p (p -> a)) -> a <-| Store p
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Store p a -> Product p (p -> a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run

instance Extendable (Store p) where
	Store ((:*:) p :. (->) p) := a
x =>> :: Store p a -> (Store p a -> b) -> Store p b
=>> Store p a -> b
f = (((:*:) p :. (->) p) := b) -> Store p b
forall p a. (((:*:) p :. (->) p) := a) -> Store p a
Store ((((:*:) p :. (->) p) := b) -> Store p b)
-> (((:*:) p :. (->) p) := b) -> Store p b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Store p a -> b
f (Store p a -> b)
-> (((->) (p -> a) :. (->) p) := Store p a)
-> ((->) (p -> a) :. (->) p) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
<$$> ((((:*:) p :. (->) p) := a) -> Store p a
forall p a. (((:*:) p :. (->) p) := a) -> Store p a
Store ((((:*:) p :. (->) p) := a) -> Store p a)
-> (((->) (p -> a) :. (->) p) := (((:*:) p :. (->) p) := a))
-> ((->) (p -> a) :. (->) p) := Store p a
forall (v :: * -> * -> *) a c d b.
(Category v, Covariant (v a)) =>
v c d -> ((v a :. v b) := c) -> (v a :. v b) := d
.|.. ((p -> a)
-> ((((:*:) p :. (->) p) := a) -> ((:*:) p :. (->) p) := a)
-> p
-> ((:*:) p :. (->) p) := a
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
a -> (t a -> b) -> u b
-| (((:*:) p :. (->) p) := a) -> ((:*:) p :. (->) p) := a
forall (m :: * -> * -> *) a. Category m => m a a
identity)) (((->) (p -> a) :. (->) p) := b)
-> (((:*:) p :. (->) p) := a) -> ((:*:) p :. (->) p) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> ((:*:) p :. (->) p) := a
x

instance Comonad (Store p) where

instance Interpreted (Store p) where
	type Primary (Store p) a = (:*:) p :. (->) p := a
	run :: Store p a -> Primary (Store p) a
run ~(Store ((:*:) p :. (->) p) := a
x) = Primary (Store p) a
((:*:) p :. (->) p) := a
x

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

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

type Storable s x = Adaptable x (Store s)

instance Covariant u => Covariant ((:*:) p <:<.>:> (->) p := u) where
	a -> b
f <$> :: (a -> b)
-> (:=) ((:*:) p <:<.>:> (->) p) u a
-> (:=) ((:*:) p <:<.>:> (->) p) u b
<$> TUT ((:*:) p :. (u :. (->) p)) := a
x = (((:*:) p :. (u :. (->) p)) := b)
-> (:=) ((:*:) p <:<.>:> (->) p) 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 ((((:*:) p :. (u :. (->) p)) := b)
 -> (:=) ((:*:) p <:<.>:> (->) p) u b)
-> (((:*:) p :. (u :. (->) p)) := b)
-> (:=) ((:*:) p <:<.>:> (->) p) u b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a -> b
f (a -> b)
-> (((:*:) p :. (u :. (->) p)) := a)
-> ((:*:) p :. (u :. (->) p)) := b
forall (t :: * -> *) (u :: * -> *) (v :: * -> *) a b.
(Covariant t, Covariant u, Covariant v) =>
(a -> b) -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b
<$$$> ((:*:) p :. (u :. (->) p)) := a
x

instance Extractable u => Extractable ((:*:) p <:<.>:> (->) p := u) where
	extract :: a <-| (((:*:) p <:<.>:> (->) p) := u)
extract = (Product p (u (p -> a)) -> (u (p -> a) -> p -> a) -> a
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
t a -> (a -> u b) -> b
|- u (p -> a) -> p -> a
forall (t :: * -> *) a. Extractable t => a <-| t
extract) (Product p (u (p -> a)) -> a)
-> (TUT Covariant Covariant Covariant ((:*:) p) ((->) p) u a
    -> Product p (u (p -> a)))
-> a <-| (((:*:) p <:<.>:> (->) p) := u)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TUT Covariant Covariant Covariant ((:*:) p) ((->) p) u a
-> Product p (u (p -> a))
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run

instance Extendable u => Extendable ((:*:) p <:<.>:> (->) p := u) where
	TUT ((:*:) p :. (u :. (->) p)) := a
x =>> :: (:=) ((:*:) p <:<.>:> (->) p) u a
-> ((:=) ((:*:) p <:<.>:> (->) p) u a -> b)
-> (:=) ((:*:) p <:<.>:> (->) p) u b
=>> (:=) ((:*:) p <:<.>:> (->) p) u a -> b
f = (((:*:) p :. (u :. (->) p)) := b)
-> (:=) ((:*:) p <:<.>:> (->) p) 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 ((((:*:) p :. (u :. (->) p)) := b)
 -> (:=) ((:*:) p <:<.>:> (->) p) u b)
-> (((:*:) p :. (u :. (->) p)) := b)
-> (:=) ((:*:) p <:<.>:> (->) p) u b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ ((:*:) p :. (u :. (->) p)) := a
x (((:*:) p :. (u :. (->) p)) := a)
-> (u (p -> a) -> p -> b) -> ((:*:) p :. (u :. (->) p)) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Extendable t, Covariant u) =>
((u :. t) := a) -> (t a -> b) -> (u :. t) := b
<<=$ (\u (p -> a)
x' -> (:=) ((:*:) p <:<.>:> (->) p) u a -> b
f ((:=) ((:*:) p <:<.>:> (->) p) u a -> b)
-> (p -> (:=) ((:*:) p <:<.>:> (->) p) u a) -> p -> b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (((:*:) p :. (u :. (->) p)) := a)
-> (:=) ((:*:) p <:<.>:> (->) p) 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 ((((:*:) p :. (u :. (->) p)) := a)
 -> (:=) ((:*:) p <:<.>:> (->) p) u a)
-> (p -> ((:*:) p :. (u :. (->) p)) := a)
-> p
-> (:=) ((:*:) p <:<.>:> (->) p) u a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (u (p -> a)
x' u (p -> a)
-> ((((:*:) p :. (u :. (->) p)) := a)
    -> ((:*:) p :. (u :. (->) p)) := a)
-> p
-> ((:*:) p :. (u :. (->) p)) := a
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
a -> (t a -> b) -> u b
-| (((:*:) p :. (u :. (->) p)) := a)
-> ((:*:) p :. (u :. (->) p)) := a
forall (m :: * -> * -> *) a. Category m => m a a
identity))

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.
Category 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.
Category 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

access :: Storable s t => s -> a <-| t
access :: s -> a <-| t
access s
p = (s -> a) <-| Product s
forall (t :: * -> *) a. Extractable t => a <-| t
extract ((s -> a) <-| Product s) -> s -> Product s (s -> a) -> a
forall a b c. (a -> b -> c) -> b -> a -> c
% s
p (Product s (s -> a) -> a) -> (t a -> Product s (s -> a)) -> a <-| t
forall (m :: * -> * -> *) b c a.
Category 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 -> Product s (s -> a))
-> (t a -> Store s a) -> t a -> Product s (s -> a)
forall (m :: * -> * -> *) b c a.
Category 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

retrofit :: (p -> p) -> Store p ~> Store p
retrofit :: (p -> p) -> Store p ~> Store p
retrofit p -> p
g (Store (p
p :*: p -> a
f)) = Product p (p -> a) -> Store p a
forall p a. (((:*:) p :. (->) p) := a) -> Store p a
Store (Product p (p -> a) -> Store p a)
-> Product p (p -> a) -> Store p a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ p -> p
g p
p p -> (p -> a) -> Product p (p -> a)
forall s a. s -> a -> Product s a
:*: p -> a
f