{-# 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 (Covariant ((<$>), (<$$>)))
import Pandora.Pattern.Functor.Extractable (Extractable (extract))
import Pandora.Pattern.Functor.Extendable (Extendable ((=>>)))
import Pandora.Pattern.Functor.Comonad (Comonad)
import Pandora.Pattern.Functor.Adjoint ((-|), (|-))
import Pandora.Paradigm.Primary.Functor (Product ((:*:)), type (:*:), attached)
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 a b -> m a b
$ a -> b
f (a -> b) -> (((:*:) s :. (->) s) := a) -> ((:*:) s :. (->) s) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
<$$> ((:*:) s :. (->) s) := a
x

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

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

instance Comonad (Store s) where

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) = ((:*:) s :. (->) s) := a
Primary (Store 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 a b -> m a b
$ s
s s -> (s -> a) -> ((:*:) s :. (->) s) := a
forall s a. s -> a -> Product s a
:*: (s -> a) <-| u
forall (t :: * -> *) a. Extractable t => a <-| t
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.
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

-- | Given an index return value
access :: Storable s t => s -> a <-| t
access :: s -> a <-| t
access s
s = (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
s (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

-- | 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)) = Product s (s -> a) -> Store s a
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store (Product s (s -> a) -> Store s a)
-> Product s (s -> a) -> Store s a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ s -> s
g s
s s -> (s -> a) -> Product s (s -> a)
forall s a. s -> a -> Product s a
:*: s -> a
f