vec 0.1 → 0.1.1

raw patch · 12 files changed

+1506/−107 lines, 12 filesdep +transformersdep ~findep ~hashabledep ~inspection-testingsetup-changedPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: transformers

Dependency ranges changed: fin, hashable, inspection-testing, semigroups

API changes (from Hackage documentation)

Files

• ChangeLog.md +6/−0
• Setup.hs +0/−2
• src/Data/Functor/Confusing.hs +109/−0
• src/Data/Vec/DataFamily/SpineStrict.hs +889/−0
• src/Data/Vec/DataFamily/SpineStrict/Pigeonhole.hs +233/−0
• src/Data/Vec/Lazy.hs +2/−2
• src/Data/Vec/Lazy/Inline.hs +15/−13
• test/Inspection.hs +2/−9
• test/Inspection/DataFamily/SpineStrict.hs +70/−0
• test/Inspection/DataFamily/SpineStrict/Pigeonhole.hs +93/−0
• test/Main.hs +6/−0
• vec.cabal +81/−81

@@ -1,5 +1,11 @@ # Revision history for boring +## 0.1.1++- Add `Data.Vec.DataFamily.SpineStrict` module+- Add `Data.Vec.DataFamily.SpineStrict.Pigeonhole` module:+  this let us define `Representable` in a handy way.+ ## 0.1  - Reverse dependencies with `boring`.

@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain

@@ -0,0 +1,109 @@+{-# LANGUAGE RankNTypes #-}+-- |+-- Csongor Kiss, Matthew Pickering, and Nicolas Wu. 2018. Generic deriving of generic traversals.+-- Proc. ACM Program. Lang. 2, ICFP, Article 85 (July 2018), 30 pages. DOI: https://doi.org/10.1145/3236780+--+-- https://arxiv.org/abs/1805.06798+--+-- This is modified version of part of @generic-lens@ library+--+-- Copyright (c) 2018, Csongor Kiss+-- +-- All rights reserved.+-- +-- Redistribution and use in source and binary forms, with or without+-- modification, are permitted provided that the following conditions are met:+-- +--     * Redistributions of source code must retain the above copyright+--       notice, this list of conditions and the following disclaimer.+-- +--     * Redistributions in binary form must reproduce the above+--       copyright notice, this list of conditions and the following+--       disclaimer in the documentation and/or other materials provided+--       with the distribution.+-- +--     * Neither the name of Csongor Kiss nor the names of other+--       contributors may be used to endorse or promote products derived+--       from this software without specific prior written permission.+-- +-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+-- "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+-- LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+-- A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+-- OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+-- SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+-- LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+-- DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+-- THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+-- (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+-- OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+-- +module Data.Functor.Confusing where++import Prelude ()+import Prelude.Compat++-------------------------------------------------------------------------------+-- Confusing+-------------------------------------------------------------------------------++type LensLike f s t a b = (a -> f b) -> s -> f t++confusing :: Applicative f => LensLike (Curried (Yoneda f)) s t a b -> (a -> f b) -> s -> f t+confusing t = \f -> lowerYoneda . lowerCurried . t (liftCurriedYoneda . f)+{-# INLINE confusing #-}++type IxLensLike f i s t a b = (i -> a -> f b) -> s -> f t++iconfusing :: Applicative f => IxLensLike (Curried (Yoneda f)) i s t a b -> (i -> a -> f b) -> s -> f t+iconfusing t = \f -> lowerYoneda . lowerCurried . t (\i a -> liftCurriedYoneda (f i a))+{-# INLINE iconfusing #-}++liftCurriedYoneda :: Applicative f => f a -> Curried (Yoneda f) a+liftCurriedYoneda fa = Curried (`yap` fa)+{-# INLINE liftCurriedYoneda #-}++yap :: Applicative f => Yoneda f (a -> b) -> f a -> Yoneda f b+yap (Yoneda k) fa = Yoneda (\ab_r -> k (ab_r .) <*> fa)+{-# INLINE yap #-}++-------------------------------------------------------------------------------+-- Curried+-------------------------------------------------------------------------------++newtype Curried f a = Curried { runCurried :: forall r. f (a -> r) -> f r }++instance Functor f => Functor (Curried f) where+    fmap f (Curried g) = Curried (g . fmap (.f))+    {-# INLINE fmap #-}++instance Functor f => Applicative (Curried f) where+    pure a = Curried (fmap ($ a))+    {-# INLINE pure #-}+    Curried mf <*> Curried ma = Curried (ma . mf . fmap (.))+    {-# INLINE (<*>) #-}++liftCurried :: Applicative f => f a -> Curried f a+liftCurried fa = Curried (<*> fa)++lowerCurried :: Applicative f => Curried f a -> f a+lowerCurried (Curried f) = f (pure id)++-------------------------------------------------------------------------------+-- Yoneda+-------------------------------------------------------------------------------++newtype Yoneda f a = Yoneda { runYoneda :: forall b. (a -> b) -> f b }++liftYoneda :: Functor f => f a -> Yoneda f a+liftYoneda a = Yoneda (\f -> fmap f a)++lowerYoneda :: Yoneda f a -> f a+lowerYoneda (Yoneda f) = f id++instance Functor (Yoneda f) where+    fmap f m = Yoneda (\k -> runYoneda m (k . f))++instance Applicative f => Applicative (Yoneda f) where+    pure a = Yoneda (\f -> pure (f a))+    Yoneda m <*> Yoneda n = Yoneda (\f -> m (f .) <*> n id)

@@ -0,0 +1,889 @@+{-# LANGUAGE CPP                    #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE RankNTypes             #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE UndecidableInstances   #-}+-- | Spine-strict length-indexed list defined as data-family: 'Vec'.+--+-- Data family variant allows  lazy pattern matching.+-- On the other hand, the 'Vec' value doesn't "know" its length (i.e. there isn't 'Data.Vec.Lazy.withDict').+--+-- == Agda +--+-- If you happen to familiar with Agda, then the difference+-- between GADT and data-family version is maybe clearer:+--+-- @+-- module Vec where+-- +-- open import Data.Nat+-- open import Relation.Binary.PropositionalEquality using (_≡_; refl)+-- +-- -- \"GADT"+-- data Vec (A : Set) : ℕ → Set where+--   []  : Vec A 0+--   _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)+-- +-- infixr 50 _∷_+-- +-- exVec : Vec ℕ 2+-- exVec = 13 ∷ 37 ∷ []+-- +-- -- "data family"+-- data Unit : Set where+--   [] : Unit+-- +-- data _×_ (A B : Set) : Set where+--   _∷_ : A → B → A × B+-- +-- infixr 50 _×_+-- +-- VecF : Set → ℕ → Set+-- VecF A zero    = Unit+-- VecF A (suc n) = A × VecF A n+-- +-- exVecF : VecF ℕ 2+-- exVecF = 13 ∷ 37 ∷ []+-- +-- reduction : VecF ℕ 2 ≡ ℕ × ℕ × Unit+-- reduction = refl+-- @+-- +module Data.Vec.DataFamily.SpineStrict (+    Vec (..),+    -- * Construction+    empty,+    singleton,+    -- * Conversions+    toPull,+    fromPull,+    _Pull,+    toList,+    fromList,+    _Vec,+    fromListPrefix,+    reifyList,+    -- * Indexing+    (!),+    ix,+    _Cons,+    _head,+    _tail,+    cons,+    head,+    tail,+    -- * Concatenation and splitting+    (++),+    split,+    concatMap,+    concat,+    chunks,+    -- * Folds+    foldMap,+    foldMap1,+    ifoldMap,+    ifoldMap1,+    foldr,+    ifoldr,+    -- * Special folds+    length,+    null,+    sum,+    product,+    -- * Mapping+    map,+    imap,+    traverse,+    traverse1,+    itraverse,+    itraverse_,+    -- * Zipping+    zipWith,+    izipWith,+    -- * Monadic+    bind,+    join,+    -- * Universe+    universe,+    -- * Extras+    ensureSpine,+    ) where++import Prelude ()+import Prelude.Compat+       (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..),+       Monoid (..), Num (..), Ord (..), Ordering (EQ), Show (..), ShowS, const,+       flip, id, seq, showParen, showString, ($), (&&), (.), (<$>))++import Control.Applicative (Applicative (..), liftA2)+import Control.DeepSeq     (NFData (..))+import Data.Distributive   (Distributive (..))+import Data.Fin            (Fin)+import Data.Functor.Apply  (Apply (..))+import Data.Functor.Rep    (Representable (..), distributeRep)+import Data.Hashable       (Hashable (..))+import Data.Nat+import Data.Semigroup      (Semigroup (..))++--- Instances+import qualified Control.Lens               as I+import qualified Data.Foldable              as I (Foldable (..))+import qualified Data.Functor.Bind          as I (Bind (..))+import qualified Data.Semigroup.Foldable    as I (Foldable1 (..))+import qualified Data.Semigroup.Traversable as I (Traversable1 (..))+import qualified Data.Traversable           as I (Traversable (..))++import qualified Data.Fin      as F+import qualified Data.Type.Nat as N+import qualified Data.Vec.Pull as P++infixr 5 :::++-- | Vector, i.e. length-indexed list.+data family   Vec (n :: Nat) a+data instance Vec 'Z     a = VNil+data instance Vec ('S n) a = a ::: !(Vec n a)++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++-- |+--+-- >>> 'a' ::: 'b' ::: VNil == 'a' ::: 'c' ::: VNil+-- False+instance (Eq a, N.InlineInduction n) => Eq (Vec n a) where+    (==) = getEqual (N.inlineInduction1 start step) where+        start :: Equal 'Z a+        start = Equal $ \_ _ -> True++        step :: Equal m a -> Equal ('S m) a+        step (Equal go) = Equal $ \(x ::: xs) (y ::: ys) ->+            x == y && go xs ys++newtype Equal n a = Equal { getEqual :: Vec n a -> Vec n a -> Bool }++-- |+--+-- >>> compare ('a' ::: 'b' ::: VNil) ('a' ::: 'c' ::: VNil)+-- LT+instance (Ord a, N.InlineInduction n) => Ord (Vec n a) where+    compare = getCompare (N.inlineInduction1 start step) where+        start :: Compare 'Z a+        start = Compare $ \_ _ -> EQ++        step :: Compare m a -> Compare ('S m) a+        step (Compare go) = Compare $ \(x ::: xs) (y ::: ys) ->+            compare x y <> go xs ys++newtype Compare n a = Compare { getCompare :: Vec n a -> Vec n a -> Ordering }++instance (Show a, N.InlineInduction n) => Show (Vec n a) where+    showsPrec = getShowsPrec (N.inlineInduction1 start step) where+        start :: ShowsPrec 'Z a+        start = ShowsPrec $ \_ _ -> showString "VNil"++        step :: ShowsPrec m a -> ShowsPrec ('S m) a+        step (ShowsPrec go) = ShowsPrec $ \d (x ::: xs) -> showParen (d > 5)+            $ showsPrec 6 x+            . showString " ::: "+            . go 5 xs++newtype ShowsPrec n a = ShowsPrec { getShowsPrec :: Int -> Vec n a -> ShowS }++instance N.InlineInduction n => Functor (Vec n) where+    fmap = map++instance N.InlineInduction n => I.Foldable (Vec n) where+    foldMap = foldMap++    foldr  = foldr+    -- foldl' = foldl'++#if MIN_VERSION_base(4,8,0)+    null    = null+    length  = length+    sum     = sum+    product = product+#endif++instance (N.InlineInduction m, n ~ 'S m) => I.Foldable1 (Vec n) where+    foldMap1 = foldMap1++instance N.InlineInduction n => I.Traversable (Vec n) where+    traverse = traverse++instance (N.InlineInduction m, n ~ 'S m) => I.Traversable1 (Vec n) where+    traverse1 = traverse1++instance (NFData a, N.InlineInduction n) => NFData (Vec n a) where+    rnf = getRnf (N.inlineInduction1 z s) where+        z           = Rnf $ \VNil -> ()+        s (Rnf rec) = Rnf $ \(x ::: xs) -> rnf x `seq` rec xs++newtype Rnf n a = Rnf { getRnf :: Vec n a -> () }++instance (Hashable a, N.InlineInduction n) => Hashable (Vec n a) where+    hashWithSalt = getHashWithSalt (N.inlineInduction1 z s) where+        z = HashWithSalt $ \salt VNil -> salt `hashWithSalt` (0 :: Int)+        s (HashWithSalt rec) = HashWithSalt $ \salt (x ::: xs) -> rec (salt+            `hashWithSalt` x) xs++newtype HashWithSalt n a = HashWithSalt { getHashWithSalt :: Int -> Vec n a -> Int }++instance N.InlineInduction n => Applicative (Vec n) where+    pure x = N.inlineInduction1 VNil (x :::)+    (<*>)  = zipWith ($)+    _ *> x = x+    x <* _ = x+#if MIN_VERSION_base(4,10,0)+    liftA2 = zipWith+#endif++instance N.InlineInduction n => Monad (Vec n) where+    return = pure+    (>>=)  = bind+    _ >> x = x++instance N.InlineInduction n => Distributive (Vec n) where+    distribute = distributeRep++instance N.InlineInduction n => Representable (Vec n) where+    type Rep (Vec n) = Fin n+    tabulate = fromPull . tabulate+    index    = index . toPull++instance (Semigroup a, N.InlineInduction n) => Semigroup (Vec n a) where+    (<>) = zipWith (<>)++instance (Monoid a, N.InlineInduction n) => Monoid (Vec n a) where+    mempty = pure mempty+    mappend = zipWith mappend++instance N.InlineInduction n => Apply (Vec n) where+    (<.>) = zipWith ($)+    _ .> x = x+    x <. _ = x++instance N.InlineInduction n => I.Bind (Vec n) where+    (>>-) = bind+    join  = join++instance N.InlineInduction n => I.FunctorWithIndex (Fin n) (Vec n) where+    imap = imap++instance N.InlineInduction n => I.FoldableWithIndex (Fin n) (Vec n) where+    ifoldMap = ifoldMap+    ifoldr   = ifoldr++instance N.InlineInduction n => I.TraversableWithIndex (Fin n) (Vec n) where+    itraverse = itraverse++instance N.InlineInduction n => I.Each (Vec n a) (Vec n b) a b where+    each = traverse++type instance I.Index (Vec n a)   = Fin n+type instance I.IxValue (Vec n a) = a++-- | 'Vec' doesn't have 'I.At' instance, as we __cannot__ remove value from 'Vec'.+-- See 'ix' in "Data.Vec.DataFamily.SpineStrict" module for an 'I.Lens' (not 'I.Traversal').+instance I.Ixed (Vec n a) where+    ix = ix++instance I.Field1 (Vec ('S n) a) (Vec ('S n) a) a a where+    _1 = _head++instance I.Field2 (Vec ('S ('S n)) a) (Vec ('S ('S n)) a) a a where+    _2 = _tail . _head++instance I.Field3 (Vec ('S ('S ('S n))) a) (Vec ('S ('S ('S n))) a) a a where+    _3 = _tail . _tail . _head++instance I.Field4 (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S ('S n)))) a) a a where+    _4 = _tail . _tail . _tail . _head++instance I.Field5 (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S ('S n))))) a) a a where+    _5 = _tail . _tail . _tail . _tail . _head++instance I.Field6 (Vec ('S ('S ('S ('S ('S ('S n)))))) a) (Vec ('S ('S ('S ('S ('S ('S n)))))) a) a a where+    _6 = _tail . _tail . _tail . _tail . _tail . _head++instance I.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 = _tail . _tail . _tail . _tail . _tail . _tail . _head++instance I.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 = _tail . _tail . _tail . _tail . _tail . _tail . _tail . _head++instance I.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 = _tail . _tail . _tail . _tail . _tail . _tail . _tail . _tail . _head++-------------------------------------------------------------------------------+-- Construction+-------------------------------------------------------------------------------++-- | Empty 'Vec'.+empty :: Vec 'Z a+empty = VNil++-- | 'Vec' with exactly one element.+--+-- >>> singleton True+-- True ::: VNil+--+singleton :: a -> Vec ('S 'Z) a+singleton x = x ::: VNil++-------------------------------------------------------------------------------+-- Conversions+-------------------------------------------------------------------------------++-- | Convert to pull 'P.Vec'.+toPull :: forall n a. N.InlineInduction n => Vec n a -> P.Vec n a+toPull = getToPull (N.inlineInduction1 start step) where+    start :: ToPull 'Z a+    start = ToPull $ \_ -> P.Vec F.absurd++    step :: ToPull m a -> ToPull ('S m) a+    step (ToPull f) = ToPull $ \(x ::: xs) -> P.Vec $ \i -> case i of+        F.Z    -> x+        F.S i' -> P.unVec (f xs) i'++newtype ToPull n a = ToPull { getToPull :: Vec n a -> P.Vec n a }++-- | Convert from pull 'P.Vec'.+fromPull :: forall n a. N.InlineInduction n => P.Vec n a -> Vec n a+fromPull = getFromPull (N.inlineInduction1 start step) where+    start :: FromPull 'Z a+    start = FromPull $ const VNil++    step :: FromPull m a -> FromPull ('S m) a+    step (FromPull f) = FromPull $ \(P.Vec v) -> v F.Z ::: f (P.Vec (v . F.S))++newtype FromPull n a = FromPull { getFromPull :: P.Vec n a -> Vec n a }++-- | An 'I.Iso' from 'toPull' and 'fromPull'.+_Pull :: N.InlineInduction n => I.Iso (Vec n a) (Vec n b) (P.Vec n a) (P.Vec n b)+_Pull = I.iso toPull fromPull++-- | Convert 'Vec' to list.+--+-- >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil+-- "foo"+toList :: forall n a. N.InlineInduction n => Vec n a -> [a]+toList = getToList (N.inlineInduction1 start step) where+    start :: ToList 'Z a+    start = ToList (const [])++    step :: ToList m a -> ToList ('S m) a+    step (ToList f) = ToList $ \(x ::: xs) -> x : f xs++newtype ToList n a = ToList { getToList :: Vec n a -> [a] }++-- | Convert list @[a]@ to @'Vec' n a@.+-- Returns 'Nothing' if lengths don't match exactly.+--+-- >>> fromList "foo" :: Maybe (Vec N.Nat3 Char)+-- Just ('f' ::: 'o' ::: 'o' ::: VNil)+--+-- >>> fromList "quux" :: Maybe (Vec N.Nat3 Char)+-- Nothing+--+-- >>> fromList "xy" :: Maybe (Vec N.Nat3 Char)+-- Nothing+--+fromList :: N.InlineInduction n => [a] -> Maybe (Vec n a)+fromList = getFromList (N.inlineInduction1 start step) where+    start :: FromList 'Z a+    start = FromList $ \xs -> case xs of+        []      -> Just VNil+        (_ : _) -> Nothing++    step :: FromList n a -> FromList ('N.S n) a+    step (FromList f) = FromList $ \xs -> case xs of+        []       -> Nothing+        (x : xs') -> (x :::) <$> f xs'++newtype FromList n a = FromList { getFromList :: [a] -> Maybe (Vec n a) }++-- | Prism from list.+--+-- >>> "foo" ^? _Vec :: Maybe (Vec N.Nat3 Char)+-- Just ('f' ::: 'o' ::: 'o' ::: VNil)+--+-- >>> "foo" ^? _Vec :: Maybe (Vec N.Nat2 Char)+-- Nothing+--+-- >>> _Vec # (True ::: False ::: VNil)+-- [True,False]+--+_Vec :: N.InlineInduction n => I.Prism' [a] (Vec n a)+_Vec = I.prism' toList fromList++-- | Convert list @[a]@ to @'Vec' n a@.+-- Returns 'Nothing' if input list is too short.+--+-- >>> fromListPrefix "foo" :: Maybe (Vec N.Nat3 Char)+-- Just ('f' ::: 'o' ::: 'o' ::: VNil)+--+-- >>> fromListPrefix "quux" :: Maybe (Vec N.Nat3 Char)+-- Just ('q' ::: 'u' ::: 'u' ::: VNil)+--+-- >>> fromListPrefix "xy" :: Maybe (Vec N.Nat3 Char)+-- Nothing+--+fromListPrefix :: N.InlineInduction n => [a] -> Maybe (Vec n a)+fromListPrefix = getFromList (N.inlineInduction1 start step) where+    start :: FromList 'Z a+    start = FromList $ \_ -> Just VNil -- different than in fromList case++    step :: FromList n a -> FromList ('N.S n) a+    step (FromList f) = FromList $ \xs -> case xs of+        []       -> Nothing+        (x : xs') -> (x :::) <$> f xs'++-- | Reify any list @[a]@ to @'Vec' n a@.+--+-- >>> reifyList "foo" length+-- 3+reifyList :: [a] -> (forall n. N.InlineInduction n => Vec n a -> r) -> r+reifyList []       f = f VNil+reifyList (x : xs) f = reifyList xs $ \xs' -> f (x ::: xs')++-------------------------------------------------------------------------------+-- Indexing+-------------------------------------------------------------------------------++flipIndex :: N.InlineInduction n => Fin n -> Vec n a -> a+flipIndex = getIndex (N.inlineInduction1 start step) where+    start :: Index 'Z a+    start = Index F.absurd++    step :: Index m a-> Index ('N.S m) a+    step (Index go) = Index $ \n (x ::: xs) -> case n of+        F.Z   -> x+        F.S m -> go m xs++newtype Index n a = Index { getIndex :: Fin n -> Vec n a -> a }++-- | Indexing.+--+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! F.S F.Z+-- 'b'+--+(!) :: N.InlineInduction n => Vec n a -> Fin n -> a+(!) = flip flipIndex++-- | Index lens.+--+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (F.S F.Z)+-- 'b'+--+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (F.S F.Z) .~ 'x'+-- 'a' ::: 'x' ::: 'c' ::: VNil+--+ix :: Fin n -> I.Lens' (Vec n a) a+ix F.Z     f (x ::: xs) = (::: xs) <$> f x+ix (F.S n) f (x ::: xs) = (x :::)  <$> ix n f xs++-- | Match on non-empty 'Vec'.+--+-- /Note:/ @lens@ 'I._Cons' is a 'I.Prism'.+-- In fact, @'Vec' n a@ cannot have an instance of 'I.Cons' as types don't match.+--+_Cons :: I.Iso (Vec ('S n) a) (Vec ('S n) b) (a, Vec n a) (b, Vec n b)+_Cons = I.iso (\(x ::: xs) -> (x, xs)) (\(x, xs) -> x ::: xs)++-- | Head lens. /Note:/ @lens@ 'I._head' is a 'I.Traversal''.+--+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. _head+-- 'a'+--+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & _head .~ 'x'+-- 'x' ::: 'b' ::: 'c' ::: VNil+--+_head :: I.Lens' (Vec ('S n) a) a+_head f (x ::: xs) = (::: xs) <$> f x+{-# INLINE head #-}++-- | Head lens. /Note:/ @lens@ 'I._head' is a 'I.Traversal''.+_tail :: I.Lens' (Vec ('S n) a) (Vec n a)+_tail f (x ::: xs) = (x :::) <$> f xs+{-# INLINE _tail #-}++-- | Cons an element in front of a 'Vec'.+cons :: a -> Vec n a -> Vec ('S n) a+cons = (:::)++-- | The first element of a 'Vec'.+head :: Vec ('S n) a -> a+head (x ::: _) = x++-- | The elements after the 'head' of a 'Vec'.+tail :: Vec ('S n) a -> Vec n a+tail (_ ::: xs) = xs++-------------------------------------------------------------------------------+-- Concatenation+-------------------------------------------------------------------------------++infixr 5 ++++-- | Append two 'Vec'.+--+-- >>> ('a' ::: 'b' ::: VNil) ++ ('c' ::: 'd' ::: VNil)+-- 'a' ::: 'b' ::: 'c' ::: 'd' ::: VNil+--+(++) :: forall n m a. N.InlineInduction n => Vec n a -> Vec m a -> Vec (N.Plus n m) a+as ++ ys = getAppend (N.inlineInduction1 start step) as where+    start :: Append m 'Z a+    start = Append $ \_ -> ys++    step :: Append m p a -> Append m ('S p) a+    step (Append f) = Append $ \(x ::: xs) -> x ::: f xs++newtype Append m n a = Append { getAppend :: Vec n a -> Vec (N.Plus n m) a }++-- | Split vector into two parts. Inverse of '++'.+--+-- >>> split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char)+-- ('a' ::: VNil,'b' ::: 'c' ::: VNil)+--+-- >>> uncurry (++) (split ('a' ::: 'b' ::: 'c' ::: VNil) :: (Vec N.Nat1 Char, Vec N.Nat2 Char))+-- 'a' ::: 'b' ::: 'c' ::: VNil+--+split :: N.InlineInduction n => Vec (N.Plus n m) a -> (Vec n a, Vec m a)+split = appSplit (N.inlineInduction1 start step) where+    start :: Split m 'Z a+    start = Split $ \xs -> (VNil, xs)++    step :: Split m n a -> Split m ('S n) a+    step (Split f) = Split $ \(x ::: xs) -> case f xs of+        (ys, zs) -> (x ::: ys, zs)++newtype Split m n a = Split { appSplit :: Vec (N.Plus n m) a -> (Vec n a, Vec m a) }++-- | Map over all the elements of a 'Vec' and concatenate the resulting 'Vec's.+--+-- >>> concatMap (\x -> x ::: x ::: VNil) ('a' ::: 'b' ::: VNil)+-- 'a' ::: 'a' ::: 'b' ::: 'b' ::: VNil+--+concatMap :: forall a b n m. (N.InlineInduction m, N.InlineInduction n) => (a -> Vec m b) -> Vec n a -> Vec (N.Mult n m) b+concatMap f = getConcatMap $ N.inlineInduction1 start step where+    start :: ConcatMap m a 'Z b+    start = ConcatMap $ \_ -> VNil++    step :: ConcatMap m a p b -> ConcatMap m a ('S p) b+    step (ConcatMap g) = ConcatMap $ \(x ::: xs) -> f x ++ g xs++newtype ConcatMap m a n b = ConcatMap { getConcatMap :: Vec n a -> Vec (N.Mult n m) b }++-- | @'concatMap' 'id'@+concat :: (N.InlineInduction m, N.InlineInduction n) => Vec n (Vec m a) -> Vec (N.Mult n m) a+concat = concatMap id++-- | Inverse of 'concat'.+--+-- >>> chunks <$> fromListPrefix [1..] :: Maybe (Vec N.Nat2 (Vec N.Nat3 Int))+-- Just ((1 ::: 2 ::: 3 ::: VNil) ::: (4 ::: 5 ::: 6 ::: VNil) ::: VNil)+--+-- >>> let idVec x = x :: Vec N.Nat2 (Vec N.Nat3 Int)+-- >>> concat . idVec . chunks <$> fromListPrefix [1..]+-- Just (1 ::: 2 ::: 3 ::: 4 ::: 5 ::: 6 ::: VNil)+--+chunks :: (N.InlineInduction n, N.InlineInduction m) => Vec (N.Mult n m) a -> Vec n (Vec m a)+chunks = getChunks $ N.induction1 start step where+    start :: Chunks m 'Z a+    start = Chunks $ \_ -> VNil++    step :: forall m n a. N.InlineInduction m => Chunks m n a -> Chunks m ('S n) a+    step (Chunks go) = Chunks $ \xs ->+        let (ys, zs) = split xs :: (Vec m a, Vec (N.Mult n m) a)+        in ys ::: go zs++newtype Chunks  m n a = Chunks  { getChunks  :: Vec (N.Mult n m) a -> Vec n (Vec m a) }++-------------------------------------------------------------------------------+-- Mapping+-------------------------------------------------------------------------------++-- | >>> map not $ True ::: False ::: VNil+-- False ::: True ::: VNil+--+map :: forall a b n. N.InlineInduction n => (a -> b) -> Vec n a -> Vec n b+map f = getMap $ N.inlineInduction1 start step where+    start :: Map a 'Z b+    start = Map $ \_ -> VNil++    step :: Map a m b -> Map a ('S m) b+    step (Map go) = Map $ \(x ::: xs) -> f x ::: go xs++newtype Map a n b = Map { getMap :: Vec n a -> Vec n b }++-- | >>> imap (,) $ 'a' ::: 'b' ::: 'c' ::: VNil+-- (0,'a') ::: (1,'b') ::: (2,'c') ::: VNil+--+imap :: N.InlineInduction n => (Fin n -> a -> b) -> Vec n a -> Vec n b+imap = getIMap $ N.inlineInduction1 start step where+    start :: IMap a 'Z b+    start = IMap $ \_ _ -> VNil++    step :: IMap a m b -> IMap a ('S m) b+    step (IMap go) = IMap $ \f (x ::: xs) -> f F.Z x ::: go (f . F.S) xs++newtype IMap a n b = IMap { getIMap :: (Fin n -> a -> b) -> Vec n a -> Vec n b }++-- | Apply an action to every element of a 'Vec', yielding a 'Vec' of results.+traverse :: forall n f a b. (Applicative f, N.InlineInduction n) => (a -> f b) -> Vec n a -> f (Vec n b)+traverse f =  getTraverse $ N.inlineInduction1 start step where+    start :: Traverse f a 'Z b+    start = Traverse $ \_ -> pure VNil++    step :: Traverse f a m b -> Traverse f a ('S m) b+    step (Traverse go) = Traverse $ \(x ::: xs) -> liftA2 (:::) (f x) (go xs)+{-# INLINE traverse #-}++newtype Traverse f a n b = Traverse { getTraverse :: Vec n a -> f (Vec n b) }++-- | Apply an action to non-empty 'Vec', yielding a 'Vec' of results.+traverse1 :: forall n f a b. (Apply f, N.InlineInduction n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)+traverse1 f = getTraverse1 $ N.inlineInduction1 start step where+    start :: Traverse1 f a 'Z b+    start = Traverse1 $ \(x ::: _) -> (::: VNil) <$> f x++    step :: Traverse1 f a m b -> Traverse1 f a ('S m) b+    step (Traverse1 go) = Traverse1 $ \(x ::: xs) -> liftF2 (:::) (f x) (go xs)++newtype Traverse1 f a n b = Traverse1 { getTraverse1 :: Vec ('S n) a -> f (Vec ('S n) b) }++-- | Apply an action to every element of a 'Vec' and its index, yielding a 'Vec' of results.+itraverse :: forall n f a b. (Applicative f, N.InlineInduction n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)+itraverse = getITraverse $ N.inlineInduction1 start step where+    start :: ITraverse f a 'Z b+    start = ITraverse $ \_ _ -> pure VNil++    step :: ITraverse f a m b -> ITraverse f a ('S m) b+    step (ITraverse go) = ITraverse $ \f (x ::: xs) -> liftA2 (:::) (f F.Z x) (go (f . F.S) xs)+{-# INLINE itraverse #-}++newtype ITraverse f a n b = ITraverse { getITraverse :: (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) }++-- | Apply an action to every element of a 'Vec' and its index, ignoring the results.+itraverse_ :: forall n f a b. (Applicative f, N.InlineInduction n) => (Fin n -> a -> f b) -> Vec n a -> f ()+itraverse_ = getITraverse_ $ N.inlineInduction1 start step where+    start :: ITraverse_ f a 'Z b+    start = ITraverse_ $ \_ _ -> pure ()++    step :: ITraverse_ f a m b -> ITraverse_ f a ('S m) b+    step (ITraverse_ go) = ITraverse_ $ \f (x ::: xs) -> f F.Z x *> go (f . F.S) xs++newtype ITraverse_ f a n b = ITraverse_ { getITraverse_ :: (Fin n -> a -> f b) -> Vec n a -> f () }++-------------------------------------------------------------------------------+-- Folding+-------------------------------------------------------------------------------++-- | See 'I.Foldable'.+foldMap :: (Monoid m, N.InlineInduction n) => (a -> m) -> Vec n a -> m+foldMap f = getFold $ N.inlineInduction1 (Fold (const mempty)) $ \(Fold go) ->+    Fold $ \(x ::: xs) -> f x `mappend` go xs++newtype Fold  a n b = Fold  { getFold  :: Vec n a -> b }++-- | See 'I.Foldable1'.+foldMap1 :: forall s a n. (Semigroup s, N.InlineInduction n) => (a -> s) -> Vec ('S n) a -> s+foldMap1 f = getFold1 $ N.inlineInduction1 start step where+    start :: Fold1 a 'Z s+    start = Fold1 $ \(x ::: _) -> f x++    step :: Fold1 a m s -> Fold1 a ('S m) s+    step (Fold1 g) = Fold1 $ \(x ::: xs) -> f x <> g xs++newtype Fold1 a n b = Fold1 { getFold1 :: Vec ('S n) a -> b }++-- | See 'I.FoldableWithIndex'.+ifoldMap :: forall a n m. (Monoid m, N.InlineInduction n) => (Fin n -> a -> m) -> Vec n a -> m+ifoldMap = getIFoldMap $ N.inlineInduction1 start step where+    start :: IFoldMap a 'Z m+    start = IFoldMap $ \_ _ -> mempty++    step :: IFoldMap a p m -> IFoldMap a ('S p) m+    step (IFoldMap go) = IFoldMap $ \f (x ::: xs) -> f F.Z x `mappend` go (f . F.S) xs++newtype IFoldMap a n m = IFoldMap { getIFoldMap :: (Fin n -> a -> m) -> Vec n a -> m }++-- | There is no type-class for this :(+ifoldMap1 :: forall a n s. (Semigroup s, N.InlineInduction n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s+ifoldMap1 = getIFoldMap1 $ N.inlineInduction1 start step where+    start :: IFoldMap1 a 'Z s+    start = IFoldMap1 $ \f (x ::: _) -> f F.Z x++    step :: IFoldMap1 a p s -> IFoldMap1 a ('S p) s+    step (IFoldMap1 go) = IFoldMap1 $ \f (x ::: xs) -> f F.Z x <> go (f . F.S) xs++newtype IFoldMap1 a n m = IFoldMap1 { getIFoldMap1 :: (Fin ('S n) -> a -> m) -> Vec ('S n) a -> m }++-- | Right fold.+foldr :: forall a b n. N.InlineInduction n => (a -> b -> b) -> b -> Vec n a -> b+foldr f z = getFold $ N.inlineInduction1 start step where+    start :: Fold a 'Z b+    start = Fold $ \_ -> z++    step :: Fold a m b -> Fold a ('S m) b+    step (Fold go) = Fold $ \(x ::: xs) -> f x (go xs)++-- | Right fold with an index.+ifoldr :: forall a b n. N.InlineInduction n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b+ifoldr = getIFoldr $ N.inlineInduction1 start step where+    start :: IFoldr a 'Z b+    start = IFoldr $ \_ z _ -> z++    step :: IFoldr a m b -> IFoldr a ('S m) b+    step (IFoldr go) = IFoldr $ \f z (x ::: xs) -> f F.Z x (go (f . F.S) z xs)++newtype IFoldr a n b = IFoldr { getIFoldr :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b }++-- | Yield the length of a 'Vec'. /O(n)/+length :: forall n a. N.InlineInduction n => Vec n a -> Int+length _ = getLength l where+    l :: Length n+    l = N.inlineInduction (Length 0) $ \(Length n) -> Length (1 + n)++newtype Length (n :: Nat) = Length { getLength :: Int }++-- | Test whether a 'Vec' is empty. /O(1)/+null :: forall n a. N.SNatI n => Vec n a -> Bool+null _ = case N.snat :: N.SNat n of+    N.SZ -> True+    N.SS -> False++-------------------------------------------------------------------------------+-- Special folds+-------------------------------------------------------------------------------++-- | Non-strict 'sum'.+sum :: (Num a, N.InlineInduction n) => Vec n a -> a+sum = getFold $ N.inlineInduction1 start step where+    start :: Num a => Fold a 'Z a+    start = Fold $ \_ -> 0++    step :: Num a => Fold a m a -> Fold a ('S m) a+    step (Fold f) = Fold $ \(x ::: xs) -> x + f xs++-- | Non-strict 'product'.+product :: (Num a, N.InlineInduction n) => Vec n a -> a+product = getFold $ N.inlineInduction1 start step where+    start :: Num a => Fold a 'Z a+    start = Fold $ \_ -> 0++    step :: Num a => Fold a m a -> Fold a ('S m) a+    step (Fold f) = Fold $ \(x ::: xs) -> x + f xs+++-------------------------------------------------------------------------------+-- Zipping+-------------------------------------------------------------------------------++-- | Zip two 'Vec's with a function.+zipWith :: forall a b c n. N.InlineInduction n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c+zipWith f = getZipWith $ N.inlineInduction start step where+    start :: ZipWith a b c 'Z+    start = ZipWith $ \_ _ -> VNil++    step :: ZipWith a b c m -> ZipWith a b c ('S m)+    step (ZipWith go) = ZipWith $ \(x ::: xs) (y ::: ys) -> f x y ::: go xs ys++newtype ZipWith a b c n = ZipWith { getZipWith :: Vec n a -> Vec n b -> Vec n c }++-- | Zip two 'Vec's. with a function that also takes the elements' indices.+izipWith :: N.InlineInduction n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c+izipWith = getIZipWith $ N.inlineInduction start step where+    start :: IZipWith a b c 'Z+    start = IZipWith $ \_ _ _ -> VNil++    step :: IZipWith a b c m -> IZipWith a b c ('S m)+    step (IZipWith go) = IZipWith $ \f (x ::: xs) (y ::: ys) -> f F.Z x y ::: go (f . F.S) xs ys++newtype IZipWith a b c n = IZipWith { getIZipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c }++-------------------------------------------------------------------------------+-- Monadic+-------------------------------------------------------------------------------++-- | Monadic bind.+bind :: N.InlineInduction n => Vec n a -> (a -> Vec n b) -> Vec n b+bind = getBind $ N.inlineInduction1 start step where+    start :: Bind a 'Z b+    start = Bind $ \_ _ -> VNil++    step :: Bind a m b -> Bind a ('S m) b+    step (Bind go) = Bind $ \(x ::: xs) f -> head (f x) ::: go xs (tail . f)++newtype Bind a n b = Bind { getBind :: Vec n a -> (a -> Vec n b) -> Vec n b }++-- | Monadic join.+--+-- >>> join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil+-- 'a' ::: 'd' ::: VNil+join :: N.InlineInduction n => Vec n (Vec n a) -> Vec n a+join = getJoin $ N.inlineInduction1 start step where+    start :: Join 'Z a+    start = Join $ \_ -> VNil++    step :: N.InlineInduction m => Join m a -> Join ('S m) a+    step (Join go) = Join $ \(x ::: xs) -> head x ::: go (map tail xs)++newtype Join n a = Join { getJoin :: Vec n (Vec n a) -> Vec n a }++-------------------------------------------------------------------------------+-- universe+-------------------------------------------------------------------------------++-- | Get all @'Fin' n@ in a @'Vec' n@.+--+-- >>> universe :: Vec N.Nat3 (Fin N.Nat3)+-- 0 ::: 1 ::: 2 ::: VNil+universe :: N.InlineInduction n => Vec n (Fin n)+universe = getUniverse (N.inlineInduction first step) where+    first :: Universe 'Z+    first = Universe VNil++    step :: N.InlineInduction m => Universe m -> Universe ('S m)+    step (Universe go) = Universe (F.Z ::: map F.S go)++newtype Universe n = Universe { getUniverse :: Vec n (Fin n) }++-------------------------------------------------------------------------------+-- EnsureSpine+-------------------------------------------------------------------------------++-- | Ensure spine.+--+-- >>> view (ix F.fin1) $ set (ix F.fin1) 'x' (error "err" :: Vec N.Nat2 Char)+-- *** Exception: err+-- ...+--+-- >>> view (ix F.fin1) $ set (ix F.fin1) 'x' $ ensureSpine (error "err" :: Vec N.Nat2 Char)+-- 'x'+--+ensureSpine :: N.InlineInduction n => Vec n a -> Vec n a+ensureSpine = getEnsureSpine (N.inlineInduction1 first step) where+    first :: EnsureSpine 'Z a+    first = EnsureSpine $ \_ -> VNil+    +    step :: EnsureSpine m a -> EnsureSpine ('S m) a+    step (EnsureSpine go) = EnsureSpine $ \ ~(x ::: xs) -> x ::: go xs++newtype EnsureSpine n a = EnsureSpine { getEnsureSpine :: Vec n a -> Vec n a }++-------------------------------------------------------------------------------+-- Doctest+-------------------------------------------------------------------------------++-- $setup+-- >>> :set -XScopedTypeVariables+-- >>> import Control.Lens ((^.), (&), (.~), (^?), (#), set, view)+-- >>> import Data.Proxy (Proxy (..))+-- >>> import Prelude.Compat (Char, not, uncurry, error)

@@ -0,0 +1,233 @@+{-# LANGUAGE ConstraintKinds        #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE DefaultSignatures      #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+module Data.Vec.DataFamily.SpineStrict.Pigeonhole (+    Pigeonhole (..),+    -- * Representable+    gindex,+    gtabulate,+    -- ** Traversable with index+    gtraverse,+    gitraverse,+    -- * Generic implementation+    gfrom, GFrom,+    gto, GTo,+    GPigeonholeSize,+    ) where++import Prelude ()+import Prelude.Compat++import Control.Arrow                   (first)+import Data.Functor.Confusing          (confusing, iconfusing)+import Data.Functor.Identity           (Identity (..))+import Data.Functor.Product            (Product (..))+import Data.Functor.Rep                (tabulate)+import Data.Nat                        (Nat)+import Data.Proxy                      (Proxy (..))+import Data.Vec.DataFamily.SpineStrict (Vec (..))+import GHC.Generics                    ((:*:) (..), M1 (..), Par1 (..), U1 (..))++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++-- $setup+-- >>> :set -XDeriveGeneric+-- >>> import Data.Void (absurd)+-- >>> import GHC.Generics (Generic, Generic1)++-------------------------------------------------------------------------------+-- 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 = 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 = gto++-- | @'Identity' x@ ~ @x ^ 1@+instance Pigeonhole Identity+--+-- | @'Proxy' x@ ~ @x ^ 0@+instance Pigeonhole Proxy++-- | @'Product' f g x@ ~ @x ^ (size f + size g)@+instance (Pigeonhole f, Pigeonhole g, N.InlineInduction (PigeonholeSize f)) => Pigeonhole (Product f g) where+    type PigeonholeSize (Product f g) = N.Plus (PigeonholeSize f) (PigeonholeSize g)++    to = f . V.split where f (a, b) = Pair (to a) (to b)+    from = uncurry (V.++) . g where g (Pair a b) = (from a, from 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.InlineInduction (GPigeonholeSize f)+       )+     => f a -> i -> a+gindex fa i = gfrom fa V.! F.gfrom i++-- | Tabulate.+--+-- >>> tabulate (\() -> 'x') :: Identity Char+-- Identity 'x'+--+-- >>> tabulate absurd :: Proxy Integer+-- Proxy+--+-- >>> tabulate absurd :: Proxy Integer+-- Proxy+--+gtabulate+    :: ( G.Generic i, F.GTo i, G.Generic1 f, GTo f+       , F.GEnumSize i ~ GPigeonholeSize f, N.InlineInduction (GPigeonholeSize f)+       )+     => (i -> a) -> f a+gtabulate idx = gto $ tabulate (idx . F.gto)++-------------------------------------------------------------------------------+-- Generic traversable with index+-------------------------------------------------------------------------------++-- | Generic traverse.+--+-- __Don't use__, rather use @DeriveTraversable@+gtraverse+    :: ( G.Generic1 t, GFrom t, GTo t+       , N.InlineInduction (GPigeonholeSize t)+       , Applicative f+       )+    => (a -> f b) -> t a -> f (t b)+gtraverse = confusing $ \afb ta -> gto <$> V.traverse afb (gfrom 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.InlineInduction (GPigeonholeSize t)+       , Applicative f+       )+    => (i -> a -> f b) -> t a -> f (t b)+gitraverse = iconfusing $ \iafb ta -> gto <$> V.itraverse (\i a -> iafb (F.gto i) a) (gfrom 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 = \x -> gfromRep1 (G.from1 x) 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 (x :*: y) z = gfromRep1 x (gfromRep1 y z)++instance GFromRep1 a => GFromRep1 (M1 d c a) where+    gfromRep1 (M1 a) z = gfromRep1 a z++instance GFromRep1 Par1 where+    gfromRep1 (Par1 x) z = x ::: z++instance GFromRep1 U1 where+    gfromRep1 _U1 z = z++-------------------------------------------------------------------------------+-- To+-------------------------------------------------------------------------------++-- | Generic version of 'to'.+gto :: forall c a. (G.Generic1 c, GTo c) => Vec (GPigeonholeSize c) a -> c a+gto = \xs -> G.to1 $ fst (gtoRep1 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 = first M1 . gtoRep1++instance (GToRep1 a, GToRep1 b) => GToRep1 (a :*: b) where+    gtoRep1 xs =+        let (a, ys) = gtoRep1 xs+            (b, zs) = gtoRep1 ys+        in (a :*: b, zs)++instance GToRep1 Par1 where+    gtoRep1 (x ::: xs) = (Par1 x, xs)++instance GToRep1 U1 where+    gtoRep1 xs = (U1, xs)

@@ -12,7 +12,7 @@ {-# LANGUAGE StandaloneDeriving     #-} {-# LANGUAGE TypeFamilies           #-} {-# LANGUAGE UndecidableInstances   #-}--- | Lazy length-indexed list: 'Vec'.+-- | Lazy (in elements and spine) length-indexed list: 'Vec'. module Data.Vec.Lazy (     Vec (..),     -- * Construction@@ -389,7 +389,7 @@ -- 'b' -- (!) :: Vec n a -> Fin n -> a-(!) (x ::: _)  (F.Z)   = x+(!) (x ::: _)  F.Z     = x (!) (_ ::: xs) (F.S n) = xs ! n (!) VNil n = case n of {} 

@@ -76,8 +76,8 @@  import Prelude () import Prelude.Compat-       (Applicative (..), Int, Maybe (..), Monoid (..), Num (..), const, id,-       ($), (.), (<$>))+       (Applicative (..), Int, Maybe (..), Monoid (..), Num (..), const, flip,+       id, ($), (.), (<$>))  import Control.Applicative (liftA2) import Data.Fin            (Fin)@@ -207,23 +207,25 @@ -- Indexing ------------------------------------------------------------------------------- +flipIndex :: N.InlineInduction n => Fin n -> Vec n a -> a+flipIndex = getIndex (N.inlineInduction1 start step) where+    start :: Index 'Z a+    start = Index F.absurd++    step :: Index m a-> Index ('N.S m) a+    step (Index go) = Index $ \n (x ::: xs) -> case n of+        F.Z   -> x+        F.S m -> go m xs++newtype Index n a = Index { getIndex :: Fin n -> Vec n a -> a }+ -- | Indexing. -- -- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! F.S F.Z -- 'b' -- (!) :: N.InlineInduction n => Vec n a -> Fin n -> a-(!) = appIndex (N.inlineInduction1 start step) where-    start :: Index 'Z a-    start = Index $ \_ -> F.absurd--    step :: Index n a -> Index ('S n) a-    step (Index f) = Index $ \xs i -> case xs of-        x ::: xs' -> case i of-            F.Z    -> x-            F.S i' -> f xs' i'--newtype Index n a = Index { appIndex :: Vec n a -> Fin n -> a }+(!) = flip flipIndex  -- | Index lens. --

@@ -1,7 +1,7 @@ {-# LANGUAGE GADTs           #-} {-# LANGUAGE TemplateHaskell #-} {-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}-module Main (main) where+module Inspection where  import Prelude hiding (zipWith) @@ -62,7 +62,7 @@  -- though, inlining isn't done if element is Num a => a  -- lhsDotProduct :: Vec N.Nat2 Int -> Vec N.Nat2 Int -> Int-lhsDotProduct xs ys = I.sum (I.zipWith (+) xs ys)+lhsDotProduct xs ys = I.sum (I.zipWith (*) xs ys)  rhsDotProduct :: Vec N.Nat2 Int -> Vec N.Nat2 Int -> Int rhsDotProduct (x0 ::: x1 ::: _) (y0 ::: y1 ::: _) =@@ -86,10 +86,3 @@  inspect $ 'lhsJoin  === 'rhsJoin inspect $ 'lhsJoin' =/= 'rhsJoin------------------------------------------------------------------------------------ Main to make GHC happy----------------------------------------------------------------------------------main :: IO ()-main = return ()

@@ -0,0 +1,70 @@+{-# LANGUAGE GADTs           #-}+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}+{-# OPTIONS_GHC -dsuppress-all #-}+module Inspection.DataFamily.SpineStrict where++import Prelude hiding (zipWith)++import Data.Vec.DataFamily.SpineStrict   (Vec (..))+import Test.Inspection++import qualified Data.Fin                        as F+import qualified Data.Type.Nat                   as N+import qualified Data.Vec.DataFamily.SpineStrict as I++-------------------------------------------------------------------------------+-- zipWith+-------------------------------------------------------------------------------++-- | This doesn't evaluate compile time.+lhsInline :: Vec N.Nat2 Int+lhsInline = I.zipWith (+) oneTwo twoThree++oneTwo :: Vec N.Nat2 Int+oneTwo = 1 ::: 2 ::: VNil++twoThree :: Vec N.Nat2 Int+twoThree = 2 ::: 3 ::: VNil++rhsZipWith :: Vec N.Nat2 Int+rhsZipWith = 3 ::: 5 ::: VNil++inspect $ 'lhsInline === 'rhsZipWith++-------------------------------------------------------------------------------+-- imap+-------------------------------------------------------------------------------++lhsIMap :: Vec N.Nat2 (F.Fin N.Nat2, Char)+lhsIMap = I.imap (,) $ 'a' ::: 'b' ::: VNil++rhsIMap :: Vec N.Nat2 (F.Fin N.Nat2, Char)+rhsIMap = (F.Z,'a') ::: (F.S F.Z,'b') ::: VNil++inspect $ 'lhsIMap  === 'rhsIMap++-------------------------------------------------------------------------------+-- dotProduct+-------------------------------------------------------------------------------++lhsDotProduct :: Vec N.Nat2 Int -> Vec N.Nat2 Int -> Int+lhsDotProduct xs ys = I.sum (I.zipWith (*) xs ys)++rhsDotProduct :: Vec N.Nat2 Int -> Vec N.Nat2 Int -> Int+rhsDotProduct (x0 ::: x1 ::: _) (y0 ::: y1 ::: _) =+    x0 * y0 + x1 * y1++inspect $ 'lhsDotProduct === 'rhsDotProduct++-------------------------------------------------------------------------------+-- join+-------------------------------------------------------------------------------++lhsJoin :: Vec N.Nat2 Char+lhsJoin = I.join $ ('a' ::: 'b' ::: VNil) ::: ('c' ::: 'd' ::: VNil) ::: VNil++rhsJoin :: Vec N.Nat2 Char+rhsJoin = 'a' ::: 'd' ::: VNil++inspect $ 'lhsJoin  === 'rhsJoin

@@ -0,0 +1,93 @@+{-# LANGUAGE DeriveGeneric   #-}+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}+-- {-# OPTIONS_GHC -dsuppress-all #-}+{-# OPTIONS_GHC -dsuppress-idinfo #-}+{-# OPTIONS_GHC -dsuppress-coercions #-}+{-# OPTIONS_GHC -dsuppress-type-applications #-}+{-# OPTIONS_GHC -dsuppress-module-prefixes #-}+{-# OPTIONS_GHC -dsuppress-type-signatures #-}+-- {-# OPTIONS_GHC -dsuppress-uniques #-}+module Inspection.DataFamily.SpineStrict.Pigeonhole where++import Data.Vec.DataFamily.SpineStrict.Pigeonhole+       (gindex, gitraverse, gtabulate, gtraverse)+import GHC.Generics                               (Generic, Generic1)+import Test.Inspection++-------------------------------------------------------------------------------+-- Simple type+-------------------------------------------------------------------------------++data Key = Key1 | Key2 | Key3 | Key4 | Key5 deriving (Show, Generic)+data Values a = Values a a a a a deriving (Show, Generic1)++-------------------------------------------------------------------------------+-- Simple+-------------------------------------------------------------------------------++lhsSimple :: Char+lhsSimple = gindex (Values 'a' 'b' 'c' 'd' 'e' ) Key2++rhsSimple :: Char+rhsSimple = 'b'++inspect $ 'lhsSimple === 'rhsSimple++-------------------------------------------------------------------------------+-- Index+-------------------------------------------------------------------------------++lhsIndex :: Values a -> Key -> a+lhsIndex = gindex++rhsIndex :: Values a -> Key -> a+rhsIndex (Values x _ _ _ _) Key1 = x+rhsIndex (Values _ x _ _ _) Key2 = x+rhsIndex (Values _ _ x _ _) Key3 = x+rhsIndex (Values _ _ _ x _) Key4 = x+rhsIndex (Values _ _ _ _ x) Key5 = x++inspect $ 'lhsIndex === 'rhsIndex++-------------------------------------------------------------------------------+-- Tabulate+-------------------------------------------------------------------------------++lhsTabulate :: (Key -> a) -> Values a+lhsTabulate = gtabulate++rhsTabulate :: (Key -> a) -> Values a+rhsTabulate f = Values (f Key1) (f Key2) (f Key3) (f Key4) (f Key5)++inspect $ 'lhsTabulate === 'rhsTabulate++-------------------------------------------------------------------------------+-- Indexed traverse+-------------------------------------------------------------------------------++lhsTraverse :: Applicative f => (a -> f b) -> Values a -> f (Values b)+lhsTraverse f xs = gtraverse f xs++rhsTraverse :: Applicative f => (a -> f b) -> Values a -> f (Values b)+rhsTraverse f (Values x y z u v) = pure Values+    <*> f x+    <*> f y+    <*> f z+    <*> f u+    <*> f v++inspect $ 'lhsTraverse === 'rhsTraverse++lhsITraverse :: Applicative f => (Key -> a -> f b) -> Values a -> f (Values b)+lhsITraverse f xs = gitraverse f xs++rhsITraverse :: Applicative f => (Key -> a -> f b) -> Values a -> f (Values b)+rhsITraverse f (Values x y z u v) = pure Values+    <*> f Key1 x+    <*> f Key2 y+    <*> f Key3 z+    <*> f Key4 u+    <*> f Key5 v++inspect $ 'lhsITraverse === 'rhsITraverse

@@ -0,0 +1,6 @@+module Main (main) where++import Inspection ()++main :: IO ()+main  = return ()

@@ -1,6 +1,8 @@-name:                vec-version:             0.1-synopsis:            Vec: length-indexed (sized) list+cabal-version:      >=1.10+name:               vec+version:            0.1.1+synopsis:           Vec: length-indexed (sized) list+category:           Data description:   This package provides length-indexed (sized) lists, also known as vectors.   .@@ -10,15 +12,17 @@   \    (:::) :: a -> Vec n a -> Vec ('Nat.S n) a   @   .-  The functions are implemented in three flavours:+  The functions are implemented in four flavours:   .   * __naive__: with explicit recursion. It's simple, constraint-less, yet slow.   .   * __pull__: using @Fin n -> a@ representation, which fuses well,-    but makes some programs hard to write. And+  but makes some programs hard to write. And   .+  * __data-family__: which allows lazy pattern matching+  .   * __inline__: which exploits how GHC dictionary inlining works, unrolling-    recursion if the size of 'Vec' is known statically.+  recursion if the size of 'Vec' is known statically.   .   As best approach depends on the application, @vec@ doesn't do any magic   transformation. Benchmark your code.@@ -33,114 +37,110 @@   === Similar packages   .   * [linear](https://hackage.haskell.org/package/linear) has 'V' type,-    which uses 'Vector' from @vector@ package as backing store.-    @Vec@ is a real GADT, but tries to provide as many useful instances (upto @lens@).+  which uses 'Vector' from @vector@ package as backing store.+  @Vec@ is a real GADT, but tries to provide as many useful instances (upto @lens@).   .   * [vector-sized](https://hackage.haskell.org/package/vector-sized)-    Great package using @GHC.TypeLits@. Current version (0.6.1.0) uses-    @finite-typelits@ and @Int@ indexes.+  Great package using @GHC.TypeLits@. Current version (0.6.1.0) uses+  @finite-typelits@ and @Int@ indexes.   .   * [sized-vector](https://hackage.haskell.org/package/sized-vector) depends-    on @singletons@ package. @vec@ isn't light on dependencies either,-    but try to provide wide GHC support.+  on @singletons@ package. @vec@ isn't light on dependencies either,+  but try to provide wide GHC support.   .   * [fixed-vector](https://hackage.haskell.org/package/fixed-vector)   .   * [sized](https://hackage.haskell.org/package/sized) also depends-    on a @singletons@ package. The @Sized f n a@ type is generalisation of-    @linear@'s @V@ for any @ListLike@.+  on a @singletons@ package. The @Sized f n a@ type is generalisation of+  @linear@'s @V@ for any @ListLike@.   .   * [clash-prelude](https://hackage.haskell.org/package/clash-prelude)-    is a kitchen sink package, which has @CLaSH.Sized.Vector@ module.-    Also depends on @singletons@.+  is a kitchen sink package, which has @CLaSH.Sized.Vector@ module.+  Also depends on @singletons@. -homepage:            https://github.com/phadej/vec-bug-reports:         https://github.com/phadej/vec/issues-license:             BSD3-license-file:        LICENSE-author:              Oleg Grenrus <oleg.grenrus@iki.fi>-maintainer:          Oleg.Grenrus <oleg.grenrus@iki.fi>-copyright:           (c) 2017 Oleg Grenrus-category:            Data-build-type:          Simple-extra-source-files:  ChangeLog.md-cabal-version:       >=1.10+homepage:           https://github.com/phadej/vec+bug-reports:        https://github.com/phadej/vec/issues+license:            BSD3+license-file:       LICENSE+author:             Oleg Grenrus <oleg.grenrus@iki.fi>+maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>+copyright:          (c) 2017 Oleg Grenrus+build-type:         Simple+extra-source-files: ChangeLog.md tested-with:-  GHC==7.8.4,-  GHC==7.10.3,-  GHC==8.0.2,-  GHC==8.2.2,-  GHC==8.4.1+  GHC ==8.8.1 ||  ==8.6.5 || ==8.4.4 || ==8.2.2 || ==8.0.2 || ==7.10.3 || ==7.8.4  source-repository head-  type:      git-  location:  https://github.com/phadej/vec.git+  type:     git+  location: https://github.com/phadej/vec.git  library   exposed-modules:+    Data.Vec.DataFamily.SpineStrict+    Data.Vec.DataFamily.SpineStrict.Pigeonhole     Data.Vec.Lazy     Data.Vec.Lazy.Inline     Data.Vec.Pull++  other-modules:+    Data.Functor.Confusing+   build-depends:-    adjunctions   >=4.4     && <4.5,-    base          >=4.7     && <4.12,-    base-compat   >=0.9.3   && <0.10,-    deepseq       >=1.3.0.2 && <1.5,-    distributive  >=0.5.3   && <0.6,-    fin           >=0.0.1   && <0.1,-    hashable      >=1.2.7.0 && <1.3,-    lens          >=4.16    && <4.17,-    semigroupoids >=5.2.2   && <5.3+      adjunctions    >=4.4     && <4.5+    , base           >=4.7     && <4.13+    , base-compat    >=0.9.3   && <0.11+    , deepseq        >=1.3.0.2 && <1.5+    , distributive   >=0.5.3   && <0.7+    , fin            >=0.0.2   && <0.1+    , hashable       >=1.2.7.0 && <1.3+    , lens           >=4.16    && <4.18+    , semigroupoids  >=5.2.2   && <5.4+    , transformers   >=0.3.0.0 && <0.6 -  if !impl(ghc >= 8.0)-    build-depends:-      semigroups  >=0.18.4  && <0.18.5+  if !impl(ghc >=8.0)+    build-depends: semigroups >=0.18.4 && <0.18.6 -  ghc-options:         -Wall -fprint-explicit-kinds-  hs-source-dirs:      src+  ghc-options:      -Wall -fprint-explicit-kinds+  hs-source-dirs:   src   other-extensions:     CPP     FlexibleContexts     GADTs     TypeOperators-  default-language:    Haskell2010 +  default-language: Haskell2010+ test-suite inspection-  type:                exitcode-stdio-1.0-  main-is:             Inspection.hs-  ghc-options:         -Wall -fprint-explicit-kinds-  hs-source-dirs:      test-  default-language:    Haskell2010+  type:             exitcode-stdio-1.0+  main-is:          Main.hs+  other-modules:+    Inspection+    Inspection.DataFamily.SpineStrict+    Inspection.DataFamily.SpineStrict.Pigeonhole++  ghc-options:      -Wall -fprint-explicit-kinds+  hs-source-dirs:   test+  default-language: Haskell2010   build-depends:-    base,-    fin,-    vec,-    tagged,-    inspection-testing >= 0.2.0.1 && <0.3+      base+    , fin+    , inspection-testing  >=0.2.0.1 && <0.5+    , tagged+    , vec -  if !impl(ghc >= 8.0)+  if !impl(ghc >=8.0)     buildable: False -  -- useful for development-  ghc-options:-    -- -dsuppress-idinfo-    -- -dsuppress-coercions-    -- -dsuppress-type-applications-    -- -dsuppress-module-prefixes-    -- -dsuppress-type-signatures-    -- -dsuppress-uniques- benchmark bench-  type:                exitcode-stdio-1.0-  main-is:             Bench.hs-  ghc-options:         -Wall -fprint-explicit-kinds-  hs-source-dirs:      bench-  default-language:    Haskell2010-  other-modules:-    DotProduct+  type:             exitcode-stdio-1.0+  main-is:          Bench.hs+  ghc-options:      -Wall -fprint-explicit-kinds+  hs-source-dirs:   bench+  default-language: Haskell2010+  other-modules:    DotProduct   build-depends:-    base,-    fin,-    vec,-    vector,-    criterion >= 1.4.0.0 && <1.5+      base+    , criterion  >=1.4.0.0 && <1.6+    , fin+    , vec+    , vector