{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE EmptyCase             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# OPTIONS_GHC -fno-warn-orphans  #-}

-- | Lenses for "Generics.SOP"
--
-- Orphan instances:
--
-- @
-- 'Wrapped' ('SOP' f xss) -- Also 'Rewrapped'
-- 'Wrapped' ('POP' f xss)
-- 'Field1' ('NP' f (x ': zs)) ('NP' f (y ': zs)) (f x) (f y) -- 'Field2' etc.
-- 'Field1' ('POP' f (x ': zs)) ('NP' f (y ': zs)) (NP f x) (NP f y)
-- @
module Generics.SOP.Lens (
    -- * Representations
    rep, productRep,
    -- * SOP & POP
    sop, pop,
    _SOP, _POP,
    -- * Functors
    _I, _K,
    -- * Products
    npSingleton,
    npHead,
    npTail,
    -- * Sums
    nsSingleton,
    _Z,
    _S,
    -- * DatatypeInfo
    Generics.SOP.Lens.moduleName,
    Generics.SOP.Lens.datatypeName,
    Generics.SOP.Lens.constructorInfo,
    Generics.SOP.Lens.constructorName,
    Generics.SOP.Lens.strictnessInfo,
    ) where

import           Control.Lens
import           Data.Kind             (Type)
import           Generics.SOP          hiding (from)
import qualified Generics.SOP          as SOP
import           Generics.SOP.Metadata


-------------------------------------------------------------------------------
-- Representations
-------------------------------------------------------------------------------

-- | Convert from the data type to its representation (or back).
--
-- >>> Just 'x' ^. rep
-- SOP (S (Z (I 'x' :* Nil)))
rep :: (Generic a, Generic b) => Iso a b (Rep a) (Rep b)
rep :: forall a b. (Generic a, Generic b) => Iso a b (Rep a) (Rep b)
rep = (a -> SOP I (Code a))
-> (SOP I (Code b) -> b)
-> Iso a b (SOP I (Code a)) (SOP I (Code b))
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso a -> SOP I (Code a)
forall a. Generic a => a -> Rep a
SOP.from SOP I (Code b) -> b
forall a. Generic a => Rep a -> a
SOP.to

-- | Convert from the product data type to its representation (or back)
--
-- >>> ('x', True) ^. productRep
-- I 'x' :* I True :* Nil
--
productRep :: (IsProductType a xs, IsProductType b ys) => Iso a b (NP I xs) (NP I ys)
productRep :: forall a (xs :: [*]) b (ys :: [*]).
(IsProductType a xs, IsProductType b ys) =>
Iso a b (NP I xs) (NP I ys)
productRep = p (SOP I '[xs]) (f (SOP I '[ys])) -> p a (f b)
p (Rep a) (f (Rep b)) -> p a (f b)
forall a b. (Generic a, Generic b) => Iso a b (Rep a) (Rep b)
Iso a b (Rep a) (Rep b)
rep (p (SOP I '[xs]) (f (SOP I '[ys])) -> p a (f b))
-> (p (NP I xs) (f (NP I ys)) -> p (SOP I '[xs]) (f (SOP I '[ys])))
-> p (NP I xs) (f (NP I ys))
-> p a (f b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (NS (NP I) '[xs]) (f (NS (NP I) '[ys]))
-> p (SOP I '[xs]) (f (SOP I '[ys]))
forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NS (NP f) xss) (f (NS (NP f) yss))
-> p (SOP f xss) (f (SOP f yss))
sop (p (NS (NP I) '[xs]) (f (NS (NP I) '[ys]))
 -> p (SOP I '[xs]) (f (SOP I '[ys])))
-> (p (NP I xs) (f (NP I ys))
    -> p (NS (NP I) '[xs]) (f (NS (NP I) '[ys])))
-> p (NP I xs) (f (NP I ys))
-> p (SOP I '[xs]) (f (SOP I '[ys]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (NP I xs) (f (NP I ys))
-> p (NS (NP I) '[xs]) (f (NS (NP I) '[ys]))
forall k (f :: k -> *) (x :: k) (y :: k) (p :: * -> * -> *)
       (f :: * -> *).
(Profunctor p, Functor f) =>
p (f x) (f (f y)) -> p (NS f '[x]) (f (NS f '[y]))
nsSingleton

-------------------------------------------------------------------------------
-- SOP & POP
-------------------------------------------------------------------------------

-- | The only field of 'SOP'.
--
-- >>> Just 'x' ^. rep . sop
-- S (Z (I 'x' :* Nil))
sop ::
    forall k (f :: k -> Type) xss yss.
    Iso (SOP f xss) (SOP f yss) (NS (NP f) xss) (NS (NP f) yss)
sop :: forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NS (NP f) xss) (f (NS (NP f) yss))
-> p (SOP f xss) (f (SOP f yss))
sop = (SOP f xss -> NS (NP f) xss)
-> (NS (NP f) yss -> SOP f yss)
-> Iso (SOP f xss) (SOP f yss) (NS (NP f) xss) (NS (NP f) yss)
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso SOP f xss -> NS (NP f) xss
forall {k} (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
unSOP NS (NP f) yss -> SOP f yss
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP

-- | Alias for 'sop'.
_SOP ::
    forall k (f :: k -> Type) xss yss.
    Iso (SOP f xss) (SOP f yss) (NS (NP f) xss) (NS (NP f) yss)
_SOP :: forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NS (NP f) xss) (f (NS (NP f) yss))
-> p (SOP f xss) (f (SOP f yss))
_SOP = p (NS (NP f) xss) (f (NS (NP f) yss))
-> p (SOP f xss) (f (SOP f yss))
forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NS (NP f) xss) (f (NS (NP f) yss))
-> p (SOP f xss) (f (SOP f yss))
sop

-- | The only field of 'POP'.
pop ::
    forall k (f :: k -> Type) xss yss.
    Iso (POP f xss) (POP f yss) (NP (NP f) xss) (NP (NP f) yss)
pop :: forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NP (NP f) xss) (f (NP (NP f) yss))
-> p (POP f xss) (f (POP f yss))
pop = (POP f xss -> NP (NP f) xss)
-> (NP (NP f) yss -> POP f yss)
-> Iso (POP f xss) (POP f yss) (NP (NP f) xss) (NP (NP f) yss)
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso POP f xss -> NP (NP f) xss
forall {k} (f :: k -> *) (xss :: [[k]]). POP f xss -> NP (NP f) xss
unPOP NP (NP f) yss -> POP f yss
forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
POP

-- | Alias for 'pop'.
_POP ::
    forall k (f :: k -> Type) xss yss.
    Iso (POP f xss) (POP f yss) (NP (NP f) xss) (NP (NP f) yss)
_POP :: forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NP (NP f) xss) (f (NP (NP f) yss))
-> p (POP f xss) (f (POP f yss))
_POP = p (NP (NP f) xss) (f (NP (NP f) yss))
-> p (POP f xss) (f (POP f yss))
forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NP (NP f) xss) (f (NP (NP f) yss))
-> p (POP f xss) (f (POP f yss))
pop

instance (t ~ SOP f xss) => Rewrapped (SOP f xss) t
instance Wrapped (SOP f xss) where
    type Unwrapped (SOP f xss) = NS (NP f) xss
    _Wrapped' :: Iso' (SOP f xss) (Unwrapped (SOP f xss))
_Wrapped' = p (NS (NP f) xss) (f (NS (NP f) xss))
-> p (SOP f xss) (f (SOP f xss))
p (Unwrapped (SOP f xss)) (f (Unwrapped (SOP f xss)))
-> p (SOP f xss) (f (SOP f xss))
forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NS (NP f) xss) (f (NS (NP f) yss))
-> p (SOP f xss) (f (SOP f yss))
sop

instance (t ~ POP f xss) => Rewrapped (POP f xss) t
instance Wrapped (POP f xss) where
    type Unwrapped (POP f xss) = NP (NP f) xss
    _Wrapped' :: Iso' (POP f xss) (Unwrapped (POP f xss))
_Wrapped' = p (NP (NP f) xss) (f (NP (NP f) xss))
-> p (POP f xss) (f (POP f xss))
p (Unwrapped (POP f xss)) (f (Unwrapped (POP f xss)))
-> p (POP f xss) (f (POP f xss))
forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NP (NP f) xss) (f (NP (NP f) yss))
-> p (POP f xss) (f (POP f yss))
pop

-------------------------------------------------------------------------------
-- Basic functors
-------------------------------------------------------------------------------

_I :: Iso (I a) (I b) a b
_I :: forall a b (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p a (f b) -> p (I a) (f (I b))
_I = (I a -> a) -> (b -> I b) -> Iso (I a) (I b) a b
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso I a -> a
forall a. I a -> a
unI b -> I b
forall a. a -> I a
I

_K :: Iso (K a c) (K b c) a b
_K :: forall {k} a (c :: k) b (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p a (f b) -> p (K a c) (f (K b c))
_K = (K a c -> a) -> (b -> K b c) -> Iso (K a c) (K b c) a b
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso K a c -> a
forall {k} a (b :: k). K a b -> a
unK b -> K b c
forall k a (b :: k). a -> K a b
K

instance (t ~ I a) => Rewrapped (I a) t
instance Wrapped (I a) where
    type Unwrapped (I a) = a
    _Wrapped' :: Iso' (I a) (Unwrapped (I a))
_Wrapped' = p a (f a) -> p (I a) (f (I a))
p (Unwrapped (I a)) (f (Unwrapped (I a))) -> p (I a) (f (I a))
forall a b (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p a (f b) -> p (I a) (f (I b))
_I

instance (t ~ K a b) => Rewrapped (K a b) t
instance Wrapped (K a b) where
    type Unwrapped (K a b) = a
    _Wrapped' :: Iso' (K a b) (Unwrapped (K a b))
_Wrapped' = p a (f a) -> p (K a b) (f (K a b))
p (Unwrapped (K a b)) (f (Unwrapped (K a b)))
-> p (K a b) (f (K a b))
forall {k} a (c :: k) b (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p a (f b) -> p (K a c) (f (K b c))
_K

-------------------------------------------------------------------------------
-- Products
-------------------------------------------------------------------------------

npSingleton ::
    forall k (f :: k -> Type) x y.
    Iso (NP f '[x]) (NP f '[y]) (f x) (f y)
npSingleton :: forall k (f :: k -> *) (x :: k) (y :: k) (p :: * -> * -> *)
       (f :: * -> *).
(Profunctor p, Functor f) =>
p (f x) (f (f y)) -> p (NP f '[x]) (f (NP f '[y]))
npSingleton = (NP f '[x] -> f x)
-> (f y -> NP f '[y]) -> Iso (NP f '[x]) (NP f '[y]) (f x) (f y)
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso NP f '[x] -> f x
g f y -> NP f '[y]
s
  where
    g :: NP f '[x] -> f x
    g :: NP f '[x] -> f x
g (f x
x  :* NP f xs
Nil)   = f x
f x
x

    s :: f y -> NP f '[y]
    s :: f y -> NP f '[y]
s f y
y = f y
y f y -> NP f '[] -> NP f '[y]
forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP f '[]
forall {k} (a :: k -> *). NP a '[]
Nil

type family UnSingleton (xs :: [k]) :: k where
    UnSingleton '[x] = x

instance (t ~ NS f xs, xs ~ '[x]) => Rewrapped (NS f xs) t
instance (xs ~ '[x]) => Wrapped (NS f xs) where
    type Unwrapped (NS f xs) = f (UnSingleton xs)
    _Wrapped' :: Iso' (NS f xs) (Unwrapped (NS f xs))
_Wrapped' = p (f x) (f (f x)) -> p (NS f '[x]) (f (NS f '[x]))
p (Unwrapped (NS f xs)) (f (Unwrapped (NS f xs)))
-> p (NS f xs) (f (NS f xs))
forall k (f :: k -> *) (x :: k) (y :: k) (p :: * -> * -> *)
       (f :: * -> *).
(Profunctor p, Functor f) =>
p (f x) (f (f y)) -> p (NS f '[x]) (f (NS f '[y]))
nsSingleton

npHead ::
    forall k (f :: k -> Type) x y zs.
    Lens (NP f (x ': zs)) (NP f (y ': zs)) (f x) (f y)
npHead :: forall k (f :: k -> *) (x :: k) (y :: k) (zs :: [k]) (f :: * -> *).
Functor f =>
(f x -> f (f y)) -> NP f (x : zs) -> f (NP f (y : zs))
npHead = (NP f (x : zs) -> f x)
-> (NP f (x : zs) -> f y -> NP f (y : zs))
-> Lens (NP f (x : zs)) (NP f (y : zs)) (f x) (f y)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens NP f (x : zs) -> f x
g NP f (x : zs) -> f y -> NP f (y : zs)
s
  where
    g :: NP f (x ': zs) -> f x
    g :: NP f (x : zs) -> f x
g (f x
x  :* NP f xs
_zs)   = f x
f x
x

    s :: NP f (x ': zs) -> f y -> NP f (y ': zs)
    s :: NP f (x : zs) -> f y -> NP f (y : zs)
s (f x
_x :*  NP f xs
zs) f y
y = f y
y f y -> NP f zs -> NP f (y : zs)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP f zs
NP f xs
zs

npTail ::
    forall k (f :: k -> Type) x ys zs.
    Lens (NP f (x ': ys)) (NP f (x ': zs)) (NP f ys) (NP f zs)
npTail :: forall k (f :: k -> *) (x :: k) (ys :: [k]) (zs :: [k])
       (f :: * -> *).
Functor f =>
(NP f ys -> f (NP f zs)) -> NP f (x : ys) -> f (NP f (x : zs))
npTail = (NP f (x : ys) -> NP f ys)
-> (NP f (x : ys) -> NP f zs -> NP f (x : zs))
-> Lens (NP f (x : ys)) (NP f (x : zs)) (NP f ys) (NP f zs)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens NP f (x : ys) -> NP f ys
g NP f (x : ys) -> NP f zs -> NP f (x : zs)
s
  where
    g :: NP f (x ': ys) -> NP f ys
    g :: NP f (x : ys) -> NP f ys
g (f x
_x :*  NP f xs
ys)    = NP f ys
NP f xs
ys

    s :: NP f (x ': ys) -> NP f zs -> NP f (x ': zs)
    s :: NP f (x : ys) -> NP f zs -> NP f (x : zs)
s (f x
x  :* NP f xs
_ys) NP f zs
zs = f x
f x
x f x -> NP f zs -> NP f (x : zs)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP f zs
zs

instance Field1 (NP f (x ': zs)) (NP f (y ': zs)) (f x) (f y) where _1 :: Lens (NP f (x : zs)) (NP f (y : zs)) (f x) (f y)
_1 = (f x -> f (f y)) -> NP f (x : zs) -> f (NP f (y : zs))
forall k (f :: k -> *) (x :: k) (y :: k) (zs :: [k]) (f :: * -> *).
Functor f =>
(f x -> f (f y)) -> NP f (x : zs) -> f (NP f (y : zs))
npHead
instance Field1 (POP f (x ': zs)) (POP f (y ': zs)) (NP f x) (NP f y) where _1 :: Lens (POP f (x : zs)) (POP f (y : zs)) (NP f x) (NP f y)
_1 = (NP (NP f) (x : zs) -> f (NP (NP f) (y : zs)))
-> POP f (x : zs) -> f (POP f (y : zs))
forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NP (NP f) xss) (f (NP (NP f) yss))
-> p (POP f xss) (f (POP f yss))
_POP ((NP (NP f) (x : zs) -> f (NP (NP f) (y : zs)))
 -> POP f (x : zs) -> f (POP f (y : zs)))
-> ((NP f x -> f (NP f y))
    -> NP (NP f) (x : zs) -> f (NP (NP f) (y : zs)))
-> (NP f x -> f (NP f y))
-> POP f (x : zs)
-> f (POP f (y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NP f x -> f (NP f y))
-> NP (NP f) (x : zs) -> f (NP (NP f) (y : zs))
forall s t a b. Field1 s t a b => Lens s t a b
Lens (NP (NP f) (x : zs)) (NP (NP f) (y : zs)) (NP f x) (NP f y)
_1

instance Field2 (NP f (a ': x ': zs)) (NP f (a ': y ': zs)) (f x) (f y) where _2 :: Lens (NP f (a : x : zs)) (NP f (a : y : zs)) (f x) (f y)
_2 = (NP f (x : zs) -> f (NP f (y : zs)))
-> NP f (a : x : zs) -> f (NP f (a : y : zs))
forall k (f :: k -> *) (x :: k) (ys :: [k]) (zs :: [k])
       (f :: * -> *).
Functor f =>
(NP f ys -> f (NP f zs)) -> NP f (x : ys) -> f (NP f (x : zs))
npTail ((NP f (x : zs) -> f (NP f (y : zs)))
 -> NP f (a : x : zs) -> f (NP f (a : y : zs)))
-> ((f x -> f (f y)) -> NP f (x : zs) -> f (NP f (y : zs)))
-> (f x -> f (f y))
-> NP f (a : x : zs)
-> f (NP f (a : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f x -> f (f y)) -> NP f (x : zs) -> f (NP f (y : zs))
forall s t a b. Field1 s t a b => Lens s t a b
Lens (NP f (x : zs)) (NP f (y : zs)) (f x) (f y)
_1
instance Field2 (POP f (a ': x ': zs)) (POP f (a ': y ': zs)) (NP f x) (NP f y) where _2 :: Lens (POP f (a : x : zs)) (POP f (a : y : zs)) (NP f x) (NP f y)
_2 = (NP (NP f) (a : x : zs) -> f (NP (NP f) (a : y : zs)))
-> POP f (a : x : zs) -> f (POP f (a : y : zs))
forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NP (NP f) xss) (f (NP (NP f) yss))
-> p (POP f xss) (f (POP f yss))
_POP ((NP (NP f) (a : x : zs) -> f (NP (NP f) (a : y : zs)))
 -> POP f (a : x : zs) -> f (POP f (a : y : zs)))
-> ((NP f x -> f (NP f y))
    -> NP (NP f) (a : x : zs) -> f (NP (NP f) (a : y : zs)))
-> (NP f x -> f (NP f y))
-> POP f (a : x : zs)
-> f (POP f (a : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NP f x -> f (NP f y))
-> NP (NP f) (a : x : zs) -> f (NP (NP f) (a : y : zs))
forall s t a b. Field2 s t a b => Lens s t a b
Lens
  (NP (NP f) (a : x : zs)) (NP (NP f) (a : y : zs)) (NP f x) (NP f y)
_2

instance Field3 (NP f (a ': b ': x ': zs)) (NP f (a ': b ': y ': zs)) (f x) (f y) where _3 :: Lens (NP f (a : b : x : zs)) (NP f (a : b : y : zs)) (f x) (f y)
_3 = (NP f (b : x : zs) -> f (NP f (b : y : zs)))
-> NP f (a : b : x : zs) -> f (NP f (a : b : y : zs))
forall k (f :: k -> *) (x :: k) (ys :: [k]) (zs :: [k])
       (f :: * -> *).
Functor f =>
(NP f ys -> f (NP f zs)) -> NP f (x : ys) -> f (NP f (x : zs))
npTail ((NP f (b : x : zs) -> f (NP f (b : y : zs)))
 -> NP f (a : b : x : zs) -> f (NP f (a : b : y : zs)))
-> ((f x -> f (f y)) -> NP f (b : x : zs) -> f (NP f (b : y : zs)))
-> (f x -> f (f y))
-> NP f (a : b : x : zs)
-> f (NP f (a : b : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f x -> f (f y)) -> NP f (b : x : zs) -> f (NP f (b : y : zs))
forall s t a b. Field2 s t a b => Lens s t a b
Lens (NP f (b : x : zs)) (NP f (b : y : zs)) (f x) (f y)
_2
instance Field3 (POP f (a ': b ': x ': zs)) (POP f (a ': b ': y ': zs)) (NP f x) (NP f y) where _3 :: Lens
  (POP f (a : b : x : zs)) (POP f (a : b : y : zs)) (NP f x) (NP f y)
_3 = (NP (NP f) (a : b : x : zs) -> f (NP (NP f) (a : b : y : zs)))
-> POP f (a : b : x : zs) -> f (POP f (a : b : y : zs))
forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NP (NP f) xss) (f (NP (NP f) yss))
-> p (POP f xss) (f (POP f yss))
_POP ((NP (NP f) (a : b : x : zs) -> f (NP (NP f) (a : b : y : zs)))
 -> POP f (a : b : x : zs) -> f (POP f (a : b : y : zs)))
-> ((NP f x -> f (NP f y))
    -> NP (NP f) (a : b : x : zs) -> f (NP (NP f) (a : b : y : zs)))
-> (NP f x -> f (NP f y))
-> POP f (a : b : x : zs)
-> f (POP f (a : b : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NP f x -> f (NP f y))
-> NP (NP f) (a : b : x : zs) -> f (NP (NP f) (a : b : y : zs))
forall s t a b. Field3 s t a b => Lens s t a b
Lens
  (NP (NP f) (a : b : x : zs))
  (NP (NP f) (a : b : y : zs))
  (NP f x)
  (NP f y)
_3

instance Field4 (NP f (a ': b ': c ': x ': zs)) (NP f (a ': b ': c ': y ': zs)) (f x) (f y) where _4 :: Lens
  (NP f (a : b : c : x : zs)) (NP f (a : b : c : y : zs)) (f x) (f y)
_4 = (NP f (b : c : x : zs) -> f (NP f (b : c : y : zs)))
-> NP f (a : b : c : x : zs) -> f (NP f (a : b : c : y : zs))
forall k (f :: k -> *) (x :: k) (ys :: [k]) (zs :: [k])
       (f :: * -> *).
Functor f =>
(NP f ys -> f (NP f zs)) -> NP f (x : ys) -> f (NP f (x : zs))
npTail ((NP f (b : c : x : zs) -> f (NP f (b : c : y : zs)))
 -> NP f (a : b : c : x : zs) -> f (NP f (a : b : c : y : zs)))
-> ((f x -> f (f y))
    -> NP f (b : c : x : zs) -> f (NP f (b : c : y : zs)))
-> (f x -> f (f y))
-> NP f (a : b : c : x : zs)
-> f (NP f (a : b : c : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f x -> f (f y))
-> NP f (b : c : x : zs) -> f (NP f (b : c : y : zs))
forall s t a b. Field3 s t a b => Lens s t a b
Lens (NP f (b : c : x : zs)) (NP f (b : c : y : zs)) (f x) (f y)
_3
instance Field4 (POP f (a ': b ': c ': x ': zs)) (POP f (a ': b ': c ': y ': zs)) (NP f x) (NP f y) where _4 :: Lens
  (POP f (a : b : c : x : zs))
  (POP f (a : b : c : y : zs))
  (NP f x)
  (NP f y)
_4 = (NP (NP f) (a : b : c : x : zs)
 -> f (NP (NP f) (a : b : c : y : zs)))
-> POP f (a : b : c : x : zs) -> f (POP f (a : b : c : y : zs))
forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NP (NP f) xss) (f (NP (NP f) yss))
-> p (POP f xss) (f (POP f yss))
_POP ((NP (NP f) (a : b : c : x : zs)
  -> f (NP (NP f) (a : b : c : y : zs)))
 -> POP f (a : b : c : x : zs) -> f (POP f (a : b : c : y : zs)))
-> ((NP f x -> f (NP f y))
    -> NP (NP f) (a : b : c : x : zs)
    -> f (NP (NP f) (a : b : c : y : zs)))
-> (NP f x -> f (NP f y))
-> POP f (a : b : c : x : zs)
-> f (POP f (a : b : c : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NP f x -> f (NP f y))
-> NP (NP f) (a : b : c : x : zs)
-> f (NP (NP f) (a : b : c : y : zs))
forall s t a b. Field4 s t a b => Lens s t a b
Lens
  (NP (NP f) (a : b : c : x : zs))
  (NP (NP f) (a : b : c : y : zs))
  (NP f x)
  (NP f y)
_4

instance Field5 (NP f (a ': b ': c ': d ': x ': zs)) (NP f (a ': b ': c ': d ': y ': zs)) (f x) (f y) where _5 :: Lens
  (NP f (a : b : c : d : x : zs))
  (NP f (a : b : c : d : y : zs))
  (f x)
  (f y)
_5 = (NP f (b : c : d : x : zs) -> f (NP f (b : c : d : y : zs)))
-> NP f (a : b : c : d : x : zs)
-> f (NP f (a : b : c : d : y : zs))
forall k (f :: k -> *) (x :: k) (ys :: [k]) (zs :: [k])
       (f :: * -> *).
Functor f =>
(NP f ys -> f (NP f zs)) -> NP f (x : ys) -> f (NP f (x : zs))
npTail ((NP f (b : c : d : x : zs) -> f (NP f (b : c : d : y : zs)))
 -> NP f (a : b : c : d : x : zs)
 -> f (NP f (a : b : c : d : y : zs)))
-> ((f x -> f (f y))
    -> NP f (b : c : d : x : zs) -> f (NP f (b : c : d : y : zs)))
-> (f x -> f (f y))
-> NP f (a : b : c : d : x : zs)
-> f (NP f (a : b : c : d : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f x -> f (f y))
-> NP f (b : c : d : x : zs) -> f (NP f (b : c : d : y : zs))
forall s t a b. Field4 s t a b => Lens s t a b
Lens
  (NP f (b : c : d : x : zs)) (NP f (b : c : d : y : zs)) (f x) (f y)
_4
instance Field5 (POP f (a ': b ': c ': d ': x ': zs)) (POP f (a ': b ': c ': d ': y ': zs)) (NP f x) (NP f y) where _5 :: Lens
  (POP f (a : b : c : d : x : zs))
  (POP f (a : b : c : d : y : zs))
  (NP f x)
  (NP f y)
_5 = (NP (NP f) (a : b : c : d : x : zs)
 -> f (NP (NP f) (a : b : c : d : y : zs)))
-> POP f (a : b : c : d : x : zs)
-> f (POP f (a : b : c : d : y : zs))
forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NP (NP f) xss) (f (NP (NP f) yss))
-> p (POP f xss) (f (POP f yss))
_POP ((NP (NP f) (a : b : c : d : x : zs)
  -> f (NP (NP f) (a : b : c : d : y : zs)))
 -> POP f (a : b : c : d : x : zs)
 -> f (POP f (a : b : c : d : y : zs)))
-> ((NP f x -> f (NP f y))
    -> NP (NP f) (a : b : c : d : x : zs)
    -> f (NP (NP f) (a : b : c : d : y : zs)))
-> (NP f x -> f (NP f y))
-> POP f (a : b : c : d : x : zs)
-> f (POP f (a : b : c : d : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NP f x -> f (NP f y))
-> NP (NP f) (a : b : c : d : x : zs)
-> f (NP (NP f) (a : b : c : d : y : zs))
forall s t a b. Field5 s t a b => Lens s t a b
Lens
  (NP (NP f) (a : b : c : d : x : zs))
  (NP (NP f) (a : b : c : d : y : zs))
  (NP f x)
  (NP f y)
_5

instance Field6 (NP f (a ': b ': c ': d ': e ': x ': zs)) (NP f (a ': b ': c ': d ': e ': y ': zs)) (f x) (f y) where _6 :: Lens
  (NP f (a : b : c : d : e : x : zs))
  (NP f (a : b : c : d : e : y : zs))
  (f x)
  (f y)
_6 = (NP f (b : c : d : e : x : zs)
 -> f (NP f (b : c : d : e : y : zs)))
-> NP f (a : b : c : d : e : x : zs)
-> f (NP f (a : b : c : d : e : y : zs))
forall k (f :: k -> *) (x :: k) (ys :: [k]) (zs :: [k])
       (f :: * -> *).
Functor f =>
(NP f ys -> f (NP f zs)) -> NP f (x : ys) -> f (NP f (x : zs))
npTail ((NP f (b : c : d : e : x : zs)
  -> f (NP f (b : c : d : e : y : zs)))
 -> NP f (a : b : c : d : e : x : zs)
 -> f (NP f (a : b : c : d : e : y : zs)))
-> ((f x -> f (f y))
    -> NP f (b : c : d : e : x : zs)
    -> f (NP f (b : c : d : e : y : zs)))
-> (f x -> f (f y))
-> NP f (a : b : c : d : e : x : zs)
-> f (NP f (a : b : c : d : e : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f x -> f (f y))
-> NP f (b : c : d : e : x : zs)
-> f (NP f (b : c : d : e : y : zs))
forall s t a b. Field5 s t a b => Lens s t a b
Lens
  (NP f (b : c : d : e : x : zs))
  (NP f (b : c : d : e : y : zs))
  (f x)
  (f y)
_5
instance Field6 (POP f (a ': b ': c ': d ': e ': x ': zs)) (POP f (a ': b ': c ': d ': e ': y ': zs)) (NP f x) (NP f y) where _6 :: Lens
  (POP f (a : b : c : d : e : x : zs))
  (POP f (a : b : c : d : e : y : zs))
  (NP f x)
  (NP f y)
_6 = (NP (NP f) (a : b : c : d : e : x : zs)
 -> f (NP (NP f) (a : b : c : d : e : y : zs)))
-> POP f (a : b : c : d : e : x : zs)
-> f (POP f (a : b : c : d : e : y : zs))
forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NP (NP f) xss) (f (NP (NP f) yss))
-> p (POP f xss) (f (POP f yss))
_POP ((NP (NP f) (a : b : c : d : e : x : zs)
  -> f (NP (NP f) (a : b : c : d : e : y : zs)))
 -> POP f (a : b : c : d : e : x : zs)
 -> f (POP f (a : b : c : d : e : y : zs)))
-> ((NP f x -> f (NP f y))
    -> NP (NP f) (a : b : c : d : e : x : zs)
    -> f (NP (NP f) (a : b : c : d : e : y : zs)))
-> (NP f x -> f (NP f y))
-> POP f (a : b : c : d : e : x : zs)
-> f (POP f (a : b : c : d : e : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NP f x -> f (NP f y))
-> NP (NP f) (a : b : c : d : e : x : zs)
-> f (NP (NP f) (a : b : c : d : e : y : zs))
forall s t a b. Field6 s t a b => Lens s t a b
Lens
  (NP (NP f) (a : b : c : d : e : x : zs))
  (NP (NP f) (a : b : c : d : e : y : zs))
  (NP f x)
  (NP f y)
_6

instance Field7 (NP f' (a ': b ': c ': d ': e ': f ': x ': zs)) (NP f' (a ': b ': c ': d ': e ': f ': y ': zs)) (f' x) (f' y) where _7 :: Lens
  (NP f' (a : b : c : d : e : f : x : zs))
  (NP f' (a : b : c : d : e : f : y : zs))
  (f' x)
  (f' y)
_7 = (NP f' (b : c : d : e : f : x : zs)
 -> f (NP f' (b : c : d : e : f : y : zs)))
-> NP f' (a : b : c : d : e : f : x : zs)
-> f (NP f' (a : b : c : d : e : f : y : zs))
forall k (f :: k -> *) (x :: k) (ys :: [k]) (zs :: [k])
       (f :: * -> *).
Functor f =>
(NP f ys -> f (NP f zs)) -> NP f (x : ys) -> f (NP f (x : zs))
npTail ((NP f' (b : c : d : e : f : x : zs)
  -> f (NP f' (b : c : d : e : f : y : zs)))
 -> NP f' (a : b : c : d : e : f : x : zs)
 -> f (NP f' (a : b : c : d : e : f : y : zs)))
-> ((f' x -> f (f' y))
    -> NP f' (b : c : d : e : f : x : zs)
    -> f (NP f' (b : c : d : e : f : y : zs)))
-> (f' x -> f (f' y))
-> NP f' (a : b : c : d : e : f : x : zs)
-> f (NP f' (a : b : c : d : e : f : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f' x -> f (f' y))
-> NP f' (b : c : d : e : f : x : zs)
-> f (NP f' (b : c : d : e : f : y : zs))
forall s t a b. Field6 s t a b => Lens s t a b
Lens
  (NP f' (b : c : d : e : f : x : zs))
  (NP f' (b : c : d : e : f : y : zs))
  (f' x)
  (f' y)
_6
instance Field7 (POP f' (a ': b ': c ': d ': e ': f ': x ': zs)) (POP f' (a ': b ': c ': d ': e ': f ': y ': zs)) (NP f' x) (NP f' y) where _7 :: Lens
  (POP f' (a : b : c : d : e : f : x : zs))
  (POP f' (a : b : c : d : e : f : y : zs))
  (NP f' x)
  (NP f' y)
_7 = (NP (NP f') (a : b : c : d : e : f : x : zs)
 -> f (NP (NP f') (a : b : c : d : e : f : y : zs)))
-> POP f' (a : b : c : d : e : f : x : zs)
-> f (POP f' (a : b : c : d : e : f : y : zs))
forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NP (NP f) xss) (f (NP (NP f) yss))
-> p (POP f xss) (f (POP f yss))
_POP ((NP (NP f') (a : b : c : d : e : f : x : zs)
  -> f (NP (NP f') (a : b : c : d : e : f : y : zs)))
 -> POP f' (a : b : c : d : e : f : x : zs)
 -> f (POP f' (a : b : c : d : e : f : y : zs)))
-> ((NP f' x -> f (NP f' y))
    -> NP (NP f') (a : b : c : d : e : f : x : zs)
    -> f (NP (NP f') (a : b : c : d : e : f : y : zs)))
-> (NP f' x -> f (NP f' y))
-> POP f' (a : b : c : d : e : f : x : zs)
-> f (POP f' (a : b : c : d : e : f : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NP f' x -> f (NP f' y))
-> NP (NP f') (a : b : c : d : e : f : x : zs)
-> f (NP (NP f') (a : b : c : d : e : f : y : zs))
forall s t a b. Field7 s t a b => Lens s t a b
Lens
  (NP (NP f') (a : b : c : d : e : f : x : zs))
  (NP (NP f') (a : b : c : d : e : f : y : zs))
  (NP f' x)
  (NP f' y)
_7

instance Field8 (NP f' (a ': b ': c ': d ': e ': f ': g ': x ': zs)) (NP f' (a ': b ': c ': d ': e ': f ': g ': y ': zs)) (f' x) (f' y) where _8 :: Lens
  (NP f' (a : b : c : d : e : f : g : x : zs))
  (NP f' (a : b : c : d : e : f : g : y : zs))
  (f' x)
  (f' y)
_8 = (NP f' (b : c : d : e : f : g : x : zs)
 -> f (NP f' (b : c : d : e : f : g : y : zs)))
-> NP f' (a : b : c : d : e : f : g : x : zs)
-> f (NP f' (a : b : c : d : e : f : g : y : zs))
forall k (f :: k -> *) (x :: k) (ys :: [k]) (zs :: [k])
       (f :: * -> *).
Functor f =>
(NP f ys -> f (NP f zs)) -> NP f (x : ys) -> f (NP f (x : zs))
npTail ((NP f' (b : c : d : e : f : g : x : zs)
  -> f (NP f' (b : c : d : e : f : g : y : zs)))
 -> NP f' (a : b : c : d : e : f : g : x : zs)
 -> f (NP f' (a : b : c : d : e : f : g : y : zs)))
-> ((f' x -> f (f' y))
    -> NP f' (b : c : d : e : f : g : x : zs)
    -> f (NP f' (b : c : d : e : f : g : y : zs)))
-> (f' x -> f (f' y))
-> NP f' (a : b : c : d : e : f : g : x : zs)
-> f (NP f' (a : b : c : d : e : f : g : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f' x -> f (f' y))
-> NP f' (b : c : d : e : f : g : x : zs)
-> f (NP f' (b : c : d : e : f : g : y : zs))
forall s t a b. Field7 s t a b => Lens s t a b
Lens
  (NP f' (b : c : d : e : f : g : x : zs))
  (NP f' (b : c : d : e : f : g : y : zs))
  (f' x)
  (f' y)
_7
instance Field8 (POP f' (a ': b ': c ': d ': e ': f ': g ': x ': zs)) (POP f' (a ': b ': c ': d ': e ': f ': g ': y ': zs)) (NP f' x) (NP f' y) where _8 :: Lens
  (POP f' (a : b : c : d : e : f : g : x : zs))
  (POP f' (a : b : c : d : e : f : g : y : zs))
  (NP f' x)
  (NP f' y)
_8 = (NP (NP f') (a : b : c : d : e : f : g : x : zs)
 -> f (NP (NP f') (a : b : c : d : e : f : g : y : zs)))
-> POP f' (a : b : c : d : e : f : g : x : zs)
-> f (POP f' (a : b : c : d : e : f : g : y : zs))
forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NP (NP f) xss) (f (NP (NP f) yss))
-> p (POP f xss) (f (POP f yss))
_POP ((NP (NP f') (a : b : c : d : e : f : g : x : zs)
  -> f (NP (NP f') (a : b : c : d : e : f : g : y : zs)))
 -> POP f' (a : b : c : d : e : f : g : x : zs)
 -> f (POP f' (a : b : c : d : e : f : g : y : zs)))
-> ((NP f' x -> f (NP f' y))
    -> NP (NP f') (a : b : c : d : e : f : g : x : zs)
    -> f (NP (NP f') (a : b : c : d : e : f : g : y : zs)))
-> (NP f' x -> f (NP f' y))
-> POP f' (a : b : c : d : e : f : g : x : zs)
-> f (POP f' (a : b : c : d : e : f : g : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NP f' x -> f (NP f' y))
-> NP (NP f') (a : b : c : d : e : f : g : x : zs)
-> f (NP (NP f') (a : b : c : d : e : f : g : y : zs))
forall s t a b. Field8 s t a b => Lens s t a b
Lens
  (NP (NP f') (a : b : c : d : e : f : g : x : zs))
  (NP (NP f') (a : b : c : d : e : f : g : y : zs))
  (NP f' x)
  (NP f' y)
_8

instance Field9 (NP f' (a ': b ': c ': d ': e ': f ': g ': h ': x ': zs)) (NP f' (a ': b ': c ': d ': e ': f ': g ': h ': y ': zs)) (f' x) (f' y) where _9 :: Lens
  (NP f' (a : b : c : d : e : f : g : h : x : zs))
  (NP f' (a : b : c : d : e : f : g : h : y : zs))
  (f' x)
  (f' y)
_9 = (NP f' (b : c : d : e : f : g : h : x : zs)
 -> f (NP f' (b : c : d : e : f : g : h : y : zs)))
-> NP f' (a : b : c : d : e : f : g : h : x : zs)
-> f (NP f' (a : b : c : d : e : f : g : h : y : zs))
forall k (f :: k -> *) (x :: k) (ys :: [k]) (zs :: [k])
       (f :: * -> *).
Functor f =>
(NP f ys -> f (NP f zs)) -> NP f (x : ys) -> f (NP f (x : zs))
npTail ((NP f' (b : c : d : e : f : g : h : x : zs)
  -> f (NP f' (b : c : d : e : f : g : h : y : zs)))
 -> NP f' (a : b : c : d : e : f : g : h : x : zs)
 -> f (NP f' (a : b : c : d : e : f : g : h : y : zs)))
-> ((f' x -> f (f' y))
    -> NP f' (b : c : d : e : f : g : h : x : zs)
    -> f (NP f' (b : c : d : e : f : g : h : y : zs)))
-> (f' x -> f (f' y))
-> NP f' (a : b : c : d : e : f : g : h : x : zs)
-> f (NP f' (a : b : c : d : e : f : g : h : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f' x -> f (f' y))
-> NP f' (b : c : d : e : f : g : h : x : zs)
-> f (NP f' (b : c : d : e : f : g : h : y : zs))
forall s t a b. Field8 s t a b => Lens s t a b
Lens
  (NP f' (b : c : d : e : f : g : h : x : zs))
  (NP f' (b : c : d : e : f : g : h : y : zs))
  (f' x)
  (f' y)
_8
instance Field9 (POP f' (a ': b ': c ': d ': e ': f ': g ': h ': x ': zs)) (POP f' (a ': b ': c ': d ': e ': f ': g ': h ': y ': zs)) (NP f' x) (NP f' y) where _9 :: Lens
  (POP f' (a : b : c : d : e : f : g : h : x : zs))
  (POP f' (a : b : c : d : e : f : g : h : y : zs))
  (NP f' x)
  (NP f' y)
_9 = (NP (NP f') (a : b : c : d : e : f : g : h : x : zs)
 -> f (NP (NP f') (a : b : c : d : e : f : g : h : y : zs)))
-> POP f' (a : b : c : d : e : f : g : h : x : zs)
-> f (POP f' (a : b : c : d : e : f : g : h : y : zs))
forall k (f :: k -> *) (xss :: [[k]]) (yss :: [[k]])
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (NP (NP f) xss) (f (NP (NP f) yss))
-> p (POP f xss) (f (POP f yss))
_POP ((NP (NP f') (a : b : c : d : e : f : g : h : x : zs)
  -> f (NP (NP f') (a : b : c : d : e : f : g : h : y : zs)))
 -> POP f' (a : b : c : d : e : f : g : h : x : zs)
 -> f (POP f' (a : b : c : d : e : f : g : h : y : zs)))
-> ((NP f' x -> f (NP f' y))
    -> NP (NP f') (a : b : c : d : e : f : g : h : x : zs)
    -> f (NP (NP f') (a : b : c : d : e : f : g : h : y : zs)))
-> (NP f' x -> f (NP f' y))
-> POP f' (a : b : c : d : e : f : g : h : x : zs)
-> f (POP f' (a : b : c : d : e : f : g : h : y : zs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NP f' x -> f (NP f' y))
-> NP (NP f') (a : b : c : d : e : f : g : h : x : zs)
-> f (NP (NP f') (a : b : c : d : e : f : g : h : y : zs))
forall s t a b. Field9 s t a b => Lens s t a b
Lens
  (NP (NP f') (a : b : c : d : e : f : g : h : x : zs))
  (NP (NP f') (a : b : c : d : e : f : g : h : y : zs))
  (NP f' x)
  (NP f' y)
_9

-------------------------------------------------------------------------------
-- Sums
-------------------------------------------------------------------------------

nsSingleton ::
    forall k (f :: k -> Type) x y.
    Iso (NS f '[x]) (NS f '[y]) (f x) (f y)
nsSingleton :: forall k (f :: k -> *) (x :: k) (y :: k) (p :: * -> * -> *)
       (f :: * -> *).
(Profunctor p, Functor f) =>
p (f x) (f (f y)) -> p (NS f '[x]) (f (NS f '[y]))
nsSingleton = (NS f '[x] -> f x)
-> (f y -> NS f '[y]) -> Iso (NS f '[x]) (NS f '[y]) (f x) (f y)
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso NS f '[x] -> f x
g f y -> NS f '[y]
forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z
  where
    g :: NS f '[x] -> f x
    g :: NS f '[x] -> f x
g (Z f x
x)   = f x
f x
x
    g (S NS f xs
v) = case NS f xs
v of {}

_Z ::
    forall k (f :: k -> Type) x y zs.
    Prism (NS f (x ': zs)) (NS f (y ': zs)) (f x) (f y)
_Z :: forall k (f :: k -> *) (x :: k) (y :: k) (zs :: [k])
       (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (f x) (f (f y)) -> p (NS f (x : zs)) (f (NS f (y : zs)))
_Z = (f y -> NS f (y : zs))
-> (NS f (x : zs) -> Either (NS f (y : zs)) (f x))
-> Prism (NS f (x : zs)) (NS f (y : zs)) (f x) (f y)
forall b t s a. (b -> t) -> (s -> Either t a) -> Prism s t a b
prism f y -> NS f (y : zs)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z NS f (x : zs) -> Either (NS f (y : zs)) (f x)
p
  where
    p :: NS f (x ': zs) -> Either (NS f (y ': zs)) (f x)
    p :: NS f (x : zs) -> Either (NS f (y : zs)) (f x)
p (Z f x
x)  = f x -> Either (NS f (y : zs)) (f x)
forall a b. b -> Either a b
Right f x
f x
x
    p (S NS f xs
xs) = NS f (y : zs) -> Either (NS f (y : zs)) (f x)
forall a b. a -> Either a b
Left (NS f zs -> NS f (y : zs)
forall {k} (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S NS f zs
NS f xs
xs)

_S ::
    forall k (f :: k -> Type) x ys zs.
    Prism (NS f (x ': ys)) (NS f (x ': zs)) (NS f ys) (NS f zs)
_S :: forall k (f :: k -> *) (x :: k) (ys :: [k]) (zs :: [k])
       (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (NS f ys) (f (NS f zs)) -> p (NS f (x : ys)) (f (NS f (x : zs)))
_S = (NS f zs -> NS f (x : zs))
-> (NS f (x : ys) -> Either (NS f (x : zs)) (NS f ys))
-> Prism (NS f (x : ys)) (NS f (x : zs)) (NS f ys) (NS f zs)
forall b t s a. (b -> t) -> (s -> Either t a) -> Prism s t a b
prism NS f zs -> NS f (x : zs)
forall {k} (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S NS f (x : ys) -> Either (NS f (x : zs)) (NS f ys)
p
  where
    p :: NS f (x ': ys) -> Either (NS f (x ': zs)) (NS f ys)
    p :: NS f (x : ys) -> Either (NS f (x : zs)) (NS f ys)
p (Z f x
x)  = NS f (x : zs) -> Either (NS f (x : zs)) (NS f ys)
forall a b. a -> Either a b
Left (NS f (x : zs) -> Either (NS f (x : zs)) (NS f ys))
-> NS f (x : zs) -> Either (NS f (x : zs)) (NS f ys)
forall a b. (a -> b) -> a -> b
$ f x -> NS f (x : zs)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z f x
f x
x
    p (S NS f xs
xs) = NS f ys -> Either (NS f (x : zs)) (NS f ys)
forall a b. b -> Either a b
Right NS f ys
NS f xs
xs

-------------------------------------------------------------------------------
-- DatatypeInfo
-------------------------------------------------------------------------------

moduleName :: Lens' (DatatypeInfo xss) ModuleName
moduleName :: forall (xss :: [[*]]) (f :: * -> *).
Functor f =>
(ModuleName -> f ModuleName)
-> DatatypeInfo xss -> f (DatatypeInfo xss)
moduleName = (DatatypeInfo xss -> ModuleName)
-> (DatatypeInfo xss -> ModuleName -> DatatypeInfo xss)
-> Lens (DatatypeInfo xss) (DatatypeInfo xss) ModuleName ModuleName
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens DatatypeInfo xss -> ModuleName
forall (xss :: [[*]]). DatatypeInfo xss -> ModuleName
g DatatypeInfo xss -> ModuleName -> DatatypeInfo xss
forall (xss :: [[*]]).
DatatypeInfo xss -> ModuleName -> DatatypeInfo xss
s
  where
    g :: DatatypeInfo xss -> ModuleName
    g :: forall (xss :: [[*]]). DatatypeInfo xss -> ModuleName
g (ADT ModuleName
m ModuleName
_ NP ConstructorInfo xss
_ POP StrictnessInfo xss
_)   = ModuleName
m
    g (Newtype ModuleName
m ModuleName
_ ConstructorInfo '[x]
_) = ModuleName
m

    s :: DatatypeInfo xss -> ModuleName -> DatatypeInfo xss
    s :: forall (xss :: [[*]]).
DatatypeInfo xss -> ModuleName -> DatatypeInfo xss
s (ADT ModuleName
_ ModuleName
n NP ConstructorInfo xss
cs POP StrictnessInfo xss
ss) ModuleName
m = ModuleName
-> ModuleName
-> NP ConstructorInfo xss
-> POP StrictnessInfo xss
-> DatatypeInfo xss
forall (a :: [[*]]).
ModuleName
-> ModuleName
-> NP ConstructorInfo a
-> POP StrictnessInfo a
-> DatatypeInfo a
ADT ModuleName
m ModuleName
n NP ConstructorInfo xss
cs POP StrictnessInfo xss
ss
    s (Newtype ModuleName
_ ModuleName
n ConstructorInfo '[x]
c) ModuleName
m = ModuleName
-> ModuleName -> ConstructorInfo '[x] -> DatatypeInfo '[ '[x]]
forall x.
ModuleName
-> ModuleName -> ConstructorInfo '[x] -> DatatypeInfo '[ '[x]]
Newtype ModuleName
m ModuleName
n ConstructorInfo '[x]
c

datatypeName :: Lens' (DatatypeInfo xss) DatatypeName
datatypeName :: forall (xss :: [[*]]) (f :: * -> *).
Functor f =>
(ModuleName -> f ModuleName)
-> DatatypeInfo xss -> f (DatatypeInfo xss)
datatypeName = (DatatypeInfo xss -> ModuleName)
-> (DatatypeInfo xss -> ModuleName -> DatatypeInfo xss)
-> Lens (DatatypeInfo xss) (DatatypeInfo xss) ModuleName ModuleName
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens DatatypeInfo xss -> ModuleName
forall (xss :: [[*]]). DatatypeInfo xss -> ModuleName
g DatatypeInfo xss -> ModuleName -> DatatypeInfo xss
forall (xss :: [[*]]).
DatatypeInfo xss -> ModuleName -> DatatypeInfo xss
s
  where
    g :: DatatypeInfo xss -> DatatypeName
    g :: forall (xss :: [[*]]). DatatypeInfo xss -> ModuleName
g (ADT ModuleName
_ ModuleName
n NP ConstructorInfo xss
_ POP StrictnessInfo xss
_)   = ModuleName
n
    g (Newtype ModuleName
_ ModuleName
n ConstructorInfo '[x]
_) = ModuleName
n

    s :: DatatypeInfo xss -> DatatypeName -> DatatypeInfo xss
    s :: forall (xss :: [[*]]).
DatatypeInfo xss -> ModuleName -> DatatypeInfo xss
s (ADT ModuleName
m ModuleName
_ NP ConstructorInfo xss
cs POP StrictnessInfo xss
ss) ModuleName
n = ModuleName
-> ModuleName
-> NP ConstructorInfo xss
-> POP StrictnessInfo xss
-> DatatypeInfo xss
forall (a :: [[*]]).
ModuleName
-> ModuleName
-> NP ConstructorInfo a
-> POP StrictnessInfo a
-> DatatypeInfo a
ADT ModuleName
m ModuleName
n NP ConstructorInfo xss
cs POP StrictnessInfo xss
ss
    s (Newtype ModuleName
m ModuleName
_ ConstructorInfo '[x]
c) ModuleName
n = ModuleName
-> ModuleName -> ConstructorInfo '[x] -> DatatypeInfo '[ '[x]]
forall x.
ModuleName
-> ModuleName -> ConstructorInfo '[x] -> DatatypeInfo '[ '[x]]
Newtype ModuleName
m ModuleName
n ConstructorInfo '[x]
c

constructorInfo :: Lens' (DatatypeInfo xss) (NP ConstructorInfo xss)
constructorInfo :: forall (xss :: [[*]]) (f :: * -> *).
Functor f =>
(NP ConstructorInfo xss -> f (NP ConstructorInfo xss))
-> DatatypeInfo xss -> f (DatatypeInfo xss)
constructorInfo = (DatatypeInfo xss -> NP ConstructorInfo xss)
-> (DatatypeInfo xss -> NP ConstructorInfo xss -> DatatypeInfo xss)
-> Lens
     (DatatypeInfo xss)
     (DatatypeInfo xss)
     (NP ConstructorInfo xss)
     (NP ConstructorInfo xss)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens DatatypeInfo xss -> NP ConstructorInfo xss
forall (xss :: [[*]]). DatatypeInfo xss -> NP ConstructorInfo xss
g DatatypeInfo xss -> NP ConstructorInfo xss -> DatatypeInfo xss
forall (xss :: [[*]]).
DatatypeInfo xss -> NP ConstructorInfo xss -> DatatypeInfo xss
s
  where
    g :: DatatypeInfo xss -> NP ConstructorInfo xss
    g :: forall (xss :: [[*]]). DatatypeInfo xss -> NP ConstructorInfo xss
g (ADT ModuleName
_ ModuleName
_ NP ConstructorInfo xss
cs POP StrictnessInfo xss
_)  = NP ConstructorInfo xss
cs
    g (Newtype ModuleName
_ ModuleName
_ ConstructorInfo '[x]
c) = ConstructorInfo '[x]
c ConstructorInfo '[x]
-> NP ConstructorInfo '[] -> NP ConstructorInfo '[ '[x]]
forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP ConstructorInfo '[]
forall {k} (a :: k -> *). NP a '[]
Nil

    s :: DatatypeInfo xss -> NP ConstructorInfo xss -> DatatypeInfo xss
    s :: forall (xss :: [[*]]).
DatatypeInfo xss -> NP ConstructorInfo xss -> DatatypeInfo xss
s (ADT ModuleName
m ModuleName
n NP ConstructorInfo xss
_ POP StrictnessInfo xss
ss)  NP ConstructorInfo xss
cs          = ModuleName
-> ModuleName
-> NP ConstructorInfo xss
-> POP StrictnessInfo xss
-> DatatypeInfo xss
forall (a :: [[*]]).
ModuleName
-> ModuleName
-> NP ConstructorInfo a
-> POP StrictnessInfo a
-> DatatypeInfo a
ADT ModuleName
m ModuleName
n NP ConstructorInfo xss
cs POP StrictnessInfo xss
ss
    s (Newtype ModuleName
m ModuleName
n ConstructorInfo '[x]
_) (ConstructorInfo x
c :* NP ConstructorInfo xs
Nil)  = ModuleName
-> ModuleName -> ConstructorInfo '[x] -> DatatypeInfo '[ '[x]]
forall x.
ModuleName
-> ModuleName -> ConstructorInfo '[x] -> DatatypeInfo '[ '[x]]
Newtype ModuleName
m ModuleName
n ConstructorInfo x
ConstructorInfo '[x]
c

-- | /Note:/ 'Infix' constructor has operator as a 'ConstructorName'. Use as
-- setter with care.
constructorName :: Lens' (ConstructorInfo xs) ConstructorName
constructorName :: forall (xs :: [*]) (f :: * -> *).
Functor f =>
(ModuleName -> f ModuleName)
-> ConstructorInfo xs -> f (ConstructorInfo xs)
constructorName ModuleName -> f ModuleName
f (Constructor ModuleName
n      ) = (\ ModuleName
n' -> ModuleName -> ConstructorInfo xs
forall (a :: [*]). SListI a => ModuleName -> ConstructorInfo a
Constructor ModuleName
n'      ) (ModuleName -> ConstructorInfo xs)
-> f ModuleName -> f (ConstructorInfo xs)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ModuleName -> f ModuleName
f ModuleName
n
constructorName ModuleName -> f ModuleName
f (Infix       ModuleName
n Associativity
a Fixity
fix) = (\ ModuleName
n' -> ModuleName -> Associativity -> Fixity -> ConstructorInfo '[x, y]
forall x y.
ModuleName -> Associativity -> Fixity -> ConstructorInfo '[x, y]
Infix       ModuleName
n' Associativity
a Fixity
fix) (ModuleName -> ConstructorInfo xs)
-> f ModuleName -> f (ConstructorInfo xs)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ModuleName -> f ModuleName
f ModuleName
n
constructorName ModuleName -> f ModuleName
f (Record      ModuleName
n NP FieldInfo xs
finfo) = (\ ModuleName
n' -> ModuleName -> NP FieldInfo xs -> ConstructorInfo xs
forall (a :: [*]).
SListI a =>
ModuleName -> NP FieldInfo a -> ConstructorInfo a
Record      ModuleName
n' NP FieldInfo xs
finfo) (ModuleName -> ConstructorInfo xs)
-> f ModuleName -> f (ConstructorInfo xs)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ModuleName -> f ModuleName
f ModuleName
n

-- | Strictness info is only aviable for 'ADT' data. This combinator is available only with @generics-sop@ 0.5 or later.
strictnessInfo :: Traversal' (DatatypeInfo xss) (POP StrictnessInfo xss)
strictnessInfo :: forall (xss :: [[*]]) (f :: * -> *).
Applicative f =>
(POP StrictnessInfo xss -> f (POP StrictnessInfo xss))
-> DatatypeInfo xss -> f (DatatypeInfo xss)
strictnessInfo POP StrictnessInfo xss -> f (POP StrictnessInfo xss)
_ di :: DatatypeInfo xss
di@Newtype {}   = DatatypeInfo xss -> f (DatatypeInfo xss)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DatatypeInfo xss
di
strictnessInfo POP StrictnessInfo xss -> f (POP StrictnessInfo xss)
f (ADT ModuleName
m ModuleName
n NP ConstructorInfo xss
cs POP StrictnessInfo xss
ss) = ModuleName
-> ModuleName
-> NP ConstructorInfo xss
-> POP StrictnessInfo xss
-> DatatypeInfo xss
forall (a :: [[*]]).
ModuleName
-> ModuleName
-> NP ConstructorInfo a
-> POP StrictnessInfo a
-> DatatypeInfo a
ADT ModuleName
m ModuleName
n NP ConstructorInfo xss
cs (POP StrictnessInfo xss -> DatatypeInfo xss)
-> f (POP StrictnessInfo xss) -> f (DatatypeInfo xss)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> POP StrictnessInfo xss -> f (POP StrictnessInfo xss)
f POP StrictnessInfo xss
ss