{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Inventory (module Exports, zoom, overlook, (=<>), (~<>)) where

import Pandora.Paradigm.Inventory.Ability as Exports
import Pandora.Paradigm.Inventory.Some as Exports

import Pandora.Core.Functor (type (~>))
import Pandora.Core.Interpreted (run, (<~))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----))
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|--)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Adjoint (Adjoint ((-|), (--|), (|-), (|--)))
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe)
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Algebraic.Exponential ((%), type (<--))
import Pandora.Paradigm.Algebraic (Pointable, extract)
import Pandora.Paradigm.Primary (Simplification)
import Pandora.Paradigm.Controlflow.Effect.Adaptable (Adaptable (adapt))

instance Adjoint (->) (->) (Store s) (State s) where
	(-|) :: (Store s a -> b) -> a -> State s b
	Store s a -> b
f -| :: (Store s a -> b) -> a -> State s b
-| 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 (m a b) (m a b)
<-- \s
s -> s -> b -> s :*: b
forall s a. s -> a -> s :*: a
(:*:) s
s (b -> s :*: b)
-> ((s :*: (s -> a)) -> b) -> (s :*: (s -> a)) -> s :*: b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Store s a -> b
f (Store s a -> b)
-> ((s :*: (s -> a)) -> Store s a) -> (s :*: (s -> a)) -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (s :*: (s -> a)) -> Store s a
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((s :*: (s -> a)) -> s :*: b) -> (s :*: (s -> a)) -> s :*: b
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
:*: a -> s -> a
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant a
x
	(|-) :: (a -> State s b) -> Store s a -> b
	a -> State s b
g |- :: (a -> State s b) -> Store s a -> b
|- Store (s
s :*: s -> a
f) = (s :*: b) -> b
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((s :*: b) -> b) -> (a -> s :*: b) -> a -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (State s b -> ((->) s :. (:*:) s) >>> b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (State s b -> ((->) s :. (:*:) s) >>> b)
-> s -> State s b -> s :*: b
forall a b c. (a -> b -> c) -> b -> a -> c
% s
s) (State s b -> s :*: b) -> (a -> State s b) -> a -> s :*: b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> State s b
g (a -> b) -> a -> b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- s -> a
f s
s

instance Adjoint (->) (->) (Accumulator e) (Imprint e) where
	Accumulator e a -> b
f -| :: (Accumulator e a -> b) -> a -> Imprint e b
-| a
x = (e -> b) -> Imprint e b
forall e a. (e -> a) -> Imprint e a
Imprint ((e -> b) -> Imprint e b) -> (e -> b) -> Imprint e b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Accumulator e a -> b
f (Accumulator e a -> b)
-> ((e :*: a) -> Accumulator e a) -> (e :*: a) -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (e :*: a) -> Accumulator e a
forall e a. (e :*: a) -> Accumulator e a
Accumulator ((e :*: a) -> b) -> a -> e -> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
source (t a) b -> target a (u b)
--| a
x
	a -> Imprint e b
g |- :: (a -> Imprint e b) -> Accumulator e a -> b
|- Accumulator e a
x = Imprint e b -> e -> b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Imprint e b -> e -> b) -> (a -> Imprint e b) -> a -> e -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Imprint e b
g (a -> e -> b) -> (e :*: a) -> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
|-- Accumulator e a -> e :*: a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run Accumulator e a
x

instance Adjoint (->) (->) (Equipment e) (Provision e) where
	Equipment e a -> b
f -| :: (Equipment e a -> b) -> a -> Provision e b
-| a
x = (e -> b) -> Provision e b
forall e a. (e -> a) -> Provision e a
Provision ((e -> b) -> Provision e b) -> (e -> b) -> Provision e b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Equipment e a -> b
f (Equipment e a -> b)
-> ((e :*: a) -> Equipment e a) -> (e :*: a) -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (e :*: a) -> Equipment e a
forall e a. (e :*: a) -> Equipment e a
Equipment ((e :*: a) -> b) -> a -> e -> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
source (t a) b -> target a (u b)
--| a
x
	a -> Provision e b
g |- :: (a -> Provision e b) -> Equipment e a -> b
|- Equipment e a
x = Provision e b -> e -> b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Provision e b -> e -> b) -> (a -> Provision e b) -> a -> e -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Provision e b
g (a -> e -> b) -> (e :*: a) -> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
|-- Equipment e a -> e :*: a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run Equipment e a
x

zoom :: forall bg ls u result . Lens u bg ls -> State (u ls) result -> State bg result
zoom :: Lens u bg ls -> State (u ls) result -> State bg result
zoom Lens u bg ls
lens State (u ls) result
less = (((->) bg :. (:*:) bg) >>> result) -> State bg result
forall s a. (((->) s :. (:*:) s) >>> a) -> State s a
State ((((->) bg :. (:*:) bg) >>> result) -> State bg result)
-> (((->) bg :. (:*:) bg) >>> result) -> State bg result
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \bg
source -> (u ls -> bg) -> u ls -> bg :*: result
restruct ((u ls -> bg) -> u ls -> bg :*: result)
-> (u ls :*: (u ls -> bg)) -> bg :*: result
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
Adjoint source target t u =>
target a (u b) -> source (t a) b
|- Store (u ls) bg -> u ls :*: (u ls -> bg)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Lens u bg ls
lens Lens u bg ls -> bg -> Store (u ls) bg
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ bg
source) where

	restruct :: (u ls -> bg) -> u ls -> bg :*: result
	restruct :: (u ls -> bg) -> u ls -> bg :*: result
restruct u ls -> bg
to u ls
target = forall (t :: * -> *) a.
Interpreted (->) t =>
((->) < t a) < Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run @(->) (Flip (:*:) result bg -> bg :*: result)
-> Flip (:*:) result bg -> bg :*: result
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- u ls -> bg
to (u ls -> bg) -> Flip (:*:) result (u ls) -> Flip (:*:) result bg
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (u ls :*: result) -> Flip (:*:) result (u ls)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (State (u ls) result
less State (u ls) result -> ((->) (u ls) :. (:*:) (u ls)) >>> result
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ u ls
target)

overlook :: (Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:*:) t) => State s result -> State (t s) (t result)
overlook :: State s result -> State (t s) (t result)
overlook (State ((->) s :. (:*:) s) >>> result
state) = (((->) (t s) :. (:*:) (t s)) >>> t result)
-> State (t s) (t result)
forall s a. (((->) s :. (:*:) s) >>> a) -> State s a
State ((((->) (t s) :. (:*:) (t s)) >>> t result)
 -> State (t s) (t result))
-> (((->) (t s) :. (:*:) (t s)) >>> t result)
-> State (t s) (t result)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \t s
ts -> forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (t :: * -> *) a b.
Semimonoidal (<--) (:*:) (:*:) t =>
(t a :*: t b) <-- t (a :*: b)
mult @(<--) @(:*:) @(:*:) ((t s :*: t result) <-- t (s :*: result))
-> t (s :*: result) -> t s :*: t result
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ (((->) s :. (:*:) s) >>> result
state (((->) s :. (:*:) s) >>> result) -> t s -> t (s :*: result)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t s
ts)

(=<>) :: (Pointable available, Stateful src t)
	=> Lens available src tgt -> tgt -> t src
Lens available src tgt
lens =<> :: Lens available src tgt -> tgt -> t src
=<> tgt
new = ((->) < State src src) < t src
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 (forall e r. Modifiable State => Modification State e r
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @State ((src -> src) -> State src src) -> (src -> src) -> State src src
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- tgt -> Lens available src tgt -> src -> src
forall k (i :: k) e r. Settable i => Setting i e r
set @(Lens _) tgt
new Lens available src tgt
lens)

(~<>) :: (Pointable available, Covariant (->) (->) available, Gettable (Lens available), Stateful src t)
	=> Lens available src tgt -> (tgt -> tgt) -> t src
Lens available src tgt
lens ~<> :: Lens available src tgt -> (tgt -> tgt) -> t src
~<> tgt -> tgt
f = ((->) < State src src) < t src
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 (forall e r. Modifiable State => Modification State e r
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @State ((src -> src) -> State src src) -> (src -> src) -> State src src
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (tgt -> tgt) -> Lens available src tgt -> src -> src
forall k (i :: k) e r. Modifiable i => Modification i e r
modify @(Lens _) tgt -> tgt
f Lens available src tgt
lens)