{-# LANGUAGE CPP                   #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DefaultSignatures     #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE Safe                  #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}
module Data.Vec.DataFamily.SpineStrict.Pigeonhole (
    Pigeonhole (..),
    -- * Representable
    gindex,
    gtabulate,
    gix,
    -- ** Traversable with index
    gtraverse,
    gitraverse,
    -- * Generic implementation
    gfrom, GFrom,
    gto, GTo,
    GPigeonholeSize,
    ) where

import Prelude (Functor (..), fst, uncurry, ($), (.))

import Control.Applicative             (Applicative (..), (<$>))
import Control.Arrow                   (first)
import Data.Fin                        (Fin (..))
import Data.Functor.Confusing          (confusing, fusing, iconfusing)
import Data.Functor.Identity           (Identity (..))
import Data.Functor.Product            (Product (..))
import Data.Nat                        (Nat (..))
import Data.Proxy                      (Proxy (..))
import Data.Vec.DataFamily.SpineStrict (Vec (..), tabulate)
import GHC.Generics                    (M1 (..), Par1 (..), U1 (..), (:*:) (..))

import qualified Control.Lens.Yocto              as YLens
import qualified Data.Fin                        as F
import qualified Data.Fin.Enum                   as F
import qualified Data.Type.Nat                   as N
import qualified Data.Vec.DataFamily.SpineStrict as V
import qualified GHC.Generics                    as G

#ifdef MIN_VERSION_transformers_compat
import Control.Monad.Trans.Instances ()
#endif

-- $setup
-- >>> :set -XDeriveGeneric
-- >>> import Control.Applicative (Const (..))
-- >>> import Data.Char (toUpper)
-- >>> import Data.Functor.Identity (Identity (..))
-- >>> import Data.Void (absurd)
-- >>> import GHC.Generics (Generic, Generic1)
-- >>> import Prelude (Int, Show, Char, Integer)
-- >>> import Data.Proxy (Proxy (..))
-- >>> import qualified Control.Lens as Lens
-- >>> import Data.Fin (Fin (..))
-- >>> import Data.Vec.DataFamily.SpineStrict (Vec (..))

-------------------------------------------------------------------------------
-- Class
-------------------------------------------------------------------------------

-- | Generic pigeonholes.
--
-- /Examples:/
--
-- >>> from (Identity 'a')
-- 'a' ::: VNil
--
-- >>> data Values a = Values a a a deriving (Generic1)
-- >>> instance Pigeonhole Values
-- >>> from (Values 1 2 3)
-- 1 ::: 2 ::: 3 ::: VNil
--
class Pigeonhole f where
    -- | The size of a pigeonhole
    type PigeonholeSize f :: Nat
    type PigeonholeSize f = GPigeonholeSize f

    -- | Converts a value to vector
    from :: f x -> Vec (PigeonholeSize f) x
    default from :: (G.Generic1 f, GFrom f, PigeonholeSize f ~ GPigeonholeSize f) => f x -> Vec (PigeonholeSize f) x
    from = f x -> Vec (PigeonholeSize f) x
forall (c :: * -> *) a.
(Generic1 @* c, GFrom c) =>
c a -> Vec (GPigeonholeSize c) a
gfrom

    -- | Converts back from vector.
    to :: Vec (PigeonholeSize f) x -> f x
    default to :: (G.Generic1 f, GTo f, PigeonholeSize f ~ GPigeonholeSize f) => Vec (PigeonholeSize f) x -> f x
    to = Vec (PigeonholeSize f) x -> f x
forall (c :: * -> *) a.
(Generic1 @* c, GTo c) =>
Vec (GPigeonholeSize c) a -> c a
gto

-- | @'Identity' x@ ~ @x ^ 1@
instance Pigeonhole Identity
--
-- | @'Proxy' x@ ~ @x ^ 0@
instance Pigeonhole Proxy where
    type PigeonholeSize Proxy = 'Z
    from :: Proxy @* x -> Vec (PigeonholeSize (Proxy @*)) x
from Proxy @* x
_ = Vec (PigeonholeSize (Proxy @*)) x
forall a. Vec 'Z a
VNil
    to :: Vec (PigeonholeSize (Proxy @*)) x -> Proxy @* x
to Vec (PigeonholeSize (Proxy @*)) x
_   = Proxy @* x
forall k (t :: k). Proxy @k t
Proxy

-- | @'Product' f g x@ ~ @x ^ (size f + size g)@
instance (Pigeonhole f, Pigeonhole g, N.SNatI (PigeonholeSize f)) => Pigeonhole (Product f g) where
    type PigeonholeSize (Product f g) = N.Plus (PigeonholeSize f) (PigeonholeSize g)

    to :: Vec (PigeonholeSize (Product @* f g)) x -> Product @* f g x
to = (Vec (PigeonholeSize f) x, Vec (PigeonholeSize g) x)
-> Product @* f g x
forall (f :: * -> *) (g :: * -> *) a.
(Pigeonhole f, Pigeonhole g) =>
(Vec (PigeonholeSize f) a, Vec (PigeonholeSize g) a)
-> Product @* f g a
f ((Vec (PigeonholeSize f) x, Vec (PigeonholeSize g) x)
 -> Product @* f g x)
-> (Vec (Plus (PigeonholeSize f) (PigeonholeSize g)) x
    -> (Vec (PigeonholeSize f) x, Vec (PigeonholeSize g) x))
-> Vec (Plus (PigeonholeSize f) (PigeonholeSize g)) x
-> Product @* f g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vec (Plus (PigeonholeSize f) (PigeonholeSize g)) x
-> (Vec (PigeonholeSize f) x, Vec (PigeonholeSize g) x)
forall (n :: Nat) (m :: Nat) a.
SNatI n =>
Vec (Plus n m) a -> (Vec n a, Vec m a)
V.split where f :: (Vec (PigeonholeSize f) a, Vec (PigeonholeSize g) a)
-> Product @* f g a
f (Vec (PigeonholeSize f) a
a, Vec (PigeonholeSize g) a
b) = f a -> g a -> Product @* f g a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product @k f g a
Pair (Vec (PigeonholeSize f) a -> f a
forall (f :: * -> *) x.
Pigeonhole f =>
Vec (PigeonholeSize f) x -> f x
to Vec (PigeonholeSize f) a
a) (Vec (PigeonholeSize g) a -> g a
forall (f :: * -> *) x.
Pigeonhole f =>
Vec (PigeonholeSize f) x -> f x
to Vec (PigeonholeSize g) a
b)
    from :: Product @* f g x -> Vec (PigeonholeSize (Product @* f g)) x
from = (Vec (PigeonholeSize f) x
 -> Vec (PigeonholeSize g) x
 -> Vec (Plus (PigeonholeSize f) (PigeonholeSize g)) x)
-> (Vec (PigeonholeSize f) x, Vec (PigeonholeSize g) x)
-> Vec (Plus (PigeonholeSize f) (PigeonholeSize g)) x
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Vec (PigeonholeSize f) x
-> Vec (PigeonholeSize g) x
-> Vec (Plus (PigeonholeSize f) (PigeonholeSize g)) x
forall (n :: Nat) (m :: Nat) a.
SNatI n =>
Vec n a -> Vec m a -> Vec (Plus n m) a
(V.++) ((Vec (PigeonholeSize f) x, Vec (PigeonholeSize g) x)
 -> Vec (Plus (PigeonholeSize f) (PigeonholeSize g)) x)
-> (Product @* f g x
    -> (Vec (PigeonholeSize f) x, Vec (PigeonholeSize g) x))
-> Product @* f g x
-> Vec (Plus (PigeonholeSize f) (PigeonholeSize g)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product @* f g x
-> (Vec (PigeonholeSize f) x, Vec (PigeonholeSize g) x)
forall (f :: * -> *) (f :: * -> *) x.
(Pigeonhole f, Pigeonhole f) =>
Product @* f f x
-> (Vec (PigeonholeSize f) x, Vec (PigeonholeSize f) x)
g where g :: Product @* f f x
-> (Vec (PigeonholeSize f) x, Vec (PigeonholeSize f) x)
g (Pair f x
a f x
b) = (f x -> Vec (PigeonholeSize f) x
forall (f :: * -> *) x.
Pigeonhole f =>
f x -> Vec (PigeonholeSize f) x
from f x
a, f x -> Vec (PigeonholeSize f) x
forall (f :: * -> *) x.
Pigeonhole f =>
f x -> Vec (PigeonholeSize f) x
from f x
b)

-------------------------------------------------------------------------------
-- Generic representable
-------------------------------------------------------------------------------

-- | Index.
--
-- >>> gindex (Identity 'y') (Proxy :: Proxy Int)
-- 'y'
--
-- >>> data Key = Key1 | Key2 | Key3 deriving (Generic)
-- >>> data Values a = Values a a a deriving (Generic1)
--
-- >>> gindex (Values 'a' 'b' 'c') Key2
-- 'b'
--
gindex
    :: ( G.Generic i, F.GFrom i, G.Generic1 f, GFrom f
       , F.GEnumSize i ~ GPigeonholeSize f, N.SNatI (GPigeonholeSize f)
       )
     => f a -> i -> a
gindex :: f a -> i -> a
gindex f a
fa i
i = f a -> Vec (PigeonholeSizeRep (Rep1 @* f) 'Z) a
forall (c :: * -> *) a.
(Generic1 @* c, GFrom c) =>
c a -> Vec (GPigeonholeSize c) a
gfrom f a
fa Vec (PigeonholeSizeRep (Rep1 @* f) 'Z) a
-> Fin (PigeonholeSizeRep (Rep1 @* f) 'Z) -> a
forall (n :: Nat) a. SNatI n => Vec n a -> Fin n -> a
V.! i -> Fin (GEnumSize i)
forall a. (Generic a, GFrom a) => a -> Fin (GEnumSize a)
F.gfrom i
i

-- | Tabulate.
--
-- >>> gtabulate (\() -> 'x') :: Identity Char
-- Identity 'x'
--
-- >>> gtabulate absurd :: Proxy Integer
-- Proxy
--
-- >>> gtabulate absurd :: Proxy Integer
-- Proxy
--
gtabulate
    :: ( G.Generic i, F.GTo i, G.Generic1 f, GTo f
       , F.GEnumSize i ~ GPigeonholeSize f, N.SNatI (GPigeonholeSize f)
       )
     => (i -> a) -> f a
gtabulate :: (i -> a) -> f a
gtabulate i -> a
idx = Vec (GPigeonholeSize f) a -> f a
forall (c :: * -> *) a.
(Generic1 @* c, GTo c) =>
Vec (GPigeonholeSize c) a -> c a
gto (Vec (GPigeonholeSize f) a -> f a)
-> Vec (GPigeonholeSize f) a -> f a
forall a b. (a -> b) -> a -> b
$ (Fin (GPigeonholeSize f) -> a) -> Vec (GPigeonholeSize f) a
forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate (i -> a
idx (i -> a)
-> (Fin (GPigeonholeSize f) -> i) -> Fin (GPigeonholeSize f) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin (GPigeonholeSize f) -> i
forall a. (Generic a, GTo a) => Fin (GEnumSize a) -> a
F.gto)

-- | A lens. @i -> Lens' (t a) a@
--
-- >>> Lens.view (gix ()) (Identity 'x')
-- 'x'
--
-- >>> Lens.over (gix ()) toUpper (Identity 'x')
-- Identity 'X'
--
gix :: ( G.Generic i, F.GFrom i, G.Generic1 t, GTo t, GFrom t
       , F.GEnumSize i ~ GPigeonholeSize t, N.SNatI (GPigeonholeSize t)
       , Functor f
       )
    => i -> (a -> f a) -> t a -> f (t a)
gix :: i -> (a -> f a) -> t a -> f (t a)
gix i
i = LensLike (Yoneda f) (t a) (t a) a a -> (a -> f a) -> t a -> f (t a)
forall (f :: * -> *) s t a b.
Functor f =>
LensLike (Yoneda f) s t a b -> LensLike f s t a b
fusing (LensLike (Yoneda f) (t a) (t a) a a
 -> (a -> f a) -> t a -> f (t a))
-> LensLike (Yoneda f) (t a) (t a) a a
-> (a -> f a)
-> t a
-> f (t a)
forall a b. (a -> b) -> a -> b
$ \a -> Yoneda f a
ab t a
ta -> Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) a -> t a
forall (c :: * -> *) a.
(Generic1 @* c, GTo c) =>
Vec (GPigeonholeSize c) a -> c a
gto (Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) a -> t a)
-> Yoneda f (Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) a)
-> Yoneda f (t a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Fin (PigeonholeSizeRep (Rep1 @* t) 'Z)
-> LensLike'
     (Yoneda f) (Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) a) a
forall (n :: Nat) (f :: * -> *) a.
(SNatI n, Functor f) =>
Fin n -> LensLike' f (Vec n a) a
ix (i -> Fin (GEnumSize i)
forall a. (Generic a, GFrom a) => a -> Fin (GEnumSize a)
F.gfrom i
i) a -> Yoneda f a
ab (t a -> Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) a
forall (c :: * -> *) a.
(Generic1 @* c, GFrom c) =>
c a -> Vec (GPigeonholeSize c) a
gfrom t a
ta)

-------------------------------------------------------------------------------
-- Vendored in ix
-------------------------------------------------------------------------------

-- | Index lens.
--
ix :: forall n f a. (N.SNatI n, Functor f) => Fin n -> YLens.LensLike' f (Vec n a) a
ix :: 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 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 :: 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. Lens' (Vec ('S n) a) a
_head
        FS Fin n1
j -> LensLike f (Vec ('S m) a) (Vec ('S m) a) (Vec m a) (Vec m a)
forall (n :: Nat) a. Lens' (Vec ('S n) a) (Vec n a)
_tail LensLike f (Vec ('S m) a) (Vec ('S m) a) (Vec m a) (Vec 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 { IxLens f n a -> Fin n -> LensLike' f (Vec n a) a
getIxLens :: Fin n -> YLens.LensLike' f (Vec n a) a }

_head :: YLens.Lens' (Vec ('S n) a) a
_head :: LensLike f (Vec ('S n) a) (Vec ('S n) a) a a
_head a -> f a
f (x ::: xs) = (a -> Vec n a -> Vec ('S n) a
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec n 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 _head #-}

-- | Head lens. /Note:/ @lens@ 'Lens._head' is a 'Lens.Traversal''.
_tail :: YLens.Lens' (Vec ('S n) a) (Vec n a)
_tail :: LensLike f (Vec ('S n) a) (Vec ('S n) a) (Vec n a) (Vec n a)
_tail Vec n a -> f (Vec n a)
f (x ::: xs) = (a
x a -> Vec n a -> Vec ('S n) a
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) 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
xs
{-# INLINE _tail #-}

-------------------------------------------------------------------------------
-- Generic traversable with index
-------------------------------------------------------------------------------

-- | Generic traverse.
--
-- __Don't use__, rather use @DeriveTraversable@
gtraverse
    :: ( G.Generic1 t, GFrom t, GTo t
       , N.SNatI (GPigeonholeSize t)
       , Applicative f
       )
    => (a -> f b) -> t a -> f (t b)
gtraverse :: (a -> f b) -> t a -> f (t b)
gtraverse = LensLike (Curried (Yoneda f)) (t a) (t b) a b
-> (a -> f b) -> t a -> f (t b)
forall (f :: * -> *) s t a b.
Applicative f =>
LensLike (Curried (Yoneda f)) s t a b -> LensLike f s t a b
confusing (LensLike (Curried (Yoneda f)) (t a) (t b) a b
 -> (a -> f b) -> t a -> f (t b))
-> LensLike (Curried (Yoneda f)) (t a) (t b) a b
-> (a -> f b)
-> t a
-> f (t b)
forall a b. (a -> b) -> a -> b
$ \a -> Curried (Yoneda f) b
afb t a
ta -> Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) b -> t b
forall (c :: * -> *) a.
(Generic1 @* c, GTo c) =>
Vec (GPigeonholeSize c) a -> c a
gto (Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) b -> t b)
-> Curried (Yoneda f) (Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) b)
-> Curried (Yoneda f) (t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> Curried (Yoneda f) b)
-> Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) a
-> Curried (Yoneda f) (Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) b)
forall (n :: Nat) (f :: * -> *) a b.
(Applicative f, SNatI n) =>
(a -> f b) -> Vec n a -> f (Vec n b)
V.traverse a -> Curried (Yoneda f) b
afb (t a -> Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) a
forall (c :: * -> *) a.
(Generic1 @* c, GFrom c) =>
c a -> Vec (GPigeonholeSize c) a
gfrom t a
ta)
{-# INLINE gtraverse #-}

-- | Traverse with index.
--
-- >>> data Key = Key1 | Key2 | Key3 deriving (Show, Generic)
-- >>> data Values a = Values a a a deriving (Generic1)
--
-- >>> gitraverse (\i a -> Const [(i :: Key, a)]) (Values 'a' 'b' 'c')
-- Const [(Key1,'a'),(Key2,'b'),(Key3,'c')]
--
gitraverse
    :: ( G.Generic i, F.GTo i
       , G.Generic1 t, GFrom t, GTo t
       , F.GEnumSize i ~ GPigeonholeSize t, N.SNatI (GPigeonholeSize t)
       , Applicative f
       )
    => (i -> a -> f b) -> t a -> f (t b)
gitraverse :: (i -> a -> f b) -> t a -> f (t b)
gitraverse = IxLensLike (Curried (Yoneda f)) i (t a) (t b) a b
-> (i -> a -> f b) -> t a -> f (t b)
forall (f :: * -> *) i s t a b.
Applicative f =>
IxLensLike (Curried (Yoneda f)) i s t a b -> IxLensLike f i s t a b
iconfusing (IxLensLike (Curried (Yoneda f)) i (t a) (t b) a b
 -> (i -> a -> f b) -> t a -> f (t b))
-> IxLensLike (Curried (Yoneda f)) i (t a) (t b) a b
-> (i -> a -> f b)
-> t a
-> f (t b)
forall a b. (a -> b) -> a -> b
$ \i -> a -> Curried (Yoneda f) b
iafb t a
ta -> Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) b -> t b
forall (c :: * -> *) a.
(Generic1 @* c, GTo c) =>
Vec (GPigeonholeSize c) a -> c a
gto (Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) b -> t b)
-> Curried (Yoneda f) (Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) b)
-> Curried (Yoneda f) (t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Fin (PigeonholeSizeRep (Rep1 @* t) 'Z)
 -> a -> Curried (Yoneda f) b)
-> Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) a
-> Curried (Yoneda f) (Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) b)
forall (n :: Nat) (f :: * -> *) a b.
(Applicative f, SNatI n) =>
(Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
V.itraverse (\Fin (PigeonholeSizeRep (Rep1 @* t) 'Z)
i a
a -> i -> a -> Curried (Yoneda f) b
iafb (Fin (GEnumSize i) -> i
forall a. (Generic a, GTo a) => Fin (GEnumSize a) -> a
F.gto Fin (GEnumSize i)
Fin (PigeonholeSizeRep (Rep1 @* t) 'Z)
i) a
a) (t a -> Vec (PigeonholeSizeRep (Rep1 @* t) 'Z) a
forall (c :: * -> *) a.
(Generic1 @* c, GFrom c) =>
c a -> Vec (GPigeonholeSize c) a
gfrom t a
ta)
{-# INLINE gitraverse #-}

-------------------------------------------------------------------------------
-- PigeonholeSize
-------------------------------------------------------------------------------

-- | Compute the size from the type.
type GPigeonholeSize c = PigeonholeSizeRep (G.Rep1 c) N.Nat0

type family PigeonholeSizeRep (c :: * -> *) (n :: Nat) :: Nat where
    PigeonholeSizeRep (a :*: b )   n = PigeonholeSizeRep a (PigeonholeSizeRep b n)
    PigeonholeSizeRep (M1 _d _c a) n = PigeonholeSizeRep a n
    PigeonholeSizeRep Par1         n = 'N.S n
    PigeonholeSizeRep U1           n = n

-------------------------------------------------------------------------------
-- From
-------------------------------------------------------------------------------

-- | Generic version of 'from'.
gfrom :: (G.Generic1 c, GFrom c) => c a -> Vec (GPigeonholeSize c) a
gfrom :: c a -> Vec (GPigeonholeSize c) a
gfrom = \c a
x -> Rep1 @* c a -> Vec 'Z a -> Vec (GPigeonholeSize c) a
forall (c :: * -> *) x (n :: Nat).
GFromRep1 c =>
c x -> Vec n x -> Vec (PigeonholeSizeRep c n) x
gfromRep1 (c a -> Rep1 @* c a
forall k (f :: k -> *) (a :: k).
Generic1 @k f =>
f a -> Rep1 @k f a
G.from1 c a
x) Vec 'Z a
forall a. Vec 'Z a
VNil

-- | Constraint for the class that computes 'gfrom'.
type GFrom c = GFromRep1 (G.Rep1 c)

class GFromRep1 (c :: * -> *)  where
    gfromRep1 :: c x -> Vec n x -> Vec (PigeonholeSizeRep c n) x

instance (GFromRep1 a, GFromRep1 b) => GFromRep1 (a :*: b) where
    gfromRep1 :: (:*:) @* a b x
-> Vec n x -> Vec (PigeonholeSizeRep ((:*:) @* a b) n) x
gfromRep1 (a x
x :*: b x
y) Vec n x
z = a x
-> Vec (PigeonholeSizeRep b n) x
-> Vec (PigeonholeSizeRep a (PigeonholeSizeRep b n)) x
forall (c :: * -> *) x (n :: Nat).
GFromRep1 c =>
c x -> Vec n x -> Vec (PigeonholeSizeRep c n) x
gfromRep1 a x
x (b x -> Vec n x -> Vec (PigeonholeSizeRep b n) x
forall (c :: * -> *) x (n :: Nat).
GFromRep1 c =>
c x -> Vec n x -> Vec (PigeonholeSizeRep c n) x
gfromRep1 b x
y Vec n x
z)

instance GFromRep1 a => GFromRep1 (M1 d c a) where
    gfromRep1 :: M1 @* d c a x
-> Vec n x -> Vec (PigeonholeSizeRep (M1 @* d c a) n) x
gfromRep1 (M1 a x
a) Vec n x
z = a x -> Vec n x -> Vec (PigeonholeSizeRep a n) x
forall (c :: * -> *) x (n :: Nat).
GFromRep1 c =>
c x -> Vec n x -> Vec (PigeonholeSizeRep c n) x
gfromRep1 a x
a Vec n x
z

instance GFromRep1 Par1 where
    gfromRep1 :: Par1 x -> Vec n x -> Vec (PigeonholeSizeRep Par1 n) x
gfromRep1 (Par1 x
x) Vec n x
z = x
x x -> Vec n x -> Vec ('S n) x
forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec n x
z

instance GFromRep1 U1 where
    gfromRep1 :: U1 @* x -> Vec n x -> Vec (PigeonholeSizeRep (U1 @*) n) x
gfromRep1 U1 @* x
_U1 Vec n x
z = Vec n x
Vec (PigeonholeSizeRep (U1 @*) n) x
z

-------------------------------------------------------------------------------
-- To
-------------------------------------------------------------------------------

-- | Generic version of 'to'.
gto :: forall c a. (G.Generic1 c, GTo c) => Vec (GPigeonholeSize c) a -> c a
gto :: Vec (GPigeonholeSize c) a -> c a
gto = \Vec (GPigeonholeSize c) a
xs -> Rep1 @* c a -> c a
forall k (f :: k -> *) (a :: k).
Generic1 @k f =>
Rep1 @k f a -> f a
G.to1 (Rep1 @* c a -> c a) -> Rep1 @* c a -> c a
forall a b. (a -> b) -> a -> b
$ (Rep1 @* c a, Vec 'Z a) -> Rep1 @* c a
forall a b. (a, b) -> a
fst (Vec (GPigeonholeSize c) a -> (Rep1 @* c a, Vec 'Z a)
forall (c :: * -> *) (n :: Nat) x.
GToRep1 c =>
Vec (PigeonholeSizeRep c n) x -> (c x, Vec n x)
gtoRep1 Vec (GPigeonholeSize c) a
xs :: (G.Rep1 c a, Vec 'N.Z a))

-- | Constraint for the class that computes 'gto'.
type GTo c = GToRep1 (G.Rep1 c)

class GToRep1 (c :: * -> *) where
    gtoRep1 :: Vec (PigeonholeSizeRep c n) x -> (c x, Vec n x)

instance GToRep1 a => GToRep1 (M1 d c a) where
    gtoRep1 :: Vec (PigeonholeSizeRep (M1 @* d c a) n) x
-> (M1 @* d c a x, Vec n x)
gtoRep1 = (a x -> M1 @* d c a x)
-> (a x, Vec n x) -> (M1 @* d c a x, Vec n x)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first a x -> M1 @* d c a x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 @k i c f p
M1 ((a x, Vec n x) -> (M1 @* d c a x, Vec n x))
-> (Vec (PigeonholeSizeRep a n) x -> (a x, Vec n x))
-> Vec (PigeonholeSizeRep a n) x
-> (M1 @* d c a x, Vec n x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vec (PigeonholeSizeRep a n) x -> (a x, Vec n x)
forall (c :: * -> *) (n :: Nat) x.
GToRep1 c =>
Vec (PigeonholeSizeRep c n) x -> (c x, Vec n x)
gtoRep1

instance (GToRep1 a, GToRep1 b) => GToRep1 (a :*: b) where
    gtoRep1 :: Vec (PigeonholeSizeRep ((:*:) @* a b) n) x
-> ((:*:) @* a b x, Vec n x)
gtoRep1 Vec (PigeonholeSizeRep ((:*:) @* a b) n) x
xs =
        let (a x
a, Vec (PigeonholeSizeRep b n) x
ys) = Vec (PigeonholeSizeRep a (PigeonholeSizeRep b n)) x
-> (a x, Vec (PigeonholeSizeRep b n) x)
forall (c :: * -> *) (n :: Nat) x.
GToRep1 c =>
Vec (PigeonholeSizeRep c n) x -> (c x, Vec n x)
gtoRep1 Vec (PigeonholeSizeRep a (PigeonholeSizeRep b n)) x
Vec (PigeonholeSizeRep ((:*:) @* a b) n) x
xs
            (b x
b, Vec n x
zs) = Vec (PigeonholeSizeRep b n) x -> (b x, Vec n x)
forall (c :: * -> *) (n :: Nat) x.
GToRep1 c =>
Vec (PigeonholeSizeRep c n) x -> (c x, Vec n x)
gtoRep1 Vec (PigeonholeSizeRep b n) x
ys
        in (a x
a a x -> b x -> (:*:) @* a b x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) @k f g p
:*: b x
b, Vec n x
zs)

instance GToRep1 Par1 where
    gtoRep1 :: Vec (PigeonholeSizeRep Par1 n) x -> (Par1 x, Vec n x)
gtoRep1 (x ::: xs) = (x -> Par1 x
forall p. p -> Par1 p
Par1 x
x, Vec n x
xs)

instance GToRep1 U1 where
    gtoRep1 :: Vec (PigeonholeSizeRep (U1 @*) n) x -> (U1 @* x, Vec n x)
gtoRep1 Vec (PigeonholeSizeRep (U1 @*) n) x
xs = (U1 @* x
forall k (p :: k). U1 @k p
U1, Vec n x
Vec (PigeonholeSizeRep (U1 @*) n) x
xs)