{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Vec.Pull (
Vec (..),
empty,
singleton,
toList,
toNonEmpty,
fromList,
fromListPrefix,
reifyList,
(!),
tabulate,
cons,
snoc,
head,
last,
tail,
init,
reverse,
foldMap,
foldMap1,
ifoldMap,
ifoldMap1,
foldr,
ifoldr,
foldl',
length,
null,
sum,
product,
map,
imap,
zipWith,
izipWith,
repeat,
bind,
join,
universe,
) where
import Prelude
(Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..), Num (..),
all, const, id, maxBound, maybe, ($), (.))
import Control.Applicative (Applicative (..), (<$>))
import Data.Boring (Boring (..))
import Data.Fin (Fin (..))
import Data.List.NonEmpty (NonEmpty (..))
import Data.Monoid (Monoid (..))
import Data.Nat (Nat (..))
import Data.Proxy (Proxy (..))
import Data.Semigroup (Semigroup (..))
import Data.Typeable (Typeable)
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 (..))
#endif
#ifdef MIN_VERSION_semigroupoids
import Data.Functor.Apply (Apply (..))
import qualified Data.Functor.Bind as I (Bind (..))
import qualified Data.Semigroup.Foldable as I (Foldable1 (..))
#endif
import qualified Data.Fin as F
import qualified Data.Type.Nat as N
newtype Vec n a = Vec { forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec :: Fin n -> a }
deriving (Typeable)
instance (Eq a, N.SNatI n) => Eq (Vec n a) where
Vec Fin n -> a
v == :: Vec n a -> Vec n a -> Bool
== Vec Fin n -> a
u = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Fin n
i -> Fin n -> a
u Fin n
i forall a. Eq a => a -> a -> Bool
== Fin n -> a
v Fin n
i) forall (n :: Nat). SNatI n => [Fin n]
F.universe
instance Functor (Vec n) where
fmap :: forall a b. (a -> b) -> Vec n a -> Vec n b
fmap a -> b
f (Vec Fin n -> a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> a
v)
instance N.SNatI n => I.Foldable (Vec n) where
foldMap :: forall m a. Monoid m => (a -> m) -> Vec n a -> m
foldMap = forall m (n :: Nat) a.
(Monoid m, SNatI n) =>
(a -> m) -> Vec n a -> m
foldMap
instance WI.FunctorWithIndex (Fin n) (Vec n) where
imap :: forall a b. (Fin n -> a -> b) -> Vec n a -> Vec n b
imap = forall (n :: Nat) a b. (Fin n -> a -> b) -> Vec n a -> Vec n b
imap
instance N.SNatI n => WI.FoldableWithIndex (Fin n) (Vec n) where
ifoldMap :: forall m a. Monoid m => (Fin n -> a -> m) -> Vec n a -> m
ifoldMap = forall m (n :: Nat) a.
(Monoid m, SNatI n) =>
(Fin n -> a -> m) -> Vec n a -> m
ifoldMap
ifoldr :: forall a b. (Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr = forall (n :: Nat) a b.
SNatI n =>
(Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr
#ifdef MIN_VERSION_semigroupoids
instance (N.SNatI m, n ~ 'S m) => I.Foldable1 (Vec n) where
foldMap1 :: forall m a. Semigroup m => (a -> m) -> Vec n a -> m
foldMap1 = forall s (n :: Nat) a.
(Semigroup s, SNatI n) =>
(a -> s) -> Vec ('S n) a -> s
foldMap1
#endif
instance Applicative (Vec n) where
pure :: forall a. a -> Vec n a
pure = forall x (n :: Nat). x -> Vec n x
repeat
<*> :: forall a b. Vec n (a -> b) -> Vec n a -> Vec n b
(<*>) = forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith forall a b. (a -> b) -> a -> b
($)
Vec n a
_ *> :: forall a b. Vec n a -> Vec n b -> Vec n b
*> Vec n b
x = Vec n b
x
Vec n a
x <* :: forall a b. Vec n a -> Vec n b -> Vec n a
<* Vec n b
_ = Vec n a
x
#if MIN_VERSION_base(4,10,0)
liftA2 :: forall a b c. (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
liftA2 = forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith
#endif
instance Monad (Vec n) where
return :: forall a. a -> Vec n a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
>>= :: forall a b. Vec n a -> (a -> Vec n b) -> Vec n b
(>>=) = forall (n :: Nat) a b. Vec n a -> (a -> Vec n b) -> Vec n b
bind
Vec n a
_ >> :: forall a b. Vec n a -> Vec n b -> Vec n b
>> Vec n b
x = Vec n b
x
#ifdef MIN_VERSION_distributive
instance Distributive (Vec n) where
distribute :: forall (f :: * -> *) a. Functor f => f (Vec n a) -> Vec n (f a)
distribute = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (g :: * -> *) (f :: * -> *) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
distribute forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec
#ifdef MIN_VERSION_adjunctions
instance I.Representable (Vec n) where
type Rep (Vec n) = Fin n
tabulate :: forall a. (Rep (Vec n) -> a) -> Vec n a
tabulate = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec
index :: forall a. Vec n a -> Rep (Vec n) -> a
index = forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec
#endif
#endif
instance Semigroup a => Semigroup (Vec n a) where
Vec Fin n -> a
a <> :: Vec n a -> Vec n a -> Vec n a
<> Vec Fin n -> a
b = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin n -> a
a forall a. Semigroup a => a -> a -> a
<> Fin n -> a
b)
instance Monoid a => Monoid (Vec n a) where
mempty :: Vec n a
mempty = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall a. Monoid a => a
mempty
Vec Fin n -> a
a mappend :: Vec n a -> Vec n a -> Vec n a
`mappend` Vec Fin n -> a
b = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (forall a. Monoid a => a -> a -> a
mappend Fin n -> a
a Fin n -> a
b)
#ifdef MIN_VERSION_semigroupoids
instance Apply (Vec n) where
<.> :: forall a b. Vec n (a -> b) -> Vec n a -> Vec n b
(<.>) = forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith forall a b. (a -> b) -> a -> b
($)
Vec n a
_ .> :: forall a b. Vec n a -> Vec n b -> Vec n b
.> Vec n b
x = Vec n b
x
Vec n a
x <. :: forall a b. Vec n a -> Vec n b -> Vec n a
<. Vec n b
_ = Vec n a
x
liftF2 :: forall a b c. (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
liftF2 = forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith
instance I.Bind (Vec n) where
>>- :: forall a b. Vec n a -> (a -> Vec n b) -> Vec n b
(>>-) = forall (n :: Nat) a b. Vec n a -> (a -> Vec n b) -> Vec n b
bind
join :: forall a. Vec n (Vec n a) -> Vec n a
join = forall (n :: Nat) a. Vec n (Vec n a) -> Vec n a
join
#endif
instance n ~ 'N.Z => Boring (Vec n a) where
boring :: Vec n a
boring = forall a. Vec 'Z a
empty
empty :: Vec 'Z a
empty :: forall a. Vec 'Z a
empty = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall b. Fin 'Z -> b
F.absurd
singleton :: a -> Vec ('S 'Z) a
singleton :: forall a. a -> Vec ('S 'Z) a
singleton = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const
toList :: N.SNatI n => Vec n a -> [a]
toList :: forall (n :: Nat) a. SNatI n => Vec n a -> [a]
toList Vec n a
v = forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec Vec n a
v forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (n :: Nat). SNatI n => [Fin n]
F.universe
toNonEmpty :: N.SNatI n => Vec ('S n) a -> NonEmpty a
toNonEmpty :: forall (n :: Nat) a. SNatI n => Vec ('S n) a -> NonEmpty a
toNonEmpty Vec ('S n) a
v = forall (n :: Nat) a. Vec ('S n) a -> a
head Vec ('S n) a
v forall a. a -> [a] -> NonEmpty a
:| forall (n :: Nat) a. SNatI n => Vec n a -> [a]
toList (forall (n :: Nat) a. Vec ('S n) a -> Vec n a
tail Vec ('S n) a
v)
fromList :: N.SNatI n => [a] -> Maybe (Vec n a)
fromList :: forall (n :: Nat) a. SNatI n => [a] -> Maybe (Vec n a)
fromList = forall (n :: Nat) a. FromList n a -> [a] -> Maybe (Vec n a)
getFromList (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 forall a. FromList 'Z a
start forall (n :: Nat) a. FromList n a -> FromList ('S n) a
step) where
start :: FromList 'Z a
start :: forall a. FromList 'Z a
start = forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList forall a b. (a -> b) -> a -> b
$ \[a]
xs -> case [a]
xs of
[] -> forall a. a -> Maybe a
Just forall a. Vec 'Z a
empty
(a
_ : [a]
_) -> forall a. Maybe a
Nothing
step :: FromList n a -> FromList ('N.S n) a
step :: forall (n :: Nat) a. FromList n a -> FromList ('S n) a
step (FromList [a] -> Maybe (Vec n a)
f) = forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList forall a b. (a -> b) -> a -> b
$ \[a]
xs -> case [a]
xs of
[] -> forall a. Maybe a
Nothing
(a
x : [a]
xs') -> forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons a
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Maybe (Vec n a)
f [a]
xs'
newtype FromList n a = FromList { forall (n :: Nat) a. FromList n a -> [a] -> Maybe (Vec n a)
getFromList :: [a] -> Maybe (Vec n a) }
fromListPrefix :: N.SNatI n => [a] -> Maybe (Vec n a)
fromListPrefix :: forall (n :: Nat) a. SNatI n => [a] -> Maybe (Vec n a)
fromListPrefix = forall (n :: Nat) a. FromList n a -> [a] -> Maybe (Vec n a)
getFromList (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 forall a. FromList 'Z a
start forall (n :: Nat) a. FromList n a -> FromList ('S n) a
step) where
start :: FromList 'Z a
start :: forall a. FromList 'Z a
start = forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList forall a b. (a -> b) -> a -> b
$ \[a]
_ -> forall a. a -> Maybe a
Just forall a. Vec 'Z a
empty
step :: FromList n a -> FromList ('N.S n) a
step :: forall (n :: Nat) a. FromList n a -> FromList ('S n) a
step (FromList [a] -> Maybe (Vec n a)
f) = forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList forall a b. (a -> b) -> a -> b
$ \[a]
xs -> case [a]
xs of
[] -> forall a. Maybe a
Nothing
(a
x : [a]
xs') -> forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons a
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Maybe (Vec n a)
f [a]
xs'
reifyList :: [a] -> (forall n. N.SNatI n => Vec n a -> r) -> r
reifyList :: forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList [] forall (n :: Nat). SNatI n => Vec n a -> r
f = forall (n :: Nat). SNatI n => Vec n a -> r
f forall a. Vec 'Z a
empty
reifyList (a
x : [a]
xs) forall (n :: Nat). SNatI n => Vec n a -> r
f = forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList [a]
xs forall a b. (a -> b) -> a -> b
$ \Vec n a
xs' -> forall (n :: Nat). SNatI n => Vec n a -> r
f (forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons a
x Vec n a
xs')
(!) :: Vec n a -> Fin n -> a
! :: forall (n :: Nat) a. Vec n a -> Fin n -> a
(!) = forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec
tabulate :: (Fin n -> a) -> Vec n a
tabulate :: forall (n :: Nat) a. (Fin n -> a) -> Vec n a
tabulate = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec
cons :: a -> Vec n a -> Vec ('S n) a
cons :: forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons a
x (Vec Fin n -> a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall a b. (a -> b) -> a -> b
$ \Fin ('S n)
i -> case Fin ('S n)
i of
Fin ('S n)
FZ -> a
x
FS Fin n1
j -> Fin n -> a
v Fin n1
j
snoc :: forall a n. N.SNatI n => Vec n a -> a -> Vec ('S n) a
snoc :: forall a (n :: Nat). SNatI n => Vec n a -> a -> Vec ('S n) a
snoc (Vec Fin n -> a
xs) a
x = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall a b. (a -> b) -> a -> b
$ \Fin ('S n)
i -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
x Fin n -> a
xs (forall (n :: Nat). SNatI n => Fin ('S n) -> Maybe (Fin n)
F.isMax Fin ('S n)
i)
head :: Vec ('S n) a -> a
head :: forall (n :: Nat) a. Vec ('S n) a -> a
head (Vec Fin ('S n) -> a
v) = Fin ('S n) -> a
v forall (n1 :: Nat). Fin ('S n1)
FZ
last :: forall n a. N.SNatI n => Vec ('S n) a -> a
last :: forall (n :: Nat) a. SNatI n => Vec ('S n) a -> a
last (Vec Fin ('S n) -> a
v) = Fin ('S n) -> a
v forall a. Bounded a => a
maxBound
tail :: Vec ('S n) a -> Vec n a
tail :: forall (n :: Nat) a. Vec ('S n) a -> Vec n a
tail (Vec Fin ('S n) -> a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin ('S n) -> a
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS)
init :: forall n a. N.SNatI n => Vec ('S n) a -> Vec n a
init :: forall (n :: Nat) a. SNatI n => Vec ('S n) a -> Vec n a
init (Vec Fin ('S n) -> a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin ('S n) -> a
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SNatI n => Fin n -> Fin ('S n)
F.weakenLeft1)
reverse :: forall n a. N.SNatI n => Vec n a -> Vec n a
reverse :: forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
reverse (Vec Fin n -> a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin n -> a
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SNatI n => Fin n -> Fin n
F.mirror)
map :: (a -> b) -> Vec n a -> Vec n b
map :: forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map a -> b
f (Vec Fin n -> a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> a
v)
imap :: (Fin n -> a -> b) -> Vec n a -> Vec n b
imap :: forall (n :: Nat) a b. (Fin n -> a -> b) -> Vec n a -> Vec n b
imap Fin n -> a -> b
f (Vec Fin n -> a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall a b. (a -> b) -> a -> b
$ \Fin n
i -> Fin n -> a -> b
f Fin n
i (Fin n -> a
v Fin n
i)
foldMap :: (Monoid m, N.SNatI n) => (a -> m) -> Vec n a -> m
foldMap :: forall m (n :: Nat) a.
(Monoid m, SNatI n) =>
(a -> m) -> Vec n a -> m
foldMap a -> m
f (Vec Fin n -> a
v) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
I.foldMap (a -> m
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> a
v) forall (n :: Nat). SNatI n => [Fin n]
F.universe
ifoldMap :: (Monoid m, N.SNatI n) => (Fin n -> a -> m) -> Vec n a -> m
ifoldMap :: forall m (n :: Nat) a.
(Monoid m, SNatI n) =>
(Fin n -> a -> m) -> Vec n a -> m
ifoldMap Fin n -> a -> m
f (Vec Fin n -> a
v) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
I.foldMap (\Fin n
i -> Fin n -> a -> m
f Fin n
i (Fin n -> a
v Fin n
i)) forall (n :: Nat). SNatI n => [Fin n]
F.universe
foldMap1 :: (Semigroup s, N.SNatI n) => (a -> s) -> Vec ('S n) a -> s
foldMap1 :: forall s (n :: Nat) a.
(Semigroup s, SNatI n) =>
(a -> s) -> Vec ('S n) a -> s
foldMap1 a -> s
f (Vec Fin ('S n) -> a
v) = forall s a. Semigroup s => (a -> s) -> NonEmpty a -> s
neFoldMap (a -> s
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin ('S n) -> a
v) forall (n :: Nat). SNatI n => NonEmpty (Fin ('S n))
F.universe1
ifoldMap1 :: (Semigroup s, N.SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
ifoldMap1 :: forall s (n :: Nat) a.
(Semigroup s, SNatI n) =>
(Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
ifoldMap1 Fin ('S n) -> a -> s
f (Vec Fin ('S n) -> a
v) = forall s a. Semigroup s => (a -> s) -> NonEmpty a -> s
neFoldMap (\Fin ('S n)
i -> Fin ('S n) -> a -> s
f Fin ('S n)
i (Fin ('S n) -> a
v Fin ('S n)
i)) forall (n :: Nat). SNatI n => NonEmpty (Fin ('S n))
F.universe1
neFoldMap :: Semigroup s => (a -> s) -> NonEmpty a -> s
neFoldMap :: forall s a. Semigroup s => (a -> s) -> NonEmpty a -> s
neFoldMap a -> s
f (a
z :| [a]
zs) = a -> [a] -> s
go a
z [a]
zs where
go :: a -> [a] -> s
go a
x [] = a -> s
f a
x
go a
x (a
y : [a]
ys) = a -> s
f a
x forall a. Semigroup a => a -> a -> a
<> a -> [a] -> s
go a
y [a]
ys
foldr :: N.SNatI n => (a -> b -> b) -> b -> Vec n a -> b
foldr :: forall (n :: Nat) a b.
SNatI n =>
(a -> b -> b) -> b -> Vec n a -> b
foldr a -> b -> b
f b
z (Vec Fin n -> a
v) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
I.foldr (\Fin n
a b
b -> a -> b -> b
f (Fin n -> a
v Fin n
a) b
b) b
z forall (n :: Nat). SNatI n => [Fin n]
F.universe
ifoldr :: N.SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr :: forall (n :: Nat) a b.
SNatI n =>
(Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr Fin n -> a -> b -> b
f b
z (Vec Fin n -> a
v) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
I.foldr (\Fin n
a b
b -> Fin n -> a -> b -> b
f Fin n
a (Fin n -> a
v Fin n
a) b
b) b
z forall (n :: Nat). SNatI n => [Fin n]
F.universe
foldl' :: N.SNatI n => (b -> a -> b) -> b -> Vec n a -> b
foldl' :: forall (n :: Nat) b a.
SNatI n =>
(b -> a -> b) -> b -> Vec n a -> b
foldl' b -> a -> b
f b
z (Vec Fin n -> a
v) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
I.foldl' (\b
b Fin n
a -> b -> a -> b
f b
b (Fin n -> a
v Fin n
a)) b
z forall (n :: Nat). SNatI n => [Fin n]
F.universe
length :: forall n a. N.SNatI n => Vec n a -> Int
length :: forall (n :: Nat) a. SNatI n => Vec n a -> Int
length Vec n a
_ = forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy n)
null :: forall n a. N.SNatI n => Vec n a -> Bool
null :: forall (n :: Nat) a. SNatI n => Vec n a -> Bool
null Vec n a
_ = case forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
SNat n
N.SZ -> Bool
True
SNat n
N.SS -> Bool
False
sum :: (Num a, N.SNatI n) => Vec n a -> a
sum :: forall a (n :: Nat). (Num a, SNatI n) => Vec n a -> a
sum (Vec Fin n -> a
v) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
I.foldl' (\a
x Fin n
i -> a
x forall a. Num a => a -> a -> a
+ Fin n -> a
v Fin n
i) a
0 forall (n :: Nat). SNatI n => [Fin n]
F.universe
product :: (Num a, N.SNatI n) => Vec n a -> a
product :: forall a (n :: Nat). (Num a, SNatI n) => Vec n a -> a
product (Vec Fin n -> a
v) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
I.foldl' (\a
x Fin n
i -> a
x forall a. Num a => a -> a -> a
* Fin n -> a
v Fin n
i) a
1 forall (n :: Nat). SNatI n => [Fin n]
F.universe
zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith :: forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith a -> b -> c
f (Vec Fin n -> a
xs) (Vec Fin n -> b
ys) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall a b. (a -> b) -> a -> b
$ \Fin n
i -> a -> b -> c
f (Fin n -> a
xs Fin n
i) (Fin n -> b
ys Fin n
i)
izipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith :: forall (n :: Nat) a b c.
(Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith Fin n -> a -> b -> c
f (Vec Fin n -> a
xs) (Vec Fin n -> b
ys) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall a b. (a -> b) -> a -> b
$ \Fin n
i -> Fin n -> a -> b -> c
f Fin n
i (Fin n -> a
xs Fin n
i) (Fin n -> b
ys Fin n
i)
repeat :: x -> Vec n x
repeat :: forall x (n :: Nat). x -> Vec n x
repeat = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure
bind :: Vec n a -> (a -> Vec n b) -> Vec n b
bind :: forall (n :: Nat) a b. Vec n a -> (a -> Vec n b) -> Vec n b
bind Vec n a
m a -> Vec n b
k = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec Vec n a
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Vec n b
k
join :: Vec n (Vec n a) -> Vec n a
join :: forall (n :: Nat) a. Vec n (Vec n a) -> Vec n a
join (Vec Fin n -> Vec n a
v) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall a b. (a -> b) -> a -> b
$ \Fin n
i -> forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec (Fin n -> Vec n a
v Fin n
i) Fin n
i
universe :: N.SNatI n => Vec n (Fin n)
universe :: forall (n :: Nat). SNatI n => Vec n (Fin n)
universe = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec forall a. a -> a
id