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

module Pandora.Paradigm.Inventory.Optics where

import Pandora.Core.Impliable (Impliable (Arguments, imply))
import Pandora.Pattern.Semigroupoid (Semigroupoid ((.)))
import Pandora.Pattern.Category (Category (identity, ($), (#)))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
import Pandora.Pattern.Functor.Invariant (Invariant ((<$<)))
import Pandora.Pattern.Functor.Divariant ((>->))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Representable (Representable (Representation, (<#>), tabulate))
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (run))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic.Exponential (type (-->), (!.), (%))
import Pandora.Paradigm.Primary.Algebraic (extract)
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Paradigm.Primary.Object.Boolean ((?))
import Pandora.Paradigm.Inventory.Store (Store (Store), position, look, retrofit)
import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))
import Pandora.Paradigm.Structure.Ability.Monotonic (resolve)

infixl 2 #=@

type Lens = P_Q_T (->) Store

instance Invariant (Flip (Lens available) tgt) where
	a -> b
f <$< :: (a -> b)
-> (b -> a)
-> Flip (Lens available) tgt a
-> Flip (Lens available) tgt b
<$< b -> a
g = \(Flip (P_Q_T a -> Store (available tgt) a
lens)) -> Lens available b tgt -> Flip (Lens available) tgt b
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (Lens available b tgt -> Flip (Lens available) tgt b)
-> ((b -> Store (available tgt) b) -> Lens available b tgt)
-> (b -> Store (available tgt) b)
-> Flip (Lens available) tgt b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (b -> Store (available tgt) b) -> Lens available b tgt
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((b -> Store (available tgt) b) -> Flip (Lens available) tgt b)
-> (b -> Store (available tgt) b) -> Flip (Lens available) tgt b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ b -> a
g (b -> a)
-> (Store (available tgt) a -> Store (available tgt) b)
-> (a -> Store (available tgt) a)
-> b
-> Store (available tgt) b
forall (left :: * -> * -> *) (right :: * -> * -> *)
       (target :: * -> * -> *) (v :: * -> * -> *) a b c d.
Divariant left right target v =>
left a b -> right c d -> target (v b c) (v a d)
>-> (a -> b
f (a -> b) -> Store (available tgt) a -> Store (available tgt) b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) ((a -> Store (available tgt) a) -> b -> Store (available tgt) b)
-> (a -> Store (available tgt) a) -> b -> Store (available tgt) b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> Store (available tgt) a
lens

type family Convex lens where
	Convex Lens = Lens Identity

instance Semigroupoid (Lens Identity) where
	(.) :: Convex Lens between target -> Convex Lens source between -> Convex Lens source target
	P_Q_T to . :: Convex Lens between target
-> Convex Lens source between -> Convex Lens source target
. P_Q_T from = (source -> Store (Identity target) source)
-> P_Q_T (->) Store Identity source target
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((source -> Store (Identity target) source)
 -> P_Q_T (->) Store Identity source target)
-> (source -> Store (Identity target) source)
-> P_Q_T (->) Store Identity source target
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \source
source ->
		let (Identity between
between :*: Identity between -> source
bs) = Store (Identity between) source
-> Identity between :*: (Identity between -> source)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Store (Identity between) source
 -> Identity between :*: (Identity between -> source))
-> Store (Identity between) source
-> Identity between :*: (Identity between -> source)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# source -> Store (Identity between) source
from source
source in
		let (Identity target
target :*: Identity target -> between
tb) = Store (Identity target) between
-> Identity target :*: (Identity target -> between)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Store (Identity target) between
 -> Identity target :*: (Identity target -> between))
-> Store (Identity target) between
-> Identity target :*: (Identity target -> between)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# between -> Store (Identity target) between
to between
between in
		(((:*:) (Identity target) :. (->) (Identity target)) := source)
-> Store (Identity target) source
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity target) :. (->) (Identity target)) := source)
 -> Store (Identity target) source)
-> (((:*:) (Identity target) :. (->) (Identity target)) := source)
-> Store (Identity target) source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ target -> Identity target
forall a. a -> Identity a
Identity target
target Identity target
-> (Identity target -> source)
-> ((:*:) (Identity target) :. (->) (Identity target)) := source
forall s a. s -> a -> s :*: a
:*: Identity between -> source
bs (Identity between -> source)
-> (Identity target -> Identity between)
-> Identity target
-> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. between -> Identity between
forall a. a -> Identity a
Identity (between -> Identity between)
-> (Identity target -> between)
-> Identity target
-> Identity between
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity target -> between
tb

instance Category (Lens Identity) where
	identity :: Convex Lens source source
	identity :: Convex Lens source source
identity = (source -> source)
-> (source -> source -> source) -> Lens Identity source source
forall k (result :: k). Impliable result => Arguments result
imply @(Convex Lens _ _) source -> source
forall (m :: * -> * -> *) a. Category m => m a a
identity ((source -> source -> source) -> source -> source -> source
forall a b c. (a -> b -> c) -> b -> a -> c
(%) source -> source -> source
forall a b. a -> b -> a
(!.))

instance Semigroup source => Semimonoidal (-->) (:*:) (:*:) (Lens Identity source) where
	mult :: (Lens Identity source a :*: Lens Identity source b)
--> Lens Identity source (a :*: b)
mult = ((Lens Identity source a :*: Lens Identity source b)
 -> Lens Identity source (a :*: b))
-> (Lens Identity source a :*: Lens Identity source b)
   --> Lens Identity source (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Lens Identity source a :*: Lens Identity source b)
  -> Lens Identity source (a :*: b))
 -> (Lens Identity source a :*: Lens Identity source b)
    --> Lens Identity source (a :*: b))
-> ((Lens Identity source a :*: Lens Identity source b)
    -> Lens Identity source (a :*: b))
-> (Lens Identity source a :*: Lens Identity source b)
   --> Lens Identity source (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(P_Q_T source -> Store (Identity a) source
x :*: P_Q_T source -> Store (Identity b) source
y) -> (source -> Store (Identity (a :*: b)) source)
-> Lens Identity source (a :*: b)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((source -> Store (Identity (a :*: b)) source)
 -> Lens Identity source (a :*: b))
-> (source -> Store (Identity (a :*: b)) source)
-> Lens Identity source (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \source
source ->
		let Store (Identity a
xt :*: Identity a -> source
ixts) :*: Store (Identity b
yt :*: Identity b -> source
iyts) = source -> Store (Identity a) source
x source
source Store (Identity a) source
-> Store (Identity b) source
-> Store (Identity a) source :*: Store (Identity b) source
forall s a. s -> a -> s :*: a
:*: source -> Store (Identity b) source
y source
source in
		(((:*:) (Identity (a :*: b)) :. (->) (Identity (a :*: b)))
 := source)
-> Store (Identity (a :*: b)) source
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (a :*: b)) :. (->) (Identity (a :*: b)))
  := source)
 -> Store (Identity (a :*: b)) source)
-> (((:*:) (Identity (a :*: b)) :. (->) (Identity (a :*: b)))
    := source)
-> Store (Identity (a :*: b)) source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (a :*: b) -> Identity (a :*: b)
forall a. a -> Identity a
Identity (a
xt a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: b
yt) Identity (a :*: b)
-> (Identity (a :*: b) -> source)
-> ((:*:) (Identity (a :*: b)) :. (->) (Identity (a :*: b)))
   := source
forall s a. s -> a -> s :*: a
:*: \(Identity (a
xt_ :*: b
yt_)) -> Identity a -> source
ixts (a -> Identity a
forall a. a -> Identity a
Identity a
xt_) source -> source -> source
forall a. Semigroup a => a -> a -> a
+ Identity b -> source
iyts (b -> Identity b
forall a. a -> Identity a
Identity b
yt_)

instance Impliable (P_Q_T (->) Store Identity source target) where
	type Arguments (P_Q_T (->) Store Identity source target) =
		(source -> target) -> (source -> target -> source) -> Lens Identity source target
	imply :: Arguments (P_Q_T (->) Store Identity source target)
imply source -> target
getter source -> target -> source
setter = (source -> Store (Identity target) source)
-> P_Q_T (->) Store Identity source target
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((source -> Store (Identity target) source)
 -> P_Q_T (->) Store Identity source target)
-> (source -> Store (Identity target) source)
-> P_Q_T (->) Store Identity source target
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \source
source -> (((:*:) (Identity target) :. (->) (Identity target)) := source)
-> Store (Identity target) source
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity target) :. (->) (Identity target)) := source)
 -> Store (Identity target) source)
-> (((:*:) (Identity target) :. (->) (Identity target)) := source)
-> Store (Identity target) source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ target -> Identity target
forall a. a -> Identity a
Identity (target -> Identity target) -> target -> Identity target
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# source -> target
getter source
source Identity target
-> (Identity target -> source)
-> ((:*:) (Identity target) :. (->) (Identity target)) := source
forall s a. s -> a -> s :*: a
:*: source -> target -> source
setter source
source (target -> source)
-> (Identity target -> target) -> Identity target -> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity target -> target
forall (t :: * -> *) a. Extractable t => t a -> a
extract

type family Obscure lens where
	Obscure Lens = Lens Maybe

instance Impliable (P_Q_T (->) Store Maybe source target) where
	type Arguments (P_Q_T (->) Store Maybe source target) =
		(source -> Maybe target) -> (source -> Maybe target -> source) -> Lens Maybe source target
	imply :: Arguments (P_Q_T (->) Store Maybe source target)
imply source -> Maybe target
getter source -> Maybe target -> source
setter = (source -> Store (Maybe target) source)
-> P_Q_T (->) Store Maybe source target
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((source -> Store (Maybe target) source)
 -> P_Q_T (->) Store Maybe source target)
-> (source -> Store (Maybe target) source)
-> P_Q_T (->) Store Maybe source target
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \source
source -> (((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe target) :. (->) (Maybe target)) := source)
 -> Store (Maybe target) source)
-> (((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ source -> Maybe target
getter source
source Maybe target
-> (Maybe target -> source)
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := source
forall s a. s -> a -> s :*: a
:*: source -> Maybe target -> source
setter source
source

instance Semigroupoid (Lens Maybe) where
	(.) :: Obscure Lens between target -> Obscure Lens source between -> Obscure Lens source target
	P_Q_T to . :: Obscure Lens between target
-> Obscure Lens source between -> Obscure Lens source target
. P_Q_T from = (source -> Store (Maybe target) source)
-> P_Q_T (->) Store Maybe source target
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((source -> Store (Maybe target) source)
 -> P_Q_T (->) Store Maybe source target)
-> (source -> Store (Maybe target) source)
-> P_Q_T (->) Store Maybe source target
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \source
source -> case Store (Maybe between) source
-> ((:*:) (Maybe between) :. (->) (Maybe between)) := source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Store (Maybe between) source
 -> ((:*:) (Maybe between) :. (->) (Maybe between)) := source)
-> Store (Maybe between) source
-> ((:*:) (Maybe between) :. (->) (Maybe between)) := source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# source -> Store (Maybe between) source
from source
source of
		(Maybe between
Nothing :*: Maybe between -> source
_) -> (((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe target) :. (->) (Maybe target)) := source)
 -> Store (Maybe target) source)
-> (((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Maybe target
forall a. Maybe a
Nothing Maybe target
-> (Maybe target -> source)
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := source
forall s a. s -> a -> s :*: a
:*: \Maybe target
_ -> source
source
		(Just between
between :*: Maybe between -> source
mbs) -> case Store (Maybe target) between
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := between
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Store (Maybe target) between
 -> ((:*:) (Maybe target) :. (->) (Maybe target)) := between)
-> Store (Maybe target) between
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := between
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# between -> Store (Maybe target) between
to between
between of
			(Maybe target
Nothing :*: Maybe target -> between
_) -> (((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe target) :. (->) (Maybe target)) := source)
 -> Store (Maybe target) source)
-> (((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Maybe target
forall a. Maybe a
Nothing Maybe target
-> (Maybe target -> source)
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := source
forall s a. s -> a -> s :*: a
:*: \Maybe target
_ -> source
source
			(Just target
target :*: Maybe target -> between
mtb) -> (((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe target) :. (->) (Maybe target)) := source)
 -> Store (Maybe target) source)
-> (((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ target -> Maybe target
forall a. a -> Maybe a
Just target
target Maybe target
-> (Maybe target -> source)
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := source
forall s a. s -> a -> s :*: a
:*: Maybe between -> source
mbs (Maybe between -> source)
-> (Maybe target -> Maybe between) -> Maybe target -> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. between -> Maybe between
forall a. a -> Maybe a
Just (between -> Maybe between)
-> (Maybe target -> between) -> Maybe target -> Maybe between
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Maybe target -> between
mtb

instance Category (Lens Maybe) where
	identity :: Obscure Lens source source
	identity :: Obscure Lens source source
identity = Impliable (Obscure Lens source source) =>
Arguments (Obscure Lens source source)
forall k (result :: k). Impliable result => Arguments result
imply @(Obscure Lens _ _) ((source -> Maybe source)
 -> (source -> Maybe source -> source) -> Lens Maybe source source)
-> (source -> Maybe source)
-> (source -> Maybe source -> source)
-> Lens Maybe source source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# source -> Maybe source
forall a. a -> Maybe a
Just ((source -> Maybe source -> source) -> Lens Maybe source source)
-> (source -> Maybe source -> source) -> Lens Maybe source source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (source -> source) -> source -> Maybe source -> source
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve source -> source
forall (m :: * -> * -> *) a. Category m => m a a
identity

-- Lens as natural transformation
type (#=@) source target available = forall a . Lens available (source a) (target a)

-- | Get focused target value
view :: Lens available source target -> source -> available target
view :: Lens available source target -> source -> available target
view Lens available source target
lens = forall a.
Storable (available target) (Store (available target)) =>
Store (available target) a -> available target
forall s (t :: * -> *) a. Storable s t => t a -> s
position @_ @(Store _) (Store (available target) source -> available target)
-> (source -> Store (available target) source)
-> source
-> available target
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens available source target
-> source -> Store (available target) source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run Lens available source target
lens

-- Replace focused target value with new value
set :: Lens available source target -> available target -> source -> source
set :: Lens available source target
-> available target -> source -> source
set Lens available source target
lens available target
new = available target -> source <:= Store (available target)
forall s (t :: * -> *) a. Storable s t => s -> a <:= t
look available target
new (source <:= Store (available target))
-> (source -> Store (available target) source) -> source -> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens available source target
-> source -> Store (available target) source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run Lens available source target
lens

-- | Modify focused target value
over :: Lens available source target -> (available target -> available target) -> source -> source
over :: Lens available source target
-> (available target -> available target) -> source -> source
over Lens available source target
lens available target -> available target
f = Store (available target) source -> source
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Store (available target) source -> source)
-> (source -> Store (available target) source) -> source -> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (available target -> available target)
-> Store (available target) ~> Store (available target)
forall s. (s -> s) -> Store s ~> Store s
retrofit available target -> available target
f (Store (available target) source
 -> Store (available target) source)
-> (source -> Store (available target) source)
-> source
-> Store (available target) source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens available source target
-> source -> Store (available target) source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run Lens available source target
lens

-- | Representable based lens
represent :: forall t a . (Representable t, Setoid (Representation t)) => Representation t -> Convex Lens (t a) a
represent :: Representation t -> Convex Lens (t a) a
represent Representation t
r = (t a -> a) -> (t a -> a -> t a) -> Lens Identity (t a) a
forall k (result :: k). Impliable result => Arguments result
imply @(Convex Lens (t a) a) (Representation t
r Representation t -> t a -> a
forall (t :: * -> *) a.
Representable t =>
Representation t -> a <:= t
<#>) (\t a
source a
target -> (Representation t -> a) -> t a
forall (t :: * -> *) a.
Representable t =>
(Representation t -> a) -> t a
tabulate ((Representation t -> a) -> t a) -> (Representation t -> a) -> t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \Representation t
r' -> Representation t
r' Representation t -> Representation t -> Boolean
forall a. Setoid a => a -> a -> Boolean
== Representation t
r Boolean -> a -> a -> a
forall a. Boolean -> a -> a -> a
? a
target (a -> a) -> a -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Representation t
r' Representation t -> t a -> a
forall (t :: * -> *) a.
Representable t =>
Representation t -> a <:= t
<#> t a
source)