{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Vec.DataFamily.SpineStrict (
Vec (..),
empty,
singleton,
toPull,
fromPull,
toList,
toNonEmpty,
fromList,
fromListPrefix,
reifyList,
(!),
tabulate,
cons,
snoc,
head,
last,
tail,
init,
reverse,
(++),
split,
concatMap,
concat,
chunks,
foldMap,
foldMap1,
ifoldMap,
ifoldMap1,
foldr,
ifoldr,
length,
null,
sum,
product,
map,
imap,
traverse,
#ifdef MIN_VERSION_semigroupoids
traverse1,
#endif
itraverse,
itraverse_,
zipWith,
izipWith,
repeat,
bind,
join,
universe,
ensureSpine,
) where
import Prelude
(Bool (..), Eq (..), Functor (..), Int, Maybe (..), Monad (..), Num (..),
Ord (..), Ordering (EQ), Show (..), ShowS, const, flip, id, seq,
showParen, showString, uncurry, ($), (&&), (.))
import Control.Applicative (Applicative (..), liftA2, (<$>))
import Control.DeepSeq (NFData (..))
import Data.Fin (Fin (..))
import Data.List.NonEmpty (NonEmpty (..))
import Data.Hashable (Hashable (..))
import Data.Monoid (Monoid (..))
import Data.Nat (Nat (..))
import Data.Semigroup (Semigroup (..))
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
infixr 5 :::
data family Vec (n :: Nat) a
data instance Vec 'Z a = VNil
data instance Vec ('S n) a = a ::: !(Vec n a)
instance (Eq a, N.SNatI n) => Eq (Vec n a) where
== :: Vec n a -> Vec n a -> Bool
(==) = forall a b (n :: Nat). Equal a b n -> Vec n a -> Vec n b -> Bool
getEqual (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Equal a a 'Z
start forall (m :: Nat). Equal a a m -> Equal a a ('S m)
step) where
start :: Equal a a 'Z
start :: Equal a a 'Z
start = forall a b (n :: Nat). (Vec n a -> Vec n b -> Bool) -> Equal a b n
Equal forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ Vec 'Z a
_ -> Bool
True
step :: Equal a a m -> Equal a a ('S m)
step :: forall (m :: Nat). Equal a a m -> Equal a a ('S m)
step (Equal Vec m a -> Vec m a -> Bool
go) = forall a b (n :: Nat). (Vec n a -> Vec n b -> Bool) -> Equal a b n
Equal forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) (a
y ::: Vec m a
ys) ->
a
x forall a. Eq a => a -> a -> Bool
== a
y Bool -> Bool -> Bool
&& Vec m a -> Vec m a -> Bool
go Vec m a
xs Vec m a
ys
newtype Equal a b n = Equal { forall a b (n :: Nat). Equal a b n -> Vec n a -> Vec n b -> Bool
getEqual :: Vec n a -> Vec n b -> Bool }
instance (Ord a, N.SNatI n) => Ord (Vec n a) where
compare :: Vec n a -> Vec n a -> Ordering
compare = forall a b (n :: Nat).
Compare a b n -> Vec n a -> Vec n b -> Ordering
getCompare (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Compare a a 'Z
start forall (m :: Nat). Compare a a m -> Compare a a ('S m)
step) where
start :: Compare a a 'Z
start :: Compare a a 'Z
start = forall a b (n :: Nat).
(Vec n a -> Vec n b -> Ordering) -> Compare a b n
Compare forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ Vec 'Z a
_ -> Ordering
EQ
step :: Compare a a m -> Compare a a ('S m)
step :: forall (m :: Nat). Compare a a m -> Compare a a ('S m)
step (Compare Vec m a -> Vec m a -> Ordering
go) = forall a b (n :: Nat).
(Vec n a -> Vec n b -> Ordering) -> Compare a b n
Compare forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) (a
y ::: Vec m a
ys) ->
forall a. Ord a => a -> a -> Ordering
compare a
x a
y forall a. Semigroup a => a -> a -> a
<> Vec m a -> Vec m a -> Ordering
go Vec m a
xs Vec m a
ys
newtype Compare a b n = Compare { forall a b (n :: Nat).
Compare a b n -> Vec n a -> Vec n b -> Ordering
getCompare :: Vec n a -> Vec n b -> Ordering }
instance (Show a, N.SNatI n) => Show (Vec n a) where
showsPrec :: Int -> Vec n a -> ShowS
showsPrec = forall (n :: Nat) a. ShowsPrec n a -> Int -> Vec n a -> ShowS
getShowsPrec (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 ShowsPrec 'Z a
start forall (m :: Nat). ShowsPrec m a -> ShowsPrec ('S m) a
step) where
start :: ShowsPrec 'Z a
start :: ShowsPrec 'Z a
start = forall (n :: Nat) a. (Int -> Vec n a -> ShowS) -> ShowsPrec n a
ShowsPrec forall a b. (a -> b) -> a -> b
$ \Int
_ Vec 'Z a
_ -> String -> ShowS
showString String
"VNil"
step :: ShowsPrec m a -> ShowsPrec ('S m) a
step :: forall (m :: Nat). ShowsPrec m a -> ShowsPrec ('S m) a
step (ShowsPrec Int -> Vec m a -> ShowS
go) = forall (n :: Nat) a. (Int -> Vec n a -> ShowS) -> ShowsPrec n a
ShowsPrec forall a b. (a -> b) -> a -> b
$ \Int
d (a
x ::: Vec m 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
. Int -> Vec m a -> ShowS
go Int
5 Vec m a
xs
newtype ShowsPrec n a = ShowsPrec { forall (n :: Nat) a. ShowsPrec n a -> Int -> Vec n a -> ShowS
getShowsPrec :: Int -> Vec n a -> ShowS }
instance N.SNatI n => Functor (Vec n) where
fmap :: forall a b. (a -> b) -> Vec n a -> Vec n b
fmap = forall a b (n :: Nat). SNatI n => (a -> b) -> Vec n a -> Vec n b
map
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
foldr :: forall a b. (a -> b -> b) -> b -> Vec n a -> b
foldr = forall a b (n :: Nat).
SNatI n =>
(a -> b -> b) -> b -> Vec n a -> b
foldr
#if MIN_VERSION_base(4,8,0)
null :: forall a. Vec n a -> Bool
null = forall (n :: Nat) a. SNatI n => Vec n a -> Bool
null
length :: forall a. Vec n a -> Int
length = forall (n :: Nat) a. SNatI n => Vec n a -> Int
length
sum :: forall a. Num a => Vec n a -> a
sum = forall a (n :: Nat). (Num a, SNatI n) => Vec n a -> a
sum
product :: forall a. Num a => Vec n a -> a
product = forall a (n :: Nat). (Num a, SNatI n) => Vec n a -> a
product
#endif
#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 a (n :: Nat).
(Semigroup s, SNatI n) =>
(a -> s) -> Vec ('S n) a -> s
foldMap1
instance (N.SNatI m, 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, SNatI n) =>
(a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
traverse1
#endif
instance N.SNatI n => 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, SNatI n) =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse
instance N.SNatI n => 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.
SNatI n =>
(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 a (n :: Nat) m.
(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 a b (n :: Nat).
SNatI n =>
(Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr
instance N.SNatI n => 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 (n :: Nat) (f :: * -> *) a b.
(Applicative f, SNatI n) =>
(Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse
instance (NFData a, N.SNatI n) => NFData (Vec n a) where
rnf :: Vec n a -> ()
rnf = forall (n :: Nat) a. Rnf n a -> Vec n a -> ()
getRnf (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}. Rnf 'Z a
z forall {a} {n :: Nat}. NFData a => Rnf n a -> Rnf ('S n) a
s) where
z :: Rnf 'Z a
z = forall (n :: Nat) a. (Vec n a -> ()) -> Rnf n a
Rnf forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
R:VecZa a
VNil -> ()
s :: Rnf n a -> Rnf ('S n) a
s (Rnf Vec n a -> ()
rec) = forall (n :: Nat) a. (Vec n a -> ()) -> Rnf n a
Rnf forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec n a
xs) -> forall a. NFData a => a -> ()
rnf a
x seq :: forall a b. a -> b -> b
`seq` Vec n a -> ()
rec Vec n a
xs
newtype Rnf n a = Rnf { forall (n :: Nat) a. Rnf n a -> Vec n a -> ()
getRnf :: Vec n a -> () }
instance (Hashable a, N.SNatI n) => Hashable (Vec n a) where
hashWithSalt :: Int -> Vec n a -> Int
hashWithSalt = forall (n :: Nat) a. HashWithSalt n a -> Int -> Vec n a -> Int
getHashWithSalt (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}. HashWithSalt 'Z a
z forall {a} {n :: Nat}.
Hashable a =>
HashWithSalt n a -> HashWithSalt ('S n) a
s) where
z :: HashWithSalt 'Z a
z = forall (n :: Nat) a. (Int -> Vec n a -> Int) -> HashWithSalt n a
HashWithSalt forall a b. (a -> b) -> a -> b
$ \Int
salt Vec 'Z a
R:VecZa a
VNil -> Int
salt forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int)
s :: HashWithSalt n a -> HashWithSalt ('S n) a
s (HashWithSalt Int -> Vec n a -> Int
rec) = forall (n :: Nat) a. (Int -> Vec n a -> Int) -> HashWithSalt n a
HashWithSalt forall a b. (a -> b) -> a -> b
$ \Int
salt (a
x ::: Vec n a
xs) -> Int -> Vec n a -> Int
rec (Int
salt
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` a
x) Vec n a
xs
newtype HashWithSalt n a = HashWithSalt { forall (n :: Nat) a. HashWithSalt n a -> Int -> Vec n a -> Int
getHashWithSalt :: Int -> Vec n a -> Int }
instance N.SNatI n => Applicative (Vec n) where
pure :: forall a. a -> Vec n a
pure a
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 (a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
:::)
<*> :: forall a b. Vec n (a -> b) -> Vec n a -> Vec n b
(<*>) = forall a b c (n :: Nat).
SNatI n =>
(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).
SNatI n =>
(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.
SNatI n =>
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. SNatI n => 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. SNatI n => Vec n a -> Fin n -> a
(!)
#endif
#endif
instance (Semigroup a, N.SNatI n) => Semigroup (Vec n a) where
<> :: Vec n a -> Vec n a -> Vec n a
(<>) = forall a b c (n :: Nat).
SNatI n =>
(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).
SNatI n =>
(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 N.SNatI n => Apply (Vec n) where
<.> :: forall a b. Vec n (a -> b) -> Vec n a -> Vec n b
(<.>) = forall a b c (n :: Nat).
SNatI n =>
(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).
SNatI n =>
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith
instance N.SNatI n => I.Bind (Vec n) where
>>- :: forall a b. Vec n a -> (a -> Vec n b) -> Vec n b
(>>-) = forall (n :: Nat) a b.
SNatI n =>
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. SNatI n => Vec n (Vec n a) -> Vec n a
join
#endif
#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 N.SNatI n => Eq1 (Vec n) where
liftEq :: forall a b. (a -> b -> Bool) -> Vec n a -> Vec n b -> Bool
liftEq :: forall a b. (a -> b -> Bool) -> Vec n a -> Vec n b -> Bool
liftEq a -> b -> Bool
eq = forall a b (n :: Nat). Equal a b n -> Vec n a -> Vec n b -> Bool
getEqual (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Equal a b 'Z
start forall (m :: Nat). Equal a b m -> Equal a b ('S m)
step) where
start :: Equal a b 'Z
start :: Equal a b 'Z
start = forall a b (n :: Nat). (Vec n a -> Vec n b -> Bool) -> Equal a b n
Equal forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ Vec 'Z b
_ -> Bool
True
step :: Equal a b m -> Equal a b ('S m)
step :: forall (m :: Nat). Equal a b m -> Equal a b ('S m)
step (Equal Vec m a -> Vec m b -> Bool
go) = forall a b (n :: Nat). (Vec n a -> Vec n b -> Bool) -> Equal a b n
Equal forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) (b
y ::: Vec m b
ys) ->
a -> b -> Bool
eq a
x b
y Bool -> Bool -> Bool
&& Vec m a -> Vec m b -> Bool
go Vec m a
xs Vec m b
ys
instance N.SNatI n => Ord1 (Vec n) where
liftCompare :: forall a b. (a -> b -> Ordering) -> Vec n a -> Vec n b -> Ordering
liftCompare :: forall a b. (a -> b -> Ordering) -> Vec n a -> Vec n b -> Ordering
liftCompare a -> b -> Ordering
cmp = forall a b (n :: Nat).
Compare a b n -> Vec n a -> Vec n b -> Ordering
getCompare (forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction Compare a b 'Z
start forall (m :: Nat). Compare a b m -> Compare a b ('S m)
step) where
start :: Compare a b 'Z
start :: Compare a b 'Z
start = forall a b (n :: Nat).
(Vec n a -> Vec n b -> Ordering) -> Compare a b n
Compare forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ Vec 'Z b
_ -> Ordering
EQ
step :: Compare a b m -> Compare a b ('S m)
step :: forall (m :: Nat). Compare a b m -> Compare a b ('S m)
step (Compare Vec m a -> Vec m b -> Ordering
go) = forall a b (n :: Nat).
(Vec n a -> Vec n b -> Ordering) -> Compare a b n
Compare forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) (b
y ::: Vec m b
ys) ->
a -> b -> Ordering
cmp a
x b
y forall a. Semigroup a => a -> a -> a
<> Vec m a -> Vec m b -> Ordering
go Vec m a
xs Vec m b
ys
instance N.SNatI n => Show1 (Vec n) where
liftShowsPrec :: forall a. (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Vec n a -> ShowS
liftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Vec n a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
_ = forall (n :: Nat) a. ShowsPrec n a -> Int -> Vec n a -> ShowS
getShowsPrec (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 ShowsPrec 'Z a
start forall (m :: Nat). ShowsPrec m a -> ShowsPrec ('S m) a
step) where
start :: ShowsPrec 'Z a
start :: ShowsPrec 'Z a
start = forall (n :: Nat) a. (Int -> Vec n a -> ShowS) -> ShowsPrec n a
ShowsPrec forall a b. (a -> b) -> a -> b
$ \Int
_ Vec 'Z a
_ -> String -> ShowS
showString String
"VNil"
step :: ShowsPrec m a -> ShowsPrec ('S m) a
step :: forall (m :: Nat). ShowsPrec m a -> ShowsPrec ('S m) a
step (ShowsPrec Int -> Vec m a -> ShowS
go) = forall (n :: Nat) a. (Int -> Vec n a -> ShowS) -> ShowsPrec n a
ShowsPrec forall a b. (a -> b) -> a -> b
$ \Int
d (a
x ::: Vec m 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
. Int -> Vec m a -> ShowS
go Int
5 Vec m a
xs
#else
instance N.SNatI n => Eq1 (Vec n) where eq1 = (==)
instance N.SNatI n => Ord1 (Vec n) where compare1 = compare
instance N.SNatI n => 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 (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: forall a. Vec 'Z a
VNil
toPull :: forall n a. N.SNatI n => Vec n a -> P.Vec n a
toPull :: forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
toPull = forall (n :: Nat) a. ToPull n a -> Vec n a -> Vec n a
getToPull (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 ToPull 'Z a
start forall (m :: Nat). ToPull m a -> ToPull ('S m) a
step) where
start :: ToPull 'Z a
start :: ToPull 'Z a
start = forall (n :: Nat) a. (Vec n a -> Vec n a) -> ToPull n a
ToPull forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec forall b. Fin 'Z -> b
F.absurd
step :: ToPull m a -> ToPull ('S m) a
step :: forall (m :: Nat). ToPull m a -> ToPull ('S m) a
step (ToPull Vec m a -> Vec m a
f) = forall (n :: Nat) a. (Vec n a -> Vec n a) -> ToPull n a
ToPull forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) -> forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec forall a b. (a -> b) -> a -> b
$ \Fin ('S m)
i -> case Fin ('S m)
i of
Fin ('S m)
FZ -> a
x
FS Fin n1
i' -> forall (n :: Nat) a. Vec n a -> Fin n -> a
P.unVec (Vec m a -> Vec m a
f Vec m a
xs) Fin n1
i'
newtype ToPull n a = ToPull { forall (n :: Nat) a. ToPull n a -> Vec n a -> Vec n a
getToPull :: Vec n a -> P.Vec n a }
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 = forall (n :: Nat) a. FromPull n a -> Vec n a -> Vec n a
getFromPull (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 FromPull 'Z a
start forall (m :: Nat). FromPull m a -> FromPull ('S m) a
step) where
start :: FromPull 'Z a
start :: FromPull 'Z a
start = forall (n :: Nat) a. (Vec n a -> Vec n a) -> FromPull n a
FromPull forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a. Vec 'Z a
VNil
step :: FromPull m a -> FromPull ('S m) a
step :: forall (m :: Nat). FromPull m a -> FromPull ('S m) a
step (FromPull Vec m a -> Vec m a
f) = forall (n :: Nat) a. (Vec n a -> Vec n a) -> FromPull n a
FromPull forall a b. (a -> b) -> a -> b
$ \(P.Vec Fin ('S m) -> a
v) -> Fin ('S m) -> a
v forall (n1 :: Nat). Fin ('S n1)
FZ forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec m a -> Vec m a
f (forall (n :: Nat) a. (Fin n -> a) -> Vec n a
P.Vec (Fin ('S m) -> a
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS))
newtype FromPull n a = FromPull { forall (n :: Nat) a. FromPull n a -> Vec n a -> Vec n a
getFromPull :: P.Vec n a -> Vec n a }
toList :: forall n a. N.SNatI n => Vec n a -> [a]
toList :: forall (n :: Nat) a. SNatI n => Vec n a -> [a]
toList = forall (n :: Nat) a. ToList n a -> Vec n a -> [a]
getToList (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 ToList 'Z a
start forall (m :: Nat). ToList m a -> ToList ('S m) a
step) where
start :: ToList 'Z a
start :: ToList 'Z a
start = forall (n :: Nat) a. (Vec n a -> [a]) -> ToList n a
ToList (forall a b. a -> b -> a
const [])
step :: ToList m a -> ToList ('S m) a
step :: forall (m :: Nat). ToList m a -> ToList ('S m) a
step (ToList Vec m a -> [a]
f) = forall (n :: Nat) a. (Vec n a -> [a]) -> ToList n a
ToList forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) -> a
x forall a. a -> [a] -> [a]
: Vec m a -> [a]
f Vec m a
xs
newtype ToList n a = ToList { forall (n :: Nat) a. ToList n a -> Vec n a -> [a]
getToList :: Vec n a -> [a] }
toNonEmpty :: forall n a. N.SNatI n => Vec ('S n) a -> NonEmpty a
toNonEmpty :: forall (n :: Nat) a. SNatI n => 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. SNatI n => 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 (n :: Nat) a. 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 (n :: Nat) a. 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 (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec n a
xs')
flipIndex :: N.SNatI n => Fin n -> Vec n a -> a
flipIndex :: forall (n :: Nat) a. SNatI n => Fin n -> Vec n a -> a
flipIndex = forall (n :: Nat) a. Index n a -> Fin n -> Vec n a -> a
getIndex (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. Index 'Z a
start forall (m :: Nat) a. Index m a -> Index ('S m) a
step) where
start :: Index 'Z a
start :: forall a. Index 'Z a
start = forall (n :: Nat) a. (Fin n -> Vec n a -> a) -> Index n a
Index forall b. Fin 'Z -> b
F.absurd
step :: Index m a-> Index ('N.S m) a
step :: forall (m :: Nat) a. Index m a -> Index ('S m) a
step (Index Fin m -> Vec m a -> a
go) = forall (n :: Nat) a. (Fin n -> Vec n a -> a) -> Index n a
Index forall a b. (a -> b) -> a -> b
$ \Fin ('S m)
n (a
x ::: Vec m a
xs) -> case Fin ('S m)
n of
Fin ('S m)
FZ -> a
x
FS Fin n1
m -> Fin m -> Vec m a -> a
go Fin n1
m Vec m a
xs
newtype Index n a = Index { forall (n :: Nat) a. Index n a -> Fin n -> Vec n a -> a
getIndex :: Fin n -> Vec n a -> a }
(!) :: N.SNatI n => Vec n a -> Fin n -> a
! :: forall (n :: Nat) a. SNatI n => Vec n a -> Fin n -> a
(!) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (n :: Nat) a. SNatI n => Fin n -> Vec n a -> a
flipIndex
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 (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
(:::)
snoc :: forall n a. N.SNatI n => Vec n a -> a -> Vec ('S n) a
snoc :: forall (n :: Nat) a. SNatI n => Vec n a -> a -> Vec ('S n) a
snoc Vec n a
xs a
x = forall (n :: Nat) a. Snoc n a -> Vec n a -> Vec ('S n) a
getSnoc (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 Snoc 'Z a
start forall (m :: Nat). Snoc m a -> Snoc ('S m) a
step) Vec n a
xs where
start :: Snoc 'Z a
start :: Snoc 'Z a
start = forall (n :: Nat) a. (Vec n a -> Vec ('S n) a) -> Snoc n a
Snoc forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
ys -> a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec 'Z a
ys
step :: Snoc m a -> Snoc ('S m) a
step :: forall (m :: Nat). Snoc m a -> Snoc ('S m) a
step (Snoc Vec m a -> Vec ('S m) a
rec) = forall (n :: Nat) a. (Vec n a -> Vec ('S n) a) -> Snoc n a
Snoc forall a b. (a -> b) -> a -> b
$ \(a
y ::: Vec m a
ys) -> a
y forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec m a -> Vec ('S m) a
rec Vec m a
ys
newtype Snoc n a = Snoc { forall (n :: Nat) a. Snoc n a -> Vec n a -> Vec ('S n) a
getSnoc :: Vec n a -> Vec ('S n) a }
head :: Vec ('S n) a -> a
head :: forall (n :: Nat) a. Vec ('S n) a -> a
head (a
x ::: Vec n a
_) = a
x
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
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 ('S n) a
xs = forall (n :: Nat) a. Last n a -> Vec ('S n) a -> a
getLast (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 Last 'Z a
start forall (m :: Nat). Last m a -> Last ('S m) a
step) Vec ('S n) a
xs where
start :: Last 'Z a
start :: Last 'Z a
start = forall (n :: Nat) a. (Vec ('S n) a -> a) -> Last n a
Last forall a b. (a -> b) -> a -> b
$ \(a
x:::Vec 'Z a
R:VecZa a
VNil) -> a
x
step :: Last m a -> Last ('S m) a
step :: forall (m :: Nat). Last m a -> Last ('S m) a
step (Last Vec ('S m) a -> a
rec) = forall (n :: Nat) a. (Vec ('S n) a -> a) -> Last n a
Last forall a b. (a -> b) -> a -> b
$ \(a
_ ::: Vec ('S m) a
ys) -> Vec ('S m) a -> a
rec Vec ('S m) a
ys
newtype Last n a = Last { forall (n :: Nat) a. Last n a -> Vec ('S n) a -> a
getLast :: Vec ('S n) a -> a }
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 ('S n) a
xs = forall (n :: Nat) a. Init n a -> Vec ('S n) a -> Vec n a
getInit (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 Init 'Z a
start forall (m :: Nat). Init m a -> Init ('S m) a
step) Vec ('S n) a
xs where
start :: Init 'Z a
start :: Init 'Z a
start = forall (n :: Nat) a. (Vec ('S n) a -> Vec n a) -> Init n a
Init (forall a b. a -> b -> a
const forall a. Vec 'Z a
VNil)
step :: Init m a -> Init ('S m) a
step :: forall (m :: Nat). Init m a -> Init ('S m) a
step (Init Vec ('S m) a -> Vec m a
rec) = forall (n :: Nat) a. (Vec ('S n) a -> Vec n a) -> Init n a
Init forall a b. (a -> b) -> a -> b
$ \(a
y ::: Vec ('S m) a
ys) -> a
y forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec ('S m) a -> Vec m a
rec Vec ('S m) a
ys
newtype Init n a = Init { forall (n :: Nat) a. Init n a -> Vec ('S n) a -> Vec n a
getInit :: Vec ('S n) a -> Vec n a}
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 = forall (n :: Nat) a. Reverse n a -> Vec n a -> Vec n a
getReverse (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 Reverse 'Z a
start forall (m :: Nat). SNatI m => Reverse m a -> Reverse ('S m) a
step) where
start :: Reverse 'Z a
start :: Reverse 'Z a
start = forall (n :: Nat) a. (Vec n a -> Vec n a) -> Reverse n a
Reverse forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> forall a. Vec 'Z a
VNil
step :: N.SNatI m => Reverse m a -> Reverse ('S m) a
step :: forall (m :: Nat). SNatI m => Reverse m a -> Reverse ('S m) a
step (Reverse Vec m a -> Vec m a
rec) = forall (n :: Nat) a. (Vec n a -> Vec n a) -> Reverse n a
Reverse forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) -> forall (n :: Nat) a. SNatI n => Vec n a -> a -> Vec ('S n) a
snoc (Vec m a -> Vec m a
rec Vec m a
xs) a
x
newtype Reverse n a = Reverse { forall (n :: Nat) a. Reverse n a -> Vec n a -> Vec n a
getReverse :: Vec n a -> Vec n a }
infixr 5 ++
(++) :: forall n m a. N.SNatI n => Vec n a -> Vec m a -> Vec (N.Plus n m) a
Vec n a
as ++ :: forall (n :: Nat) (m :: Nat) a.
SNatI n =>
Vec n a -> Vec m a -> Vec (Plus n m) a
++ Vec m a
ys = forall (m :: Nat) (n :: Nat) a.
Append m n a -> Vec n a -> Vec (Plus n m) a
getAppend (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 Append m 'Z a
start forall (p :: Nat). Append m p a -> Append m ('S p) a
step) Vec n a
as where
start :: Append m 'Z a
start :: Append m 'Z a
start = forall (m :: Nat) (n :: Nat) a.
(Vec n a -> Vec (Plus n m) a) -> Append m n a
Append forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> Vec m a
ys
step :: Append m p a -> Append m ('S p) a
step :: forall (p :: Nat). Append m p a -> Append m ('S p) a
step (Append Vec p a -> Vec (Plus p m) a
f) = forall (m :: Nat) (n :: Nat) a.
(Vec n a -> Vec (Plus n m) a) -> Append m n a
Append forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec p a
xs) -> a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec p a -> Vec (Plus p m) a
f Vec p a
xs
newtype Append m n a = Append { forall (m :: Nat) (n :: Nat) a.
Append m n a -> Vec n a -> Vec (Plus n m) a
getAppend :: Vec n a -> Vec (N.Plus n m) a }
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 (Plus n m) a
xs) -> case Vec (Plus n m) a -> (Vec n a, Vec m a)
f Vec (Plus n m) a
xs of
(Vec n a
ys, Vec m a
zs) -> (a
x forall (n :: Nat) a. 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 :: forall a b n m. (N.SNatI m, N.SNatI n) => (a -> Vec m b) -> Vec n a -> Vec (N.Mult n m) b
concatMap :: forall a b (n :: Nat) (m :: Nat).
(SNatI m, SNatI n) =>
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap a -> Vec m b
f = forall (m :: Nat) a (n :: Nat) b.
ConcatMap m a n b -> Vec n a -> Vec (Mult n m) b
getConcatMap 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 ConcatMap m a 'Z b
start forall (p :: Nat). ConcatMap m a p b -> ConcatMap m a ('S p) b
step where
start :: ConcatMap m a 'Z b
start :: ConcatMap m a 'Z b
start = forall (m :: Nat) a (n :: Nat) b.
(Vec n a -> Vec (Mult n m) b) -> ConcatMap m a n b
ConcatMap forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> forall a. Vec 'Z a
VNil
step :: ConcatMap m a p b -> ConcatMap m a ('S p) b
step :: forall (p :: Nat). ConcatMap m a p b -> ConcatMap m a ('S p) b
step (ConcatMap Vec p a -> Vec (Mult p m) b
g) = forall (m :: Nat) a (n :: Nat) b.
(Vec n a -> Vec (Mult n m) b) -> ConcatMap m a n b
ConcatMap forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec p a
xs) -> a -> Vec m b
f a
x forall (n :: Nat) (m :: Nat) a.
SNatI n =>
Vec n a -> Vec m a -> Vec (Plus n m) a
++ Vec p a -> Vec (Mult p m) b
g Vec p a
xs
newtype ConcatMap m a n b = ConcatMap { forall (m :: Nat) a (n :: Nat) b.
ConcatMap m a n b -> Vec n a -> Vec (Mult n m) b
getConcatMap :: Vec n a -> Vec (N.Mult n m) b }
concat :: (N.SNatI m, N.SNatI n) => Vec n (Vec m a) -> Vec (N.Mult n m) a
concat :: forall (m :: Nat) (n :: Nat) a.
(SNatI m, SNatI n) =>
Vec n (Vec m a) -> Vec (Mult n m) a
concat = forall a b (n :: Nat) (m :: Nat).
(SNatI m, SNatI n) =>
(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 (n :: Nat) a. 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) }
map :: forall a b n. N.SNatI n => (a -> b) -> Vec n a -> Vec n b
map :: forall a b (n :: Nat). SNatI n => (a -> b) -> Vec n a -> Vec n b
map a -> b
f = forall a (n :: Nat) b. Map a n b -> Vec n a -> Vec n b
getMap 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 Map a 'Z b
start forall (m :: Nat). Map a m b -> Map a ('S m) b
step where
start :: Map a 'Z b
start :: Map a 'Z b
start = forall a (n :: Nat) b. (Vec n a -> Vec n b) -> Map a n b
Map forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> forall a. Vec 'Z a
VNil
step :: Map a m b -> Map a ('S m) b
step :: forall (m :: Nat). Map a m b -> Map a ('S m) b
step (Map Vec m a -> Vec m b
go) = forall a (n :: Nat) b. (Vec n a -> Vec n b) -> Map a n b
Map forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) -> a -> b
f a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec m a -> Vec m b
go Vec m a
xs
newtype Map a n b = Map { forall a (n :: Nat) b. Map a n b -> Vec n a -> Vec n b
getMap :: Vec n a -> Vec n b }
imap :: N.SNatI n => (Fin n -> a -> b) -> Vec n a -> Vec n b
imap :: forall (n :: Nat) a b.
SNatI n =>
(Fin n -> a -> b) -> Vec n a -> Vec n b
imap = forall a (n :: Nat) b.
IMap a n b -> (Fin n -> a -> b) -> Vec n a -> Vec n b
getIMap 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 a b. IMap a 'Z b
start forall a (m :: Nat) b. IMap a m b -> IMap a ('S m) b
step where
start :: IMap a 'Z b
start :: forall a b. IMap a 'Z b
start = forall a (n :: Nat) b.
((Fin n -> a -> b) -> Vec n a -> Vec n b) -> IMap a n b
IMap forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> b
_ Vec 'Z a
_ -> forall a. Vec 'Z a
VNil
step :: IMap a m b -> IMap a ('S m) b
step :: forall a (m :: Nat) b. IMap a m b -> IMap a ('S m) b
step (IMap (Fin m -> a -> b) -> Vec m a -> Vec m b
go) = forall a (n :: Nat) b.
((Fin n -> a -> b) -> Vec n a -> Vec n b) -> IMap a n b
IMap forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> b
f (a
x ::: Vec m a
xs) -> Fin ('S m) -> a -> b
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: (Fin m -> a -> b) -> Vec m a -> Vec m b
go (Fin ('S m) -> a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec m a
xs
newtype IMap a n b = IMap { forall a (n :: Nat) b.
IMap a n b -> (Fin n -> a -> b) -> Vec n a -> Vec n b
getIMap :: (Fin n -> a -> b) -> Vec n a -> Vec n b }
traverse :: forall n f a b. (Applicative f, N.SNatI n) => (a -> f b) -> Vec n a -> f (Vec n b)
traverse :: forall (n :: Nat) (f :: * -> *) a b.
(Applicative f, SNatI n) =>
(a -> f b) -> Vec n a -> f (Vec n b)
traverse a -> f b
f = forall (f :: * -> *) a (n :: Nat) b.
Traverse f a n b -> Vec n a -> f (Vec n b)
getTraverse 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 Traverse f a 'Z b
start forall (m :: Nat). Traverse f a m b -> Traverse f a ('S m) b
step where
start :: Traverse f a 'Z b
start :: Traverse f a 'Z b
start = forall (f :: * -> *) a (n :: Nat) b.
(Vec n a -> f (Vec n b)) -> Traverse f a n b
Traverse forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Vec 'Z a
VNil
step :: Traverse f a m b -> Traverse f a ('S m) b
step :: forall (m :: Nat). Traverse f a m b -> Traverse f a ('S m) b
step (Traverse Vec m a -> f (Vec m b)
go) = forall (f :: * -> *) a (n :: Nat) b.
(Vec n a -> f (Vec n b)) -> Traverse f a n b
Traverse forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) -> forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
(:::) (a -> f b
f a
x) (Vec m a -> f (Vec m b)
go Vec m a
xs)
{-# INLINE traverse #-}
newtype Traverse f a n b = Traverse { forall (f :: * -> *) a (n :: Nat) b.
Traverse f a n b -> Vec n a -> f (Vec n b)
getTraverse :: Vec n a -> f (Vec n b) }
#ifdef MIN_VERSION_semigroupoids
traverse1 :: forall n f a b. (Apply f, N.SNatI n) => (a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
traverse1 :: forall (n :: Nat) (f :: * -> *) a b.
(Apply f, SNatI n) =>
(a -> f b) -> Vec ('S n) a -> f (Vec ('S n) b)
traverse1 a -> f b
f = forall (f :: * -> *) a (n :: Nat) b.
Traverse1 f a n b -> Vec ('S n) a -> f (Vec ('S n) b)
getTraverse1 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 Traverse1 f a 'Z b
start forall (m :: Nat). Traverse1 f a m b -> Traverse1 f a ('S m) b
step where
start :: Traverse1 f a 'Z b
start :: Traverse1 f a 'Z b
start = forall (f :: * -> *) a (n :: Nat) b.
(Vec ('S n) a -> f (Vec ('S n) b)) -> Traverse1 f a n b
Traverse1 forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec 'Z a
_) -> (forall (n :: Nat) a. 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
step :: Traverse1 f a m b -> Traverse1 f a ('S m) b
step :: forall (m :: Nat). Traverse1 f a m b -> Traverse1 f a ('S m) b
step (Traverse1 Vec ('S m) a -> f (Vec ('S m) b)
go) = forall (f :: * -> *) a (n :: Nat) b.
(Vec ('S n) a -> f (Vec ('S n) b)) -> Traverse1 f a n b
Traverse1 forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec ('S m) a
xs) -> forall (f :: * -> *) a b c.
Apply f =>
(a -> b -> c) -> f a -> f b -> f c
liftF2 forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
(:::) (a -> f b
f a
x) (Vec ('S m) a -> f (Vec ('S m) b)
go Vec ('S m) a
xs)
newtype Traverse1 f a n b = Traverse1 { forall (f :: * -> *) a (n :: Nat) b.
Traverse1 f a n b -> Vec ('S n) a -> f (Vec ('S n) b)
getTraverse1 :: Vec ('S n) a -> f (Vec ('S n) b) }
#endif
itraverse :: forall n f a b. (Applicative f, N.SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse :: forall (n :: Nat) (f :: * -> *) a b.
(Applicative f, SNatI n) =>
(Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
itraverse = forall (f :: * -> *) a (n :: Nat) b.
ITraverse f a n b -> (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
getITraverse 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 ITraverse f a 'Z b
start forall (m :: Nat). ITraverse f a m b -> ITraverse f a ('S m) b
step where
start :: ITraverse f a 'Z b
start :: ITraverse f a 'Z b
start = forall (f :: * -> *) a (n :: Nat) b.
((Fin n -> a -> f b) -> Vec n a -> f (Vec n b))
-> ITraverse f a n b
ITraverse forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> f b
_ Vec 'Z a
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Vec 'Z a
VNil
step :: ITraverse f a m b -> ITraverse f a ('S m) b
step :: forall (m :: Nat). ITraverse f a m b -> ITraverse f a ('S m) b
step (ITraverse (Fin m -> a -> f b) -> Vec m a -> f (Vec m b)
go) = forall (f :: * -> *) a (n :: Nat) b.
((Fin n -> a -> f b) -> Vec n a -> f (Vec n b))
-> ITraverse f a n b
ITraverse forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> f b
f (a
x ::: Vec m a
xs) -> forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
(:::) (Fin ('S m) -> a -> f b
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x) ((Fin m -> a -> f b) -> Vec m a -> f (Vec m b)
go (Fin ('S m) -> a -> f b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec m a
xs)
{-# INLINE itraverse #-}
newtype ITraverse f a n b = ITraverse { forall (f :: * -> *) a (n :: Nat) b.
ITraverse f a n b -> (Fin n -> a -> f b) -> Vec n a -> f (Vec n b)
getITraverse :: (Fin n -> a -> f b) -> Vec n a -> f (Vec n b) }
itraverse_ :: forall n f a b. (Applicative f, N.SNatI n) => (Fin n -> a -> f b) -> Vec n a -> f ()
itraverse_ :: forall (n :: Nat) (f :: * -> *) a b.
(Applicative f, SNatI n) =>
(Fin n -> a -> f b) -> Vec n a -> f ()
itraverse_ = forall (f :: * -> *) a (n :: Nat) b.
ITraverse_ f a n b -> (Fin n -> a -> f b) -> Vec n a -> f ()
getITraverse_ 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 ITraverse_ f a 'Z b
start forall (m :: Nat). ITraverse_ f a m b -> ITraverse_ f a ('S m) b
step where
start :: ITraverse_ f a 'Z b
start :: ITraverse_ f a 'Z b
start = forall (f :: * -> *) a (n :: Nat) b.
((Fin n -> a -> f b) -> Vec n a -> f ()) -> ITraverse_ f a n b
ITraverse_ forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> f b
_ Vec 'Z a
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
step :: ITraverse_ f a m b -> ITraverse_ f a ('S m) b
step :: forall (m :: Nat). ITraverse_ f a m b -> ITraverse_ f a ('S m) b
step (ITraverse_ (Fin m -> a -> f b) -> Vec m a -> f ()
go) = forall (f :: * -> *) a (n :: Nat) b.
((Fin n -> a -> f b) -> Vec n a -> f ()) -> ITraverse_ f a n b
ITraverse_ forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> f b
f (a
x ::: Vec m a
xs) -> Fin ('S m) -> 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
*> (Fin m -> a -> f b) -> Vec m a -> f ()
go (Fin ('S m) -> a -> f b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec m a
xs
newtype ITraverse_ f a n b = ITraverse_ { forall (f :: * -> *) a (n :: Nat) b.
ITraverse_ f a n b -> (Fin n -> a -> f b) -> Vec n a -> f ()
getITraverse_ :: (Fin n -> a -> f b) -> Vec n a -> f () }
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 = forall a (n :: Nat) b. Fold a n b -> Vec n a -> b
getFold 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 a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold (forall a b. a -> b -> a
const forall a. Monoid a => a
mempty)) forall a b. (a -> b) -> a -> b
$ \(Fold Vec m a -> m
go) ->
forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) -> a -> m
f a
x forall a. Monoid a => a -> a -> a
`mappend` Vec m a -> m
go Vec m a
xs
newtype Fold a n b = Fold { forall a (n :: Nat) b. Fold a n b -> Vec n a -> b
getFold :: Vec n a -> b }
foldMap1 :: forall s a n. (Semigroup s, N.SNatI n) => (a -> s) -> Vec ('S n) a -> s
foldMap1 :: forall s a (n :: Nat).
(Semigroup s, SNatI n) =>
(a -> s) -> Vec ('S n) a -> s
foldMap1 a -> s
f = forall a (n :: Nat) b. Fold1 a n b -> Vec ('S n) a -> b
getFold1 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 Fold1 a 'Z s
start forall (m :: Nat). Fold1 a m s -> Fold1 a ('S m) s
step where
start :: Fold1 a 'Z s
start :: Fold1 a 'Z s
start = forall a (n :: Nat) b. (Vec ('S n) a -> b) -> Fold1 a n b
Fold1 forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec 'Z a
_) -> a -> s
f a
x
step :: Fold1 a m s -> Fold1 a ('S m) s
step :: forall (m :: Nat). Fold1 a m s -> Fold1 a ('S m) s
step (Fold1 Vec ('S m) a -> s
g) = forall a (n :: Nat) b. (Vec ('S n) a -> b) -> Fold1 a n b
Fold1 forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec ('S m) a
xs) -> a -> s
f a
x forall a. Semigroup a => a -> a -> a
<> Vec ('S m) a -> s
g Vec ('S m) a
xs
newtype Fold1 a n b = Fold1 { forall a (n :: Nat) b. Fold1 a n b -> Vec ('S n) a -> b
getFold1 :: Vec ('S n) a -> b }
ifoldMap :: forall a n m. (Monoid m, N.SNatI n) => (Fin n -> a -> m) -> Vec n a -> m
ifoldMap :: forall a (n :: Nat) m.
(Monoid m, SNatI n) =>
(Fin n -> a -> m) -> Vec n a -> m
ifoldMap = forall a (n :: Nat) m.
IFoldMap a n m -> (Fin n -> a -> m) -> Vec n a -> m
getIFoldMap 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 IFoldMap a 'Z m
start forall (p :: Nat). IFoldMap a p m -> IFoldMap a ('S p) m
step where
start :: IFoldMap a 'Z m
start :: IFoldMap a 'Z m
start = forall a (n :: Nat) m.
((Fin n -> a -> m) -> Vec n a -> m) -> IFoldMap a n m
IFoldMap forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> m
_ Vec 'Z a
_ -> forall a. Monoid a => a
mempty
step :: IFoldMap a p m -> IFoldMap a ('S p) m
step :: forall (p :: Nat). IFoldMap a p m -> IFoldMap a ('S p) m
step (IFoldMap (Fin p -> a -> m) -> Vec p a -> m
go) = forall a (n :: Nat) m.
((Fin n -> a -> m) -> Vec n a -> m) -> IFoldMap a n m
IFoldMap forall a b. (a -> b) -> a -> b
$ \Fin ('S p) -> a -> m
f (a
x ::: Vec p a
xs) -> Fin ('S p) -> a -> m
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x forall a. Monoid a => a -> a -> a
`mappend` (Fin p -> a -> m) -> Vec p a -> m
go (Fin ('S p) -> a -> m
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec p a
xs
newtype IFoldMap a n m = IFoldMap { forall a (n :: Nat) m.
IFoldMap a n m -> (Fin n -> a -> m) -> Vec n a -> m
getIFoldMap :: (Fin n -> a -> m) -> Vec n a -> m }
ifoldMap1 :: forall a n s. (Semigroup s, N.SNatI n) => (Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
ifoldMap1 :: forall a (n :: Nat) s.
(Semigroup s, SNatI n) =>
(Fin ('S n) -> a -> s) -> Vec ('S n) a -> s
ifoldMap1 = forall a (n :: Nat) m.
IFoldMap1 a n m -> (Fin ('S n) -> a -> m) -> Vec ('S n) a -> m
getIFoldMap1 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 IFoldMap1 a 'Z s
start forall (p :: Nat). IFoldMap1 a p s -> IFoldMap1 a ('S p) s
step where
start :: IFoldMap1 a 'Z s
start :: IFoldMap1 a 'Z s
start = forall a (n :: Nat) m.
((Fin ('S n) -> a -> m) -> Vec ('S n) a -> m) -> IFoldMap1 a n m
IFoldMap1 forall a b. (a -> b) -> a -> b
$ \Fin ('S 'Z) -> a -> s
f (a
x ::: Vec 'Z a
_) -> Fin ('S 'Z) -> a -> s
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x
step :: IFoldMap1 a p s -> IFoldMap1 a ('S p) s
step :: forall (p :: Nat). IFoldMap1 a p s -> IFoldMap1 a ('S p) s
step (IFoldMap1 (Fin ('S p) -> a -> s) -> Vec ('S p) a -> s
go) = forall a (n :: Nat) m.
((Fin ('S n) -> a -> m) -> Vec ('S n) a -> m) -> IFoldMap1 a n m
IFoldMap1 forall a b. (a -> b) -> a -> b
$ \Fin ('S ('S p)) -> a -> s
f (a
x ::: Vec ('S p) a
xs) -> Fin ('S ('S p)) -> a -> s
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x forall a. Semigroup a => a -> a -> a
<> (Fin ('S p) -> a -> s) -> Vec ('S p) a -> s
go (Fin ('S ('S p)) -> a -> s
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec ('S p) a
xs
newtype IFoldMap1 a n m = IFoldMap1 { forall a (n :: Nat) m.
IFoldMap1 a n m -> (Fin ('S n) -> a -> m) -> Vec ('S n) a -> m
getIFoldMap1 :: (Fin ('S n) -> a -> m) -> Vec ('S n) a -> m }
foldr :: forall a b n. N.SNatI n => (a -> b -> b) -> b -> Vec n a -> b
foldr :: forall a b (n :: Nat).
SNatI n =>
(a -> b -> b) -> b -> Vec n a -> b
foldr a -> b -> b
f b
z = forall a (n :: Nat) b. Fold a n b -> Vec n a -> b
getFold 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 Fold a 'Z b
start forall (m :: Nat). Fold a m b -> Fold a ('S m) b
step where
start :: Fold a 'Z b
start :: Fold a 'Z b
start = forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> b
z
step :: Fold a m b -> Fold a ('S m) b
step :: forall (m :: Nat). Fold a m b -> Fold a ('S m) b
step (Fold Vec m a -> b
go) = forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) -> a -> b -> b
f a
x (Vec m a -> b
go Vec m a
xs)
ifoldr :: forall a b n. N.SNatI n => (Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr :: forall a b (n :: Nat).
SNatI n =>
(Fin n -> a -> b -> b) -> b -> Vec n a -> b
ifoldr = forall a (n :: Nat) b.
IFoldr a n b -> (Fin n -> a -> b -> b) -> b -> Vec n a -> b
getIFoldr 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 IFoldr a 'Z b
start forall (m :: Nat). IFoldr a m b -> IFoldr a ('S m) b
step where
start :: IFoldr a 'Z b
start :: IFoldr a 'Z b
start = forall a (n :: Nat) b.
((Fin n -> a -> b -> b) -> b -> Vec n a -> b) -> IFoldr a n b
IFoldr forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> b -> b
_ b
z Vec 'Z a
_ -> b
z
step :: IFoldr a m b -> IFoldr a ('S m) b
step :: forall (m :: Nat). IFoldr a m b -> IFoldr a ('S m) b
step (IFoldr (Fin m -> a -> b -> b) -> b -> Vec m a -> b
go) = forall a (n :: Nat) b.
((Fin n -> a -> b -> b) -> b -> Vec n a -> b) -> IFoldr a n b
IFoldr forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> b -> b
f b
z (a
x ::: Vec m a
xs) -> Fin ('S m) -> a -> b -> b
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x ((Fin m -> a -> b -> b) -> b -> Vec m a -> b
go (Fin ('S m) -> 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 m a
xs)
newtype IFoldr a n b = IFoldr { forall a (n :: Nat) b.
IFoldr a n b -> (Fin n -> a -> b -> b) -> b -> Vec n a -> b
getIFoldr :: (Fin n -> a -> b -> b) -> b -> Vec n a -> b }
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). Length n -> Int
getLength Length n
l where
l :: Length n
l :: Length n
l = forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction (forall (n :: Nat). Int -> Length n
Length Int
0) forall a b. (a -> b) -> a -> b
$ \(Length Int
n) -> forall (n :: Nat). Int -> Length n
Length (Int
1 forall a. Num a => a -> a -> a
+ Int
n)
newtype Length (n :: Nat) = Length { forall (n :: Nat). Length n -> Int
getLength :: Int }
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 = forall a (n :: Nat) b. Fold a n b -> Vec n a -> b
getFold 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 a. Num a => Fold a 'Z a
start forall a (m :: Nat). Num a => Fold a m a -> Fold a ('S m) a
step where
start :: Num a => Fold a 'Z a
start :: forall a. Num a => Fold a 'Z a
start = forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> a
0
step :: Num a => Fold a m a -> Fold a ('S m) a
step :: forall a (m :: Nat). Num a => Fold a m a -> Fold a ('S m) a
step (Fold Vec m a -> a
f) = forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) -> a
x forall a. Num a => a -> a -> a
+ Vec m a -> a
f Vec m a
xs
product :: (Num a, N.SNatI n) => Vec n a -> a
product :: forall a (n :: Nat). (Num a, SNatI n) => Vec n a -> a
product = forall a (n :: Nat) b. Fold a n b -> Vec n a -> b
getFold 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 a. Num a => Fold a 'Z a
start forall a (m :: Nat). Num a => Fold a m a -> Fold a ('S m) a
step where
start :: Num a => Fold a 'Z a
start :: forall a. Num a => Fold a 'Z a
start = forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> a
1
step :: Num a => Fold a m a -> Fold a ('S m) a
step :: forall a (m :: Nat). Num a => Fold a m a -> Fold a ('S m) a
step (Fold Vec m a -> a
f) = forall a (n :: Nat) b. (Vec n a -> b) -> Fold a n b
Fold forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) -> a
x forall a. Num a => a -> a -> a
* Vec m a -> a
f Vec m a
xs
zipWith :: forall a b c n. N.SNatI n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith :: forall a b c (n :: Nat).
SNatI n =>
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith a -> b -> c
f = forall a b c (n :: Nat).
ZipWith a b c n -> Vec n a -> Vec n b -> Vec n c
getZipWith forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction ZipWith a b c 'Z
start forall (m :: Nat). ZipWith a b c m -> ZipWith a b c ('S m)
step where
start :: ZipWith a b c 'Z
start :: ZipWith a b c 'Z
start = forall a b c (n :: Nat).
(Vec n a -> Vec n b -> Vec n c) -> ZipWith a b c n
ZipWith forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ Vec 'Z b
_ -> forall a. Vec 'Z a
VNil
step :: ZipWith a b c m -> ZipWith a b c ('S m)
step :: forall (m :: Nat). ZipWith a b c m -> ZipWith a b c ('S m)
step (ZipWith Vec m a -> Vec m b -> Vec m c
go) = forall a b c (n :: Nat).
(Vec n a -> Vec n b -> Vec n c) -> ZipWith a b c n
ZipWith forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) (b
y ::: Vec m b
ys) -> a -> b -> c
f a
x b
y forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec m a -> Vec m b -> Vec m c
go Vec m a
xs Vec m b
ys
newtype ZipWith a b c n = ZipWith { forall a b c (n :: Nat).
ZipWith a b c n -> Vec n a -> Vec n b -> Vec n c
getZipWith :: Vec n a -> Vec n b -> Vec n c }
izipWith :: N.SNatI n => (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith :: forall (n :: Nat) a b c.
SNatI n =>
(Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
izipWith = forall a b c (n :: Nat).
IZipWith a b c n
-> (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
getIZipWith forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
N.induction forall a b c. IZipWith a b c 'Z
start forall a b c (m :: Nat). IZipWith a b c m -> IZipWith a b c ('S m)
step where
start :: IZipWith a b c 'Z
start :: forall a b c. IZipWith a b c 'Z
start = forall a b c (n :: Nat).
((Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c)
-> IZipWith a b c n
IZipWith forall a b. (a -> b) -> a -> b
$ \Fin 'Z -> a -> b -> c
_ Vec 'Z a
_ Vec 'Z b
_ -> forall a. Vec 'Z a
VNil
step :: IZipWith a b c m -> IZipWith a b c ('S m)
step :: forall a b c (m :: Nat). IZipWith a b c m -> IZipWith a b c ('S m)
step (IZipWith (Fin m -> a -> b -> c) -> Vec m a -> Vec m b -> Vec m c
go) = forall a b c (n :: Nat).
((Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c)
-> IZipWith a b c n
IZipWith forall a b. (a -> b) -> a -> b
$ \Fin ('S m) -> a -> b -> c
f (a
x ::: Vec m a
xs) (b
y ::: Vec m b
ys) -> Fin ('S m) -> a -> b -> c
f forall (n1 :: Nat). Fin ('S n1)
FZ a
x b
y forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: (Fin m -> a -> b -> c) -> Vec m a -> Vec m b -> Vec m c
go (Fin ('S m) -> a -> b -> c
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS) Vec m a
xs Vec m b
ys
newtype IZipWith a b c n = IZipWith { forall a b c (n :: Nat).
IZipWith a b c n
-> (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
getIZipWith :: (Fin n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c }
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 (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
:::)
bind :: N.SNatI n => Vec n a -> (a -> Vec n b) -> Vec n b
bind :: forall (n :: Nat) a b.
SNatI n =>
Vec n a -> (a -> Vec n b) -> Vec n b
bind = forall a (n :: Nat) b.
Bind a n b -> Vec n a -> (a -> Vec n b) -> Vec n b
getBind 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 a b. Bind a 'Z b
start forall a (m :: Nat) b. Bind a m b -> Bind a ('S m) b
step where
start :: Bind a 'Z b
start :: forall a b. Bind a 'Z b
start = forall a (n :: Nat) b.
(Vec n a -> (a -> Vec n b) -> Vec n b) -> Bind a n b
Bind forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ a -> Vec 'Z b
_ -> forall a. Vec 'Z a
VNil
step :: Bind a m b -> Bind a ('S m) b
step :: forall a (m :: Nat) b. Bind a m b -> Bind a ('S m) b
step (Bind Vec m a -> (a -> Vec m b) -> Vec m b
go) = forall a (n :: Nat) b.
(Vec n a -> (a -> Vec n b) -> Vec n b) -> Bind a n b
Bind forall a b. (a -> b) -> a -> b
$ \(a
x ::: Vec m a
xs) a -> Vec ('S m) b
f -> forall (n :: Nat) a. Vec ('S n) a -> a
head (a -> Vec ('S m) b
f a
x) forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec m a -> (a -> Vec m b) -> Vec m b
go Vec m 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 ('S m) b
f)
newtype Bind a n b = Bind { forall a (n :: Nat) b.
Bind a n b -> Vec n a -> (a -> Vec n b) -> Vec n b
getBind :: Vec n a -> (a -> Vec n b) -> Vec n b }
join :: N.SNatI n => Vec n (Vec n a) -> Vec n a
join :: forall (n :: Nat) a. SNatI n => Vec n (Vec n a) -> Vec n a
join = forall (n :: Nat) a. Join n a -> Vec n (Vec n a) -> Vec n a
getJoin 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 a. Join 'Z a
start forall (m :: Nat) a. SNatI m => Join m a -> Join ('S m) a
step where
start :: Join 'Z a
start :: forall a. Join 'Z a
start = forall (n :: Nat) a. (Vec n (Vec n a) -> Vec n a) -> Join n a
Join forall a b. (a -> b) -> a -> b
$ \Vec 'Z (Vec 'Z a)
_ -> forall a. Vec 'Z a
VNil
step :: N.SNatI m => Join m a -> Join ('S m) a
step :: forall (m :: Nat) a. SNatI m => Join m a -> Join ('S m) a
step (Join Vec m (Vec m a) -> Vec m a
go) = forall (n :: Nat) a. (Vec n (Vec n a) -> Vec n a) -> Join n a
Join forall a b. (a -> b) -> a -> b
$ \(Vec ('S m) a
x ::: Vec m (Vec ('S m) a)
xs) -> forall (n :: Nat) a. Vec ('S n) a -> a
head Vec ('S m) a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec m (Vec m a) -> Vec m a
go (forall a b (n :: Nat). SNatI n => (a -> b) -> Vec n a -> Vec n b
map forall (n :: Nat) a. Vec ('S n) a -> Vec n a
tail Vec m (Vec ('S m) a)
xs)
newtype Join n a = Join { forall (n :: Nat) a. Join n a -> Vec n (Vec n a) -> Vec n a
getJoin :: Vec n (Vec n a) -> Vec n a }
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). SNatI m => 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 :: N.SNatI m => Universe m -> Universe ('S m)
step :: forall (m :: Nat). SNatI m => 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 (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: forall a b (n :: Nat). SNatI n => (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) }
ensureSpine :: N.SNatI n => Vec n a -> Vec n a
ensureSpine :: forall (n :: Nat) a. SNatI n => Vec n a -> Vec n a
ensureSpine = forall (n :: Nat) a. EnsureSpine n a -> Vec n a -> Vec n a
getEnsureSpine (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. EnsureSpine 'Z a
first forall (m :: Nat) a. EnsureSpine m a -> EnsureSpine ('S m) a
step) where
first :: EnsureSpine 'Z a
first :: forall a. EnsureSpine 'Z a
first = forall (n :: Nat) a. (Vec n a -> Vec n a) -> EnsureSpine n a
EnsureSpine forall a b. (a -> b) -> a -> b
$ \Vec 'Z a
_ -> forall a. Vec 'Z a
VNil
step :: EnsureSpine m a -> EnsureSpine ('S m) a
step :: forall (m :: Nat) a. EnsureSpine m a -> EnsureSpine ('S m) a
step (EnsureSpine Vec m a -> Vec m a
go) = forall (n :: Nat) a. (Vec n a -> Vec n a) -> EnsureSpine n a
EnsureSpine forall a b. (a -> b) -> a -> b
$ \ ~(a
x ::: Vec m a
xs) -> a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec m a -> Vec m a
go Vec m a
xs
newtype EnsureSpine n a = EnsureSpine { forall (n :: Nat) a. EnsureSpine n a -> Vec n a -> Vec n a
getEnsureSpine :: Vec n a -> Vec n a }
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 (n :: Nat) a. 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
R:VecZa 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 m a
xs) ->
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (n :: Nat) a. 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 m 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 n1 a
xs) -> forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary (a
x, Vec n1 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
R:VecZa 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 n1 a
xs) -> (a
x, Vec n1 a
xs)) (\(a
x,Vec n1 a
xs) -> a
x forall (n :: Nat) a. a -> Vec n a -> Vec ('S n) a
::: Vec n1 a
xs)