{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Generics.SOP.Lens (
rep, productRep,
sop, pop,
_SOP, _POP,
_I, _K,
npSingleton,
npHead,
npTail,
nsSingleton,
_Z,
_S,
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
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
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 ::
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
_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
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
_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
_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
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
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
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
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
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