{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Vec.Lazy (
Vec (..),
empty,
singleton,
withDict,
toPull,
fromPull,
toList,
toNonEmpty,
fromList,
fromListPrefix,
reifyList,
(!),
tabulate,
cons,
snoc,
head,
last,
tail,
init,
reverse,
dfoldr,
dfoldl,
dfoldl',
(++),
split,
concatMap,
concat,
chunks,
take,
drop,
foldMap,
foldMap1,
ifoldMap,
ifoldMap1,
foldr,
ifoldr,
foldl',
length,
null,
sum,
product,
map,
imap,
traverse,
#ifdef MIN_VERSION_semigroupoids
traverse1,
#endif
itraverse,
itraverse_,
zipWith,
izipWith,
repeat,
bind,
join,
universe,
VecEach (..),
) where
import Prelude
(Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..), Num (..),
Ord (..), Ordering (..), Show (..), flip, id, seq, showParen, showString,
uncurry, ($), (&&), (.))
import Control.Applicative (Applicative (..), (<$>))
import Control.DeepSeq (NFData (..))
import Control.Lens.Yocto ((<&>))
import Data.Boring (Boring (..))
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 (..))
import Data.Typeable (Typeable)
import SafeCompat (coerce)
import qualified Data.Foldable as I (Foldable (..))
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
#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 (..))
import qualified Data.Semigroup.Traversable as I (Traversable1 (..))
#endif
import qualified Data.Fin as F
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
infixr 5 :::
data Vec (n :: Nat) a where
VNil :: Vec 'Z a
(:::) :: a -> Vec n a -> Vec ('S n) a
deriving (Typeable)
deriving instance Eq a => Eq (Vec n a)
deriving instance Ord a => Ord (Vec n a)
instance Show a => Show (Vec n a) where
showsPrec :: Int -> Vec n a -> ShowS
showsPrec Int
_ Vec n a
VNil = String -> ShowS
showString String
"VNil"
showsPrec Int
d (a
x ::: Vec n a
xs) = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
5)
forall a b. (a -> b) -> a -> b
$ forall a. Show a => Int -> a -> ShowS
showsPrec Int
6 a
x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" ::: "
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
5 Vec n a
xs
instance Functor (Vec n) where
fmap :: forall a b. (a -> b) -> Vec n a -> Vec n b
fmap = forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map
instance I.Foldable (Vec n) where
foldMap :: forall m a. Monoid m => (a -> m) -> Vec n a -> m
foldMap = forall m a (n :: Nat). Monoid m => (a -> m) -> Vec n a -> m
foldMap
foldr :: forall a b. (a -> b -> b) -> b -> Vec n a -> b
foldr = forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
foldr
foldl' :: forall b a. (b -> a -> b) -> b -> Vec n a -> b
foldl' = forall a b (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
foldl'
#if MIN_VERSION_base(4,8,0)
null :: forall a. Vec n a -> Bool
null = forall (n :: Nat) a. Vec n a -> Bool
null
length :: forall a. Vec n a -> Int
length = forall (n :: Nat) a. Vec n a -> Int
length
sum :: forall a. Num a => Vec n a -> a
sum = forall a (n :: Nat). Num a => Vec n a -> a
sum
product :: forall a. Num a => Vec n a -> a
product = forall a (n :: Nat). Num a => Vec n a -> a
product
#endif
instance I.Traversable (Vec n) where
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse = forall (n :: Nat) (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse
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 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 =>
(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 a b (n :: Nat). (Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr
instance WI.TraversableWithIndex (Fin n) (Vec n) where
itraverse :: forall (f :: * -> *) a b.
Applicative f =>
(Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse = forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse
#ifdef MIN_VERSION_semigroupoids
instance n ~ 'S m => I.Foldable1 (Vec n) where
foldMap1 :: forall m a. Semigroup m => (a -> m) -> Vec n a -> m
foldMap1 = forall s a (n :: Nat). Semigroup s => (a -> s) -> Vec ('S n) a -> s
foldMap1
instance n ~ 'S m => I.Traversable1 (Vec n) where
traverse1 :: forall (f :: * -> *) a b.
Apply f =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse1 = forall (n :: Nat) (f :: * -> *) a b.
Apply f =>
(a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
traverse1
#endif
instance NFData a => NFData (Vec n a) where
rnf :: Vec n a -> ()
rnf Vec n a
VNil = ()
rnf (a
x ::: Vec n a
xs) = forall a. NFData a => a -> ()
rnf a
x seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Vec n a
xs
instance Hashable a => Hashable (Vec n a) where
hashWithSalt :: Int -> Vec n a -> Int
hashWithSalt Int
salt Vec n a
VNil = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt (Int
0 :: Int)
hashWithSalt Int
salt (a
x ::: Vec n a
xs) = Int
salt
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` a
x
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Vec n a
xs
instance N.SNatI n => Applicative (Vec n) where
pure :: forall a. a -> Vec n a
pure = forall (n :: Nat) x. SNatI n => 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 N.SNatI n => 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 N.SNatI n => Distributive (Vec n) where
distribute :: forall (f :: * -> *) a. Functor f => f (Vec n a) -> Vec n (f a)
distribute f (Vec n a)
f = forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate (\Fin n
k -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
k) f (Vec n a)
f)
#ifdef MIN_VERSION_adjunctions
instance N.SNatI n => 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. SNatI n => (Fin n -> a) -> Vec n a
tabulate
index :: forall a. Vec n a -> Rep (Vec n) -> a
index = forall (n :: Nat) a. Vec n a -> Fin n -> a
(!)
#endif
#endif
instance Semigroup a => Semigroup (Vec n a) where
<> :: Vec n a -> Vec n a -> Vec n a
(<>) = forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith forall a. Semigroup a => a -> a -> a
(<>)
instance (Monoid a, N.SNatI n) => Monoid (Vec n a) where
mempty :: Vec n a
mempty = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
mappend :: Vec n a -> Vec n a -> Vec n a
mappend = forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith forall a. Monoid a => a -> a -> a
mappend
#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
#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
instance Eq1 (Vec n) where
liftEq :: forall a b. (a -> b -> Bool) -> Vec n a -> Vec n b -> Bool
liftEq a -> b -> Bool
_eq Vec n a
VNil Vec n b
VNil = Bool
True
liftEq a -> b -> Bool
eq (a
x ::: Vec n a
xs) (b
y ::: Vec n b
ys) = a -> b -> Bool
eq a
x b
y Bool -> Bool -> Bool
&& forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
eq Vec n a
xs Vec n b
ys
instance Ord1 (Vec n) where
liftCompare :: forall a b. (a -> b -> Ordering) -> Vec n a -> Vec n b -> Ordering
liftCompare a -> b -> Ordering
_cmp Vec n a
VNil Vec n b
VNil = Ordering
EQ
liftCompare a -> b -> Ordering
cmp (a
x ::: Vec n a
xs) (b
y ::: Vec n b
ys) = a -> b -> Ordering
cmp a
x b
y forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare a -> b -> Ordering
cmp Vec n a
xs Vec n b
ys
instance Show1 (Vec n) where
liftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Vec n a -> ShowS
liftShowsPrec Int -> a -> ShowS
_ [a] -> ShowS
_ Int
_ Vec n a
VNil = String -> ShowS
showString String
"VNil"
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
d (a
x ::: Vec n a
xs) = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
5)
forall a b. (a -> b) -> a -> b
$ Int -> a -> ShowS
sp Int
6 a
x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" ::: "
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
5 Vec n a
xs
#else
instance Eq1 (Vec n) where eq1 = (==)
instance Ord1 (Vec n) where compare1 = compare
instance Show1 (Vec n) where showsPrec1 = showsPrec
#endif
empty :: Vec 'Z a
empty :: forall a. Vec 'Z a
empty = forall a. Vec 'Z a
VNil
singleton :: a -> Vec ('S 'Z) a
singleton :: forall a. a -> Vec ('S 'Z) a
singleton a
x = a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall a. Vec 'Z a
VNil
withDict :: Vec n a -> (N.SNatI n => r) -> r
withDict :: forall (n :: Nat) a r. Vec n a -> (SNatI n => r) -> r
withDict Vec n a
VNil SNatI n => r
r = SNatI n => r
r
withDict (a
_ ::: Vec n a
xs) SNatI n => r
r = forall (n :: Nat) a r. Vec n a -> (SNatI n => r) -> r
withDict Vec n a
xs SNatI n => r
r
toPull :: Vec n a -> P.Vec n a
toPull :: forall (n :: Nat) a. Vec n a -> Vec n a
toPull Vec n a
VNil = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec forall b. Fin 'Z -> b
F.absurd
toPull (a
x ::: Vec n a
xs) = forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec forall a b. (a -> b) -> a -> b
$ \Fin n
n -> case Fin n
n of
Fin n
FZ -> a
x
FS Fin n1
m -> forall (n :: Nat) a. Vec n a -> Fin n -> a
P.unVec (forall (n :: Nat) a. Vec n a -> Vec n a
toPull Vec n a
xs) Fin n1
m
fromPull :: forall n a. N.SNatI n => P.Vec n a -> Vec n a
fromPull :: forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
fromPull (P.Vec Fin n -> a
f) = case forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
SNat n
N.SZ -> forall a. Vec 'Z a
VNil
SNat n
N.SS -> Fin n -> a
f forall (n1 :: Nat). Fin ('S n1)
FZ forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
fromPull (forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec (Fin n -> a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS))
toList :: Vec n a -> [a]
toList :: forall (n :: Nat) a. Vec n a -> [a]
toList Vec n a
VNil = []
toList (a
x ::: Vec n a
xs) = a
x forall a. a -> [a] -> [a]
: forall (n :: Nat) a. Vec n a -> [a]
toList Vec n a
xs
toNonEmpty :: Vec ('S n) a -> NonEmpty a
toNonEmpty :: forall (n :: Nat) a. Vec ('S n) a -> NonEmpty a
toNonEmpty (a
x ::: Vec n a
xs) = a
x forall a. a -> [a] -> NonEmpty a
:| forall (n :: Nat) a. Vec n a -> [a]
toList Vec n a
xs
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
VNil
(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') -> (a
x forall a (n :: Nat). a -> Vec n a -> 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 = 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
VNil
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') -> (a
x forall a (n :: Nat). a -> Vec n a -> 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 = forall (n :: Nat). SNatI n => Vec n a -> r
f forall a. Vec 'Z a
VNil
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 (a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec n a
xs')
(!) :: Vec n a -> Fin n -> a
! :: forall (n :: Nat) a. Vec n a -> Fin n -> a
(!) (a
x ::: Vec n a
_) Fin n
FZ = a
x
(!) (a
_ ::: Vec n a
xs) (FS Fin n1
n) = Vec n a
xs forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n1
n
(!) Vec n a
VNil Fin n
n = case Fin n
n of {}
tabulate :: N.SNatI n => (Fin n -> a) -> Vec n a
tabulate :: forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate = forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
fromPull forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.tabulate
cons :: a -> Vec n a -> Vec ('S n) a
cons :: forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
cons = forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::)
snoc :: Vec n a -> a -> Vec ('S n) a
snoc :: forall (n :: Nat) a. Vec n a -> a -> Vec ('S n) a
snoc Vec n a
VNil a
x = a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall a. Vec 'Z a
VNil
snoc (a
y ::: Vec n a
ys) a
x = a
y forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall (n :: Nat) a. Vec n a -> a -> Vec ('S n) a
snoc Vec n a
ys a
x
head :: Vec ('S n) a -> a
head :: forall (n :: Nat) a. Vec ('S n) a -> a
head (a
x ::: Vec n a
_) = a
x
last :: Vec ('S n) a -> a
last :: forall (n :: Nat) a. Vec ('S n) a -> a
last (a
x ::: Vec n a
VNil) = a
x
last (a
_ ::: xs :: Vec n a
xs@(a
_ ::: Vec n a
_)) = forall (n :: Nat) a. Vec ('S n) a -> a
last Vec n a
xs
tail :: Vec ('S n) a -> Vec n a
tail :: forall (n :: Nat) a. Vec ('S n) a -> Vec n a
tail (a
_ ::: Vec n a
xs) = Vec n a
xs
init :: Vec ('S n) a -> Vec n a
init :: forall (n :: Nat) a. Vec ('S n) a -> Vec n a
init (a
_ ::: Vec n a
VNil) = forall a. Vec 'Z a
VNil
init (a
x ::: xs :: Vec n a
xs@(a
_ ::: Vec n a
_)) = a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall (n :: Nat) a. Vec ('S n) a -> Vec n a
init Vec n a
xs
reverse :: Vec n a -> Vec n a
reverse :: forall (n :: Nat) a. Vec n a -> Vec n a
reverse Vec n a
xs = forall a (n :: Nat). FlippedVec a n -> Vec n a
unflipVec (forall (n :: Nat) a (f :: Nat -> *).
(forall (m :: Nat). f m -> a -> f ('S m)) -> f 'Z -> Vec n a -> f n
dfoldl forall a (m :: Nat). FlippedVec a m -> a -> FlippedVec a ('S m)
c (forall a (n :: Nat). Vec n a -> FlippedVec a n
FlipVec forall a. Vec 'Z a
VNil) Vec n a
xs)
where
c :: forall a m. FlippedVec a m -> a -> FlippedVec a ('S m)
c :: forall a (m :: Nat). FlippedVec a m -> a -> FlippedVec a ('S m)
c = coerce :: forall a b. Coercible @(*) a b => a -> b
coerce (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::) :: Vec m a -> a -> Vec ('S m) a)
newtype FlippedVec a n = FlipVec { forall a (n :: Nat). FlippedVec a n -> Vec n a
unflipVec :: Vec n a }
dfoldr :: forall n a f. (forall m. a -> f m -> f ('S m)) -> f 'Z -> Vec n a -> f n
dfoldr :: forall (n :: Nat) a (f :: Nat -> *).
(forall (m :: Nat). a -> f m -> f ('S m)) -> f 'Z -> Vec n a -> f n
dfoldr forall (m :: Nat). a -> f m -> f ('S m)
c f 'Z
n = forall (m :: Nat). Vec m a -> f m
go where
go :: Vec m a -> f m
go :: forall (m :: Nat). Vec m a -> f m
go Vec m a
VNil = f 'Z
n
go (a
x ::: Vec n a
xs) = forall (m :: Nat). a -> f m -> f ('S m)
c a
x (forall (m :: Nat). Vec m a -> f m
go Vec n a
xs)
dfoldl :: forall n a f. (forall m. f m -> a -> f ('S m))-> f 'Z -> Vec n a -> f n
dfoldl :: forall (n :: Nat) a (f :: Nat -> *).
(forall (m :: Nat). f m -> a -> f ('S m)) -> f 'Z -> Vec n a -> f n
dfoldl forall (m :: Nat). f m -> a -> f ('S m)
_ f 'Z
n Vec n a
VNil = f 'Z
n
dfoldl forall (m :: Nat). f m -> a -> f ('S m)
c f 'Z
n (a
x ::: Vec n a
xs) = forall (f :: Nat -> *) (n :: Nat). WrappedSucc f n -> f ('S n)
unwrapSucc (forall (n :: Nat) a (f :: Nat -> *).
(forall (m :: Nat). f m -> a -> f ('S m)) -> f 'Z -> Vec n a -> f n
dfoldl forall (m :: Nat). WrappedSucc f m -> a -> WrappedSucc f ('S m)
c' (forall (f :: Nat -> *) (n :: Nat). f ('S n) -> WrappedSucc f n
WrapSucc (forall (m :: Nat). f m -> a -> f ('S m)
c f 'Z
n a
x)) Vec n a
xs)
where
c' :: forall m. WrappedSucc f m -> a -> WrappedSucc f ('S m)
c' :: forall (m :: Nat). WrappedSucc f m -> a -> WrappedSucc f ('S m)
c' = coerce :: forall a b. Coercible @(*) a b => a -> b
coerce (forall (m :: Nat). f m -> a -> f ('S m)
c :: f ('S m) -> a -> f ('S ('S m)))
dfoldl' :: forall n a f. (forall m. f m -> a -> f ('S m))-> f 'Z -> Vec n a -> f n
dfoldl' :: forall (n :: Nat) a (f :: Nat -> *).
(forall (m :: Nat). f m -> a -> f ('S m)) -> f 'Z -> Vec n a -> f n
dfoldl' forall (m :: Nat). f m -> a -> f ('S m)
_ !f 'Z
n Vec n a
VNil = f 'Z
n
dfoldl' forall (m :: Nat). f m -> a -> f ('S m)
c !f 'Z
n (a
x ::: Vec n a
xs) = forall (f :: Nat -> *) (n :: Nat). WrappedSucc f n -> f ('S n)
unwrapSucc (forall (n :: Nat) a (f :: Nat -> *).
(forall (m :: Nat). f m -> a -> f ('S m)) -> f 'Z -> Vec n a -> f n
dfoldl' forall (m :: Nat). WrappedSucc f m -> a -> WrappedSucc f ('S m)
c' (forall (f :: Nat -> *) (n :: Nat). f ('S n) -> WrappedSucc f n
WrapSucc (forall (m :: Nat). f m -> a -> f ('S m)
c f 'Z
n a
x)) Vec n a
xs)
where
c' :: forall m. WrappedSucc f m -> a -> WrappedSucc f ('S m)
c' :: forall (m :: Nat). WrappedSucc f m -> a -> WrappedSucc f ('S m)
c' = coerce :: forall a b. Coercible @(*) a b => a -> b
coerce (forall (m :: Nat). f m -> a -> f ('S m)
c :: f ('S m) -> a -> f ('S ('S m)))
newtype WrappedSucc f n = WrapSucc { forall (f :: Nat -> *) (n :: Nat). WrappedSucc f n -> f ('S n)
unwrapSucc :: f ('S n) }
infixr 5 ++
(++) :: Vec n a -> Vec m a -> Vec (N.Plus n m) a
Vec n a
VNil ++ :: forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ Vec m a
ys = Vec m a
ys
(a
x ::: Vec n a
xs) ++ Vec m a
ys = a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec n a
xs forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ Vec m a
ys
split :: N.SNatI n => Vec (N.Plus n m) a -> (Vec n a, Vec m a)
split :: forall (n :: Nat) (m :: Nat) a.
SNatI n =>
Vec (Plus n m) a -> (Vec n a, Vec m a)
split = forall (m :: Nat) (n :: Nat) a.
Split m n a -> Vec (Plus n m) a -> (Vec n a, Vec m a)
appSplit (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 (m :: Nat) a. Split m 'Z a
start forall (m :: Nat) (n :: Nat) a. Split m n a -> Split m ('S n) a
step) where
start :: Split m 'Z a
start :: forall (m :: Nat) a. Split m 'Z a
start = forall (m :: Nat) (n :: Nat) a.
(Vec (Plus n m) a -> (Vec n a, Vec m a)) -> Split m n a
Split forall a b. (a -> b) -> a -> b
$ \Vec (Plus 'Z m) a
xs -> (forall a. Vec 'Z a
VNil, Vec (Plus 'Z m) a
xs)
step :: Split m n a -> Split m ('S n) a
step :: forall (m :: Nat) (n :: Nat) a. Split m n a -> Split m ('S n) a
step (Split Vec (Plus n m) a -> (Vec n a, Vec m a)
f) = forall (m :: Nat) (n :: Nat) a.
(Vec (Plus n m) a -> (Vec n a, Vec m a)) -> Split m n a
Split forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> case Vec (Plus n m) a -> (Vec n a, Vec m a)
f Vec n a
xs of
(Vec n a
ys, Vec m a
zs) -> (a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec n a
ys, Vec m a
zs)
newtype Split m n a = Split { forall (m :: Nat) (n :: Nat) a.
Split m n a -> Vec (Plus n m) a -> (Vec n a, Vec m a)
appSplit :: Vec (N.Plus n m) a -> (Vec n a, Vec m a) }
concatMap :: (a -> Vec m b) -> Vec n a -> Vec (N.Mult n m) b
concatMap :: forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap a -> Vec m b
_ Vec n a
VNil = forall a. Vec 'Z a
VNil
concatMap a -> Vec m b
f (a
x ::: Vec n a
xs) = a -> Vec m b
f a
x forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap a -> Vec m b
f Vec n a
xs
concat :: Vec n (Vec m a) -> Vec (N.Mult n m) a
concat :: forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (Mult n m) a
concat = forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap forall a. a -> a
id
chunks :: (N.SNatI n, N.SNatI m) => Vec (N.Mult n m) a -> Vec n (Vec m a)
chunks :: forall (n :: Nat) (m :: Nat) a.
(SNatI n, SNatI m) =>
Vec (Mult n m) a -> Vec n (Vec m a)
chunks = forall (m :: Nat) (n :: Nat) a.
Chunks m n a -> Vec (Mult n m) a -> Vec n (Vec m a)
getChunks forall a b. (a -> b) -> a -> b
$ 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 (m :: Nat) a. Chunks m 'Z a
start forall (m :: Nat) (n :: Nat) a.
SNatI m =>
Chunks m n a -> Chunks m ('S n) a
step where
start :: Chunks m 'Z a
start :: forall (m :: Nat) a. Chunks m 'Z a
start = forall (m :: Nat) (n :: Nat) a.
(Vec (Mult n m) a -> Vec n (Vec m a)) -> Chunks m n a
Chunks forall a b. (a -> b) -> a -> b
$ \Vec (Mult 'Z m) a
_ -> forall a. Vec 'Z a
VNil
step :: forall m n a. N.SNatI m => Chunks m n a -> Chunks m ('S n) a
step :: forall (m :: Nat) (n :: Nat) a.
SNatI m =>
Chunks m n a -> Chunks m ('S n) a
step (Chunks Vec (Mult n m) a -> Vec n (Vec m a)
go) = forall (m :: Nat) (n :: Nat) a.
(Vec (Mult n m) a -> Vec n (Vec m a)) -> Chunks m n a
Chunks forall a b. (a -> b) -> a -> b
$ \Vec (Mult ('S n) m) a
xs ->
let (Vec m a
ys, Vec (Mult n m) a
zs) = forall (n :: Nat) (m :: Nat) a.
SNatI n =>
Vec (Plus n m) a -> (Vec n a, Vec m a)
split Vec (Mult ('S n) m) a
xs :: (Vec m a, Vec (N.Mult n m) a)
in Vec m a
ys forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec (Mult n m) a -> Vec n (Vec m a)
go Vec (Mult n m) a
zs
newtype Chunks m n a = Chunks { forall (m :: Nat) (n :: Nat) a.
Chunks m n a -> Vec (Mult n m) a -> Vec n (Vec m a)
getChunks :: Vec (N.Mult n m) a -> Vec n (Vec m a) }
take :: forall n m a. (LE.ZS.LE n m) => Vec m a -> Vec n a
take :: forall (n :: Nat) (m :: Nat) a. LE n m => Vec m a -> Vec n a
take = forall (n' :: Nat) (m' :: Nat).
LEProof n' m' -> Vec m' a -> Vec n' a
go forall (n :: Nat) (m :: Nat). LE n m => LEProof n m
LE.ZS.leProof where
go :: LE.ZS.LEProof n' m' -> Vec m' a -> Vec n' a
go :: forall (n' :: Nat) (m' :: Nat).
LEProof n' m' -> Vec m' a -> Vec n' a
go LEProof n' m'
LE.ZS.LEZero Vec m' a
_ = forall a. Vec 'Z a
VNil
go (LE.ZS.LESucc LEProof n1 m1
p) (a
x ::: Vec n a
xs) = a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall (n' :: Nat) (m' :: Nat).
LEProof n' m' -> Vec m' a -> Vec n' a
go LEProof n1 m1
p Vec n a
xs
drop :: forall n m a. (LE.ZS.LE n m, N.SNatI m) => Vec m a -> Vec n a
drop :: forall (n :: Nat) (m :: Nat) a.
(LE n m, SNatI m) =>
Vec m a -> Vec n a
drop = forall (n' :: Nat) (m' :: Nat).
LEProof n' m' -> Vec m' a -> Vec n' a
go (forall (n :: Nat) (m :: Nat). SNatI m => LEProof n m -> LEProof n m
LE.RS.fromZeroSucc forall (n :: Nat) (m :: Nat). LE n m => LEProof n m
LE.ZS.leProof) where
go :: LE.RS.LEProof n' m' -> Vec m' a -> Vec n' a
go :: forall (n' :: Nat) (m' :: Nat).
LEProof n' m' -> Vec m' a -> Vec n' a
go LEProof n' m'
LE.RS.LERefl Vec m' a
xs = Vec m' a
xs
go (LE.RS.LEStep LEProof n' m1
p) (a
_ ::: Vec n a
xs) = forall (n' :: Nat) (m' :: Nat).
LEProof n' m' -> Vec m' a -> Vec n' a
go LEProof n' m1
p Vec n a
xs
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
_ Vec n a
VNil = forall a. Vec 'Z a
VNil
map a -> b
f (a
x ::: Vec n a
xs) = a -> b
f a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Vec n a
xs
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
_ Vec n a
VNil = forall a. Vec 'Z a
VNil
imap Fin n -> a -> b
f (a
x ::: Vec n a
xs) = Fin n -> a -> b
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall (n :: Nat) a b. (Fin n -> a -> b) -> Vec n a -> Vec n b
imap (Fin n -> a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs
traverse :: forall n f a b. Applicative f => (a -> f b) -> Vec n a -> f (Vec n b)
traverse :: forall (n :: Nat) (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse a -> f b
f = forall (m :: Nat). Vec m a -> f (Vec m b)
go where
go :: Vec m a -> f (Vec m b)
go :: forall (m :: Nat). Vec m a -> f (Vec m b)
go Vec m a
VNil = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Vec 'Z a
VNil
go (a
x ::: Vec n a
xs) = forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: Nat). Vec m a -> f (Vec m b)
go Vec n a
xs
#ifdef MIN_VERSION_semigroupoids
traverse1 :: forall n f a b. Apply f => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
traverse1 :: forall (n :: Nat) (f :: * -> *) a b.
Apply f =>
(a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
traverse1 a -> f b
f = forall (m :: Nat). Vec ('S m) a -> f (Vec ('S m) b)
go where
go :: Vec ('S m) a -> f (Vec ('S m) b)
go :: forall (m :: Nat). Vec ('S m) a -> f (Vec ('S m) b)
go (a
x ::: Vec n a
VNil) = (forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall a. Vec 'Z a
VNil) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x
go (a
x ::: xs :: Vec n a
xs@(a
_ ::: Vec n a
_)) = forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> forall (m :: Nat). Vec ('S m) a -> f (Vec ('S m) b)
go Vec n a
xs
#endif
itraverse :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse :: forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse Fin n -> a -> f b
_ Vec n a
VNil = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Vec 'Z a
VNil
itraverse Fin n -> a -> f b
f (a
x ::: Vec n a
xs) = forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Fin n -> a -> f b
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse (Fin n -> a -> f b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs
itraverse_ :: Applicative f => (Fin n -> a -> f b) -> Vec n a -> f ()
itraverse_ :: forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Fin n -> a -> f b) -> Vec n a -> f ()
itraverse_ Fin n -> a -> f b
_ Vec n a
VNil = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
itraverse_ Fin n -> a -> f b
f (a
x ::: Vec n a
xs) = Fin n -> a -> f b
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) (n :: Nat) a b.
Applicative f =>
(Fin n -> a -> f b) -> Vec n a -> f ()
itraverse_ (Fin n -> a -> f b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs
foldMap :: Monoid m => (a -> m) -> Vec n a -> m
foldMap :: forall m a (n :: Nat). Monoid m => (a -> m) -> Vec n a -> m
foldMap a -> m
_ Vec n a
VNil = forall a. Monoid a => a
mempty
foldMap a -> m
f (a
x ::: Vec n a
xs) = forall a. Monoid a => a -> a -> a
mappend (a -> m
f a
x) (forall m a (n :: Nat). Monoid m => (a -> m) -> Vec n a -> m
foldMap a -> m
f Vec n a
xs)
foldMap1 :: Semigroup s => (a -> s) -> Vec ('S n) a -> s
foldMap1 :: forall s a (n :: Nat). Semigroup s => (a -> s) -> Vec ('S n) a -> s
foldMap1 a -> s
f (a
x ::: Vec n a
VNil) = a -> s
f a
x
foldMap1 a -> s
f (a
x ::: xs :: Vec n a
xs@(a
_ ::: Vec n a
_)) = a -> s
f a
x forall a. Semigroup a => a -> a -> a
<> forall s a (n :: Nat). Semigroup s => (a -> s) -> Vec ('S n) a -> s
foldMap1 a -> s
f Vec n a
xs
ifoldMap :: Monoid m => (Fin n -> a -> m) -> Vec n a -> m
ifoldMap :: forall m (n :: Nat) a.
Monoid m =>
(Fin n -> a -> m) -> Vec n a -> m
ifoldMap Fin n -> a -> m
_ Vec n a
VNil = forall a. Monoid a => a
mempty
ifoldMap Fin n -> a -> m
f (a
x ::: Vec n a
xs) = forall a. Monoid a => a -> a -> a
mappend (Fin n -> a -> m
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x) (forall m (n :: Nat) a.
Monoid m =>
(Fin n -> a -> m) -> Vec n a -> m
ifoldMap (Fin n -> a -> m
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs)
ifoldMap1 :: Semigroup s => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
ifoldMap1 :: forall s (n :: Nat) a.
Semigroup s =>
(Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
ifoldMap1 Fin ('S n) -> a -> s
f (a
x ::: Vec n a
VNil) = Fin ('S n) -> a -> s
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x
ifoldMap1 Fin ('S n) -> a -> s
f (a
x ::: xs :: Vec n a
xs@(a
_ ::: Vec n a
_)) = Fin ('S n) -> a -> s
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x forall a. Semigroup a => a -> a -> a
<> forall s (n :: Nat) a.
Semigroup s =>
(Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
ifoldMap1 (Fin ('S n) -> a -> s
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs
foldr :: forall a b n. (a -> b -> b) -> b -> Vec n a -> b
foldr :: forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
foldr a -> b -> b
f b
z = forall (m :: Nat). Vec m a -> b
go where
go :: Vec m a -> b
go :: forall (m :: Nat). Vec m a -> b
go Vec m a
VNil = b
z
go (a
x ::: Vec n a
xs) = a -> b -> b
f a
x (forall (m :: Nat). Vec m a -> b
go Vec n a
xs)
ifoldr :: forall a b n. (Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr :: forall a b (n :: Nat). (Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr Fin n -> a -> b -> b
_ b
z Vec n a
VNil = b
z
ifoldr Fin n -> a -> b -> b
f b
z (a
x ::: Vec n a
xs) = Fin n -> a -> b -> b
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x (forall a b (n :: Nat). (Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr (Fin n -> a -> b -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) b
z Vec n a
xs)
foldl' :: forall a b n. (b -> a -> b) -> b -> Vec n a -> b
foldl' :: forall a b (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
foldl' b -> a -> b
f b
z = forall (m :: Nat). b -> Vec m a -> b
go b
z where
go :: b -> Vec m a -> b
go :: forall (m :: Nat). b -> Vec m a -> b
go !b
acc Vec m a
VNil = b
acc
go !b
acc (a
x ::: Vec n a
xs) = forall (m :: Nat). b -> Vec m a -> b
go (b -> a -> b
f b
acc a
x) Vec n a
xs
length :: Vec n a -> Int
length :: forall (n :: Nat) a. Vec n a -> Int
length = forall (n :: Nat) a. Int -> Vec n a -> Int
go Int
0 where
go :: Int -> Vec n a -> Int
go :: forall (n :: Nat) a. Int -> Vec n a -> Int
go !Int
acc Vec n a
VNil = Int
acc
go Int
acc (a
_ ::: Vec n a
xs) = forall (n :: Nat) a. Int -> Vec n a -> Int
go (Int
1 forall a. Num a => a -> a -> a
+ Int
acc) Vec n a
xs
null :: Vec n a -> Bool
null :: forall (n :: Nat) a. Vec n a -> Bool
null Vec n a
VNil = Bool
True
null (a
_ ::: Vec n a
_) = Bool
False
sum :: Num a => Vec n a -> a
sum :: forall a (n :: Nat). Num a => Vec n a -> a
sum Vec n a
VNil = a
0
sum (a
x ::: Vec n a
xs) = a
x forall a. Num a => a -> a -> a
+ forall a (n :: Nat). Num a => Vec n a -> a
sum Vec n a
xs
product :: Num a => Vec n a -> a
product :: forall a (n :: Nat). Num a => Vec n a -> a
product Vec n a
VNil = a
1
product (a
x ::: Vec n a
xs) = a
x forall a. Num a => a -> a -> a
* forall a (n :: Nat). Num a => Vec n a -> a
product Vec n a
xs
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
_ Vec n a
VNil Vec n b
VNil = forall a. Vec 'Z a
VNil
zipWith a -> b -> c
f (a
x ::: Vec n a
xs) (b
y ::: Vec n b
ys) = a -> b -> c
f a
x b
y forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith a -> b -> c
f Vec n a
xs Vec n b
ys
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
_ Vec n a
VNil Vec n b
VNil = forall a. Vec 'Z a
VNil
izipWith Fin n -> a -> b -> c
f (a
x ::: Vec n a
xs) (b
y ::: Vec n b
ys) = Fin n -> a -> b -> c
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x b
y forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec n a
xs Vec n b
ys
repeat :: N.SNatI n => x -> Vec n x
repeat :: forall (n :: Nat) x. SNatI n => x -> Vec n x
repeat x
x = 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. Vec 'Z a
VNil (x
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
:::)
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
VNil a -> Vec n b
_ = forall a. Vec 'Z a
VNil
bind (a
x ::: Vec n a
xs) a -> Vec n b
f = forall (n :: Nat) a. Vec ('S n) a -> a
head (a -> Vec n b
f a
x) forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall (n :: Nat) a b. Vec n a -> (a -> Vec n b) -> Vec n b
bind Vec n a
xs (forall (n :: Nat) a. Vec ('S n) a -> Vec n a
tail forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Vec n b
f)
join :: Vec n (Vec n a) -> Vec n a
join :: forall (n :: Nat) a. Vec n (Vec n a) -> Vec n a
join Vec n (Vec n a)
VNil = forall a. Vec 'Z a
VNil
join (Vec n a
x ::: Vec n (Vec n a)
xs) = forall (n :: Nat) a. Vec ('S n) a -> a
head Vec n a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall (n :: Nat) a. Vec n (Vec n a) -> Vec n a
join (forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map forall (n :: Nat) a. Vec ('S n) a -> Vec n a
tail Vec n (Vec n a)
xs)
universe :: N.SNatI n => Vec n (Fin n)
universe :: forall (n :: Nat). SNatI n => Vec n (Fin n)
universe = forall (n :: Nat). Universe n -> Vec n (Fin n)
getUniverse (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Universe 'Z
first forall (m :: Nat). Universe m -> Universe ('S m)
step) where
first :: Universe 'Z
first :: Universe 'Z
first = forall (n :: Nat). Vec n (Fin n) -> Universe n
Universe forall a. Vec 'Z a
VNil
step :: Universe m -> Universe ('S m)
step :: forall (m :: Nat). Universe m -> Universe ('S m)
step (Universe Vec m (Fin m)
go) = forall (n :: Nat). Vec n (Fin n) -> Universe n
Universe (forall (n1 :: Nat). Fin ('S n1)
FZ forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
map forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS Vec m (Fin m)
go)
newtype Universe n = Universe { forall (n :: Nat). Universe n -> Vec n (Fin n)
getUniverse :: Vec n (Fin n) }
class VecEach s t a b | s -> a, t -> b, s b -> t, t a -> s where
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 :: (forall (n :: Nat). SNatI n => Vec n a -> Vec n b)
-> (a, a') -> (b, b')
mapWithVec forall (n :: Nat). SNatI n => Vec n a -> Vec n b
f ~(a
x, a'
y) = case forall (n :: Nat). SNatI n => Vec n a -> Vec n b
f (a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a'
y forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall a. Vec 'Z a
VNil) of
b
x' ::: b
y' ::: Vec n b
VNil -> (b
x', b
y')
traverseWithVec :: forall (f :: * -> *).
Applicative f =>
(forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b))
-> (a, a') -> f (b, b')
traverseWithVec forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)
f ~(a
x, a'
y) = forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)
f (a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a'
y forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall a. Vec 'Z a
VNil) forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Vec ('S ('S 'Z)) b
res -> case Vec ('S ('S 'Z)) b
res of
b
x' ::: b
y' ::: Vec n b
VNil -> (b
x', b
y')
instance (a ~ a2, a ~ a3, b ~ b2, b ~ b3) => VecEach (a, a2, a3) (b, b2, b3) a b where
mapWithVec :: (forall (n :: Nat). SNatI n => Vec n a -> Vec n b)
-> (a, a2, a3) -> (b, b2, b3)
mapWithVec forall (n :: Nat). SNatI n => Vec n a -> Vec n b
f ~(a
x, a2
y, a3
z) = case forall (n :: Nat). SNatI n => Vec n a -> Vec n b
f (a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a2
y forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a3
z forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall a. Vec 'Z a
VNil) of
b
x' ::: b
y' ::: b
z' ::: Vec n b
VNil -> (b
x', b
y', b
z')
traverseWithVec :: forall (f :: * -> *).
Applicative f =>
(forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b))
-> (a, a2, a3) -> f (b, b2, b3)
traverseWithVec forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)
f ~(a
x, a2
y, a3
z) = forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)
f (a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a2
y forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a3
z forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall a. Vec 'Z a
VNil) forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Vec ('S ('S ('S 'Z))) b
res -> case Vec ('S ('S ('S 'Z))) b
res of
b
x' ::: b
y' ::: b
z' ::: Vec n b
VNil -> (b
x', b
y', b
z')
instance (a ~ a2, a ~ a3, a ~ a4, b ~ b2, b ~ b3, b ~ b4) => VecEach (a, a2, a3, a4) (b, b2, b3, b4) a b where
mapWithVec :: (forall (n :: Nat). SNatI n => Vec n a -> Vec n b)
-> (a, a2, a3, a4) -> (b, b2, b3, b4)
mapWithVec forall (n :: Nat). SNatI n => Vec n a -> Vec n b
f ~(a
x, a2
y, a3
z, a4
u) = case forall (n :: Nat). SNatI n => Vec n a -> Vec n b
f (a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a2
y forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a3
z forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a4
u forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall a. Vec 'Z a
VNil) of
b
x' ::: b
y' ::: b
z' ::: b
u' ::: Vec n b
VNil -> (b
x', b
y', b
z', b
u')
traverseWithVec :: forall (f :: * -> *).
Applicative f =>
(forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b))
-> (a, a2, a3, a4) -> f (b, b2, b3, b4)
traverseWithVec forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)
f ~(a
x, a2
y, a3
z, a4
u) = forall (n :: Nat). SNatI n => Vec n a -> f (Vec n b)
f (a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a2
y forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a3
z forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: a4
u forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: forall a. Vec 'Z a
VNil) forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Vec ('S ('S ('S ('S 'Z)))) b
res -> case Vec ('S ('S ('S ('S 'Z)))) b
res of
b
x' ::: b
y' ::: b
z' ::: b
u' ::: Vec n b
VNil -> (b
x', b
y', b
z', b
u')
instance N.SNatI n => QC.Arbitrary1 (Vec n) where
liftArbitrary :: forall a. Gen a -> Gen (Vec n a)
liftArbitrary = forall (n :: Nat) a. SNatI n => Gen a -> Gen (Vec n a)
liftArbitrary
liftShrink :: forall a. (a -> [a]) -> Vec n a -> [Vec n a]
liftShrink = forall (n :: Nat) a. SNatI n => (a -> [a]) -> Vec n a -> [Vec n a]
liftShrink
liftArbitrary :: forall n a. N.SNatI n => QC.Gen a -> QC.Gen (Vec n a)
liftArbitrary :: forall (n :: Nat) a. SNatI n => Gen a -> Gen (Vec n a)
liftArbitrary Gen a
arb = forall (n :: Nat) a. Arb n a -> Gen (Vec n a)
getArb forall a b. (a -> b) -> a -> b
$ 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 (n :: Nat) a. Gen (Vec n a) -> Arb n a
Arb (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Vec 'Z a
VNil)) forall (m :: Nat). Arb m a -> Arb ('S m) a
step where
step :: Arb m a -> Arb ('S m) a
step :: forall (m :: Nat). Arb m a -> Arb ('S m) a
step (Arb Gen (Vec m a)
rec) = forall (n :: Nat) a. Gen (Vec n a) -> Arb n a
Arb forall a b. (a -> b) -> a -> b
$ forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a
arb forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Vec m a)
rec
newtype Arb n a = Arb { forall (n :: Nat) a. Arb n a -> Gen (Vec n a)
getArb :: QC.Gen (Vec n a) }
liftShrink :: forall n a. N.SNatI n => (a -> [a]) -> Vec n a -> [Vec n a]
liftShrink :: forall (n :: Nat) a. SNatI n => (a -> [a]) -> Vec n a -> [Vec n a]
liftShrink a -> [a]
shr = forall (n :: Nat) a. Shr n a -> Vec n a -> [Vec n a]
getShr forall a b. (a -> b) -> a -> b
$ 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 (n :: Nat) a. (Vec n a -> [Vec n a]) -> Shr n a
Shr forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
VNil -> []) forall (m :: Nat). Shr m a -> Shr ('S m) a
step where
step :: Shr m a -> Shr ('S m) a
step :: forall (m :: Nat). Shr m a -> Shr ('S m) a
step (Shr Vec m a -> [Vec m a]
rec) = forall (n :: Nat) a. (Vec n a -> [Vec n a]) -> Shr n a
Shr forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) ->
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
(:::) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> * -> *) a b.
Arbitrary2 f =>
(a -> [a]) -> (b -> [b]) -> f a b -> [f a b]
QC.liftShrink2 a -> [a]
shr Vec m a -> [Vec m a]
rec (a
x, Vec n a
xs)
newtype Shr n a = Shr { forall (n :: Nat) a. Shr n a -> Vec n a -> [Vec n a]
getShr :: Vec n a -> [Vec n a] }
instance (N.SNatI n, QC.Arbitrary a) => QC.Arbitrary (Vec n a) where
arbitrary :: Gen (Vec n a)
arbitrary = forall (f :: * -> *) a. (Arbitrary1 f, Arbitrary a) => Gen (f a)
QC.arbitrary1
shrink :: Vec n a -> [Vec n a]
shrink = forall (f :: * -> *) a. (Arbitrary1 f, Arbitrary a) => f a -> [f a]
QC.shrink1
instance (N.SNatI n, QC.CoArbitrary a) => QC.CoArbitrary (Vec n a) where
coarbitrary :: forall b. Vec n a -> Gen b -> Gen b
coarbitrary Vec n a
v = case forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
SNat n
N.SZ -> forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
0 :: Int)
SNat n
N.SS -> forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
1 :: Int) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (case Vec n a
v of (a
x ::: Vec n a
xs) -> forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary (a
x, Vec n a
xs))
instance (N.SNatI n, QC.Function a) => QC.Function (Vec n a) where
function :: forall b. (Vec n a -> b) -> Vec n a :-> b
function = case forall (n :: Nat). SNatI n => SNat n
N.snat :: N.SNat n of
SNat n
N.SZ -> forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\Vec n a
VNil -> ()) (\() -> forall a. Vec 'Z a
VNil)
SNat n
N.SS -> forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap (\(a
x ::: Vec n a
xs) -> (a
x, Vec n a
xs)) (\(a
x,Vec n1 a
xs) -> a
x forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a
::: Vec n1 a
xs)