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

module Pandora.Paradigm.Inventory (module Exports, zoom) where

import Pandora.Paradigm.Inventory.Optics as Exports
import Pandora.Paradigm.Inventory.Store as Exports
import Pandora.Paradigm.Inventory.State as Exports
import Pandora.Paradigm.Inventory.Imprint as Exports
import Pandora.Paradigm.Inventory.Equipment as Exports
import Pandora.Paradigm.Inventory.Environment as Exports
import Pandora.Paradigm.Inventory.Accumulator as Exports

import Pandora.Core.Morphism ((!), (%))
import Pandora.Pattern.Category ((.), ($), identity)
import Pandora.Pattern.Functor (Adjoint ((-|), (|-)), extract, (<->))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)
import Pandora.Paradigm.Controlflow.Effect.Adaptable (adapt)

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

instance Adjoint (Accumulator e) (Imprint e) where
	a
x -| :: a -> (Accumulator e a -> b) -> Imprint e b
-| Accumulator e a -> b
f = (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 a b -> m a b
$ a
x a -> (Product e a -> b) -> e -> b
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
a -> (t a -> b) -> u b
-| Accumulator e a -> b
f (Accumulator e a -> b)
-> (Product e a -> Accumulator e a) -> Product e a -> b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product e a -> Accumulator e a
forall e a. (e :*: a) -> Accumulator e a
Accumulator
	Accumulator e a
x |- :: Accumulator e a -> (a -> Imprint e b) -> b
|- a -> Imprint e b
g = Accumulator e a -> Primary (Accumulator e) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Accumulator e a
x (e :*: a) -> (a -> e -> b) -> b
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
t a -> (a -> u b) -> b
|- Imprint e b -> e -> b
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Imprint e b -> e -> b) -> (a -> Imprint e b) -> a -> e -> b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Imprint e b
g

instance Adjoint (Equipment e) (Environment e) where
	a
x -| :: a -> (Equipment e a -> b) -> Environment e b
-| Equipment e a -> b
f = (e -> b) -> Environment e b
forall e a. (e -> a) -> Environment e a
Environment ((e -> b) -> Environment e b) -> (e -> b) -> Environment e b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a
x a -> (Product e a -> b) -> e -> b
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
a -> (t a -> b) -> u b
-| Equipment e a -> b
f (Equipment e a -> b)
-> (Product e a -> Equipment e a) -> Product e a -> b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product e a -> Equipment e a
forall e a. (e :*: a) -> Equipment e a
Equipment
	Equipment e a
x |- :: Equipment e a -> (a -> Environment e b) -> b
|- a -> Environment e b
g = Equipment e a -> Primary (Equipment e) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Equipment e a
x (e :*: a) -> (a -> e -> b) -> b
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
t a -> (a -> u b) -> b
|- Environment e b -> e -> b
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Environment e b -> e -> b)
-> (a -> Environment e b) -> a -> e -> b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Environment e b
g

zoom :: Stateful bg t => Lens bg ls -> State ls a -> t a
zoom :: Lens bg ls -> State ls a -> t a
zoom Lens bg ls
lens (State ((->) ls :. (:*:) ls) := a
f) = State bg a -> t a
forall k (t :: k -> *) (u :: k -> *). Adaptable t u => t ~> u
adapt (State bg a -> t a)
-> ((((->) bg :. (:*:) bg) := a) -> State bg a)
-> (((->) bg :. (:*:) bg) := a)
-> t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (((->) bg :. (:*:) bg) := a) -> State bg a
forall s a. (((->) s :. (:*:) s) := a) -> State s a
State ((((->) bg :. (:*:) bg) := a) -> t a)
-> (((->) bg :. (:*:) bg) := a) -> t a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (\(Store (ls
p :*: ls -> bg
g)) -> (ls -> bg
g (ls -> bg) -> (a -> a) -> Product ls a -> Product bg a
forall (v :: * -> * -> *) a b c d.
Bivariant v =>
(a -> b) -> (c -> d) -> v a c -> v b d
<-> a -> a
forall (m :: * -> * -> *) a. Category m => m a a
identity) (Product ls a -> Product bg a)
-> (((->) ls :. (:*:) ls) := a) -> ls -> Product bg a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((->) ls :. (:*:) ls) := a
f (ls -> Product bg a) -> ls -> Product bg a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ ls
p) (Store ls bg -> Product bg a)
-> Lens bg ls -> ((->) bg :. (:*:) bg) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Lens bg ls
lens