{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}

module Data.SOP.Lenses (
    Lens (..)
  , lenses_NP
  ) where

import           Data.SOP.Sing
import           Data.SOP.Strict

-- | Simple lens to access an element of an n-ary product.
data Lens f xs a = Lens {
      forall (f :: * -> *) (xs :: [*]) a. Lens f xs a -> NP f xs -> f a
getter :: NP f xs -> f a
    , forall (f :: * -> *) (xs :: [*]) a.
Lens f xs a -> f a -> NP f xs -> NP f xs
setter :: f a -> NP f xs -> NP f xs
    }

-- | Generate all lenses to access the element of an n-ary product.
lenses_NP :: SListI xs => NP (Lens f xs) xs
lenses_NP :: forall (xs :: [*]) (f :: * -> *). SListI xs => NP (Lens f xs) xs
lenses_NP = SList xs -> NP (Lens f xs) xs
forall (xs' :: [*]) (f :: * -> *). SList xs' -> NP (Lens f xs') xs'
go SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: SList xs' -> NP (Lens f xs') xs'
    go :: forall (xs' :: [*]) (f :: * -> *). SList xs' -> NP (Lens f xs') xs'
go SList xs'
SNil  = NP (Lens f xs') xs'
NP (Lens f xs') '[]
forall {k} (f :: k -> *). NP f '[]
Nil
    go SList xs'
SCons = Lens f xs' x
Lens f (x : xs) x
forall (f :: * -> *) x (xs' :: [*]). Lens f (x : xs') x
lensFirst Lens f xs' x -> NP (Lens f xs') xs -> NP (Lens f xs') (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* (forall a. Lens f xs a -> Lens f xs' a)
-> NP (Lens f xs) xs -> NP (Lens f xs') 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
hmap Lens f xs a -> Lens f xs' a
Lens f xs a -> Lens f (x : xs) a
forall a. Lens f xs a -> Lens f xs' a
forall (f :: * -> *) (xs' :: [*]) a x.
Lens f xs' a -> Lens f (x : xs') a
shiftLens (SList xs -> NP (Lens f xs) xs
forall (xs' :: [*]) (f :: * -> *). SList xs' -> NP (Lens f xs') xs'
go SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList)

    lensFirst :: Lens f (x ': xs') x
    lensFirst :: forall (f :: * -> *) x (xs' :: [*]). Lens f (x : xs') x
lensFirst = Lens {
          getter :: NP f (x : xs') -> f x
getter = NP f (x : xs') -> f x
forall {k} (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> f x
hd
        , setter :: f x -> NP f (x : xs') -> NP f (x : xs')
setter = \f x
a' (f x
_ :* NP f xs1
as) -> f x
a' f x -> NP f xs' -> NP f (x : xs')
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* NP f xs'
NP f xs1
as
        }

    shiftLens :: Lens f xs' a -> Lens f (x ': xs') a
    shiftLens :: forall (f :: * -> *) (xs' :: [*]) a x.
Lens f xs' a -> Lens f (x : xs') a
shiftLens Lens f xs' a
l = Lens {
          getter :: NP f (x : xs') -> f a
getter = Lens f xs' a -> NP f xs' -> f a
forall (f :: * -> *) (xs :: [*]) a. Lens f xs a -> NP f xs -> f a
getter Lens f xs' a
l (NP f xs' -> f a)
-> (NP f (x : xs') -> NP f xs') -> NP f (x : xs') -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP f (x : xs') -> NP f xs'
forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
NP f (x : xs) -> NP f xs
tl
        , setter :: f a -> NP f (x : xs') -> NP f (x : xs')
setter = \f a
a' (f x
a :* NP f xs1
as) -> f x
f x
a f x -> NP f xs' -> NP f (x : xs')
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* Lens f xs' a -> f a -> NP f xs' -> NP f xs'
forall (f :: * -> *) (xs :: [*]) a.
Lens f xs a -> f a -> NP f xs -> NP f xs
setter Lens f xs' a
l f a
a' NP f xs'
NP f xs1
as
        }