-- | Generalized lenses
--
-- Intended to be imported qualified
--
-- > import Generics.SOP.Lens as GLens
--
module Generics.SOP.Lens (
    -- * Generalized lenses
    GLens
  , lens
  , get
  , modify
  , set
    -- * Conversion
  , fromLens
  , fromIso
  , toLens
    -- * Generic computation of lenses for record type
  , glenses
    -- * Labels for the representation types
  , np
  , rep
  , sop
  , head
  , tail
  , i
  ) where

import Prelude hiding (id, (.), head, tail)

import Control.Category
import Control.Monad
import Data.Functor.Identity
import Data.Kind
import Generics.SOP
import Optics.Core (Optic', Is, A_Getter, A_Setter)

import qualified Optics.Core as Optics

{-------------------------------------------------------------------------------
  Generalized lens using two categories
-------------------------------------------------------------------------------}

-- | GLens generalizes a monomorphic lens by allowing for different monads
-- for the getter and modifier
data GLens (r :: Type -> Type) (w :: Type -> Type) a b =
    GLens (a -> r b) ((b -> w b) -> (a -> w a))

instance Monad r => Category (GLens r w) where
  id :: forall a. GLens r w a a
id = forall (r :: * -> *) (w :: * -> *) a b.
(a -> r b) -> ((b -> w b) -> a -> w a) -> GLens r w a b
GLens forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  (GLens b -> r c
f (c -> w c) -> b -> w b
m) . :: forall b c a. GLens r w b c -> GLens r w a b -> GLens r w a c
. (GLens a -> r b
g (b -> w b) -> a -> w a
n) = forall (r :: * -> *) (w :: * -> *) a b.
(a -> r b) -> ((b -> w b) -> a -> w a) -> GLens r w a b
GLens (b -> r c
f forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< a -> r b
g) ((b -> w b) -> a -> w a
n forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (c -> w c) -> b -> w b
m)

lens :: (a -> r b) -> ((b -> w b) -> a -> w a) -> GLens r w a b
lens :: forall a (r :: * -> *) b (w :: * -> *).
(a -> r b) -> ((b -> w b) -> a -> w a) -> GLens r w a b
lens = forall (r :: * -> *) (w :: * -> *) a b.
(a -> r b) -> ((b -> w b) -> a -> w a) -> GLens r w a b
GLens

get :: GLens r w a b -> a -> r b
get :: forall (r :: * -> *) (w :: * -> *) a b. GLens r w a b -> a -> r b
get (GLens a -> r b
f (b -> w b) -> a -> w a
_) = a -> r b
f

modify :: GLens r w a b -> (b -> w b) -> a -> w a
modify :: forall (r :: * -> *) (w :: * -> *) a b.
GLens r w a b -> (b -> w b) -> a -> w a
modify (GLens a -> r b
_ (b -> w b) -> a -> w a
g) = (b -> w b) -> a -> w a
g

set :: Monad w => GLens r w a b -> b -> a -> w a
set :: forall (w :: * -> *) (r :: * -> *) a b.
Monad w =>
GLens r w a b -> b -> a -> w a
set GLens r w a b
l = forall (r :: * -> *) (w :: * -> *) a b.
GLens r w a b -> (b -> w b) -> a -> w a
modify GLens r w a b
l forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. a -> b -> a
const forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure

{-------------------------------------------------------------------------------
  Conversion
-------------------------------------------------------------------------------}

fromOptics ::
     (Is k A_Getter, Is k A_Setter, Monad r, Monad w)
  => Optic' k is a b -> GLens r w a b
fromOptics :: forall k (r :: * -> *) (w :: * -> *) (is :: IxList) a b.
(Is k A_Getter, Is k A_Setter, Monad r, Monad w) =>
Optic' k is a b -> GLens r w a b
fromOptics Optic' k is a b
l =
    forall (r :: * -> *) (w :: * -> *) a b.
(a -> r b) -> ((b -> w b) -> a -> w a) -> GLens r w a b
GLens
      (forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
Optics.view Optic' k is a b
l)
      (\b -> w b
f a
a -> (\b
b -> forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
Optics.set Optic' k is a b
l b
b a
a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> w b
f (forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
Optics.view Optic' k is a b
l a
a))

fromLens :: (Monad r, Monad w) => Optics.Lens' a b -> GLens r w a b
fromLens :: forall (r :: * -> *) (w :: * -> *) a b.
(Monad r, Monad w) =>
Lens' a b -> GLens r w a b
fromLens = forall k (r :: * -> *) (w :: * -> *) (is :: IxList) a b.
(Is k A_Getter, Is k A_Setter, Monad r, Monad w) =>
Optic' k is a b -> GLens r w a b
fromOptics

fromIso :: (Monad r, Monad w) => Optics.Iso' a b -> GLens r w a b
fromIso :: forall (r :: * -> *) (w :: * -> *) a b.
(Monad r, Monad w) =>
Iso' a b -> GLens r w a b
fromIso = forall k (r :: * -> *) (w :: * -> *) (is :: IxList) a b.
(Is k A_Getter, Is k A_Setter, Monad r, Monad w) =>
Optic' k is a b -> GLens r w a b
fromOptics

toLens :: GLens Identity Identity a b -> Optics.Lens' a b
toLens :: forall a b. GLens Identity Identity a b -> Lens' a b
toLens GLens Identity Identity a b
l = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Optics.lens (forall a. Identity a -> a
runIdentity forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (r :: * -> *) (w :: * -> *) a b. GLens r w a b -> a -> r b
get GLens Identity Identity a b
l) (\a
a b
b -> forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall (w :: * -> *) (r :: * -> *) a b.
Monad w =>
GLens r w a b -> b -> a -> w a
set GLens Identity Identity a b
l b
b a
a)

{-------------------------------------------------------------------------------
  Generic computation of all lenses for a record type
-------------------------------------------------------------------------------}

glenses :: forall r w a xs.
     (Generic a, Code a ~ '[xs], Monad r, Monad w)
  => NP (GLens r w a) xs
glenses :: forall (r :: * -> *) (w :: * -> *) a (xs :: IxList).
(Generic a, Code a ~ '[xs], Monad r, Monad w) =>
NP (GLens r w a) xs
glenses =
    case forall {k} (xs :: [k]). SListI xs => SList xs
sList :: SList (Code a) of
      SList (Code a)
SCons -> forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hliftA (\GLens r w (NP I xs) a
l -> GLens r w (NP I xs) a
l forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (r :: * -> *) (w :: * -> *) (f :: * -> *) (xs :: IxList).
(Monad r, Monad w) =>
GLens r w (SOP f '[xs]) (NP f xs)
sop forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (r :: * -> *) (w :: * -> *) a.
(Monad r, Monad w, Generic a) =>
GLens r w a (Rep a)
rep) forall (r :: * -> *) (w :: * -> *) (xs :: IxList).
(Monad r, Monad w, SListI xs) =>
NP (GLens r w (NP I xs)) xs
np

{-------------------------------------------------------------------------------
  Generalized lenses for representation types
-------------------------------------------------------------------------------}

np :: forall r w xs.
     (Monad r, Monad w, SListI xs)
  => NP (GLens r w (NP I xs)) xs
np :: forall (r :: * -> *) (w :: * -> *) (xs :: IxList).
(Monad r, Monad w, SListI xs) =>
NP (GLens r w (NP I xs)) xs
np = case forall {k} (xs :: [k]). SListI xs => SList xs
sList :: SList xs of
      SList xs
SNil  -> forall {k} (a :: k -> *). NP a '[]
Nil
      SList xs
SCons -> forall (r :: * -> *) (w :: * -> *) a.
(Monad r, Monad w) =>
GLens r w (I a) a
i forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (r :: * -> *) (w :: * -> *) (f :: * -> *) x (xs :: IxList).
(Monad r, Monad w) =>
GLens r w (NP f (x : xs)) (f x)
head forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hliftA (forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (r :: * -> *) (w :: * -> *) (f :: * -> *) x (xs :: IxList).
(Monad r, Monad w) =>
GLens r w (NP f (x : xs)) (NP f xs)
tail) forall (r :: * -> *) (w :: * -> *) (xs :: IxList).
(Monad r, Monad w, SListI xs) =>
NP (GLens r w (NP I xs)) xs
np

rep :: (Monad r, Monad w, Generic a) => GLens r w a (Rep a)
rep :: forall (r :: * -> *) (w :: * -> *) a.
(Monad r, Monad w, Generic a) =>
GLens r w a (Rep a)
rep = forall (r :: * -> *) (w :: * -> *) a b.
(Monad r, Monad w) =>
Iso' a b -> GLens r w a b
fromIso forall a b. (a -> b) -> a -> b
$ forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
Optics.iso forall a. Generic a => a -> Rep a
from forall a. Generic a => Rep a -> a
to

sop :: (Monad r, Monad w) => GLens r w (SOP f '[xs]) (NP f xs)
sop :: forall (r :: * -> *) (w :: * -> *) (f :: * -> *) (xs :: IxList).
(Monad r, Monad w) =>
GLens r w (SOP f '[xs]) (NP f xs)
sop = forall (r :: * -> *) (w :: * -> *) a b.
(Monad r, Monad w) =>
Iso' a b -> GLens r w a b
fromIso forall a b. (a -> b) -> a -> b
$ forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
Optics.iso (forall {k} (f :: k -> *) (x :: k). NS f '[x] -> f x
unZ forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {k} (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
unSOP) (forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z)

head :: (Monad r, Monad w) => GLens r w (NP f (x ': xs)) (f x)
head :: forall (r :: * -> *) (w :: * -> *) (f :: * -> *) x (xs :: IxList).
(Monad r, Monad w) =>
GLens r w (NP f (x : xs)) (f x)
head = forall (r :: * -> *) (w :: * -> *) a b.
(Monad r, Monad w) =>
Lens' a b -> GLens r w a b
fromLens forall a b. (a -> b) -> a -> b
$ forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Optics.lens (\(f x
x :* NP f xs
_) -> f x
x) (\(f x
_ :* NP f xs
xs) f x
x -> f x
x forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP f xs
xs)

tail :: (Monad r, Monad w) => GLens r w (NP f (x ': xs)) (NP f xs)
tail :: forall (r :: * -> *) (w :: * -> *) (f :: * -> *) x (xs :: IxList).
(Monad r, Monad w) =>
GLens r w (NP f (x : xs)) (NP f xs)
tail = forall (r :: * -> *) (w :: * -> *) a b.
(Monad r, Monad w) =>
Lens' a b -> GLens r w a b
fromLens forall a b. (a -> b) -> a -> b
$ forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Optics.lens (\(f x
_ :* NP f xs
xs) -> NP f xs
xs) (\(f x
x :* NP f xs
_) NP f xs
xs -> (f x
x forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP f xs
xs))

i :: (Monad r, Monad w) => GLens r w (I a) a
i :: forall (r :: * -> *) (w :: * -> *) a.
(Monad r, Monad w) =>
GLens r w (I a) a
i = forall (r :: * -> *) (w :: * -> *) a b.
(Monad r, Monad w) =>
Iso' a b -> GLens r w a b
fromIso forall a b. (a -> b) -> a -> b
$ forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
Optics.iso forall a. I a -> a
unI forall a. a -> I a
I