{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE Rank2Types             #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Generics.Product.Internal.GLens
-- Copyright   :  (C) 2020 Csongor Kiss
-- License     :  BSD3
-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Derive record field getters and setters generically.
--
-----------------------------------------------------------------------------

module Data.Generics.Product.Internal.GLens
  ( GLens (..)
  , GLens'
  , TyFun
  , Eval
  ) where

import Data.Generics.Internal.Profunctor.Lens (Lens, choosing, first, second)
import Data.Generics.Internal.Profunctor.Iso (kIso, sumIso, mIso)

import Data.Kind    (Type)
import GHC.Generics

type Pred = TyFun (Type -> Type) (Maybe Type)

type TyFun a b = a -> b -> Type
type family Eval (f :: TyFun a b) (x :: a) :: b

-- A generic lens that uses some predicate to determine which field to focus on
class GLens (pred :: Pred) (s :: Type -> Type) (t :: Type -> Type) a b | s pred -> a, t pred -> b where
  glens :: Lens (s x) (t x) a b

type GLens' pred s a = GLens pred s s a a

instance GProductLens (Eval pred l) pred l r l' r' a b
      => GLens pred (l :*: r) (l' :*: r') a b where

  glens :: p i a b -> p i ((:*:) l r x) ((:*:) l' r' x)
glens = forall k (left :: Maybe *) (pred :: Pred) (l :: k -> *)
       (r :: k -> *) (l' :: k -> *) (r' :: k -> *) a b (x :: k).
GProductLens left pred l r l' r' a b =>
Lens ((:*:) l r x) ((:*:) l' r' x) a b
forall (l :: * -> *) (r :: * -> *) (l' :: * -> *) (r' :: * -> *) a
       b x.
GProductLens (Eval pred l) pred l r l' r' a b =>
Lens ((:*:) l r x) ((:*:) l' r' x) a b
gproductLens @(Eval pred l) @pred
  {-# INLINE glens #-}

instance (GLens pred l l' a b, GLens pred r r' a b) =>  GLens pred (l :+: r) (l' :+: r') a b where
  glens :: p i a b -> p i ((:+:) l r x) ((:+:) l' r' x)
glens = p i (Either (l x) (r x)) (Either (l' x) (r' x))
-> p i ((:+:) l r x) ((:+:) l' r' x)
forall (a :: * -> *) (b :: * -> *) x (a' :: * -> *) (b' :: * -> *).
Iso
  ((:+:) a b x)
  ((:+:) a' b' x)
  (Either (a x) (b x))
  (Either (a' x) (b' x))
sumIso (p i (Either (l x) (r x)) (Either (l' x) (r' x))
 -> p i ((:+:) l r x) ((:+:) l' r' x))
-> (p i a b -> p i (Either (l x) (r x)) (Either (l' x) (r' x)))
-> p i a b
-> p i ((:+:) l r x) ((:+:) l' r' x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens (l x) (l' x) a b
-> Lens (r x) (r' x) a b
-> Lens (Either (l x) (r x)) (Either (l' x) (r' x)) a b
forall s t a b s' t'.
Lens s t a b
-> Lens s' t' a b -> Lens (Either s s') (Either t t') a b
choosing (forall (s :: * -> *) (t :: * -> *) a b x.
GLens pred s t a b =>
Lens (s x) (t x) a b
forall (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
GLens pred s t a b =>
Lens (s x) (t x) a b
glens @pred) (forall (s :: * -> *) (t :: * -> *) a b x.
GLens pred s t a b =>
Lens (s x) (t x) a b
forall (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
GLens pred s t a b =>
Lens (s x) (t x) a b
glens @pred)
  {-# INLINE glens #-}

instance GLens pred (K1 r a) (K1 r b) a b where
  glens :: p i a b -> p i (K1 r a x) (K1 r b x)
glens = p i a b -> p i (K1 r a x) (K1 r b x)
forall r a p b. Iso (K1 r a p) (K1 r b p) a b
kIso
  {-# INLINE glens #-}

instance (GLens pred f g a b) => GLens pred (M1 m meta f) (M1 m meta g) a b where
  glens :: p i a b -> p i (M1 m meta f x) (M1 m meta g x)
glens = p i (f x) (g x) -> p i (M1 m meta f x) (M1 m meta g x)
forall i (c :: Meta) (f :: * -> *) p (g :: * -> *).
Iso (M1 i c f p) (M1 i c g p) (f p) (g p)
mIso (p i (f x) (g x) -> p i (M1 m meta f x) (M1 m meta g x))
-> (p i a b -> p i (f x) (g x))
-> p i a b
-> p i (M1 m meta f x) (M1 m meta g x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: * -> *) (t :: * -> *) a b x.
GLens pred s t a b =>
Lens (s x) (t x) a b
forall (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
GLens pred s t a b =>
Lens (s x) (t x) a b
glens @pred
  {-# INLINE glens #-}

class GProductLens (left :: Maybe Type) (pred :: Pred) l r l' r' a b | pred l r -> a, pred l' r' -> b where
  gproductLens :: Lens ((l :*: r) x) ((l' :*: r') x) a b

instance GLens pred l l' a b => GProductLens ('Just x) pred l r l' r a b where
  gproductLens :: p i a b -> p i ((:*:) l r x) ((:*:) l' r x)
gproductLens = p i (l x) (l' x) -> p i ((:*:) l r x) ((:*:) l' r x)
forall (a :: * -> *) (b :: * -> *) x (a' :: * -> *).
Lens ((:*:) a b x) ((:*:) a' b x) (a x) (a' x)
first (p i (l x) (l' x) -> p i ((:*:) l r x) ((:*:) l' r x))
-> (p i a b -> p i (l x) (l' x))
-> p i a b
-> p i ((:*:) l r x) ((:*:) l' r x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: * -> *) (t :: * -> *) a b x.
GLens pred s t a b =>
Lens (s x) (t x) a b
forall (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
GLens pred s t a b =>
Lens (s x) (t x) a b
glens @pred
  {-# INLINE gproductLens #-}

instance GLens pred r r' a b => GProductLens 'Nothing pred l r l r' a b where
  gproductLens :: p i a b -> p i ((:*:) l r x) ((:*:) l r' x)
gproductLens = p i (r x) (r' x) -> p i ((:*:) l r x) ((:*:) l r' x)
forall (a :: * -> *) (b :: * -> *) x (b' :: * -> *).
Lens ((:*:) a b x) ((:*:) a b' x) (b x) (b' x)
second (p i (r x) (r' x) -> p i ((:*:) l r x) ((:*:) l r' x))
-> (p i a b -> p i (r x) (r' x))
-> p i a b
-> p i ((:*:) l r x) ((:*:) l r' x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: * -> *) (t :: * -> *) a b x.
GLens pred s t a b =>
Lens (s x) (t x) a b
forall (pred :: Pred) (s :: * -> *) (t :: * -> *) a b x.
GLens pred s t a b =>
Lens (s x) (t x) a b
glens @pred
  {-# INLINE gproductLens #-}