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

import Pandora.Core.Impliable (Impliable (Arguments, imply))
import Pandora.Pattern.Semigroupoid (Semigroupoid ((.)))
import Pandora.Pattern.Category (Category (identity, (#)))
import Pandora.Pattern.Kernel (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.Object.Setoid (Setoid ((==)))
import Pandora.Paradigm.Controlflow.Effect.Conditional (Conditional ((?)))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (run, (!)))
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.Primary.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic.Exponential (type (-->), (%))
import Pandora.Paradigm.Primary.Algebraic (Pointable, point, 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.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)

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)) -> P_Q_T (->) Store available b tgt -> Flip (Lens available) tgt b
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (P_Q_T (->) Store available b tgt -> Flip (Lens available) tgt b)
-> ((b -> Store (available tgt) b)
    -> P_Q_T (->) Store 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) -> P_Q_T (->) Store 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (b -> a
g (b -> a)
-> (Store (available tgt) a -> Store (available tgt) b)
-> (b -> a)
   :*: (Store (available tgt) a -> Store (available tgt) b)
forall s a. s -> a -> s :*: a
:*: (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)
<-|-) ((b -> a) :*: (Store (available tgt) a -> Store (available tgt) b))
-> (a -> Store (available tgt) a) -> b -> Store (available tgt) b
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d.
(Contravariant m m (Flip p d), Covariant m m (p b),
 Interpreted m (Flip p d)) =>
(m a b :*: m c d) -> m (p b c) (p a d)
>-|-<-|-) 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant)

instance 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \source
source ->
		let Store (Identity a
xt :*: Identity a -> source
ixts) :*: Store (Identity b
yt :*: Identity b -> source
_) = 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (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_)) ->
			let modified :: source
modified = Identity a -> source
ixts (a -> Identity a
forall a. a -> Identity a
Identity a
xt_) in
			(Identity b :*: (Identity b -> source)) -> Identity b -> source
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((Identity b :*: (Identity b -> source)) -> Identity b -> source)
-> (Identity b :*: (Identity b -> source)) -> Identity b -> source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Store (Identity b) source -> Identity b :*: (Identity b -> source)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (source -> Store (Identity b) source
y source
modified) (Identity b -> source) -> Identity b -> source
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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)

-- | 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \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 clause a. Conditional clause => clause -> a -> a -> a
? a
target (a -> a) -> a -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 Identity where
	type Lensally Maybe Identity = Maybe
	P_Q_T source -> Store (Maybe between) source
from >>> :: Lens Maybe source between
-> Lens Identity between target
-> Lens (Lensally Maybe Identity) source target
>>> P_Q_T between -> Store (Identity 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 (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 of
			(Identity target
target :*: Identity 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Identity target -> between
itb (Identity target -> between)
-> (target -> Identity target) -> target -> between
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. target -> Identity target
forall a. a -> Identity a
Identity (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 Identity Maybe where
	type Lensally Identity Maybe = Maybe
	P_Q_T source -> Store (Identity between) source
from >>> :: Lens Identity source between
-> Lens Maybe between target
-> Lens (Lensally Identity 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \source
source -> case 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 of
		(Identity between
between :*: Identity 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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
:*: Identity between -> source
ibs (Identity between -> source)
-> (Maybe target -> Identity between) -> Maybe 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)
-> (Maybe target -> between) -> Maybe target -> Identity 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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

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

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 = 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)
-> (e -> Store (Maybe r) e) -> e -> Maybe r
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. 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)
run P_Q_T (->) Store Maybe e r
lens

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 -> e -> Store (t r) e
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run P_Q_T (->) Store t e r
lens 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 = Store (t r) e -> e
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Store (t r) e -> e) -> (e -> Store (t r) e) -> 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 -> Store (t r) e)
-> (e -> Store (t r) e) -> e -> Store (t r) e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. 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)
run P_Q_T (->) Store t e r
lens