{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE UndecidableInstances #-}
module Pandora.Paradigm.Inventory.Some.Optics where

import Pandora.Core.Functor (type (<))
import Pandora.Core.Impliable (Impliable (Arguments, imply))
import Pandora.Core.Interpreted (Interpreted (Primary, run, unite, (<~)))
import Pandora.Pattern.Semigroupoid (Semigroupoid ((.)))
import Pandora.Pattern.Category (Category (identity, (<--), (<---), (<----), (<-----), (<-------)))
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|-|-)))
import Pandora.Pattern.Functor.Invariant (Invariant ((<!<)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Representable (Representable (Representation, (<#>), tabulate))
import Pandora.Pattern.Transformer.Liftable (Liftable (lift))
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Pattern.Object.Setoid (Setoid ((?=)))
import Pandora.Paradigm.Inventory.Ability.Gettable (Gettable (Getting, get))
import Pandora.Paradigm.Inventory.Ability.Settable (Settable (Setting, set))
import Pandora.Paradigm.Inventory.Ability.Modifiable (Modifiable (Modification, modify))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Algebraic.Exponential (type (-->), (%))
import Pandora.Paradigm.Algebraic (Pointable, point, extract, (>-||---))
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
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.Inventory.Some.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)

infixr 6 @>>>
infixl 7 #=@

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)
-> (a -> Store (available tgt) b) -> b -> Store (available tgt) b
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c.
(Contravariant m m (Flip p c), Interpreted m (Flip p c)) =>
m a b -> m (p b c) (p a c)
>-||--- a -> b
f (a -> b)
-> (a -> Store (available tgt) a) -> a -> Store (available tgt) b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
<-|-|- a -> Store (available tgt) a
lens

type family Convex lens where
	Convex Lens = Lens Exactly

instance Semigroupoid (Lens Exactly) 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 (Exactly target) source)
-> P_Q_T (->) Store Exactly 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 (Exactly target) source)
 -> P_Q_T (->) Store Exactly source target)
-> (source -> Store (Exactly target) source)
-> P_Q_T (->) Store Exactly source target
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \source
source ->
		let (Exactly between
between :*: Exactly between -> source
bs) = Store (Exactly between) source
-> Exactly between :*: (Exactly between -> source)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Store (Exactly between) source
 -> Exactly between :*: (Exactly between -> source))
-> Store (Exactly between) source
-> Exactly between :*: (Exactly between -> source)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- source -> Store (Exactly between) source
from source
source in
		let (Exactly target
target :*: Exactly target -> between
tb) = Store (Exactly target) between
-> Exactly target :*: (Exactly target -> between)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Store (Exactly target) between
 -> Exactly target :*: (Exactly target -> between))
-> Store (Exactly target) between
-> Exactly target :*: (Exactly target -> between)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- between -> Store (Exactly target) between
to between
between in
		(((:*:) (Exactly target) :. (->) (Exactly target)) >>> source)
-> Store (Exactly target) source
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (Exactly target) :. (->) (Exactly target)) >>> source)
 -> Store (Exactly target) source)
-> (((:*:) (Exactly target) :. (->) (Exactly target)) >>> source)
-> Store (Exactly target) source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- target -> Exactly target
forall a. a -> Exactly a
Exactly target
target Exactly target
-> (Exactly target -> source)
-> ((:*:) (Exactly target) :. (->) (Exactly target)) >>> source
forall s a. s -> a -> s :*: a
:*: Exactly between -> source
bs (Exactly between -> source)
-> (Exactly target -> Exactly between) -> Exactly target -> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. between -> Exactly between
forall a. a -> Exactly a
Exactly (between -> Exactly between)
-> (Exactly target -> between) -> Exactly target -> Exactly between
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly target -> between
tb

instance Category (Lens Exactly) where
	identity :: Convex Lens source source
	identity :: Convex Lens source source
identity = (source -> source)
-> (source -> source -> source) -> Lens Exactly 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 (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant)

instance Semimonoidal (-->) (:*:) (:*:) (Lens Exactly source) where
	mult :: (Lens Exactly source a :*: Lens Exactly source b)
--> Lens Exactly source (a :*: b)
mult = ((Lens Exactly source a :*: Lens Exactly source b)
 -> Lens Exactly source (a :*: b))
-> (Lens Exactly source a :*: Lens Exactly source b)
   --> Lens Exactly source (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Lens Exactly source a :*: Lens Exactly source b)
  -> Lens Exactly source (a :*: b))
 -> (Lens Exactly source a :*: Lens Exactly source b)
    --> Lens Exactly source (a :*: b))
-> ((Lens Exactly source a :*: Lens Exactly source b)
    -> Lens Exactly source (a :*: b))
-> (Lens Exactly source a :*: Lens Exactly source b)
   --> Lens Exactly source (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(P_Q_T source -> Store (Exactly a) source
x :*: P_Q_T source -> Store (Exactly b) source
y) -> (source -> Store (Exactly (a :*: b)) source)
-> Lens Exactly 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 (Exactly (a :*: b)) source)
 -> Lens Exactly source (a :*: b))
-> (source -> Store (Exactly (a :*: b)) source)
-> Lens Exactly source (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \source
source ->
		let Store (Exactly a
xt :*: Exactly a -> source
ixts) :*: Store (Exactly b
yt :*: Exactly b -> source
_) = source -> Store (Exactly a) source
x source
source Store (Exactly a) source
-> Store (Exactly b) source
-> Store (Exactly a) source :*: Store (Exactly b) source
forall s a. s -> a -> s :*: a
:*: source -> Store (Exactly b) source
y source
source in
		(((:*:) (Exactly (a :*: b)) :. (->) (Exactly (a :*: b)))
 >>> source)
-> Store (Exactly (a :*: b)) source
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (Exactly (a :*: b)) :. (->) (Exactly (a :*: b)))
  >>> source)
 -> Store (Exactly (a :*: b)) source)
-> (((:*:) (Exactly (a :*: b)) :. (->) (Exactly (a :*: b)))
    >>> source)
-> Store (Exactly (a :*: b)) source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (a :*: b) -> Exactly (a :*: b)
forall a. a -> Exactly a
Exactly (a
xt a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: b
yt) Exactly (a :*: b)
-> (Exactly (a :*: b) -> source)
-> ((:*:) (Exactly (a :*: b)) :. (->) (Exactly (a :*: b)))
   >>> source
forall s a. s -> a -> s :*: a
:*: \(Exactly (a
xt_ :*: b
yt_)) ->
			let modified :: source
modified = Exactly a -> source
ixts (Exactly a -> source) -> Exactly a -> source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> Exactly a
forall a. a -> Exactly a
Exactly a
xt_ in
			(Exactly b :*: (Exactly b -> source)) -> Exactly b -> source
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((Exactly b :*: (Exactly b -> source)) -> Exactly b -> source)
-> (Exactly b :*: (Exactly b -> source)) -> Exactly b -> source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Store (Exactly b) source -> Exactly b :*: (Exactly b -> source)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Store (Exactly b) source -> Exactly b :*: (Exactly b -> source))
-> Store (Exactly b) source -> Exactly b :*: (Exactly b -> source)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- source -> Store (Exactly b) source
y source
modified (Exactly b -> source) -> Exactly b -> source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- b -> Exactly b
forall a. a -> Exactly a
Exactly b
yt_

instance Impliable (P_Q_T (->) Store Exactly source target) where
	type Arguments (P_Q_T (->) Store Exactly source target) =
		(source -> target) -> (source -> target -> source) -> Lens Exactly source target
	imply :: Arguments (P_Q_T (->) Store Exactly source target)
imply source -> target
getter source -> target -> source
setter = (source -> Store (Exactly target) source)
-> P_Q_T (->) Store Exactly 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 (Exactly target) source)
 -> P_Q_T (->) Store Exactly source target)
-> (source -> Store (Exactly target) source)
-> P_Q_T (->) Store Exactly source target
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \source
source -> (((:*:) (Exactly target) :. (->) (Exactly target)) >>> source)
-> Store (Exactly target) source
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (Exactly target) :. (->) (Exactly target)) >>> source)
 -> Store (Exactly target) source)
-> (((:*:) (Exactly target) :. (->) (Exactly target)) >>> source)
-> Store (Exactly target) source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- target -> Exactly target
forall a. a -> Exactly a
Exactly (source -> target
getter source
source) Exactly target
-> (Exactly target -> source)
-> ((:*:) (Exactly target) :. (->) (Exactly target)) >>> source
forall s a. s -> a -> s :*: a
:*: source -> target -> source
setter source
source (target -> source)
-> (Exactly target -> target) -> Exactly target -> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly 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

-- This type of lens leave whole structure untouched if we set target = Nothing
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
:*: source -> Maybe target -> source
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant 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
:*: source -> Maybe target -> source
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant 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)

type (@>>>) source target = forall a . Lens target (source a) a

-- | 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 Exactly (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 -> a -> a -> a
forall a r. Setoid a => a -> a -> r -> r -> r
?= Representation t
r (a -> a -> a) -> a -> a -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- 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)

class Lensic previous next where
	type Lensally previous next :: * -> *
	(>>>) :: Lens previous source between -> Lens next between target -> Lens (Lensally previous next) source target

instance Semigroupoid (Lens t) => Lensic t t where
	type Lensally t t = t
	Lens t source between
x >>> :: Lens t source between
-> Lens t between target -> Lens (Lensally t t) source target
>>> Lens t between target
y = Lens t between target
y Lens t between target
-> Lens t source between -> P_Q_T (->) Store t source target
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens t source between
x

instance Lensic Maybe Exactly where
	type Lensally Maybe Exactly = Maybe
	P_Q_T source -> Store (Maybe between) source
from >>> :: Lens Maybe source between
-> Lens Exactly between target
-> Lens (Lensally Maybe Exactly) source target
>>> P_Q_T between -> Store (Exactly target) between
to = (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 (Exactly target) between
-> ((:*:) (Exactly target) :. (->) (Exactly target)) >>> between
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Store (Exactly target) between
 -> ((:*:) (Exactly target) :. (->) (Exactly target)) >>> between)
-> Store (Exactly target) between
-> ((:*:) (Exactly target) :. (->) (Exactly target)) >>> between
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- between -> Store (Exactly target) between
to between
between of
			Exactly target
target :*: Exactly target -> between
itb -> (((:*:) (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 target
mt -> Maybe between -> source
mbs (Maybe between -> source) -> Maybe between -> source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- Exactly target -> between
itb (Exactly target -> between)
-> (target -> Exactly target) -> target -> between
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. target -> Exactly target
forall a. a -> Exactly a
Exactly (target -> between) -> Maybe target -> Maybe between
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- Maybe target
mt

instance Lensic Exactly Maybe where
	type Lensally Exactly Maybe = Maybe
	P_Q_T source -> Store (Exactly between) source
from >>> :: Lens Exactly source between
-> Lens Maybe between target
-> Lens (Lensally Exactly Maybe) source target
>>> P_Q_T between -> Store (Maybe target) between
to = (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 (Exactly between) source
-> ((:*:) (Exactly between) :. (->) (Exactly between)) >>> source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Store (Exactly between) source
 -> ((:*:) (Exactly between) :. (->) (Exactly between)) >>> source)
-> Store (Exactly between) source
-> ((:*:) (Exactly between) :. (->) (Exactly between)) >>> source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- source -> Store (Exactly between) source
from source
source of
		Exactly between
between :*: Exactly between -> source
ibs -> 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
			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
:*: Exactly between -> source
ibs (Exactly between -> source)
-> (Maybe target -> Exactly between) -> Maybe target -> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. between -> Exactly between
forall a. a -> Exactly a
Exactly (between -> Exactly between)
-> (Maybe target -> between) -> Maybe target -> Exactly between
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Maybe target -> between
mtb
			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
:*: source -> Maybe target -> source
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant source
source

instance Gettable (Lens Exactly) where
	type instance Getting (Lens Exactly) source target = Lens Exactly source target -> source -> target
	get :: Getting (Lens Exactly) e r
get P_Q_T (->) Store Exactly e r
lens e
source = forall a. Extractable Exactly => Exactly a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract @Exactly (Exactly r -> r)
-> (Store (Exactly r) e -> Exactly r) -> Store (Exactly r) e -> r
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a.
Storable (Exactly r) (Store (Exactly r)) =>
Store (Exactly r) a -> Exactly r
forall s (t :: * -> *) a. Storable s t => t a -> s
position @_ @(Store _) (Store (Exactly r) e -> r) -> Store (Exactly r) e -> r
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- P_Q_T (->) Store Exactly e r
lens P_Q_T (->) Store Exactly e r -> e -> Store (Exactly r) e
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ e
source

instance Gettable (Lens Maybe) where
	type instance Getting (Lens Maybe) source target = Lens Maybe source target -> source -> Maybe target
	get :: Getting (Lens Maybe) e r
get P_Q_T (->) Store Maybe e r
lens e
source = forall a.
Storable (Maybe r) (Store (Maybe r)) =>
Store (Maybe r) a -> Maybe r
forall s (t :: * -> *) a. Storable s t => t a -> s
position @_ @(Store _) (Store (Maybe r) e -> Maybe r) -> Store (Maybe r) e -> Maybe r
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- P_Q_T (->) Store Maybe e r
lens P_Q_T (->) Store Maybe e r -> e -> Store (Maybe r) e
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ e
source

instance Pointable t => Settable (Lens t) where
	type instance Setting (Lens t) source target = target -> Lens t source target -> source -> source
	set :: Setting (Lens t) e r
set r
new P_Q_T (->) Store t e r
lens e
source = forall s (t :: * -> *) a. Storable s t => s -> a <:= t
forall (t :: * -> *) a. Storable (t r) t => t r -> a <:= t
look @(t _) (t r -> e <:= Store (t r)) -> t r -> e <:= Store (t r)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- r -> t r
forall (t :: * -> *) a. Pointable t => a -> t a
point r
new (e <:= Store (t r)) -> e <:= Store (t r)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- P_Q_T (->) Store t e r
lens P_Q_T (->) Store t e r -> e -> Store (t r) e
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ e
source

instance (Gettable (Lens t), Covariant (->) (->) t, Pointable t) => Modifiable (Lens t) where
	type instance Modification (Lens t) source target = (target -> target) -> Lens t source target -> source -> source
	modify :: Modification (Lens t) e r
modify r -> r
f P_Q_T (->) Store t e r
lens e
source = Store (t r) e -> e
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Store (t r) e -> e)
-> (Store (t r) e -> Store (t r) e) -> Store (t r) e -> e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (t r -> t r) -> Store (t r) ~> Store (t r)
forall s. (s -> s) -> Store s ~> Store s
retrofit (r -> r
f (r -> r) -> t r -> t r
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (Store (t r) e -> e) -> Store (t r) e -> e
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- P_Q_T (->) Store t e r
lens P_Q_T (->) Store t e r -> e -> Store (t r) e
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ e
source

view :: Lens i source target -> source -> i target
view :: Lens i source target -> source -> i target
view Lens i source target
lens source
source = forall a.
Storable (i target) (Store (i target)) =>
Store (i target) a -> i target
forall s (t :: * -> *) a. Storable s t => t a -> s
position @_ @(Store _) (Store (i target) source -> i target)
-> Store (i target) source -> i target
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Lens i source target
lens Lens i source target -> source -> Store (i target) source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ source
source

replace :: forall i source target . i target -> Lens i source target -> source -> source
replace :: i target -> Lens i source target -> source -> source
replace i target
new Lens i source target
lens source
source = forall s (t :: * -> *) a. Storable s t => s -> a <:= t
forall (t :: * -> *) a.
Storable (i target) t =>
i target -> a <:= t
look @(i _) (i target -> source <:= Store (i target))
-> i target -> source <:= Store (i target)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- i target
new (source <:= Store (i target)) -> source <:= Store (i target)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Lens i source target
lens Lens i source target -> source -> Store (i target) source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ source
source

mutate :: (i target -> i target) -> Lens i source target -> source -> source
mutate :: (i target -> i target) -> Lens i source target -> source -> source
mutate i target -> i target
mut Lens i source target
lens source
source = Store (i target) source -> source
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Store (i target) source -> source)
-> (Store (i target) source -> Store (i target) source)
-> Store (i target) source
-> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (i target -> i target) -> Store (i target) ~> Store (i target)
forall s. (s -> s) -> Store s ~> Store s
retrofit i target -> i target
mut (Store (i target) source -> source)
-> Store (i target) source -> source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Lens i source target
lens Lens i source target -> source -> Store (i target) source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ source
source

transwrap :: (Covariant (->) (->) u, Liftable (->) t, Lowerable (->) t) => Lens u < t u e < e
transwrap :: (Lens u < t u e) < e
transwrap = (t u e -> Store (u e) (t u e)) -> (Lens u < t u e) < e
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((t u e -> Store (u e) (t u e)) -> (Lens u < t u e) < e)
-> (t u e -> Store (u e) (t u e)) -> (Lens u < t u e) < e
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \t u e
origin -> (((:*:) (u e) :. (->) (u e)) >>> t u e) -> Store (u e) (t u e)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (u e) :. (->) (u e)) >>> t u e) -> Store (u e) (t u e))
-> (((:*:) (u e) :. (->) (u e)) >>> t u e) -> Store (u e) (t u e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- t u e -> u e
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower t u e
origin u e -> (u e -> t u e) -> ((:*:) (u e) :. (->) (u e)) >>> t u e
forall s a. s -> a -> s :*: a
:*: u e -> t u e
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift

primary :: Interpreted (->) t => Lens Exactly < t a < Primary t a
primary :: (Lens Exactly < t a) < Primary t a
primary = (t a -> Store (Exactly (Primary t a)) (t a))
-> (Lens Exactly < t a) < Primary t a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((t a -> Store (Exactly (Primary t a)) (t a))
 -> (Lens Exactly < t a) < Primary t a)
-> (t a -> Store (Exactly (Primary t a)) (t a))
-> (Lens Exactly < t a) < Primary t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \t a
origin -> (((:*:) (Exactly (Primary t a)) :. (->) (Exactly (Primary t a)))
 >>> t a)
-> Store (Exactly (Primary t a)) (t a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (Exactly (Primary t a)) :. (->) (Exactly (Primary t a)))
  >>> t a)
 -> Store (Exactly (Primary t a)) (t a))
-> (((:*:) (Exactly (Primary t a)) :. (->) (Exactly (Primary t a)))
    >>> t a)
-> Store (Exactly (Primary t a)) (t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Primary t a -> Exactly (Primary t a)
forall a. a -> Exactly a
Exactly (((->) < t a) < Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run t a
origin) Exactly (Primary t a)
-> (Exactly (Primary t a) -> t a)
-> ((:*:) (Exactly (Primary t a)) :. (->) (Exactly (Primary t a)))
   >>> t a
forall s a. s -> a -> s :*: a
:*: ((->) < Primary t a) < t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < Primary t a) < t a
unite (((->) < Primary t a) < t a)
-> (Exactly (Primary t a) -> Primary t a)
-> Exactly (Primary t a)
-> t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly (Primary t a) -> Primary t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract