{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Data.Vec.Lazy.Inline.Optics (
    -- * Indexing
    ix,
    _Cons,
    _head,
    _tail,
    -- * Conversions
    _Pull,
    _Vec,
    ) where

import Control.Applicative  ((<$>))
import Data.Fin             (Fin (..))
import Data.Nat             (Nat (..))
import Data.Vec.Lazy.Optics (_Cons, _head, _tail)
import Prelude              (Functor, ($), (.))

import qualified Data.Fin      as F
import qualified Data.Type.Nat as N
import qualified Data.Vec.Pull as P
import qualified Optics.Core   as L

import Data.Vec.Lazy.Inline

-- $setup
-- >>> :set -XScopedTypeVariables
-- >>> import Data.Fin (Fin (..))
-- >>> import Data.Vec.Lazy.Inline
-- >>> import Prelude (Maybe (..), Char, Bool (..))
-- >>> import Optics.Core (over, view, set, (%), review, preview)
-- >>> import qualified Data.Type.Nat as N

type LensLikeVL f s t a b = (a -> f b) -> s -> f t
type LensLikeVL' f s a = LensLikeVL f s s a a

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

-- | Index lens.
--
-- >>> view (ix (FS FZ)) ('a' ::: 'b' ::: 'c' ::: VNil)
-- 'b'
--
-- >>> set (ix (FS FZ)) 'x' ('a' ::: 'b' ::: 'c' ::: VNil)
-- 'a' ::: 'x' ::: 'c' ::: VNil
--
ix :: forall n a. N.SNatI n => Fin n -> L.Lens' (Vec n a) a
ix :: forall (n :: Nat) a. SNatI n => 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 (n :: Nat) (f :: * -> *) a.
(SNatI n, Functor f) =>
Fin n -> LensLikeVL' f (Vec n a) a
ixVL Fin n
i)
{-# INLINE ix #-}

ixVL :: forall n f a. (N.SNatI n, Functor f) => Fin n -> LensLikeVL' f (Vec n a) a
ixVL :: forall (n :: Nat) (f :: * -> *) a.
(SNatI n, Functor f) =>
Fin n -> LensLikeVL' f (Vec n a) a
ixVL = IxLens f n a -> Fin n -> LensLikeVL' f (Vec n a) a
forall (f :: * -> *) (n :: Nat) a.
IxLens f n a -> Fin n -> LensLikeVL' f (Vec n a) a
getIxLens (IxLens f n a -> Fin n -> LensLikeVL' f (Vec n a) a)
-> IxLens f n a -> Fin n -> LensLikeVL' 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 -> LensLikeVL' f (Vec 'Z a) a) -> IxLens f 'Z a
forall (f :: * -> *) (n :: Nat) a.
(Fin n -> LensLikeVL' f (Vec n a) a) -> IxLens f n a
IxLens Fin 'Z -> LensLikeVL' 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 -> LensLikeVL' f (Vec m a) a
l) = (Fin ('S m) -> LensLikeVL' f (Vec ('S m) a) a) -> IxLens f ('S m) a
forall (f :: * -> *) (n :: Nat) a.
(Fin n -> LensLikeVL' f (Vec n a) a) -> IxLens f n a
IxLens ((Fin ('S m) -> LensLikeVL' f (Vec ('S m) a) a)
 -> IxLens f ('S m) a)
-> (Fin ('S m) -> LensLikeVL' 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   -> LensLikeVL' f (Vec ('S m) a) a
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) a
headVL
        FS Fin n1
j -> LensLikeVL' f (Vec ('S m) a) (Vec m a)
forall (f :: * -> *) (n :: Nat) a.
Functor f =>
LensLikeVL' f (Vec ('S n) a) (Vec n a)
tailVL LensLikeVL' f (Vec ('S m) a) (Vec m a)
-> LensLikeVL' f (Vec m a) a -> LensLikeVL' f (Vec ('S m) a) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin m -> LensLikeVL' f (Vec m a) a
l Fin m
Fin n1
j
{-# INLINE ixVL #-}

newtype IxLens f n a = IxLens { forall (f :: * -> *) (n :: Nat) a.
IxLens f n a -> Fin n -> LensLikeVL' f (Vec n a) a
getIxLens :: Fin n -> LensLikeVL' f (Vec n a) a }

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 #-}

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 #-}

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

-- | An 'L.Iso' from 'toPull' and 'fromPull'.
_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

-- | Prism from list.
--
-- >>> preview _Vec "foo" :: Maybe (Vec N.Nat3 Char)
-- Just ('f' ::: 'o' ::: 'o' ::: VNil)
--
-- >>> preview _Vec "foo" :: Maybe (Vec N.Nat2 Char)
-- Nothing
--
-- >>> review _Vec (True ::: False ::: VNil)
-- [True,False]
--
_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