{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.Vec.Lazy.Optics (
ix,
_Cons,
_head,
_tail,
_Pull,
_Vec,
) where
import Control.Applicative ((<$>))
import Data.Fin (Fin (..))
import Data.Nat (Nat (..))
import Prelude ((.), Functor, ($))
import qualified Optics.Core as L
import qualified Data.Type.Nat as N
import qualified Data.Vec.Pull as P
import Data.Vec.Lazy
type LensLikeVL f s t a b = (a -> f b) -> s -> f t
type LensLikeVL' f s a = LensLikeVL f s s a a
ix :: Fin n -> L.Lens' (Vec n a) a
ix :: forall (n :: Nat) a. Fin n -> Lens' (Vec n a) a
ix Fin n
i = LensVL (Vec n a) (Vec n a) a a -> Lens (Vec n a) (Vec n a) a a
forall s t a b. LensVL s t a b -> Lens s t a b
L.lensVL (Fin n -> LensLikeVL' f (Vec n a) a
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
Fin n -> LensLikeVL' f (Vec n a) a
ixVL Fin n
i)
{-# INLINE ix #-}
ixVL :: Functor f => Fin n -> LensLikeVL' f (Vec n a) a
ixVL :: forall (f :: * -> *) (n :: Nat) a.
Functor f =>
Fin n -> LensLikeVL' f (Vec n a) a
ixVL Fin n
FZ a -> f a
f (a
x ::: Vec n1 a
xs) = (a -> Vec n1 a -> Vec ('S n1) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec n1 a
xs) (a -> Vec n a) -> f a -> f (Vec n a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f a
x
ixVL (FS Fin n1
n) a -> f a
f (a
x ::: Vec n1 a
xs) = (a
x a -> Vec n1 a -> Vec ('S n1) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
:::) (Vec n1 a -> Vec n a) -> f (Vec n1 a) -> f (Vec n a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Fin n1 -> LensLikeVL' f (Vec n1 a) a
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
Fin n -> LensLikeVL' f (Vec n a) a
ixVL Fin n1
n a -> f a
f Vec n1 a
Vec n1 a
xs
_Cons :: L.Iso (Vec ('S n) a) (Vec ('S n) b) (a, Vec n a) (b, Vec n b)
_Cons :: forall (n :: Nat) a b.
Iso (Vec ('S n) a) (Vec ('S n) b) (a, Vec n a) (b, Vec n b)
_Cons = (Vec ('S n) a -> (a, Vec n a))
-> ((b, Vec n b) -> Vec ('S n) b)
-> Iso (Vec ('S n) a) (Vec ('S n) b) (a, Vec n a) (b, Vec n b)
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
L.iso (\(a
x ::: Vec n1 a
xs) -> (a
x, Vec n a
Vec n1 a
xs)) (\(b
x, Vec n b
xs) -> b
x b -> Vec n b -> Vec ('S n) b
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec n b
xs)
_head :: L.Lens' (Vec ('S n) a) a
_head :: forall (n :: Nat) a. Lens' (Vec ('S n) a) a
_head = LensVL (Vec ('S n) a) (Vec ('S n) a) a a
-> Lens (Vec ('S n) a) (Vec ('S n) a) a a
forall s t a b. LensVL s t a b -> Lens s t a b
L.lensVL LensLikeVL' f (Vec ('S n) a) a
LensVL (Vec ('S n) a) (Vec ('S n) a) a a
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) a
headVL
{-# INLINE _head #-}
headVL :: Functor f => LensLikeVL' f (Vec ('S n) a) a
headVL :: forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) a
headVL a -> f a
f (a
x ::: Vec n1 a
xs) = (a -> Vec n1 a -> Vec ('S n1) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec n1 a
xs) (a -> Vec ('S n) a) -> f a -> f (Vec ('S n) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f a
x
{-# INLINE headVL #-}
_tail :: L.Lens' (Vec ('S n) a) (Vec n a)
_tail :: forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail = LensVL (Vec ('S n) a) (Vec ('S n) a) (Vec n a) (Vec n a)
-> Lens (Vec ('S n) a) (Vec ('S n) a) (Vec n a) (Vec n a)
forall s t a b. LensVL s t a b -> Lens s t a b
L.lensVL LensLikeVL' f (Vec ('S n) a) (Vec n a)
LensVL (Vec ('S n) a) (Vec ('S n) a) (Vec n a) (Vec n a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL
{-# INLINE _tail #-}
tailVL :: Functor f => LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL :: forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL Vec n a -> f (Vec n a)
f (a
x ::: Vec n1 a
xs) = (a
x a -> Vec n a -> Vec ('S n) a
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
:::) (Vec n a -> Vec ('S n) a) -> f (Vec n a) -> f (Vec ('S n) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Vec n a -> f (Vec n a)
f Vec n a
Vec n1 a
xs
{-# INLINE tailVL #-}
_Pull :: N.SNatI n => L.Iso (Vec n a) (Vec n b) (P.Vec n a) (P.Vec n b)
_Pull :: forall (n :: Nat) a b.
SNatI n =>
Iso (Vec n a) (Vec n b) (Vec n a) (Vec n b)
_Pull = (Vec n a -> Vec n a)
-> (Vec n b -> Vec n b)
-> Iso (Vec n a) (Vec n b) (Vec n a) (Vec n b)
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
L.iso Vec n a -> Vec n a
forall (n :: Nat) a. Vec n a -> Vec n a
toPull Vec n b -> Vec n b
forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
fromPull
_Vec :: N.SNatI n => L.Prism' [a] (Vec n a)
_Vec :: forall (n :: Nat) a. SNatI n => Prism' [a] (Vec n a)
_Vec = (Vec n a -> [a])
-> ([a] -> Maybe (Vec n a)) -> Prism [a] [a] (Vec n a) (Vec n a)
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
L.prism' Vec n a -> [a]
forall (n :: Nat) a. Vec n a -> [a]
toList [a] -> Maybe (Vec n a)
forall (n :: Nat) a. SNatI n => [a] -> Maybe (Vec n a)
fromList
instance L.Each (Fin n) (Vec n a) (Vec n b) a b where
type instance L.Index (Vec n a) = Fin n
type instance L.IxValue (Vec n a) = a
instance L.Ixed (Vec n a) where
type IxKind (Vec n a) = L.A_Lens
ix :: Index (Vec n a)
-> Optic' (IxKind (Vec n a)) NoIx (Vec n a) (IxValue (Vec n a))
ix = Fin n -> Lens' (Vec n a) a
Index (Vec n a)
-> Optic' (IxKind (Vec n a)) NoIx (Vec n a) (IxValue (Vec n a))
forall (n :: Nat) a. Fin n -> Lens' (Vec n a) a
ix
instance L.Field1 (Vec ('S n) a) (Vec ('S n) a) a a where
_1 :: Lens (Vec ('S n) a) (Vec ('S n) a) a a
_1 = Lens (Vec ('S n) a) (Vec ('S n) a) a a
forall (n :: Nat) a. Lens' (Vec ('S n) a) a
_head
instance L.Field2 (Vec ('S ('S n)) a) (Vec ('S ('S n)) a) a a where
_2 :: Lens (Vec ('S ('S n)) a) (Vec ('S ('S n)) a) a a
_2 = LensVL (Vec ('S ('S n)) a) (Vec ('S ('S n)) a) a a
-> Lens (Vec ('S ('S n)) a) (Vec ('S ('S n)) a) a a
forall s t a b. LensVL s t a b -> Lens s t a b
L.lensVL (LensVL (Vec ('S ('S n)) a) (Vec ('S ('S n)) a) a a
-> Lens (Vec ('S ('S n)) a) (Vec ('S ('S n)) a) a a)
-> LensVL (Vec ('S ('S n)) a) (Vec ('S ('S n)) a) a a
-> Lens (Vec ('S ('S n)) a) (Vec ('S ('S n)) a) a a
forall a b. (a -> b) -> a -> b
$ LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) a
headVL
instance L.Field3 (Vec ('S ('S ('S n))) a) (Vec ('S ('S ('S n))) a) a a where
_3 :: Lens (Vec ('S ('S ('S n))) a) (Vec ('S ('S ('S n))) a) a a
_3 = LensVL (Vec ('S ('S ('S n))) a) (Vec ('S ('S ('S n))) a) a a
-> Lens (Vec ('S ('S ('S n))) a) (Vec ('S ('S ('S n))) a) a a
forall s t a b. LensVL s t a b -> Lens s t a b
L.lensVL (LensVL (Vec ('S ('S ('S n))) a) (Vec ('S ('S ('S n))) a) a a
-> Lens (Vec ('S ('S ('S n))) a) (Vec ('S ('S ('S n))) a) a a)
-> LensVL (Vec ('S ('S ('S n))) a) (Vec ('S ('S ('S n))) a) a a
-> Lens (Vec ('S ('S ('S n))) a) (Vec ('S ('S ('S n))) a) a a
forall a b. (a -> b) -> a -> b
$ LensLikeVL' f (Vec ('S ('S ('S n))) a) (Vec ('S ('S n)) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S ('S n))) a) (Vec ('S ('S n)) a)
-> ((a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> (a -> f a)
-> Vec ('S ('S ('S n))) a
-> f (Vec ('S ('S ('S n))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) a
headVL
instance L.Field4 (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S ('S n)))) a) a a where
_4 :: Lens
(Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S ('S n)))) a) a a
_4 = LensVL
(Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S ('S n)))) a) a a
-> Lens
(Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S ('S n)))) a) a a
forall s t a b. LensVL s t a b -> Lens s t a b
L.lensVL (LensVL
(Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S ('S n)))) a) a a
-> Lens
(Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S ('S n)))) a) a a)
-> LensVL
(Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S ('S n)))) a) a a
-> Lens
(Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S ('S n)))) a) a a
forall a b. (a -> b) -> a -> b
$ LensLikeVL'
f (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S n))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S n))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S n)))) a
-> f (Vec ('S ('S ('S ('S n)))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL' f (Vec ('S ('S ('S n))) a) (Vec ('S ('S n)) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S ('S n))) a) (Vec ('S ('S n)) a)
-> ((a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> (a -> f a)
-> Vec ('S ('S ('S n))) a
-> f (Vec ('S ('S ('S n))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) a
headVL
instance L.Field5 (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S ('S n))))) a) a a where
_5 :: Lens
(Vec ('S ('S ('S ('S ('S n))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
a
a
_5 = LensVL
(Vec ('S ('S ('S ('S ('S n))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S n))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
a
a
forall s t a b. LensVL s t a b -> Lens s t a b
L.lensVL (LensVL
(Vec ('S ('S ('S ('S ('S n))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S n))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
a
a)
-> LensVL
(Vec ('S ('S ('S ('S ('S n))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S n))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
a
a
forall a b. (a -> b) -> a -> b
$ LensLikeVL'
f (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S n)))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S n)))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S n))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S n))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S n)))) a
-> f (Vec ('S ('S ('S ('S n)))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL' f (Vec ('S ('S ('S n))) a) (Vec ('S ('S n)) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S ('S n))) a) (Vec ('S ('S n)) a)
-> ((a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> (a -> f a)
-> Vec ('S ('S ('S n))) a
-> f (Vec ('S ('S ('S n))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) a
headVL
instance L.Field6 (Vec ('S ('S ('S ('S ('S ('S n)))))) a) (Vec ('S ('S ('S ('S ('S ('S n)))))) a) a a where
_6 :: Lens
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
a
a
_6 = LensVL
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
a
a
forall s t a b. LensVL s t a b -> Lens s t a b
L.lensVL (LensVL
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
a
a)
-> LensVL
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
a
a
forall a b. (a -> b) -> a -> b
$ LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S n)))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S n)))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S n))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S n))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S n)))) a
-> f (Vec ('S ('S ('S ('S n)))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL' f (Vec ('S ('S ('S n))) a) (Vec ('S ('S n)) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S ('S n))) a) (Vec ('S ('S n)) a)
-> ((a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> (a -> f a)
-> Vec ('S ('S ('S n))) a
-> f (Vec ('S ('S ('S n))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) a
headVL
instance L.Field7 (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a) a a where
_7 :: Lens
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
a
a
_7 = LensVL
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
a
a
forall s t a b. LensVL s t a b -> Lens s t a b
L.lensVL (LensVL
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
a
a)
-> LensVL
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
a
a
forall a b. (a -> b) -> a -> b
$ LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S n)))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S n)))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S n))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S n))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S n)))) a
-> f (Vec ('S ('S ('S ('S n)))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL' f (Vec ('S ('S ('S n))) a) (Vec ('S ('S n)) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S ('S n))) a) (Vec ('S ('S n)) a)
-> ((a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> (a -> f a)
-> Vec ('S ('S ('S n))) a
-> f (Vec ('S ('S ('S n))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) a
headVL
instance L.Field8 (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a) a a where
_8 :: Lens
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
a
a
_8 = LensVL
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
a
a
forall s t a b. LensVL s t a b -> Lens s t a b
L.lensVL (LensVL
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
a
a)
-> LensVL
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
a
a
forall a b. (a -> b) -> a -> b
$ LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S n)))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S n)))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S n))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S n))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S n)))) a
-> f (Vec ('S ('S ('S ('S n)))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL' f (Vec ('S ('S ('S n))) a) (Vec ('S ('S n)) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S ('S n))) a) (Vec ('S ('S n)) a)
-> ((a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> (a -> f a)
-> Vec ('S ('S ('S n))) a
-> f (Vec ('S ('S ('S n))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) a
headVL
instance L.Field9 (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a) a a where
_9 :: Lens
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
a
a
_9 = LensVL
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
a
a
forall s t a b. LensVL s t a b -> Lens s t a b
L.lensVL (LensVL
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
a
a)
-> LensVL
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
a
a
-> Lens
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
a
a
forall a b. (a -> b) -> a -> b
$ LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f
(Vec ('S ('S ('S ('S ('S ('S n)))))) a)
(Vec ('S ('S ('S ('S ('S n))))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S ('S n)))))) a
-> f (Vec ('S ('S ('S ('S ('S ('S n)))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S n)))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S n)))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S ('S n)))) a -> f (Vec ('S ('S ('S ('S n)))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S ('S n))))) a
-> f (Vec ('S ('S ('S ('S ('S n))))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL'
f (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S n))) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL'
f (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S n))) a)
-> ((a -> f a)
-> Vec ('S ('S ('S n))) a -> f (Vec ('S ('S ('S n))) a))
-> (a -> f a)
-> Vec ('S ('S ('S ('S n)))) a
-> f (Vec ('S ('S ('S ('S n)))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL' f (Vec ('S ('S ('S n))) a) (Vec ('S ('S n)) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S ('S n))) a) (Vec ('S ('S n)) a)
-> ((a -> f a) -> Vec ('S ('S n)) a -> f (Vec ('S ('S n)) a))
-> (a -> f a)
-> Vec ('S ('S ('S n))) a
-> f (Vec ('S ('S ('S n))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S ('S n)) a) (Vec ('S n) a)
-> ((a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a))
-> (a -> f a)
-> Vec ('S ('S n)) a
-> f (Vec ('S ('S n)) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) a
headVL