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

module Pandora.Paradigm.Inventory (module Exports, zoom, magnify, (=<>), (~<>), adjust) 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.Functor (type (~>))
import Pandora.Pattern.Category ((.), ($), (/), identity)
import Pandora.Pattern.Functor.Adjoint (Adjoint ((-|), (|-)))
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Functor.Bivariant ((<->))
import Pandora.Paradigm.Primary.Functor.Function ((!), (%))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)
import Pandora.Paradigm.Controlflow.Effect.Adaptable (adapt)
import Pandora.Paradigm.Structure.Ability.Accessible (Accessible (access))

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 :: * -> * -> *). Category m => m ~~> m
$ \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 s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) s :. (->) s) := a) -> Product s b)
-> (((:*:) s :. (->) s) := a) -> Product s b
forall (m :: * -> * -> *). Category m => m ~~> m
$ 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 :: * -> * -> *). Category m => m ~~> m
$ 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 :: * -> * -> *). Category m => m ~~> m
$ 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 :: * -> * -> *). Category m => m ~~> m
$ 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 ~> t
zoom :: Lens bg ls -> State ls ~> t
zoom Lens bg ls
lens State ls a
less = let restruct :: (ls -> bg) -> ls -> Product bg a
restruct ls -> bg
f ls
v = ls -> bg
f (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) -> Product ls a -> Product bg a
forall (m :: * -> * -> *). Category m => m ~~> m
$ State ls a -> ((->) ls :. (:*:) ls) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run State ls a
less ls
v
	in 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 :: * -> * -> *). Category m => m ~~> m
$ (Product ls (ls -> bg)
-> ((ls -> bg) -> ls -> Product bg a) -> Product bg a
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
t a -> (a -> u b) -> b
|- (ls -> bg) -> ls -> Product bg a
restruct) (Product ls (ls -> bg) -> Product bg a)
-> (bg -> Product ls (ls -> bg)) -> ((->) bg :. (:*:) bg) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Store ls bg -> Product ls (ls -> bg)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Store ls bg -> Product ls (ls -> bg))
-> Lens bg ls -> bg -> Product ls (ls -> bg)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Lens bg ls
lens

(=<>) :: Stateful src t => src :-. tgt -> tgt -> t src
src :-. tgt
lens =<> :: (src :-. tgt) -> tgt -> t src
=<> tgt
new = (src -> src) -> t src
forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
modify ((src -> src) -> t src) -> (src -> src) -> t src
forall (m :: * -> * -> *). Category m => m ~~> m
$ (src :-. tgt) -> tgt -> src -> src
forall src tgt. Lens src tgt -> tgt -> src -> src
set src :-. tgt
lens tgt
new

(~<>) :: Stateful src t => src :-. tgt -> (tgt -> tgt) -> t src
src :-. tgt
lens ~<> :: (src :-. tgt) -> (tgt -> tgt) -> t src
~<> tgt -> tgt
f = (src -> src) -> t src
forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
modify ((src -> src) -> t src) -> (src -> src) -> t src
forall (m :: * -> * -> *). Category m => m ~~> m
$ (src :-. tgt) -> (tgt -> tgt) -> src -> src
forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src
over src :-. tgt
lens tgt -> tgt
f

magnify :: forall bg ls t . (Accessible ls bg, Stateful bg t) => t ls
magnify :: t ls
magnify = forall bg (t :: * -> *) ls.
Stateful bg t =>
Lens bg ls -> State ls ~> t
forall (t :: * -> *) ls.
Stateful bg t =>
Lens bg ls -> State ls ~> t
zoom @bg (Lens bg ls -> State ls ls -> t ls)
-> Lens bg ls -> State ls ls -> t ls
forall (m :: * -> * -> *). Category m => m ~~> m
/ Accessible ls bg => Lens bg ls
forall tgt src. Accessible tgt src => src :-. tgt
access @ls @bg (State ls ls -> t ls) -> State ls ls -> t ls
forall (m :: * -> * -> *). Category m => m ~~> m
/ State ls ls
forall s (t :: * -> *). Stateful s t => t s
current

adjust :: forall bg ls t . (Accessible ls bg, Stateful bg t) => (ls -> ls) -> t ls
adjust :: (ls -> ls) -> t ls
adjust = Lens bg ls -> State ls ~> t
forall bg (t :: * -> *) ls.
Stateful bg t =>
Lens bg ls -> State ls ~> t
zoom @bg (Accessible ls bg => Lens bg ls
forall tgt src. Accessible tgt src => src :-. tgt
access @ls @bg) (State ls ls -> t ls)
-> ((ls -> ls) -> State ls ls) -> (ls -> ls) -> t ls
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (ls -> ls) -> State ls ls
forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
modify