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

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

import Pandora.Core.Functor (type (~>))
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), Simplification)
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe)
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic.Exponential ((%), type (<--))
import Pandora.Paradigm.Primary.Algebraic (Pointable, extract)
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (!))
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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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

class Zoomable (tool :: * -> * -> *) (available :: * -> *) where
	zoom :: forall bg ls t . Adaptable t (->) (tool bg) => Lens available bg ls -> tool (Simplification available ls) ~> t

instance Zoomable State Exactly where
	zoom :: forall bg ls t result . Stateful bg t => Convex Lens bg ls -> State ls result -> t result
	zoom :: Convex Lens bg ls -> State ls result -> t result
zoom Convex Lens bg ls
lens State ls result
less = State bg result -> t result
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 (State bg result -> t result)
-> ((((->) bg :. (:*:) bg) := result) -> State bg result)
-> (((->) bg :. (:*:) bg) := result)
-> t result
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (((->) bg :. (:*:) bg) := result) -> State bg result
forall s a. (((->) s :. (:*:) s) := a) -> State s a
State ((((->) bg :. (:*:) bg) := result) -> t result)
-> (((->) bg :. (:*:) bg) := result) -> t result
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \bg
source -> (Exactly ls -> bg) -> Exactly ls -> bg :*: result
restruct ((Exactly ls -> bg) -> Exactly ls -> bg :*: result)
-> (Exactly ls :*: (Exactly 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 (Exactly ls) bg -> Exactly ls :*: (Exactly ls -> bg)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Lens Exactly bg ls
Convex Lens bg ls
lens Lens Exactly bg ls -> bg -> Store (Exactly ls) bg
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! bg
source) where

		restruct :: (Exactly ls -> bg) -> Exactly ls -> bg :*: result
		restruct :: (Exactly ls -> bg) -> Exactly ls -> bg :*: result
restruct Exactly ls -> bg
to (Exactly ls
target) = Flip (:*:) result bg -> bg :*: result
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)
# Exactly ls -> bg
to (Exactly ls -> bg) -> (ls -> Exactly ls) -> ls -> bg
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ls -> Exactly ls
forall a. a -> Exactly a
Exactly (ls -> bg) -> Flip (:*:) result ls -> Flip (:*:) result bg
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (ls :*: result) -> Flip (:*:) result ls
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (State ls result
less State ls result -> ((->) ls :. (:*:) ls) := result
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! ls
target)

instance Zoomable State Maybe where
	zoom :: forall bg ls t result . Stateful bg t => Obscure Lens bg ls -> State (Maybe ls) result -> t result
	zoom :: Obscure Lens bg ls -> State (Maybe ls) result -> t result
zoom Obscure Lens bg ls
lens State (Maybe ls) result
less = State bg result -> t result
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 (State bg result -> t result)
-> ((((->) bg :. (:*:) bg) := result) -> State bg result)
-> (((->) bg :. (:*:) bg) := result)
-> t result
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (((->) bg :. (:*:) bg) := result) -> State bg result
forall s a. (((->) s :. (:*:) s) := a) -> State s a
State ((((->) bg :. (:*:) bg) := result) -> t result)
-> (((->) bg :. (:*:) bg) := result) -> t result
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \bg
source -> (Maybe ls -> bg) -> Maybe ls -> bg :*: result
restruct ((Maybe ls -> bg) -> Maybe ls -> bg :*: result)
-> (Maybe ls :*: (Maybe 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 (Maybe ls) bg -> Maybe ls :*: (Maybe ls -> bg)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Lens Maybe bg ls
Obscure Lens bg ls
lens Lens Maybe bg ls -> bg -> Store (Maybe ls) bg
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! bg
source) where

		restruct :: (Maybe ls -> bg) -> Maybe ls -> bg :*: result
		restruct :: (Maybe ls -> bg) -> Maybe ls -> bg :*: result
restruct Maybe ls -> bg
to Maybe ls
target = Flip (:*:) result bg -> bg :*: result
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Maybe ls -> bg
to (Maybe ls -> bg)
-> Flip (:*:) result (Maybe ls) -> Flip (:*:) result bg
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-- (Maybe ls :*: result) -> Flip (:*:) result (Maybe ls)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Maybe ls :*: result) -> Flip (:*:) result (Maybe ls))
-> (Maybe ls :*: result) -> Flip (:*:) result (Maybe ls)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- State (Maybe ls) result
-> ((->) (Maybe ls) :. (:*:) (Maybe ls)) := result
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run State (Maybe ls) result
less Maybe 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (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)