{-# 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.Representable (Representable (Representation, (<#>), tabulate))
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (run))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic.Exponential ((!.), (%))
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.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 -> (between -> Store (Identity target) between
to (between -> Store (Identity target) between)
-> (Store (Identity between) source -> between)
-> Store (Identity between) source
-> Store (Identity target) between
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a. Extractable Identity => Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract @Identity (Identity between -> between)
-> (Store (Identity between) source -> Identity between)
-> Store (Identity between) source
-> between
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Store (Identity between) source -> Identity between
forall s (t :: * -> *) a. Storable s t => t a -> s
position (Store (Identity between) source
 -> Store (Identity target) between)
-> Store (Identity between) source
-> Store (Identity target) between
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ source -> Store (Identity between) source
from source
source) Store (Identity target) between
-> source -> Store (Identity target) source
forall (t :: * -> *) a b. Covariant (->) (->) t => t a -> b -> t b
$>- source
source

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 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
forall s (t :: * -> *) a. Storable s t => t a -> s
position (Store (Maybe between) source -> Maybe between)
-> Store (Maybe between) source -> Maybe between
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 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
:*: (source
source source -> Maybe target -> source
forall a b. a -> b -> a
!.)
		Just between
between -> between -> Store (Maybe target) between
to between
between Store (Maybe target) between
-> source -> Store (Maybe target) source
forall (t :: * -> *) a b. Covariant (->) (->) t => t a -> b -> t b
$>- source
source

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)