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

module Pandora.Paradigm.Inventory.Optics where

import Pandora.Pattern.Category (Category (identity, (.), ($)))
import Pandora.Pattern.Functor.Covariant ((<$))
import Pandora.Pattern.Functor.Extractable (Extractable (extract))
import Pandora.Pattern.Functor.Representable (Representable (Representation, (<#>), tabulate))
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)))
import Pandora.Paradigm.Primary.Object.Boolean ((?))
import Pandora.Paradigm.Inventory.Store (Store (Store), position, look, retrofit)
import Pandora.Paradigm.Schemes.PQ_ (PQ_ (PQ_))

infixr 0 :-.
infixr 0 :~.

type (:-.) src tgt = Lens src tgt

-- Reference to taret within some source
type Lens = PQ_ (->) Store

instance Category Lens where
	identity :: Lens a a
identity = (a -> Store a a) -> Lens a a
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ ((a -> Store a a) -> Lens a a) -> (a -> Store a a) -> Lens a a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \a
src -> (((:*:) a :. (->) a) := a) -> Store a a
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) a :. (->) a) := a) -> Store a a)
-> (((:*:) a :. (->) a) := a) -> Store a a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a
src a -> (a -> a) -> ((:*:) a :. (->) a) := a
forall s a. s -> a -> Product s a
:*: a -> a
forall (m :: * -> * -> *) a. Category m => m a a
identity
	PQ_ b -> Store c b
to . :: Lens b c -> Lens a b -> Lens a c
. PQ_ a -> Store b a
from = (a -> Store c a) -> Lens a c
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ ((a -> Store c a) -> Lens a c) -> (a -> Store c a) -> Lens a c
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \a
src -> a
src a -> Store c b -> Store c a
forall (t :: * -> *) a b. Covariant t => a -> t b -> t a
<$ (b -> Store c b
to (b -> Store c b) -> (Store b a -> b) -> Store b a -> Store c b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Store b a -> b
forall s (t :: * -> *) a. Storable s t => t a -> s
position (Store b a -> Store c b) -> Store b a -> Store c b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> Store b a
from a
src)

-- Lens as natural transformation
type (:~.) src tgt = forall a . Lens (src a) (tgt a)

-- | Get the target of a lens
view :: Lens src tgt -> src -> tgt
view :: Lens src tgt -> src -> tgt
view Lens src tgt
lens = Store tgt src -> tgt
forall s (t :: * -> *) a. Storable s t => t a -> s
position (Store tgt src -> tgt) -> (src -> Store tgt src) -> src -> tgt
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Lens src tgt -> Primary (PQ_ (->) Store src) tgt
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Lens src tgt
lens

-- | Replace the target of a lens
set :: Lens src tgt -> tgt -> src -> src
set :: Lens src tgt -> tgt -> src -> src
set Lens src tgt
lens tgt
new = tgt -> src <:= Store tgt
forall s (t :: * -> *) a. Storable s t => s -> a <:= t
look tgt
new (src <:= Store tgt) -> (src -> Store tgt src) -> src -> src
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Lens src tgt -> Primary (PQ_ (->) Store src) tgt
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Lens src tgt
lens

-- | Modify the target of a lens
over :: Lens src tgt -> (tgt -> tgt) -> src -> src
over :: Lens src tgt -> (tgt -> tgt) -> src -> src
over Lens src tgt
lens tgt -> tgt
f = src <:= Store tgt
forall (t :: * -> *) a. Extractable t => a <:= t
extract (src <:= Store tgt) -> (src -> Store tgt src) -> src -> src
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (tgt -> tgt) -> Store tgt ~> Store tgt
forall s. (s -> s) -> Store s ~> Store s
retrofit tgt -> tgt
f (Store tgt src -> Store tgt src)
-> (src -> Store tgt src) -> src -> Store tgt src
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Lens src tgt -> Primary (PQ_ (->) Store src) tgt
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Lens src tgt
lens

-- | Representable based lens
represent :: (Representable t, Setoid (Representation t)) => Representation t -> t a :-. a
represent :: Representation t -> t a :-. a
represent Representation t
r = (t a -> Store a (t a)) -> t a :-. a
forall k k k (p :: k -> k -> *) (q :: k -> k -> k) (a :: k)
       (b :: k).
p a (q b a) -> PQ_ p q a b
PQ_ ((t a -> Store a (t a)) -> t a :-. a)
-> (t a -> Store a (t a)) -> t a :-. a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \t a
x -> (((:*:) a :. (->) a) := t a) -> Store a (t a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) a :. (->) a) := t a) -> Store a (t a))
-> (((:*:) a :. (->) a) := t a) -> Store a (t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Representation t
r Representation t -> a <:= t
forall (t :: * -> *) a.
Representable t =>
Representation t -> a <:= t
<#> t a
x a -> (a -> t a) -> ((:*:) a :. (->) a) := t a
forall s a. s -> a -> Product s a
:*: \a
new -> (Representation t -> a) -> t a
forall (t :: * -> *) a.
Representable t =>
(Representation t -> a) -> t a
tabulate (\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
new (a -> a) -> a -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Representation t
r' Representation t -> a <:= t
forall (t :: * -> *) a.
Representable t =>
Representation t -> a <:= t
<#> t a
x)