{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Data.Vec.Lazy.Inline.Lens (
ix,
_Cons,
_head,
_tail,
_Pull,
_Vec,
) where
import Data.Fin (Fin (..))
import Data.Nat (Nat (..))
import Data.Vec.Lazy.Lens (_Cons, _head, _tail)
import Prelude (Functor, ($), (.))
import qualified Control.Lens as L
import qualified Data.Fin as F
import qualified Data.Type.Nat as N
import qualified Data.Vec.Pull as P
import Data.Vec.Lazy.Inline
ix :: forall n f a. (N.SNatI n, Functor f) => Fin n -> L.LensLike' f (Vec n a) a
ix :: forall (n :: Nat) (f :: * -> *) a.
(SNatI n, Functor f) =>
Fin n -> LensLike' f (Vec n a) a
ix = IxLens f n a -> Fin n -> LensLike' f (Vec n a) a
forall (f :: * -> *) (n :: Nat) a.
IxLens f n a -> Fin n -> LensLike' f (Vec n a) a
getIxLens (IxLens f n a -> Fin n -> LensLike' f (Vec n a) a)
-> IxLens f n a -> Fin n -> LensLike' f (Vec n a) a
forall a b. (a -> b) -> a -> b
$ IxLens f 'Z a
-> (forall (m :: Nat).
SNatI m =>
IxLens f m a -> IxLens f ('S m) a)
-> IxLens f n a
forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 IxLens f 'Z a
start IxLens f m a -> IxLens f ('S m) a
forall (m :: Nat). SNatI m => IxLens f m a -> IxLens f ('S m) a
forall (m :: Nat). IxLens f m a -> IxLens f ('S m) a
step where
start :: IxLens f 'Z a
start :: IxLens f 'Z a
start = (Fin 'Z -> LensLike' f (Vec 'Z a) a) -> IxLens f 'Z a
forall (f :: * -> *) (n :: Nat) a.
(Fin n -> LensLike' f (Vec n a) a) -> IxLens f n a
IxLens Fin 'Z -> LensLike' f (Vec 'Z a) a
forall b. Fin 'Z -> b
F.absurd
step :: IxLens f m a -> IxLens f ('S m) a
step :: forall (m :: Nat). IxLens f m a -> IxLens f ('S m) a
step (IxLens Fin m -> LensLike' f (Vec m a) a
l) = (Fin ('S m) -> LensLike' f (Vec ('S m) a) a) -> IxLens f ('S m) a
forall (f :: * -> *) (n :: Nat) a.
(Fin n -> LensLike' f (Vec n a) a) -> IxLens f n a
IxLens ((Fin ('S m) -> LensLike' f (Vec ('S m) a) a) -> IxLens f ('S m) a)
-> (Fin ('S m) -> LensLike' f (Vec ('S m) a) a)
-> IxLens f ('S m) a
forall a b. (a -> b) -> a -> b
$ \Fin ('S m)
i -> case Fin ('S m)
i of
Fin ('S m)
FZ -> LensLike' f (Vec ('S m) a) a
forall (n :: Nat) a (f :: * -> *).
Functor f =>
(a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
_head
FS Fin n1
j -> (Vec m a -> f (Vec m a)) -> Vec ('S m) a -> f (Vec ('S m) a)
forall (n :: Nat) a (f :: * -> *).
Functor f =>
(Vec n a -> f (Vec n a)) -> Vec ('S n) a -> f (Vec ('S n) a)
_tail ((Vec m a -> f (Vec m a)) -> Vec ('S m) a -> f (Vec ('S m) a))
-> LensLike' f (Vec m a) a -> LensLike' f (Vec ('S m) a) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin m -> LensLike' f (Vec m a) a
l Fin m
Fin n1
j
newtype IxLens f n a = IxLens { forall (f :: * -> *) (n :: Nat) a.
IxLens f n a -> Fin n -> LensLike' f (Vec n a) a
getIxLens :: Fin n -> L.LensLike' f (Vec n a) a }
_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. SNatI n => 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. SNatI n => Vec n a -> [a]
toList [a] -> Maybe (Vec n a)
forall (n :: Nat) a. SNatI n => [a] -> Maybe (Vec n a)
fromList