{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.Vec.Pull.Lens (
    -- * Indexing
    ix,
    _Cons,
    _head,
    _tail,
    -- * Conversions
    _Vec,
    ) where

import Control.Lens ((<&>))
import Data.Fin     (Fin (..))
import Data.Nat     (Nat (..))

import qualified Control.Lens  as L
import qualified Data.Type.Nat as N

import Data.Vec.Pull

-- $setup
-- >>> :set -XScopedTypeVariables
-- >>> import Data.Vec.Pull
-- >>> import Data.Fin (Fin (..))
-- >>> import Control.Lens ((^.), (&), (.~), over)
-- >>> import qualified Data.Vec.Lazy as L
-- >>> import qualified Data.Vec.Lazy.Lens as L

-------------------------------------------------------------------------------
-- Indexing
-------------------------------------------------------------------------------

-- | Index lens.
--
-- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) ^. L._Pull . ix (FS FZ)
-- 'b'
--
-- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) & L._Pull . ix (FS FZ) .~ 'x'
-- 'a' ::: 'x' ::: 'c' ::: VNil
--
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 a -> f a
f (Vec Fin n -> a
v) = a -> f a
f (Fin n -> a
v Fin n
i) f a -> (a -> Vec n a) -> f (Vec n a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \a
a -> (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> a) -> Vec n a) -> (Fin n -> a) -> Vec n a
forall a b. (a -> b) -> a -> b
$ \Fin n
j ->
    if Fin n
i Fin n -> Fin n -> Bool
forall a. Eq a => a -> a -> Bool
== Fin n
j
    then a
a
    else Fin n -> a
v Fin n
j

-- | Match on non-empty 'Vec'.
--
-- /Note:/ @lens@ 'L._Cons' is a 'L.Prism'.
-- In fact, @'Vec' n a@ cannot have an instance of 'L.Cons' as types don't match.
--
_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 (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (a, Vec n a) (f (b, Vec n b))
-> p (Vec ('S n) a) (f (Vec ('S 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 (\(Vec Fin ('S n) -> a
v) -> (Fin ('S n) -> a
v Fin ('S n)
forall (n1 :: Nat). Fin ('S n1)
FZ, (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin ('S n) -> a
v (Fin ('S n) -> a) -> (Fin n -> Fin ('S n)) -> Fin n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Fin ('S n)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS))) (\(b
x, Vec n b
xs) -> b -> Vec n b -> Vec ('S n) b
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons b
x Vec n b
xs)

-- | Head lens. /Note:/ @lens@ 'L._head' is a 'L.Traversal''.
--
-- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) ^. L._Pull . _head
-- 'a'
--
-- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) & L._Pull . _head .~ 'x'
-- 'x' ::: 'b' ::: 'c' ::: VNil
--
_head :: L.Lens' (Vec ('S n) a) a
_head :: forall (n :: Nat) a (f :: * -> *).
Functor f =>
(a -> f a) -> Vec ('S n) a -> f (Vec ('S n) a)
_head a -> f a
f (Vec Fin ('S n) -> a
v) = a -> f a
f (Fin ('S n) -> a
v Fin ('S n)
forall (n1 :: Nat). Fin ('S n1)
FZ) f a -> (a -> Vec ('S n) a) -> f (Vec ('S n) a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \a
a -> (Fin ('S n) -> a) -> Vec ('S n) a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin ('S n) -> a) -> Vec ('S n) a)
-> (Fin ('S n) -> a) -> Vec ('S n) a
forall a b. (a -> b) -> a -> b
$ \Fin ('S n)
j -> case Fin ('S n)
j of
    Fin ('S n)
FZ -> a
a
    Fin ('S n)
_   -> Fin ('S n) -> a
v Fin ('S n)
j
{-# INLINE _head #-}

-- | Head lens. /Note:/ @lens@ 'L._head' is a 'L.Traversal''.
_tail :: L.Lens' (Vec ('S n) a) (Vec n a)
_tail :: 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 n a -> f (Vec n a)
f (Vec Fin ('S n) -> a
v) = Vec n a -> f (Vec n a)
f ((Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin ('S n) -> a
v (Fin ('S n) -> a) -> (Fin n -> Fin ('S n)) -> Fin n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Fin ('S n)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS)) f (Vec n a) -> (Vec n a -> Vec ('S n) a) -> f (Vec ('S n) a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Vec n a
xs -> a -> Vec n a -> Vec ('S n) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons (Fin ('S n) -> a
v Fin ('S n)
forall (n1 :: Nat). Fin ('S n1)
FZ) Vec n a
xs
{-# INLINE _tail #-}

-------------------------------------------------------------------------------
-- Conversions
-------------------------------------------------------------------------------

-- | Prism from list.
_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