{-# 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 = (Fin n -> Bool) -> [Fin n] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Fin n
i -> Fin n -> a
u Fin n
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== Fin n -> a
v Fin n
i) [Fin n]
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) = (Fin n -> b) -> Vec n b
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (a -> b
f (a -> b) -> (Fin n -> a) -> Fin n -> b
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 = (a -> m) -> Vec n a -> m
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 = (Fin n -> a -> b) -> Vec n a -> Vec n b
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 = (Fin n -> a -> m) -> Vec n a -> m
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 = (Fin n -> a -> b -> b) -> b -> Vec n a -> b
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 = (a -> m) -> Vec n a -> m
(a -> m) -> Vec ('S m) a -> m
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 = a -> Vec n a
forall x (n :: Nat). x -> Vec n x
repeat
<*> :: forall a b. Vec n (a -> b) -> Vec n a -> Vec n b
(<*>) = ((a -> b) -> 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 (a -> b) -> a -> b
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
liftA2 :: forall a b c. (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
liftA2 = (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith
instance Monad (Vec n) where
return :: forall a. a -> Vec n a
return = a -> Vec n a
forall a. a -> Vec n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
>>= :: forall a b. Vec n a -> (a -> Vec n b) -> Vec n 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 = (Fin n -> f a) -> Vec n (f a)
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> f a) -> Vec n (f a))
-> (f (Vec n a) -> Fin n -> f a) -> f (Vec n a) -> Vec n (f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Fin n -> a) -> Fin n -> f a
forall (g :: * -> *) (f :: * -> *) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
forall (f :: * -> *) a. Functor f => f (Fin n -> a) -> Fin n -> f a
distribute (f (Fin n -> a) -> Fin n -> f a)
-> (f (Vec n a) -> f (Fin n -> a)) -> f (Vec n a) -> Fin n -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec n a -> Fin n -> a) -> f (Vec n a) -> f (Fin n -> a)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Vec n a -> Fin n -> a
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 = (Rep (Vec n) -> a) -> Vec n a
(Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec
index :: forall a. Vec n a -> Rep (Vec n) -> a
index = Vec n a -> Rep (Vec n) -> a
Vec n a -> Fin n -> a
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 = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin n -> a
a (Fin n -> a) -> (Fin n -> a) -> Fin n -> 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 = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec Fin n -> a
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 = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> a) -> (Fin n -> a) -> Fin n -> a
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
(<.>) = ((a -> b) -> 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 (a -> b) -> a -> b
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 = (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
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
(>>-) = 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 = Vec n (Vec n a) -> Vec n a
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 = Vec n a
Vec 'Z a
forall a. Vec 'Z a
empty
empty :: Vec 'Z a
empty :: forall a. Vec 'Z a
empty = (Fin 'Z -> a) -> Vec 'Z a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec Fin 'Z -> a
forall b. Fin 'Z -> b
F.absurd
singleton :: a -> Vec ('S 'Z) a
singleton :: forall a. a -> Vec ('S 'Z) a
singleton = (Fin ('S 'Z) -> a) -> Vec ('S 'Z) a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin ('S 'Z) -> a) -> Vec ('S 'Z) a)
-> (a -> Fin ('S 'Z) -> a) -> a -> Vec ('S 'Z) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Fin ('S 'Z) -> a
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 = Vec n a -> Fin n -> a
forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec Vec n a
v (Fin n -> a) -> [Fin n] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Fin n]
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 = Vec ('S n) a -> a
forall (n :: Nat) a. Vec ('S n) a -> a
head Vec ('S n) a
v a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| Vec n a -> [a]
forall (n :: Nat) a. SNatI n => Vec n a -> [a]
toList (Vec ('S n) a -> Vec n a
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 = FromList n a -> [a] -> Maybe (Vec n a)
forall (n :: Nat) a. FromList n a -> [a] -> Maybe (Vec n a)
getFromList (FromList 'Z a
-> (forall (m :: Nat).
SNatI m =>
FromList m a -> FromList ('S m) a)
-> FromList n a
forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 FromList 'Z a
forall a. FromList 'Z a
start FromList m a -> FromList ('S m) a
forall (m :: Nat). SNatI m => FromList m a -> FromList ('S m) a
forall (n :: Nat) a. FromList n a -> FromList ('S n) a
step) where
start :: FromList 'Z a
start :: forall a. FromList 'Z a
start = ([a] -> Maybe (Vec 'Z a)) -> FromList 'Z a
forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList (([a] -> Maybe (Vec 'Z a)) -> FromList 'Z a)
-> ([a] -> Maybe (Vec 'Z a)) -> FromList 'Z a
forall a b. (a -> b) -> a -> b
$ \[a]
xs -> case [a]
xs of
[] -> Vec 'Z a -> Maybe (Vec 'Z a)
forall a. a -> Maybe a
Just Vec 'Z a
forall a. Vec 'Z a
empty
(a
_ : [a]
_) -> Maybe (Vec 'Z 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) = ([a] -> Maybe (Vec ('S n) a)) -> FromList ('S n) a
forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList (([a] -> Maybe (Vec ('S n) a)) -> FromList ('S n) a)
-> ([a] -> Maybe (Vec ('S n) a)) -> FromList ('S n) a
forall a b. (a -> b) -> a -> b
$ \[a]
xs -> case [a]
xs of
[] -> Maybe (Vec ('S n) a)
forall a. Maybe a
Nothing
(a
x : [a]
xs') -> a -> Vec n a -> Vec ('S n) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons a
x (Vec n a -> Vec ('S n) a)
-> Maybe (Vec n a) -> Maybe (Vec ('S n) a)
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 = FromList n a -> [a] -> Maybe (Vec n a)
forall (n :: Nat) a. FromList n a -> [a] -> Maybe (Vec n a)
getFromList (FromList 'Z a
-> (forall (m :: Nat).
SNatI m =>
FromList m a -> FromList ('S m) a)
-> FromList n a
forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 FromList 'Z a
forall a. FromList 'Z a
start FromList m a -> FromList ('S m) a
forall (m :: Nat). SNatI m => FromList m a -> FromList ('S m) a
forall (n :: Nat) a. FromList n a -> FromList ('S n) a
step) where
start :: FromList 'Z a
start :: forall a. FromList 'Z a
start = ([a] -> Maybe (Vec 'Z a)) -> FromList 'Z a
forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList (([a] -> Maybe (Vec 'Z a)) -> FromList 'Z a)
-> ([a] -> Maybe (Vec 'Z a)) -> FromList 'Z a
forall a b. (a -> b) -> a -> b
$ \[a]
_ -> Vec 'Z a -> Maybe (Vec 'Z a)
forall a. a -> Maybe a
Just Vec 'Z a
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) = ([a] -> Maybe (Vec ('S n) a)) -> FromList ('S n) a
forall (n :: Nat) a. ([a] -> Maybe (Vec n a)) -> FromList n a
FromList (([a] -> Maybe (Vec ('S n) a)) -> FromList ('S n) a)
-> ([a] -> Maybe (Vec ('S n) a)) -> FromList ('S n) a
forall a b. (a -> b) -> a -> b
$ \[a]
xs -> case [a]
xs of
[] -> Maybe (Vec ('S n) a)
forall a. Maybe a
Nothing
(a
x : [a]
xs') -> a -> Vec n a -> Vec ('S n) a
forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons a
x (Vec n a -> Vec ('S n) a)
-> Maybe (Vec n a) -> Maybe (Vec ('S n) a)
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 = Vec 'Z a -> r
forall (n :: Nat). SNatI n => Vec n a -> r
f Vec 'Z a
forall a. Vec 'Z a
empty
reifyList (a
x : [a]
xs) forall (n :: Nat). SNatI n => Vec n a -> r
f = [a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList [a]
xs ((forall (n :: Nat). SNatI n => Vec n a -> r) -> r)
-> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Vec n a
xs' -> Vec ('S n) a -> r
forall (n :: Nat). SNatI n => Vec n a -> r
f (a -> Vec n a -> Vec ('S n) a
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
(!) = 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 = (Fin n -> a) -> Vec n a
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) = (Fin ('S n) -> a) -> Vec ('S n) a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin ('S n) -> a) -> Vec ('S n) a)
-> (Fin ('S n) -> a) -> Vec ('S n) a
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 n
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 = (Fin ('S n) -> a) -> Vec ('S n) a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin ('S n) -> a) -> Vec ('S n) a)
-> (Fin ('S n) -> a) -> Vec ('S n) a
forall a b. (a -> b) -> a -> b
$ \Fin ('S n)
i -> a -> (Fin n -> a) -> Maybe (Fin n) -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
x Fin n -> a
xs (Fin ('S n) -> Maybe (Fin n)
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 Fin ('S n)
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 Fin ('S n)
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) = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin ('S n) -> a
v (Fin ('S n) -> a) -> (Fin n -> Fin ('S n)) -> Fin n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Fin ('S n)
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) = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin ('S n) -> a
v (Fin ('S n) -> a) -> (Fin n -> Fin ('S n)) -> Fin n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Fin ('S n)
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) = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (Fin n -> a
v (Fin n -> a) -> (Fin n -> Fin n) -> Fin n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> Fin n
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) = (Fin n -> b) -> Vec n b
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec (a -> b
f (a -> b) -> (Fin n -> a) -> Fin n -> b
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) = (Fin n -> b) -> Vec n b
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> b) -> Vec n b) -> (Fin n -> b) -> Vec n b
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) = (Fin n -> m) -> [Fin n] -> m
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
I.foldMap (a -> m
f (a -> m) -> (Fin n -> a) -> Fin n -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin n -> a
v) [Fin n]
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) = (Fin n -> m) -> [Fin n] -> m
forall m a. Monoid m => (a -> m) -> [a] -> m
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)) [Fin n]
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) = (Fin ('S n) -> s) -> NonEmpty (Fin ('S n)) -> s
forall s a. Semigroup s => (a -> s) -> NonEmpty a -> s
neFoldMap (a -> s
f (a -> s) -> (Fin ('S n) -> a) -> Fin ('S n) -> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fin ('S n) -> a
v) NonEmpty (Fin ('S n))
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) = (Fin ('S n) -> s) -> NonEmpty (Fin ('S n)) -> s
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)) NonEmpty (Fin ('S n))
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 s -> s -> s
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) = (Fin n -> b -> b) -> b -> [Fin n] -> b
forall a b. (a -> b -> b) -> b -> [a] -> b
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 [Fin n]
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) = (Fin n -> b -> b) -> b -> [Fin n] -> b
forall a b. (a -> b -> b) -> b -> [a] -> b
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 [Fin n]
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) = (b -> Fin n -> b) -> b -> [Fin n] -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
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 [Fin n]
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
_ = Proxy @Nat n -> Int
forall (n :: Nat) m (proxy :: Nat -> *).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (Proxy @Nat n
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 SNat n
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) = (a -> Fin n -> a) -> a -> [Fin n] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
I.foldl' (\a
x Fin n
i -> a
x a -> a -> a
forall a. Num a => a -> a -> a
+ Fin n -> a
v Fin n
i) a
0 [Fin n]
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) = (a -> Fin n -> a) -> a -> [Fin n] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
I.foldl' (\a
x Fin n
i -> a
x a -> a -> a
forall a. Num a => a -> a -> a
* Fin n -> a
v Fin n
i) a
1 [Fin n]
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) = (Fin n -> c) -> Vec n c
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> c) -> Vec n c) -> (Fin n -> c) -> Vec n c
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) = (Fin n -> c) -> Vec n c
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> c) -> Vec n c) -> (Fin n -> c) -> Vec n c
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 = (Fin n -> x) -> Vec n x
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> x) -> Vec n x) -> (x -> Fin n -> x) -> x -> Vec n x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Fin n -> x
forall a. a -> Fin n -> a
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 = (Fin n -> b) -> Vec n b
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> b) -> Vec n b) -> (Fin n -> b) -> Vec n b
forall a b. (a -> b) -> a -> b
$ Vec n a -> Fin n -> a
forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec Vec n a
m (Fin n -> a) -> (a -> Fin n -> b) -> Fin n -> b
forall a b. (Fin n -> a) -> (a -> Fin n -> b) -> Fin n -> b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Vec n b -> Fin n -> b
forall (n :: Nat) a. Vec n a -> Fin n -> a
unVec (Vec n b -> Fin n -> b) -> (a -> Vec n b) -> a -> Fin n -> b
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) = (Fin n -> a) -> Vec n a
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec ((Fin n -> a) -> Vec n a) -> (Fin n -> a) -> Vec n a
forall a b. (a -> b) -> a -> b
$ \Fin n
i -> Vec n a -> Fin n -> a
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 = (Fin n -> Fin n) -> Vec n (Fin n)
forall (n :: Nat) a. (Fin n -> a) -> Vec n a
Vec Fin n -> Fin n
forall a. a -> a
id