vec 0.3 → 0.4
raw patch · 11 files changed
+659/−245 lines, 11 filesdep +indexed-traversabledep ~QuickCheckdep ~basedep ~fin
Dependencies added: indexed-traversable
Dependency ranges changed: QuickCheck, base, fin, semigroupoids, transformers
Files
- ChangeLog.md +12/−0
- bench/DotProduct.hs +1/−1
- src/Control/Lens/Yocto.hs +4/−3
- src/Data/Vec/DataFamily/SpineStrict.hs +242/−111
- src/Data/Vec/DataFamily/SpineStrict/Pigeonhole.hs +23/−20
- src/Data/Vec/Lazy.hs +143/−10
- src/Data/Vec/Lazy/Inline.hs +120/−77
- src/Data/Vec/Pull.hs +38/−10
- test/Inspection.hs +49/−0
- test/Inspection/DataFamily/SpineStrict/Pigeonhole.hs +1/−1
- vec.cabal +26/−12
ChangeLog.md view
@@ -1,5 +1,17 @@ # Revision history for vec +## 0.4++- Support `fin-0.2`+- Add `indexed-traversable` instances+- Explicitly mark all modules as Safe or Trustworthy.+- Add `Eq1`, `Ord1` and `Show1` instances+- Add `init`, `last` and `toNonEmpty`++## 0.3.0.1++- Fix `product`+ ## 0.3 - Split `lens` utilities into [`vec-lens`](https://hackage.haskell.org/package/vec-lens) package.
bench/DotProduct.hs view
@@ -25,5 +25,5 @@ pullDotProduct' :: N.SNatI n => P.Vec n Int -> P.Vec n Int -> Int pullDotProduct' xs ys = P.sum (P.zipWith (*) xs ys) -inlineDotProduct :: N.InlineInduction n => L.Vec n Int -> L.Vec n Int -> Int+inlineDotProduct :: N.SNatI n => L.Vec n Int -> L.Vec n Int -> Int inlineDotProduct xs ys = I.sum (I.zipWith (*) xs ys)
src/Control/Lens/Yocto.hs view
@@ -1,5 +1,6 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Trustworthy #-} -- | A small module defining the least you need to support -- van-Laarhoven lenses without depending on @lens@ or @microlens@ or ... --@@ -43,7 +44,7 @@ #endif #if MIN_VERSION_base(4,11,0)-import Data.Functor ((<&>))+import Data.Functor ((<&>)) #endif -------------------------------------------------------------------------------
src/Data/Vec/DataFamily/SpineStrict.hs view
@@ -1,8 +1,10 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}@@ -61,6 +63,7 @@ toPull, fromPull, toList,+ toNonEmpty, fromList, fromListPrefix, reifyList,@@ -70,7 +73,9 @@ cons, snoc, head,+ last, tail,+ init, -- * Reverse reverse, -- * Concatenation and splitting@@ -114,13 +119,14 @@ ) where import Prelude- (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..),- Num (..), Ord (..), Ordering (EQ), Show (..), ShowS, const, flip, id,- seq, showParen, showString, uncurry, ($), (&&), (.))+ (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..), Num (..),+ Ord (..), Ordering (EQ), Show (..), ShowS, const, flip, id, seq,+ showParen, showString, uncurry, ($), (&&), (.)) import Control.Applicative (Applicative (..), liftA2, (<$>)) import Control.DeepSeq (NFData (..)) import Data.Fin (Fin (..))+import Data.List.NonEmpty (NonEmpty (..)) import Data.Hashable (Hashable (..)) import Data.Monoid (Monoid (..)) import Data.Nat (Nat (..))@@ -131,6 +137,12 @@ import qualified Data.Traversable as I (Traversable (..)) import qualified Test.QuickCheck as QC +import qualified Data.Foldable.WithIndex as WI (FoldableWithIndex (..))+import qualified Data.Functor.WithIndex as WI (FunctorWithIndex (..))+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))++import Data.Functor.Classes (Eq1 (..), Ord1 (..), Show1 (..))+ #ifdef MIN_VERSION_adjunctions import qualified Data.Functor.Rep as I (Representable (..)) #endif@@ -155,7 +167,11 @@ -- $setup -- >>> :set -XScopedTypeVariables -XDataKinds -- >>> import Data.Proxy (Proxy (..))--- >>> import Prelude (Char, not, uncurry, error)+-- >>> import Control.Applicative ((<$>))+-- >>> import Prelude (Char, not, uncurry, error, Eq (..), Ord (..), Bool (..), Maybe (..), ($), id, (.), Int)+-- >>> import qualified Data.Type.Nat as N+-- >>> import Data.Fin (Fin (..))+-- >>> import Data.Nat (Nat (..)) ------------------------------------------------------------------------------- -- Type@@ -176,34 +192,34 @@ -- -- >>> '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+instance (Eq a, N.SNatI n) => Eq (Vec n a) where+ (==) = getEqual (N.induction start step) where+ start :: Equal a a 'Z start = Equal $ \_ _ -> True - step :: Equal m a -> Equal ('S m) a+ step :: Equal a a m -> Equal a a ('S m) 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 }+newtype Equal a b n = Equal { getEqual :: Vec n a -> Vec n b -> 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+instance (Ord a, N.SNatI n) => Ord (Vec n a) where+ compare = getCompare (N.induction start step) where+ start :: Compare a a 'Z start = Compare $ \_ _ -> EQ - step :: Compare m a -> Compare ('S m) a+ step :: Compare a a m -> Compare a a ('S m) 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 }+newtype Compare a b n = Compare { getCompare :: Vec n a -> Vec n b -> Ordering } -instance (Show a, N.InlineInduction n) => Show (Vec n a) where- showsPrec = getShowsPrec (N.inlineInduction1 start step) where+instance (Show a, N.SNatI n) => Show (Vec n a) where+ showsPrec = getShowsPrec (N.induction1 start step) where start :: ShowsPrec 'Z a start = ShowsPrec $ \_ _ -> showString "VNil" @@ -215,10 +231,10 @@ newtype ShowsPrec n a = ShowsPrec { getShowsPrec :: Int -> Vec n a -> ShowS } -instance N.InlineInduction n => Functor (Vec n) where+instance N.SNatI n => Functor (Vec n) where fmap = map -instance N.InlineInduction n => I.Foldable (Vec n) where+instance N.SNatI n => I.Foldable (Vec n) where foldMap = foldMap foldr = foldr@@ -232,34 +248,46 @@ #endif #ifdef MIN_VERSION_semigroupoids-instance (N.InlineInduction m, n ~ 'S m) => I.Foldable1 (Vec n) where+instance (N.SNatI m, n ~ 'S m) => I.Foldable1 (Vec n) where foldMap1 = foldMap1 -instance (N.InlineInduction m, n ~ 'S m) => I.Traversable1 (Vec n) where+instance (N.SNatI m, n ~ 'S m) => I.Traversable1 (Vec n) where traverse1 = traverse1 #endif -instance N.InlineInduction n => I.Traversable (Vec n) where+instance N.SNatI n => I.Traversable (Vec n) where traverse = traverse +-- | @since 0.4+instance N.SNatI n => WI.FunctorWithIndex (Fin n) (Vec n) where+ imap = imap -instance (NFData a, N.InlineInduction n) => NFData (Vec n a) where- rnf = getRnf (N.inlineInduction1 z s) where+-- | @since 0.4+instance N.SNatI n => WI.FoldableWithIndex (Fin n) (Vec n) where+ ifoldMap = ifoldMap+ ifoldr = ifoldr++-- | @since 0.4+instance N.SNatI n => WI.TraversableWithIndex (Fin n) (Vec n) where+ itraverse = itraverse++instance (NFData a, N.SNatI n) => NFData (Vec n a) where+ rnf = getRnf (N.induction1 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+instance (Hashable a, N.SNatI n) => Hashable (Vec n a) where+ hashWithSalt = getHashWithSalt (N.induction1 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 :::)+instance N.SNatI n => Applicative (Vec n) where+ pure x = N.induction1 VNil (x :::) (<*>) = zipWith ($) _ *> x = x x <* _ = x@@ -267,43 +295,110 @@ liftA2 = zipWith #endif -instance N.InlineInduction n => Monad (Vec n) where+instance N.SNatI n => Monad (Vec n) where return = pure (>>=) = bind _ >> x = x #ifdef MIN_VERSION_distributive-instance N.InlineInduction n => Distributive (Vec n) where+instance N.SNatI n => Distributive (Vec n) where distribute f = tabulate (\k -> fmap (! k) f) #ifdef MIN_VERSION_adjunctions-instance N.InlineInduction n => I.Representable (Vec n) where+instance N.SNatI n => I.Representable (Vec n) where type Rep (Vec n) = Fin n tabulate = tabulate index = (!) #endif #endif -instance (Semigroup a, N.InlineInduction n) => Semigroup (Vec n a) where+instance (Semigroup a, N.SNatI n) => Semigroup (Vec n a) where (<>) = zipWith (<>) -instance (Monoid a, N.InlineInduction n) => Monoid (Vec n a) where+instance (Monoid a, N.SNatI n) => Monoid (Vec n a) where mempty = pure mempty mappend = zipWith mappend #ifdef MIN_VERSION_semigroupoids-instance N.InlineInduction n => Apply (Vec n) where+instance N.SNatI n => Apply (Vec n) where (<.>) = zipWith ($) _ .> x = x x <. _ = x liftF2 = zipWith -instance N.InlineInduction n => I.Bind (Vec n) where+instance N.SNatI n => I.Bind (Vec n) where (>>-) = bind join = join #endif -------------------------------------------------------------------------------+-- Data.Functor.Classes+-------------------------------------------------------------------------------++#ifndef MIN_VERSION_transformers_compat+#define MIN_VERSION_transformers_compat(x,y,z) 0+#endif+++#if MIN_VERSION_base(4,9,0)+#define LIFTED_FUNCTOR_CLASSES 1+#else+#if MIN_VERSION_transformers(0,5,0)+#define LIFTED_FUNCTOR_CLASSES 1+#else+#if MIN_VERSION_transformers_compat(0,5,0) && !MIN_VERSION_transformers(0,4,0)+#define LIFTED_FUNCTOR_CLASSES 1+#endif+#endif+#endif++#if LIFTED_FUNCTOR_CLASSES++-- | @since 0.4+instance N.SNatI n => Eq1 (Vec n) where+ liftEq :: forall a b. (a -> b -> Bool) -> Vec n a -> Vec n b -> Bool+ liftEq eq = getEqual (N.induction start step) where+ start :: Equal a b 'Z+ start = Equal $ \_ _ -> True++ step :: Equal a b m -> Equal a b ('S m)+ step (Equal go) = Equal $ \(x ::: xs) (y ::: ys) ->+ eq x y && go xs ys++-- | @since 0.4+instance N.SNatI n => Ord1 (Vec n) where+ liftCompare :: forall a b. (a -> b -> Ordering) -> Vec n a -> Vec n b -> Ordering+ liftCompare cmp = getCompare (N.induction start step) where+ start :: Compare a b 'Z+ start = Compare $ \_ _ -> EQ++ step :: Compare a b m -> Compare a b ('S m)+ step (Compare go) = Compare $ \(x ::: xs) (y ::: ys) ->+ cmp x y <> go xs ys++-- | @since 0.4+instance N.SNatI n => Show1 (Vec n) where+ liftShowsPrec :: forall a. (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Vec n a -> ShowS+ liftShowsPrec sp _ = getShowsPrec (N.induction1 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)+ $ sp 6 x+ . showString " ::: "+ . go 5 xs+#else+-- | @since 0.4+instance N.SNatI n => Eq1 (Vec n) where eq1 = (==)++-- | @since 0.4+instance N.SNatI n => Ord1 (Vec n) where compare1 = compare++-- | @since 0.4+instance N.SNatI n => Show1 (Vec n) where showsPrec1 = showsPrec+#endif+------------------------------------------------------------------------------- -- Construction ------------------------------------------------------------------------------- @@ -324,8 +419,8 @@ ------------------------------------------------------------------------------- -- | 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+toPull :: forall n a. N.SNatI n => Vec n a -> P.Vec n a+toPull = getToPull (N.induction1 start step) where start :: ToPull 'Z a start = ToPull $ \_ -> P.Vec F.absurd @@ -337,8 +432,8 @@ 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+fromPull :: forall n a. N.SNatI n => P.Vec n a -> Vec n a+fromPull = getFromPull (N.induction1 start step) where start :: FromPull 'Z a start = FromPull $ const VNil @@ -351,8 +446,8 @@ -- -- >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil -- "foo"-toList :: forall n a. N.InlineInduction n => Vec n a -> [a]-toList = getToList (N.inlineInduction1 start step) where+toList :: forall n a. N.SNatI n => Vec n a -> [a]+toList = getToList (N.induction1 start step) where start :: ToList 'Z a start = ToList (const []) @@ -361,6 +456,15 @@ newtype ToList n a = ToList { getToList :: Vec n a -> [a] } +-- |+--+-- >>> toNonEmpty $ 1 ::: 2 ::: 3 ::: VNil+-- 1 :| [2,3]+--+-- @since 0.4+toNonEmpty :: forall n a. N.SNatI n => Vec ('S n) a -> NonEmpty a+toNonEmpty (x ::: xs) = x :| toList xs+ -- | Convert list @[a]@ to @'Vec' n a@. -- Returns 'Nothing' if lengths don't match exactly. --@@ -373,8 +477,8 @@ -- >>> fromList "xy" :: Maybe (Vec N.Nat3 Char) -- Nothing ---fromList :: N.InlineInduction n => [a] -> Maybe (Vec n a)-fromList = getFromList (N.inlineInduction1 start step) where+fromList :: N.SNatI n => [a] -> Maybe (Vec n a)+fromList = getFromList (N.induction1 start step) where start :: FromList 'Z a start = FromList $ \xs -> case xs of [] -> Just VNil@@ -399,8 +503,8 @@ -- >>> fromListPrefix "xy" :: Maybe (Vec N.Nat3 Char) -- Nothing ---fromListPrefix :: N.InlineInduction n => [a] -> Maybe (Vec n a)-fromListPrefix = getFromList (N.inlineInduction1 start step) where+fromListPrefix :: N.SNatI n => [a] -> Maybe (Vec n a)+fromListPrefix = getFromList (N.induction1 start step) where start :: FromList 'Z a start = FromList $ \_ -> Just VNil -- different than in fromList case @@ -413,7 +517,7 @@ -- -- >>> reifyList "foo" length -- 3-reifyList :: [a] -> (forall n. N.InlineInduction n => Vec n a -> r) -> r+reifyList :: [a] -> (forall n. N.SNatI n => Vec n a -> r) -> r reifyList [] f = f VNil reifyList (x : xs) f = reifyList xs $ \xs' -> f (x ::: xs') @@ -421,8 +525,8 @@ -- Indexing ------------------------------------------------------------------------------- -flipIndex :: N.InlineInduction n => Fin n -> Vec n a -> a-flipIndex = getIndex (N.inlineInduction1 start step) where+flipIndex :: N.SNatI n => Fin n -> Vec n a -> a+flipIndex = getIndex (N.induction1 start step) where start :: Index 'Z a start = Index F.absurd @@ -438,14 +542,14 @@ -- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ -- 'b' ---(!) :: N.InlineInduction n => Vec n a -> Fin n -> a+(!) :: N.SNatI n => Vec n a -> Fin n -> a (!) = flip flipIndex -- | Tabulating, inverse of '!'. -- -- >>> tabulate id :: Vec N.Nat3 (Fin N.Nat3) -- 0 ::: 1 ::: 2 ::: VNil-tabulate :: N.InlineInduction n => (Fin n -> a) -> Vec n a+tabulate :: N.SNatI n => (Fin n -> a) -> Vec n a tabulate = fromPull . P.tabulate -- | Cons an element in front of a 'Vec'.@@ -453,8 +557,8 @@ cons = (:::) -- | Add a single element at the end of a 'Vec'.-snoc :: forall n a. N.InlineInduction n => Vec n a -> a -> Vec ('S n) a-snoc xs x = getSnoc (N.inlineInduction1 start step) xs where+snoc :: forall n a. N.SNatI n => Vec n a -> a -> Vec ('S n) a+snoc xs x = getSnoc (N.induction1 start step) xs where start :: Snoc 'Z a start = Snoc $ \ys -> x ::: ys @@ -471,6 +575,33 @@ tail :: Vec ('S n) a -> Vec n a tail (_ ::: xs) = xs +-- | The last element of a 'Vec'.+--+-- @since 0.4+last :: forall n a. N.SNatI n => Vec ('S n) a -> a+last xs = getLast (N.induction1 start step) xs where+ start :: Last 'Z a+ start = Last $ \(x:::VNil) -> x+ + step :: Last m a -> Last ('S m) a+ step (Last rec) = Last $ \(_ ::: ys) -> rec ys+ ++newtype Last n a = Last { getLast :: Vec ('S n) a -> a }++-- | The elements before the 'last' of a 'Vec'.+--+-- @since 0.4+init :: forall n a. N.SNatI n => Vec ('S n) a -> Vec n a+init xs = getInit (N.induction1 start step) xs where+ start :: Init 'Z a+ start = Init (const VNil)+ + step :: Init m a -> Init ('S m) a+ step (Init rec) = Init $ \(y ::: ys) -> y ::: rec ys++newtype Init n a = Init { getInit :: Vec ('S n) a -> Vec n a}+ ------------------------------------------------------------------------------- -- Reverse -------------------------------------------------------------------------------@@ -482,12 +613,12 @@ -- -- @since 0.2.1 ---reverse :: forall n a. N.InlineInduction n => Vec n a -> Vec n a-reverse = getReverse (N.inlineInduction1 start step) where+reverse :: forall n a. N.SNatI n => Vec n a -> Vec n a+reverse = getReverse (N.induction1 start step) where start :: Reverse 'Z a start = Reverse $ \_ -> VNil - step :: N.InlineInduction m => Reverse m a -> Reverse ('S m) a+ step :: N.SNatI m => Reverse m a -> Reverse ('S m) a step (Reverse rec) = Reverse $ \(x ::: xs) -> snoc (rec xs) x newtype Reverse n a = Reverse { getReverse :: Vec n a -> Vec n a }@@ -503,8 +634,8 @@ -- >>> ('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+(++) :: forall n m a. N.SNatI n => Vec n a -> Vec m a -> Vec (N.Plus n m) a+as ++ ys = getAppend (N.induction1 start step) as where start :: Append m 'Z a start = Append $ \_ -> ys @@ -521,8 +652,8 @@ -- >>> 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+split :: N.SNatI n => Vec (N.Plus n m) a -> (Vec n a, Vec m a)+split = appSplit (N.induction1 start step) where start :: Split m 'Z a start = Split $ \xs -> (VNil, xs) @@ -537,8 +668,8 @@ -- >>> 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+concatMap :: forall a b n m. (N.SNatI m, N.SNatI n) => (a -> Vec m b) -> Vec n a -> Vec (N.Mult n m) b+concatMap f = getConcatMap $ N.induction1 start step where start :: ConcatMap m a 'Z b start = ConcatMap $ \_ -> VNil @@ -548,7 +679,7 @@ 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 :: (N.SNatI m, N.SNatI n) => Vec n (Vec m a) -> Vec (N.Mult n m) a concat = concatMap id -- | Inverse of 'concat'.@@ -560,12 +691,12 @@ -- >>> 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 :: (N.SNatI n, N.SNatI 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 :: forall m n a. N.SNatI 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@@ -579,8 +710,8 @@ -- | >>> 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+map :: forall a b n. N.SNatI n => (a -> b) -> Vec n a -> Vec n b+map f = getMap $ N.induction1 start step where start :: Map a 'Z b start = Map $ \_ -> VNil @@ -592,8 +723,8 @@ -- | >>> 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+imap :: N.SNatI n => (Fin n -> a -> b) -> Vec n a -> Vec n b+imap = getIMap $ N.induction1 start step where start :: IMap a 'Z b start = IMap $ \_ _ -> VNil @@ -603,8 +734,8 @@ 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+traverse :: forall n f a b. (Applicative f, N.SNatI n) => (a -> f b) -> Vec n a -> f (Vec n b)+traverse f = getTraverse $ N.induction1 start step where start :: Traverse f a 'Z b start = Traverse $ \_ -> pure VNil @@ -616,8 +747,8 @@ #ifdef MIN_VERSION_semigroupoids -- | 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+traverse1 :: forall n f a b. (Apply f, N.SNatI n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)+traverse1 f = getTraverse1 $ N.induction1 start step where start :: Traverse1 f a 'Z b start = Traverse1 $ \(x ::: _) -> (::: VNil) <$> f x @@ -628,8 +759,8 @@ #endif -- | 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+itraverse :: forall n f a b. (Applicative f, N.SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)+itraverse = getITraverse $ N.induction1 start step where start :: ITraverse f a 'Z b start = ITraverse $ \_ _ -> pure VNil @@ -640,8 +771,8 @@ 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+itraverse_ :: forall n f a b. (Applicative f, N.SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f ()+itraverse_ = getITraverse_ $ N.induction1 start step where start :: ITraverse_ f a 'Z b start = ITraverse_ $ \_ _ -> pure () @@ -655,15 +786,15 @@ ------------------------------------------------------------------------------- -- | 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) ->+foldMap :: (Monoid m, N.SNatI n) => (a -> m) -> Vec n a -> m+foldMap f = getFold $ N.induction1 (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+foldMap1 :: forall s a n. (Semigroup s, N.SNatI n) => (a -> s) -> Vec ('S n) a -> s+foldMap1 f = getFold1 $ N.induction1 start step where start :: Fold1 a 'Z s start = Fold1 $ \(x ::: _) -> f x @@ -673,8 +804,8 @@ 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+ifoldMap :: forall a n m. (Monoid m, N.SNatI n) => (Fin n -> a -> m) -> Vec n a -> m+ifoldMap = getIFoldMap $ N.induction1 start step where start :: IFoldMap a 'Z m start = IFoldMap $ \_ _ -> mempty @@ -684,8 +815,8 @@ 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+ifoldMap1 :: forall a n s. (Semigroup s, N.SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s+ifoldMap1 = getIFoldMap1 $ N.induction1 start step where start :: IFoldMap1 a 'Z s start = IFoldMap1 $ \f (x ::: _) -> f FZ x @@ -695,8 +826,8 @@ 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+foldr :: forall a b n. N.SNatI n => (a -> b -> b) -> b -> Vec n a -> b+foldr f z = getFold $ N.induction1 start step where start :: Fold a 'Z b start = Fold $ \_ -> z @@ -704,8 +835,8 @@ 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+ifoldr :: forall a b n. N.SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b+ifoldr = getIFoldr $ N.induction1 start step where start :: IFoldr a 'Z b start = IFoldr $ \_ z _ -> z @@ -715,10 +846,10 @@ 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 :: forall n a. N.SNatI n => Vec n a -> Int length _ = getLength l where l :: Length n- l = N.inlineInduction (Length 0) $ \(Length n) -> Length (1 + n)+ l = N.induction (Length 0) $ \(Length n) -> Length (1 + n) newtype Length (n :: Nat) = Length { getLength :: Int } @@ -733,8 +864,8 @@ ------------------------------------------------------------------------------- -- | Non-strict 'sum'.-sum :: (Num a, N.InlineInduction n) => Vec n a -> a-sum = getFold $ N.inlineInduction1 start step where+sum :: (Num a, N.SNatI n) => Vec n a -> a+sum = getFold $ N.induction1 start step where start :: Num a => Fold a 'Z a start = Fold $ \_ -> 0 @@ -742,13 +873,13 @@ 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+product :: (Num a, N.SNatI n) => Vec n a -> a+product = getFold $ N.induction1 start step where start :: Num a => Fold a 'Z a- start = Fold $ \_ -> 0+ start = Fold $ \_ -> 1 step :: Num a => Fold a m a -> Fold a ('S m) a- step (Fold f) = Fold $ \(x ::: xs) -> x + f xs+ step (Fold f) = Fold $ \(x ::: xs) -> x * f xs -------------------------------------------------------------------------------@@ -756,8 +887,8 @@ ------------------------------------------------------------------------------- -- | 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+zipWith :: forall a b c n. N.SNatI n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c+zipWith f = getZipWith $ N.induction start step where start :: ZipWith a b c 'Z start = ZipWith $ \_ _ -> VNil @@ -767,8 +898,8 @@ 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+izipWith :: N.SNatI n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c+izipWith = getIZipWith $ N.induction start step where start :: IZipWith a b c 'Z start = IZipWith $ \_ _ _ -> VNil @@ -783,16 +914,16 @@ -- 'x' ::: 'x' ::: 'x' ::: VNil -- -- @since 0.2.1-repeat :: N.InlineInduction n => x -> Vec n x-repeat x = N.inlineInduction1 VNil (x :::)+repeat :: N.SNatI n => x -> Vec n x+repeat x = N.induction1 VNil (x :::) ------------------------------------------------------------------------------- -- Monadic ------------------------------------------------------------------------------- -- | Monadic bind.-bind :: N.InlineInduction n => Vec n a -> (a -> Vec n b) -> Vec n b-bind = getBind $ N.inlineInduction1 start step where+bind :: N.SNatI n => Vec n a -> (a -> Vec n b) -> Vec n b+bind = getBind $ N.induction1 start step where start :: Bind a 'Z b start = Bind $ \_ _ -> VNil @@ -805,12 +936,12 @@ -- -- >>> 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+join :: N.SNatI n => Vec n (Vec n a) -> Vec n a+join = getJoin $ N.induction1 start step where start :: Join 'Z a start = Join $ \_ -> VNil - step :: N.InlineInduction m => Join m a -> Join ('S m) a+ step :: N.SNatI 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 }@@ -823,12 +954,12 @@ -- -- >>> 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+universe :: N.SNatI n => Vec n (Fin n)+universe = getUniverse (N.induction first step) where first :: Universe 'Z first = Universe VNil - step :: N.InlineInduction m => Universe m -> Universe ('S m)+ step :: N.SNatI m => Universe m -> Universe ('S m) step (Universe go) = Universe (FZ ::: map FS go) newtype Universe n = Universe { getUniverse :: Vec n (Fin n) }@@ -858,8 +989,8 @@ -- >>> head $ setHead 'x' $ ensureSpine v -- 'x' ---ensureSpine :: N.InlineInduction n => Vec n a -> Vec n a-ensureSpine = getEnsureSpine (N.inlineInduction1 first step) where+ensureSpine :: N.SNatI n => Vec n a -> Vec n a+ensureSpine = getEnsureSpine (N.induction1 first step) where first :: EnsureSpine 'Z a first = EnsureSpine $ \_ -> VNil
src/Data/Vec/DataFamily/SpineStrict/Pigeonhole.hs view
@@ -6,6 +6,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-}+{-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}@@ -36,9 +37,9 @@ import Data.Nat (Nat (..)) import Data.Proxy (Proxy (..)) import Data.Vec.DataFamily.SpineStrict (Vec (..), tabulate)-import GHC.Generics ((:*:) (..), M1 (..), Par1 (..), U1 (..))+import GHC.Generics (M1 (..), Par1 (..), U1 (..), (:*:) (..)) -import qualified Control.Lens.Yocto as Lens+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@@ -53,9 +54,14 @@ -- >>> :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@@ -92,10 +98,13 @@ instance Pigeonhole Identity -- -- | @'Proxy' x@ ~ @x ^ 0@-instance Pigeonhole Proxy+instance Pigeonhole Proxy where+ type PigeonholeSize Proxy = 'Z+ from _ = VNil+ to _ = Proxy -- | @'Product' f g x@ ~ @x ^ (size f + size g)@-instance (Pigeonhole f, Pigeonhole g, N.InlineInduction (PigeonholeSize f)) => Pigeonhole (Product f g) where+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 = f . V.split where f (a, b) = Pair (to a) (to b)@@ -118,7 +127,7 @@ -- gindex :: ( G.Generic i, F.GFrom i, G.Generic1 f, GFrom f- , F.GEnumSize i ~ GPigeonholeSize f, N.InlineInduction (GPigeonholeSize f)+ , F.GEnumSize i ~ GPigeonholeSize f, N.SNatI (GPigeonholeSize f) ) => f a -> i -> a gindex fa i = gfrom fa V.! F.gfrom i@@ -136,7 +145,7 @@ -- gtabulate :: ( G.Generic i, F.GTo i, G.Generic1 f, GTo f- , F.GEnumSize i ~ GPigeonholeSize f, N.InlineInduction (GPigeonholeSize f)+ , F.GEnumSize i ~ GPigeonholeSize f, N.SNatI (GPigeonholeSize f) ) => (i -> a) -> f a gtabulate idx = gto $ tabulate (idx . F.gto)@@ -150,7 +159,7 @@ -- Identity 'X' -- gix :: ( G.Generic i, F.GFrom i, G.Generic1 t, GTo t, GFrom t- , F.GEnumSize i ~ GPigeonholeSize t, N.InlineInduction (GPigeonholeSize t)+ , F.GEnumSize i ~ GPigeonholeSize t, N.SNatI (GPigeonholeSize t) , Functor f ) => i -> (a -> f a) -> t a -> f (t a)@@ -162,14 +171,8 @@ -- | Index lens. ----- >>> Lens.view (ix (FS FZ)) ('a' ::: 'b' ::: 'c' ::: VNil)--- 'b'------ >>> Lens.set (ix (FS FZ)) 'x' ('a' ::: 'b' ::: 'c' ::: VNil)--- 'a' ::: 'x' ::: 'c' ::: VNil----ix :: forall n f a. (N.InlineInduction n, Functor f) => Fin n -> Lens.LensLike' f (Vec n a) a-ix = getIxLens $ N.inlineInduction1 start step where+ix :: forall n f a. (N.SNatI n, Functor f) => Fin n -> YLens.LensLike' f (Vec n a) a+ix = getIxLens $ N.induction1 start step where start :: IxLens f 'Z a start = IxLens F.absurd @@ -178,14 +181,14 @@ FZ -> _head FS j -> _tail . l j -newtype IxLens f n a = IxLens { getIxLens :: Fin n -> Lens.LensLike' f (Vec n a) a }+newtype IxLens f n a = IxLens { getIxLens :: Fin n -> YLens.LensLike' f (Vec n a) a } -_head :: Lens.Lens' (Vec ('S n) a) a+_head :: YLens.Lens' (Vec ('S n) a) a _head f (x ::: xs) = (::: xs) <$> f x {-# INLINE _head #-} -- | Head lens. /Note:/ @lens@ 'Lens._head' is a 'Lens.Traversal''.-_tail :: Lens.Lens' (Vec ('S n) a) (Vec n a)+_tail :: YLens.Lens' (Vec ('S n) a) (Vec n a) _tail f (x ::: xs) = (x :::) <$> f xs {-# INLINE _tail #-} @@ -198,7 +201,7 @@ -- __Don't use__, rather use @DeriveTraversable@ gtraverse :: ( G.Generic1 t, GFrom t, GTo t- , N.InlineInduction (GPigeonholeSize t)+ , N.SNatI (GPigeonholeSize t) , Applicative f ) => (a -> f b) -> t a -> f (t b)@@ -216,7 +219,7 @@ gitraverse :: ( G.Generic i, F.GTo i , G.Generic1 t, GFrom t, GTo t- , F.GEnumSize i ~ GPigeonholeSize t, N.InlineInduction (GPigeonholeSize t)+ , F.GEnumSize i ~ GPigeonholeSize t, N.SNatI (GPigeonholeSize t) , Applicative f ) => (i -> a -> f b) -> t a -> f (t b)
src/Data/Vec/Lazy.hs view
@@ -7,6 +7,7 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-}@@ -22,6 +23,7 @@ toPull, fromPull, toList,+ toNonEmpty, fromList, fromListPrefix, reifyList,@@ -31,7 +33,9 @@ cons, snoc, head,+ last, tail,+ init, -- * Reverse reverse, -- * Concatenation and splitting@@ -40,6 +44,9 @@ concatMap, concat, chunks,+ -- * Take and drop+ take,+ drop, -- * Folds foldMap, foldMap1,@@ -76,14 +83,15 @@ ) where import Prelude- (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..),- Num (..), Ord (..), Show (..), id, seq, uncurry, showParen, showString, ($), (.))+ (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..), Num (..),+ Ord (..), Show (..), id, seq, showParen, showString, uncurry, ($), (.), (&&), Ordering (..)) import Control.Applicative (Applicative (..), (<$>)) import Control.DeepSeq (NFData (..)) import Control.Lens.Yocto ((<&>)) import Data.Fin (Fin (..)) import Data.Hashable (Hashable (..))+import Data.List.NonEmpty (NonEmpty (..)) import Data.Monoid (Monoid (..)) import Data.Nat (Nat (..)) import Data.Semigroup (Semigroup (..))@@ -94,6 +102,12 @@ import qualified Data.Traversable as I (Traversable (..)) import qualified Test.QuickCheck as QC +import qualified Data.Foldable.WithIndex as WI (FoldableWithIndex (..))+import qualified Data.Functor.WithIndex as WI (FunctorWithIndex (..))+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))++import Data.Functor.Classes (Eq1 (..), Ord1 (..), Show1 (..))+ #ifdef MIN_VERSION_adjunctions import qualified Data.Functor.Rep as I (Representable (..)) #endif@@ -115,10 +129,16 @@ import qualified Data.Type.Nat as N import qualified Data.Vec.Pull as P +import qualified Data.Type.Nat.LE as LE.ZS+import qualified Data.Type.Nat.LE.ReflStep as LE.RS++ -- $setup -- >>> :set -XScopedTypeVariables -- >>> import Data.Proxy (Proxy (..))--- >>> import Prelude (Char, not, uncurry)+-- >>> import Prelude (Char, not, uncurry, Bool (..), Maybe (..), ($), (<$>), id, (.), Int)+-- >>> import qualified Data.Type.Nat as N+-- >>> import Data.Fin (Fin (..)) ------------------------------------------------------------------------------- -- Type@@ -165,6 +185,19 @@ instance I.Traversable (Vec n) where traverse = traverse +-- | @since 0.4+instance WI.FunctorWithIndex (Fin n) (Vec n) where+ imap = imap++-- | @since 0.4+instance WI.FoldableWithIndex (Fin n) (Vec n) where+ ifoldMap = ifoldMap+ ifoldr = ifoldr++-- | @since 0.4+instance WI.TraversableWithIndex (Fin n) (Vec n) where+ itraverse = itraverse+ #ifdef MIN_VERSION_semigroupoids instance n ~ 'S m => I.Foldable1 (Vec n) where foldMap1 = foldMap1@@ -229,6 +262,55 @@ #endif -------------------------------------------------------------------------------+-- Data.Functor.Classes+-------------------------------------------------------------------------------++#ifndef MIN_VERSION_transformers_compat+#define MIN_VERSION_transformers_compat(x,y,z) 0+#endif++#if MIN_VERSION_base(4,9,0)+#define LIFTED_FUNCTOR_CLASSES 1+#else+#if MIN_VERSION_transformers(0,5,0)+#define LIFTED_FUNCTOR_CLASSES 1+#else+#if MIN_VERSION_transformers_compat(0,5,0) && !MIN_VERSION_transformers(0,4,0)+#define LIFTED_FUNCTOR_CLASSES 1+#endif+#endif+#endif++#if LIFTED_FUNCTOR_CLASSES+-- | @since 0.4+instance Eq1 (Vec n) where+ liftEq _eq VNil VNil = True+ liftEq eq (x ::: xs) (y ::: ys) = eq x y && liftEq eq xs ys++-- | @since 0.4+instance Ord1 (Vec n) where+ liftCompare _cmp VNil VNil = EQ+ liftCompare cmp (x ::: xs) (y ::: ys) = cmp x y <> liftCompare cmp xs ys++-- | @since 0.4+instance Show1 (Vec n) where+ liftShowsPrec _ _ _ VNil = showString "VNil"+ liftShowsPrec sp sl d (x ::: xs) = showParen (d > 5)+ $ sp 6 x+ . showString " ::: "+ . liftShowsPrec sp sl 5 xs+#else+-- | @since 0.4+instance Eq1 (Vec n) where eq1 = (==)++-- | @since 0.4+instance Ord1 (Vec n) where compare1 = compare++-- | @since 0.4+instance Show1 (Vec n) where showsPrec1 = showsPrec+#endif++------------------------------------------------------------------------------- -- Construction ------------------------------------------------------------------------------- @@ -244,7 +326,7 @@ singleton :: a -> Vec ('S 'Z) a singleton x = x ::: VNil --- | /O(n)/. Recover 'N.InlineInduction' (and 'N.SNatI') dictionary from a 'Vec' value.+-- | /O(n)/. Recover 'N.SNatI' (and 'N.SNatI') dictionary from a 'Vec' value. -- -- Example: 'N.reflect' is constrained with @'N.SNatI' n@, but if we have a -- @'Vec' n a@, we can recover that dictionary:@@ -252,11 +334,11 @@ -- >>> let f :: forall n a. Vec n a -> N.Nat; f v = withDict v (N.reflect (Proxy :: Proxy n)) in f (True ::: VNil) -- 1 ----- /Note:/ using 'N.InlineInduction' will be suboptimal, as if GHC has no+-- /Note:/ using 'N.SNatI' will be suboptimal, as if GHC has no -- opportunity to optimise the code, the recusion won't be unfold. -- How bad such code will perform? I don't know, we'll need benchmarks. ---withDict :: Vec n a -> (N.InlineInduction n => r) -> r+withDict :: Vec n a -> (N.SNatI n => r) -> r withDict VNil r = r withDict (_ ::: xs) r = withDict xs r @@ -285,6 +367,15 @@ toList VNil = [] toList (x ::: xs) = x : toList xs +-- | +--+-- >>> toNonEmpty $ 1 ::: 2 ::: 3 ::: VNil+-- 1 :| [2,3]+--+-- @since 0.4+toNonEmpty :: Vec ('S n) a -> NonEmpty a+toNonEmpty (x ::: xs) = x :| toList xs+ -- | Convert list @[a]@ to @'Vec' n a@. -- Returns 'Nothing' if lengths don't match exactly. --@@ -337,7 +428,7 @@ -- -- >>> reifyList "foo" length -- 3-reifyList :: [a] -> (forall n. N.InlineInduction n => Vec n a -> r) -> r+reifyList :: [a] -> (forall n. N.SNatI n => Vec n a -> r) -> r reifyList [] f = f VNil reifyList (x : xs) f = reifyList xs $ \xs' -> f (x ::: xs') @@ -378,10 +469,24 @@ head :: Vec ('S n) a -> a head (x ::: _) = x +-- | The last element of a 'Vec'.+--+-- @since 0.4+last :: Vec ('S n) a -> a+last (x ::: VNil) = x+last (_ ::: xs@(_ ::: _)) = last xs+ -- | The elements after the 'head' of a 'Vec'. tail :: Vec ('S n) a -> Vec n a tail (_ ::: xs) = xs +-- | The elements before the 'last' of a 'Vec'.+--+-- @since 0.4+init :: Vec ('S n) a -> Vec n a+init (_ ::: VNil) = VNil+init (x ::: xs@(_ ::: _)) = x ::: init xs+ ------------------------------------------------------------------------------- -- Reverse -------------------------------------------------------------------------------@@ -466,6 +571,34 @@ newtype Chunks m n a = Chunks { getChunks :: Vec (N.Mult n m) a -> Vec n (Vec m a) } -------------------------------------------------------------------------------+-- take and drop+-------------------------------------------------------------------------------++-- |+--+-- >>> let xs = 'a' ::: 'b' ::: 'c' ::: 'd' ::: 'e' ::: VNil+-- >>> take xs :: Vec N.Nat3 Char+-- 'a' ::: 'b' ::: 'c' ::: VNil+--+take :: forall n m a. (LE.ZS.LE n m) => Vec m a -> Vec n a+take = go LE.ZS.leProof where+ go :: LE.ZS.LEProof n' m' -> Vec m' a -> Vec n' a+ go LE.ZS.LEZero _ = VNil+ go (LE.ZS.LESucc p) (x ::: xs) = x ::: go p xs++-- |+--+-- >>> let xs = 'a' ::: 'b' ::: 'c' ::: 'd' ::: 'e' ::: VNil+-- >>> drop xs :: Vec N.Nat3 Char+-- 'c' ::: 'd' ::: 'e' ::: VNil+--+drop :: forall n m a. (LE.ZS.LE n m, N.SNatI m) => Vec m a -> Vec n a+drop = go (LE.RS.fromZeroSucc LE.ZS.leProof) where+ go :: LE.RS.LEProof n' m' -> Vec m' a -> Vec n' a+ go LE.RS.LERefl xs = xs+ go (LE.RS.LEStep p) (_ ::: xs) = go p xs++------------------------------------------------------------------------------- -- Mapping ------------------------------------------------------------------------------- @@ -576,7 +709,7 @@ -- | Non-strict 'product'. product :: Num a => Vec n a -> a product VNil = 1-product (x ::: xs) = x * sum xs+product (x ::: xs) = x * product xs ------------------------------------------------------------------------------- -- Zipping@@ -663,8 +796,8 @@ -- there's no strict need for it. -- class VecEach s t a b | s -> a, t -> b, s b -> t, t a -> s where- mapWithVec :: (forall n. N.InlineInduction n => Vec n a -> Vec n b) -> s -> t- traverseWithVec :: Applicative f => (forall n. N.InlineInduction n => Vec n a -> f (Vec n b)) -> s -> f t+ mapWithVec :: (forall n. N.SNatI n => Vec n a -> Vec n b) -> s -> t+ traverseWithVec :: Applicative f => (forall n. N.SNatI n => Vec n a -> f (Vec n b)) -> s -> f t instance (a ~ a', b ~ b') => VecEach (a, a') (b, b') a b where mapWithVec f ~(x, y) = case f (x ::: y ::: VNil) of
src/Data/Vec/Lazy/Inline.hs view
@@ -4,10 +4,11 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}--- | A variant of "Data.Vec.Lazy" with functions written using 'N.InlineInduction'.+-- | A variant of "Data.Vec.Lazy" with functions written using 'N.SNatI'. -- The hypothesis is that these (goursive) functions could be fully unrolled, -- if the 'Vec' size @n@ is known at compile time. --@@ -22,6 +23,7 @@ toPull, fromPull, toList,+ toNonEmpty, fromList, fromListPrefix, reifyList,@@ -31,7 +33,9 @@ cons, snoc, head,+ last, tail,+ init, -- * Concatenation and splitting (++), split,@@ -78,6 +82,7 @@ import Control.Applicative (Applicative (pure, (*>)), liftA2, (<$>)) import Data.Fin (Fin (..))+import Data.List.NonEmpty (NonEmpty (..)) import Data.Monoid (Monoid (..)) import Data.Nat (Nat (..)) import Data.Semigroup (Semigroup (..))@@ -88,7 +93,7 @@ --- Instances #ifdef MIN_VERSION_semigroupoids-import Data.Functor.Apply (Apply, liftF2)+import Data.Functor.Apply (Apply, liftF2) #endif -- vec siblings@@ -99,15 +104,17 @@ -- $setup -- >>> :set -XScopedTypeVariables -- >>> import Data.Proxy (Proxy (..))--- >>> import Prelude (Char, not, uncurry, Bool (..))+-- >>> import Prelude (Char, not, uncurry, Bool (..), Maybe (..), ($), (<$>), id, (.), Int)+-- >>> import qualified Data.Type.Nat as N+-- >>> import Data.Fin (Fin (..)) ------------------------------------------------------------------------------- -- 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+toPull :: forall n a. N.SNatI n => Vec n a -> P.Vec n a+toPull = getToPull (N.induction1 start step) where start :: ToPull 'Z a start = ToPull $ \_ -> P.Vec F.absurd @@ -119,8 +126,8 @@ 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+fromPull :: forall n a. N.SNatI n => P.Vec n a -> Vec n a+fromPull = getFromPull (N.induction1 start step) where start :: FromPull 'Z a start = FromPull $ const VNil @@ -133,8 +140,8 @@ -- -- >>> toList $ 'f' ::: 'o' ::: 'o' ::: VNil -- "foo"-toList :: forall n a. N.InlineInduction n => Vec n a -> [a]-toList = getToList (N.inlineInduction1 start step) where+toList :: forall n a. N.SNatI n => Vec n a -> [a]+toList = getToList (N.induction1 start step) where start :: ToList 'Z a start = ToList (const []) @@ -143,6 +150,15 @@ newtype ToList n a = ToList { getToList :: Vec n a -> [a] } +-- |+--+-- >>> toNonEmpty $ 1 ::: 2 ::: 3 ::: VNil+-- 1 :| [2,3]+--+-- @since 0.4+toNonEmpty :: forall n a. N.SNatI n => Vec ('S n) a -> NonEmpty a+toNonEmpty (x ::: xs) = x :| toList xs+ -- | Convert list @[a]@ to @'Vec' n a@. -- Returns 'Nothing' if lengths don't match exactly. --@@ -155,8 +171,8 @@ -- >>> fromList "xy" :: Maybe (Vec N.Nat3 Char) -- Nothing ---fromList :: N.InlineInduction n => [a] -> Maybe (Vec n a)-fromList = getFromList (N.inlineInduction1 start step) where+fromList :: N.SNatI n => [a] -> Maybe (Vec n a)+fromList = getFromList (N.induction1 start step) where start :: FromList 'Z a start = FromList $ \xs -> case xs of [] -> Just VNil@@ -181,8 +197,8 @@ -- >>> fromListPrefix "xy" :: Maybe (Vec N.Nat3 Char) -- Nothing ---fromListPrefix :: N.InlineInduction n => [a] -> Maybe (Vec n a)-fromListPrefix = getFromList (N.inlineInduction1 start step) where+fromListPrefix :: N.SNatI n => [a] -> Maybe (Vec n a)+fromListPrefix = getFromList (N.induction1 start step) where start :: FromList 'Z a start = FromList $ \_ -> Just VNil -- different than in fromList case @@ -195,8 +211,8 @@ -- Indexing ------------------------------------------------------------------------------- -flipIndex :: N.InlineInduction n => Fin n -> Vec n a -> a-flipIndex = getIndex (N.inlineInduction1 start step) where+flipIndex :: N.SNatI n => Fin n -> Vec n a -> a+flipIndex = getIndex (N.induction1 start step) where start :: Index 'Z a start = Index F.absurd @@ -212,7 +228,7 @@ -- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ! FS FZ -- 'b' ---(!) :: N.InlineInduction n => Vec n a -> Fin n -> a+(!) :: N.SNatI n => Vec n a -> Fin n -> a (!) = flip flipIndex -- | Tabulating, inverse of '!'.@@ -220,15 +236,15 @@ -- >>> tabulate id :: Vec N.Nat3 (Fin N.Nat3) -- 0 ::: 1 ::: 2 ::: VNil ---tabulate :: N.InlineInduction n => (Fin n -> a) -> Vec n a+tabulate :: N.SNatI n => (Fin n -> a) -> Vec n a tabulate = fromPull . P.tabulate -- | Add a single element at the end of a 'Vec'. -- -- @since 0.2.1 ---snoc :: forall n a. N.InlineInduction n => Vec n a -> a -> Vec ('S n) a-snoc xs x = getSnoc (N.inlineInduction1 start step) xs where+snoc :: forall n a. N.SNatI n => Vec n a -> a -> Vec ('S n) a+snoc xs x = getSnoc (N.induction1 start step) xs where start :: Snoc 'Z a start = Snoc $ \ys -> x ::: ys @@ -237,6 +253,33 @@ newtype Snoc n a = Snoc { getSnoc :: Vec n a -> Vec ('S n) a } +-- | The last element of a 'Vec'.+--+-- @since 0.4+last :: forall n a. N.SNatI n => Vec ('S n) a -> a+last xs = getLast (N.induction1 start step) xs where+ start :: Last 'Z a+ start = Last $ \(x:::VNil) -> x+ + step :: Last m a -> Last ('S m) a+ step (Last rec) = Last $ \(_ ::: ys) -> rec ys+ ++newtype Last n a = Last { getLast :: Vec ('S n) a -> a }++-- | The elements before the 'last' of a 'Vec'.+--+-- @since 0.4+init :: forall n a. N.SNatI n => Vec ('S n) a -> Vec n a+init xs = getInit (N.induction1 start step) xs where+ start :: Init 'Z a+ start = Init (const VNil)+ + step :: Init m a -> Init ('S m) a+ step (Init rec) = Init $ \(y ::: ys) -> y ::: rec ys++newtype Init n a = Init { getInit :: Vec ('S n) a -> Vec n a}+ ------------------------------------------------------------------------------- -- Reverse -------------------------------------------------------------------------------@@ -248,12 +291,12 @@ -- -- @since 0.2.1 ---reverse :: forall n a. N.InlineInduction n => Vec n a -> Vec n a-reverse = getReverse (N.inlineInduction1 start step) where+reverse :: forall n a. N.SNatI n => Vec n a -> Vec n a+reverse = getReverse (N.induction1 start step) where start :: Reverse 'Z a start = Reverse $ \_ -> VNil - step :: N.InlineInduction m => Reverse m a -> Reverse ('S m) a+ step :: N.SNatI m => Reverse m a -> Reverse ('S m) a step (Reverse rec) = Reverse $ \(x ::: xs) -> snoc (rec xs) x newtype Reverse n a = Reverse { getReverse :: Vec n a -> Vec n a }@@ -269,8 +312,8 @@ -- >>> ('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+(++) :: forall n m a. N.SNatI n => Vec n a -> Vec m a -> Vec (N.Plus n m) a+as ++ ys = getAppend (N.induction1 start step) as where start :: Append m 'Z a start = Append $ \_ -> ys @@ -287,8 +330,8 @@ -- >>> 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+split :: N.SNatI n => Vec (N.Plus n m) a -> (Vec n a, Vec m a)+split = appSplit (N.induction1 start step) where start :: Split m 'Z a start = Split $ \xs -> (VNil, xs) @@ -302,8 +345,8 @@ -- >>> 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+concatMap :: forall a b n m. (N.SNatI m, N.SNatI n) => (a -> Vec m b) -> Vec n a -> Vec (N.Mult n m) b+concatMap f = getConcatMap $ N.induction1 start step where start :: ConcatMap m a 'Z b start = ConcatMap $ \_ -> VNil @@ -313,7 +356,7 @@ 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 :: (N.SNatI m, N.SNatI n) => Vec n (Vec m a) -> Vec (N.Mult n m) a concat = concatMap id -- | Inverse of 'concat'.@@ -325,12 +368,12 @@ -- >>> 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 :: (N.SNatI n, N.SNatI 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 :: forall m n a. N.SNatI 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@@ -344,8 +387,8 @@ -- | >>> 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+map :: forall a b n. N.SNatI n => (a -> b) -> Vec n a -> Vec n b+map f = getMap $ N.induction1 start step where start :: Map a 'Z b start = Map $ \_ -> VNil @@ -357,8 +400,8 @@ -- | >>> 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+imap :: N.SNatI n => (Fin n -> a -> b) -> Vec n a -> Vec n b+imap = getIMap $ N.induction1 start step where start :: IMap a 'Z b start = IMap $ \_ _ -> VNil @@ -368,8 +411,8 @@ 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+traverse :: forall n f a b. (Applicative f, N.SNatI n) => (a -> f b) -> Vec n a -> f (Vec n b)+traverse f = getTraverse $ N.induction1 start step where start :: Traverse f a 'Z b start = Traverse $ \_ -> pure VNil @@ -380,8 +423,8 @@ #ifdef MIN_VERSION_semigroupoids -- | 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+traverse1 :: forall n f a b. (Apply f, N.SNatI n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)+traverse1 f = getTraverse1 $ N.induction1 start step where start :: Traverse1 f a 'Z b start = Traverse1 $ \(x ::: _) -> (::: VNil) <$> f x @@ -392,8 +435,8 @@ #endif -- | 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+itraverse :: forall n f a b. (Applicative f, N.SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)+itraverse = getITraverse $ N.induction1 start step where start :: ITraverse f a 'Z b start = ITraverse $ \_ _ -> pure VNil @@ -403,8 +446,8 @@ 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+itraverse_ :: forall n f a b. (Applicative f, N.SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f ()+itraverse_ = getITraverse_ $ N.induction1 start step where start :: ITraverse_ f a 'Z b start = ITraverse_ $ \_ _ -> pure () @@ -418,15 +461,15 @@ ------------------------------------------------------------------------------- -- | 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) ->+foldMap :: (Monoid m, N.SNatI n) => (a -> m) -> Vec n a -> m+foldMap f = getFold $ N.induction1 (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+foldMap1 :: forall s a n. (Semigroup s, N.SNatI n) => (a -> s) -> Vec ('S n) a -> s+foldMap1 f = getFold1 $ N.induction1 start step where start :: Fold1 a 'Z s start = Fold1 $ \(x ::: _) -> f x @@ -436,8 +479,8 @@ 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+ifoldMap :: forall a n m. (Monoid m, N.SNatI n) => (Fin n -> a -> m) -> Vec n a -> m+ifoldMap = getIFoldMap $ N.induction1 start step where start :: IFoldMap a 'Z m start = IFoldMap $ \_ _ -> mempty @@ -447,8 +490,8 @@ 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+ifoldMap1 :: forall a n s. (Semigroup s, N.SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s+ifoldMap1 = getIFoldMap1 $ N.induction1 start step where start :: IFoldMap1 a 'Z s start = IFoldMap1 $ \f (x ::: _) -> f FZ x @@ -458,8 +501,8 @@ 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+foldr :: forall a b n. N.SNatI n => (a -> b -> b) -> b -> Vec n a -> b+foldr f z = getFold $ N.induction1 start step where start :: Fold a 'Z b start = Fold $ \_ -> z @@ -467,8 +510,8 @@ 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+ifoldr :: forall a b n. N.SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b+ifoldr = getIFoldr $ N.induction1 start step where start :: IFoldr a 'Z b start = IFoldr $ \_ z _ -> z @@ -478,10 +521,10 @@ 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 :: forall n a. N.SNatI n => Vec n a -> Int length _ = getLength l where l :: Length n- l = N.inlineInduction (Length 0) $ \(Length n) -> Length (1 + n)+ l = N.induction (Length 0) $ \(Length n) -> Length (1 + n) newtype Length (n :: Nat) = Length { getLength :: Int } @@ -490,8 +533,8 @@ ------------------------------------------------------------------------------- -- | Non-strict 'sum'.-sum :: (Num a, N.InlineInduction n) => Vec n a -> a-sum = getFold $ N.inlineInduction1 start step where+sum :: (Num a, N.SNatI n) => Vec n a -> a+sum = getFold $ N.induction1 start step where start :: Num a => Fold a 'Z a start = Fold $ \_ -> 0 @@ -499,21 +542,21 @@ 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+product :: (Num a, N.SNatI n) => Vec n a -> a+product = getFold $ N.induction1 start step where start :: Num a => Fold a 'Z a- start = Fold $ \_ -> 0+ start = Fold $ \_ -> 1 step :: Num a => Fold a m a -> Fold a ('S m) a- step (Fold f) = Fold $ \(x ::: xs) -> x + f xs+ 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+zipWith :: forall a b c n. N.SNatI n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c+zipWith f = getZipWith $ N.induction start step where start :: ZipWith a b c 'Z start = ZipWith $ \_ _ -> VNil @@ -523,8 +566,8 @@ 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+izipWith :: N.SNatI n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c+izipWith = getIZipWith $ N.induction start step where start :: IZipWith a b c 'Z start = IZipWith $ \_ _ _ -> VNil @@ -539,16 +582,16 @@ -- 'x' ::: 'x' ::: 'x' ::: VNil -- -- @since 0.2.1-repeat :: N.InlineInduction n => x -> Vec n x-repeat x = N.inlineInduction1 VNil (x :::)+repeat :: N.SNatI n => x -> Vec n x+repeat x = N.induction1 VNil (x :::) ------------------------------------------------------------------------------- -- Monadic ------------------------------------------------------------------------------- -- | Monadic bind.-bind :: N.InlineInduction n => Vec n a -> (a -> Vec n b) -> Vec n b-bind = getBind $ N.inlineInduction1 start step where+bind :: N.SNatI n => Vec n a -> (a -> Vec n b) -> Vec n b+bind = getBind $ N.induction1 start step where start :: Bind a 'Z b start = Bind $ \_ _ -> VNil @@ -561,12 +604,12 @@ -- -- >>> 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+join :: N.SNatI n => Vec n (Vec n a) -> Vec n a+join = getJoin $ N.induction1 start step where start :: Join 'Z a start = Join $ \_ -> VNil - step :: N.InlineInduction m => Join m a -> Join ('S m) a+ step :: N.SNatI 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 }@@ -579,12 +622,12 @@ -- -- >>> 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+universe :: N.SNatI n => Vec n (Fin n)+universe = getUniverse (N.induction first step) where first :: Universe 'Z first = Universe VNil - step :: N.InlineInduction m => Universe m -> Universe ('S m)+ step :: N.SNatI m => Universe m -> Universe ('S m) step (Universe go) = Universe (FZ ::: map FS go) newtype Universe n = Universe { getUniverse :: Vec n (Fin n) }
src/Data/Vec/Pull.hs view
@@ -4,6 +4,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}@@ -19,6 +20,7 @@ singleton, -- * Conversions toList,+ toNonEmpty, fromList, fromListPrefix, reifyList,@@ -28,7 +30,9 @@ cons, snoc, head,+ last, tail,+ init, -- * Reverse reverse, -- * Folds@@ -59,8 +63,8 @@ ) where import Prelude- (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..),- Num (..), all, const, id, ($), (.))+ (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..), Num (..),+ all, const, id, maxBound, maybe, ($), (.)) import Control.Applicative (Applicative (..), (<$>)) import Data.Fin (Fin (..))@@ -74,12 +78,15 @@ --- Instances import qualified Data.Foldable as I (Foldable (..)) +import qualified Data.Foldable.WithIndex as WI (FoldableWithIndex (..))+import qualified Data.Functor.WithIndex as WI (FunctorWithIndex (..))+ #ifdef MIN_VERSION_adjunctions import qualified Data.Functor.Rep as I (Representable (..)) #endif #ifdef MIN_VERSION_distributive-import Data.Distributive (Distributive (..))+import Data.Distributive (Distributive (..)) #endif #ifdef MIN_VERSION_semigroupoids@@ -96,8 +103,10 @@ -- $setup -- >>> :set -XScopedTypeVariables -- >>> import Data.Proxy (Proxy (..))--- >>> import Prelude (Char, Bool (..), not)+-- >>> import Prelude (Char, Bool (..), not, Maybe (..), (<$>), ($)) -- >>> import qualified Data.Vec.Lazy as L+-- >>> import qualified Data.Type.Nat as N+-- >>> import Data.Fin (Fin (..)) ------------------------------------------------------------------------------- -- Type@@ -119,6 +128,15 @@ instance N.SNatI n => I.Foldable (Vec n) where foldMap = foldMap +-- | @since 0.4+instance WI.FunctorWithIndex (Fin n) (Vec n) where+ imap = imap++-- | @since 0.4+instance N.SNatI n => WI.FoldableWithIndex (Fin n) (Vec n) where+ ifoldMap = ifoldMap+ ifoldr = ifoldr+ #ifdef MIN_VERSION_semigroupoids instance (N.SNatI m, n ~ 'S m) => I.Foldable1 (Vec n) where foldMap1 = foldMap1@@ -193,6 +211,10 @@ toList :: N.SNatI n => Vec n a -> [a] toList v = unVec v <$> F.universe +-- | Convert 'Vec' to NonEmpty.+toNonEmpty :: N.SNatI n => Vec ('S n) a -> NonEmpty a+toNonEmpty v = head v :| toList (tail v)+ -- | Convert list @[a]@ to @'Vec' n a@. -- Returns 'Nothing' if lengths don't match exactly. --@@ -245,7 +267,7 @@ -- -- >>> reifyList "foo" length -- 3-reifyList :: [a] -> (forall n. N.InlineInduction n => Vec n a -> r) -> r+reifyList :: [a] -> (forall n. N.SNatI n => Vec n a -> r) -> r reifyList [] f = f empty reifyList (x : xs) f = reifyList xs $ \xs' -> f (cons x xs') @@ -270,19 +292,25 @@ -- | Add a single element at the end of a 'Vec'. -- -- @since 0.2.1-snoc :: forall a n. N.InlineInduction n => Vec n a -> a -> Vec ('S n) a-snoc (Vec xs) x = Vec $ \i -> case F.isMax i of- Nothing -> x- Just i' -> xs i'+snoc :: forall a n. N.SNatI n => Vec n a -> a -> Vec ('S n) a+snoc (Vec xs) x = Vec $ \i -> maybe x xs (F.isMax i) -- | The first element of a 'Vec'. head :: Vec ('S n) a -> a head (Vec v) = v FZ +-- | The last element of a 'Vec'.+last :: forall n a. N.SNatI n => Vec ('S n) a -> a+last (Vec v) = v maxBound + -- | The elements after the 'head' of a 'Vec'. tail :: Vec ('S n) a -> Vec n a tail (Vec v) = Vec (v . FS) +-- | The elements before the 'last' of a 'Vec'.+init :: forall n a. N.SNatI n => Vec ('S n) a -> Vec n a+init (Vec v) = Vec (v . F.weakenLeft1)+ ------------------------------------------------------------------------------- -- Reverse -------------------------------------------------------------------------------@@ -291,7 +319,7 @@ -- -- @since 0.2.1 ---reverse :: forall n a. N.InlineInduction n => Vec n a -> Vec n a+reverse :: forall n a. N.SNatI n => Vec n a -> Vec n a reverse (Vec v) = Vec (v . F.mirror) -------------------------------------------------------------------------------
test/Inspection.hs view
@@ -6,6 +6,7 @@ import Prelude hiding (zipWith) import Data.Fin (Fin (..))+import Data.List.NonEmpty (NonEmpty (..)) import Data.Vec.Lazy (Vec (..)) import Test.Inspection @@ -119,3 +120,51 @@ inspect $ 'lhsReverse === 'rhsReverse inspect $ 'lhsReverse' =/= 'rhsReverse++-------------------------------------------------------------------------------+-- last+-------------------------------------------------------------------------------++lhsLast :: Char+lhsLast = I.last $ 'a' ::: 'b' ::: 'c' ::: VNil++lhsLast' :: Char+lhsLast' = L.last $ 'a' ::: 'b' ::: 'c' :::VNil++rhsLast :: Char +rhsLast = 'c'++inspect $ 'lhsLast === 'rhsLast+inspect $ 'lhsLast' =/= 'rhsLast++-------------------------------------------------------------------------------+-- init+-------------------------------------------------------------------------------++lhsInit :: Vec N.Nat2 Char+lhsInit = I.init $ 'a' ::: 'b' ::: 'c' ::: VNil++lhsInit' :: Vec N.Nat2 Char+lhsInit' = L.init $ 'a' ::: 'b' ::: 'c' ::: VNil++rhsInit :: Vec N.Nat2 Char+rhsInit = 'a' ::: 'b' ::: VNil++inspect $ 'lhsInit === 'rhsInit+inspect $ 'lhsInit' =/= 'rhsInit++-------------------------------------------------------------------------------+-- toNonEmpty+-------------------------------------------------------------------------------++lhsToNonEmpty :: NonEmpty Char+lhsToNonEmpty = I.toNonEmpty $ 'a' ::: 'b' ::: 'c' ::: VNil++lhsToNonEmpty' :: NonEmpty Char+lhsToNonEmpty' = L.toNonEmpty $ 'a' ::: 'b' ::: 'c' ::: VNil++rhsToNonEmpty :: NonEmpty Char+rhsToNonEmpty = 'a' :| ['b', 'c']++inspect $ 'lhsToNonEmpty === 'rhsToNonEmpty+inspect $ 'lhsToNonEmpty' =/= 'rhsToNonEmpty
test/Inspection/DataFamily/SpineStrict/Pigeonhole.hs view
@@ -9,7 +9,7 @@ {-# OPTIONS_GHC -dsuppress-type-signatures #-} -- {-# OPTIONS_GHC -dsuppress-uniques #-} -- This makes gix tests pass, default is 60-{-# OPTIONS_GHC -funfolding-use-threshold=200 #-}+{-# OPTIONS_GHC -funfolding-use-threshold=240 #-} module Inspection.DataFamily.SpineStrict.Pigeonhole where import Data.Functor.Compat ((<&>))
vec.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.2 name: vec-version: 0.3+version: 0.4 synopsis: Vec: length-indexed (sized) list category: Data, Dependent Types description:@@ -66,7 +66,7 @@ license-file: LICENSE author: Oleg Grenrus <oleg.grenrus@iki.fi> maintainer: Oleg.Grenrus <oleg.grenrus@iki.fi>-copyright: (c) 2017-2019 Oleg Grenrus+copyright: (c) 2017-2021 Oleg Grenrus build-type: Simple extra-source-files: ChangeLog.md tested-with:@@ -76,7 +76,9 @@ || ==8.2.2 || ==8.4.4 || ==8.6.5- || ==8.8.1+ || ==8.8.4+ || ==8.10.4+ || ==9.0.1 source-repository head type: git@@ -103,9 +105,9 @@ default: True library- default-language: Haskell2010- ghc-options: -Wall -fprint-explicit-kinds- hs-source-dirs: src+ default-language: Haskell2010+ ghc-options: -Wall -fprint-explicit-kinds+ hs-source-dirs: src exposed-modules: Data.Vec.DataFamily.SpineStrict Data.Vec.DataFamily.SpineStrict.Pigeonhole@@ -119,23 +121,27 @@ -- GHC boot libs build-depends:- , base >=4.7 && <4.14+ , base >=4.7 && <4.16 , deepseq >=1.3.0.1 && <1.5 , transformers >=0.3.0.0 && <0.6 if !impl(ghc >=8.0) build-depends: semigroups >=0.18.4 && <0.20 - if !impl(ghc >=7.10)+ -- Ensure Data.Functor.Classes is always available+ if impl(ghc >= 7.10)+ build-depends: transformers >= 0.4.2.0+ else build-depends: transformers-compat ^>=0.6.5 -- siblings- build-depends: fin ^>=0.1.1+ build-depends: fin ^>=0.2 -- other dependencies build-depends:- , hashable >=1.2.7.0 && <1.4- , QuickCheck ^>=2.13.2+ , hashable >=1.2.7.0 && <1.4+ , indexed-traversable ^>=0.1.1+ , QuickCheck ^>=2.14.2 if flag(distributive) build-depends: distributive >=0.5.3 && <0.7@@ -144,13 +150,21 @@ build-depends: adjunctions ^>=4.4 if flag(semigroupoids)- build-depends: semigroupoids >=5.2.2 && <5.4+ build-depends: semigroupoids >=5.3.5 && <5.4 other-extensions: CPP FlexibleContexts GADTs TypeOperators++ if impl(ghc >=9.0)+ -- these flags may abort compilation with GHC-8.10+ -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295+ ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode++ x-docspec-extra-packages: void+ x-docspec-extra-packages: lens test-suite inspection type: exitcode-stdio-1.0