clash-prelude-1.8.4: Clash: a functional hardware description language - Prelude library

Copyright | (C) 2013-2016 University of Twente 2017 Myrtle Software Ltd 2022-2025 QBayLogic B.V. 2024 Alex Mason
License | BSD2 (see the file LICENSE)
Maintainer | QBayLogic B.V. <devops@qbaylogic.com>
Safe Haskell | Trustworthy
Language | Haskell2010

Extensions

- Cpp
- UndecidableInstances
- MonoLocalBinds
- TemplateHaskell
- TemplateHaskellQuotes
- QuasiQuotes
- ScopedTypeVariables
- BangPatterns
- TypeFamilies
- ViewPatterns
- GADTs
- GADTSyntax
- DataKinds
- InstanceSigs
- StandaloneDeriving
- DeriveDataTypeable
- DeriveFunctor
- DeriveTraversable
- DeriveFoldable
- DeriveGeneric
- DefaultSignatures
- DeriveLift
- DerivingStrategies
- TypeSynonymInstances
- FlexibleInstances
- MagicHash
- KindSignatures
- PostfixOperators
- TupleSections
- RankNTypes
- TypeOperators
- ExplicitNamespaces
- ExplicitForAll
- LambdaCase
- BinaryLiterals
- PatternSynonyms
- TypeApplications

Clash.Sized.Vector

Contents

- `Vec`tor data type
- Accessors
  - Length information
  - Indexing
  - Extracting sub-vectors (slicing)
    - Splitting
- Construction
  - Initialization
    - Initialization from a list
  - Concatenation
- Modifying vectors
  - Permutations
    - Specialized permutations
- Element-wise operations
  - Mapping
  - Zipping
  - Unzipping
- Folding
  - Specialized folds
- Prefix sums (scans)
- Stencil computations
- Conversions
- Misc
- Primitives
  - `Traversable` instance
  - `BitPack` instance

Description

Synopsis

- data Vec (a :: Nat) b where
  - Nil :: forall b. Vec 0 b
  - Cons :: forall b (n :: Natural). b -> Vec n b -> Vec (n + 1) b
  - pattern (:>) :: a -> Vec n a -> Vec (n + 1) a
  - pattern (:<) :: Vec n a -> a -> Vec (n + 1) a
- length :: forall (n :: Nat) a. KnownNat n => Vec n a -> Int
- lengthS :: forall (n :: Nat) a. KnownNat n => Vec n a -> SNat n
- (!!) :: forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a
- head :: forall (n :: Natural) a. Vec (n + 1) a -> a
- last :: forall (n :: Natural) a. Vec (n + 1) a -> a
- at :: forall (m :: Nat) (n :: Natural) a. SNat m -> Vec (m + (n + 1)) a -> a
- indices :: forall (n :: Nat). KnownNat n => SNat n -> Vec n (Index n)
- indicesI :: forall (n :: Nat). KnownNat n => Vec n (Index n)
- findIndex :: forall (n :: Nat) a. KnownNat n => (a -> Bool) -> Vec n a -> Maybe (Index n)
- elemIndex :: forall (n :: Nat) a. (KnownNat n, Eq a) => a -> Vec n a -> Maybe (Index n)
- tail :: forall (n :: Natural) a. Vec (n + 1) a -> Vec n a
- init :: forall (n :: Natural) a. Vec (n + 1) a -> Vec n a
- take :: forall (m :: Nat) (n :: Natural) a. SNat m -> Vec (m + n) a -> Vec m a
- takeI :: forall (m :: Nat) (n :: Natural) a. KnownNat m => Vec (m + n) a -> Vec m a
- drop :: forall (m :: Nat) (n :: Natural) a. SNat m -> Vec (m + n) a -> Vec n a
- dropI :: forall (m :: Nat) (n :: Natural) a. KnownNat m => Vec (m + n) a -> Vec n a
- select :: forall (i :: Natural) (s :: Natural) (n :: Natural) (f :: Nat) a. CmpNat (i + s) (s * n) ~ 'GT => SNat f -> SNat s -> SNat n -> Vec (f + i) a -> Vec n a
- selectI :: forall (i :: Natural) (s :: Natural) (n :: Natural) (f :: Nat) a. (CmpNat (i + s) (s * n) ~ 'GT, KnownNat n) => SNat f -> SNat s -> Vec (f + i) a -> Vec n a
- splitAt :: forall (m :: Nat) (n :: Natural) a. SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
- splitAtI :: forall (m :: Nat) (n :: Natural) a. KnownNat m => Vec (m + n) a -> (Vec m a, Vec n a)
- unconcat :: forall (n :: Nat) (m :: Nat) a. KnownNat n => SNat m -> Vec (n * m) a -> Vec n (Vec m a)
- unconcatI :: forall (n :: Nat) (m :: Nat) a. (KnownNat n, KnownNat m) => Vec (n * m) a -> Vec n (Vec m a)
- singleton :: a -> Vec 1 a
- replicate :: forall (n :: Nat) a. SNat n -> a -> Vec n a
- repeat :: forall (n :: Nat) a. KnownNat n => a -> Vec n a
- iterate :: forall (n :: Nat) a. SNat n -> (a -> a) -> a -> Vec n a
- iterateI :: forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
- generate :: forall (n :: Nat) a. SNat n -> (a -> a) -> a -> Vec n a
- generateI :: forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a
- unfoldr :: forall (n :: Nat) s a. SNat n -> (s -> (a, s)) -> s -> Vec n a
- unfoldrI :: forall (n :: Nat) s a. KnownNat n => (s -> (a, s)) -> s -> Vec n a
- listToVecTH :: Lift a => [a] -> ExpQ
- (++) :: forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a
- (+>>) :: forall (n :: Nat) a. KnownNat n => a -> Vec n a -> Vec n a
- (<<+) :: forall (n :: Nat) a. Vec n a -> a -> Vec n a
- concat :: forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (n * m) a
- concatMap :: forall a (m :: Nat) b (n :: Nat). (a -> Vec m b) -> Vec n a -> Vec (n * m) b
- shiftInAt0 :: forall (n :: Nat) a (m :: Nat). KnownNat n => Vec n a -> Vec m a -> (Vec n a, Vec m a)
- shiftInAtN :: forall (m :: Nat) (n :: Nat) a. KnownNat m => Vec n a -> Vec m a -> (Vec n a, Vec m a)
- shiftOutFrom0 :: forall a (m :: Nat) (n :: Natural). (Default a, KnownNat m) => SNat m -> Vec (m + n) a -> (Vec (m + n) a, Vec m a)
- shiftOutFromN :: forall a (n :: Nat) (m :: Nat). (Default a, KnownNat n) => SNat m -> Vec (m + n) a -> (Vec (m + n) a, Vec m a)
- merge :: forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a -> Vec (2 * n) a
- replace :: forall (n :: Nat) i a. (KnownNat n, Enum i) => i -> a -> Vec n a -> Vec n a
- permute :: forall i (n :: Nat) (m :: Nat) a (k :: Natural). (Enum i, KnownNat n, KnownNat m) => (a -> a -> a) -> Vec n a -> Vec m i -> Vec (m + k) a -> Vec n a
- backpermute :: forall i (n :: Nat) a (m :: Nat). (Enum i, KnownNat n) => Vec n a -> Vec m i -> Vec m a
- scatter :: forall i (n :: Nat) (m :: Nat) a (k :: Natural). (Enum i, KnownNat n, KnownNat m) => Vec n a -> Vec m i -> Vec (m + k) a -> Vec n a
- gather :: forall i (n :: Nat) a (m :: Nat). (Enum i, KnownNat n) => Vec n a -> Vec m i -> Vec m a
- reverse :: forall (n :: Nat) a. Vec n a -> Vec n a
- transpose :: forall (n :: Nat) (m :: Nat) a. KnownNat n => Vec m (Vec n a) -> Vec n (Vec m a)
- interleave :: forall (n :: Nat) (d :: Nat) a. (KnownNat n, KnownNat d) => SNat d -> Vec (n * d) a -> Vec (d * n) a
- rotateLeft :: forall i (n :: Nat) a. (Enum i, KnownNat n) => Vec n a -> i -> Vec n a
- rotateRight :: forall i (n :: Nat) a. (Enum i, KnownNat n) => Vec n a -> i -> Vec n a
- rotateLeftS :: forall (n :: Nat) a (d :: Nat). KnownNat n => Vec n a -> SNat d -> Vec n a
- rotateRightS :: forall (n :: Nat) a (d :: Nat). KnownNat n => Vec n a -> SNat d -> Vec n a
- map :: forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
- imap :: forall (n :: Nat) a b. KnownNat n => (Index n -> a -> b) -> Vec n a -> Vec n b
- smap :: forall (k :: Nat) a b. KnownNat k => (forall (l :: Nat). SNat l -> a -> b) -> Vec k a -> Vec k b
- zipWith :: forall a b c (n :: Nat). (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
- zipWith3 :: forall a b c d (n :: Nat). (a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n d
- zipWith4 :: forall a b c d e (n :: Nat). (a -> b -> c -> d -> e) -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e
- zipWith5 :: forall a b c d e f (n :: Nat). (a -> b -> c -> d -> e -> f) -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n f
- zipWith6 :: forall a b c d e f g (n :: Nat). (a -> b -> c -> d -> e -> f -> g) -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n f -> Vec n g
- zipWith7 :: forall a b c d e f g h (n :: Nat). (a -> b -> c -> d -> e -> f -> g -> h) -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n f -> Vec n g -> Vec n h
- zip :: forall (n :: Nat) a b. Vec n a -> Vec n b -> Vec n (a, b)
- zip3 :: forall (n :: Nat) a b c. Vec n a -> Vec n b -> Vec n c -> Vec n (a, b, c)
- zip4 :: forall (n :: Nat) a b c d. Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n (a, b, c, d)
- zip5 :: forall (n :: Nat) a b c d e. Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n (a, b, c, d, e)
- zip6 :: forall (n :: Nat) a b c d e f. Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n f -> Vec n (a, b, c, d, e, f)
- zip7 :: forall (n :: Nat) a b c d e f g. Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n f -> Vec n g -> Vec n (a, b, c, d, e, f, g)
- izipWith :: forall (n :: Nat) a b c. KnownNat n => (Index n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
- unzip :: forall (n :: Nat) a b. Vec n (a, b) -> (Vec n a, Vec n b)
- unzip3 :: forall (n :: Nat) a b c. Vec n (a, b, c) -> (Vec n a, Vec n b, Vec n c)
- unzip4 :: forall (n :: Nat) a b c d. Vec n (a, b, c, d) -> (Vec n a, Vec n b, Vec n c, Vec n d)
- unzip5 :: forall (n :: Nat) a b c d e. Vec n (a, b, c, d, e) -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e)
- unzip6 :: forall (n :: Nat) a b c d e f. Vec n (a, b, c, d, e, f) -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f)
- unzip7 :: forall (n :: Nat) a b c d e f g. Vec n (a, b, c, d, e, f, g) -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f, Vec n g)
- foldr :: forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b
- foldl :: forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b
- foldr1 :: forall a (n :: Natural). (a -> a -> a) -> Vec (n + 1) a -> a
- foldl1 :: forall a (n :: Natural). (a -> a -> a) -> Vec (n + 1) a -> a
- fold :: forall (n :: Natural) a. (a -> a -> a) -> Vec (n + 1) a -> a
- ifoldr :: forall (n :: Nat) a b. KnownNat n => (Index n -> a -> b -> b) -> b -> Vec n a -> b
- ifoldl :: forall (n :: Nat) a b. KnownNat n => (a -> Index n -> b -> a) -> a -> Vec n b -> a
- dfold :: forall (p :: TyFun Nat Type -> Type) (k :: Nat) a. KnownNat k => Proxy p -> (forall (l :: Nat). SNat l -> a -> (p @@ l) -> p @@ (l + 1)) -> (p @@ 0) -> Vec k a -> p @@ k
- dtfold :: forall (p :: TyFun Nat Type -> Type) (k :: Nat) a. KnownNat k => Proxy p -> (a -> p @@ 0) -> (forall (l :: Nat). SNat l -> (p @@ l) -> (p @@ l) -> p @@ (l + 1)) -> Vec (2 ^ k) a -> p @@ k
- vfold :: forall (k :: Nat) a b. KnownNat k => (forall (l :: Nat). SNat l -> a -> Vec l b -> Vec (l + 1) b) -> Vec k a -> Vec k b
- maximum :: forall a (n :: Natural). Ord a => Vec (n + 1) a -> a
- minimum :: forall a (n :: Natural). Ord a => Vec (n + 1) a -> a
- scanl :: forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
- scanl1 :: forall (n :: Nat) a. KnownNat n => (a -> a -> a) -> Vec (n + 1) a -> Vec (n + 1) a
- scanr :: forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> Vec (n + 1) b
- scanr1 :: forall (n :: Nat) a. KnownNat n => (a -> a -> a) -> Vec (n + 1) a -> Vec (n + 1) a
- postscanl :: forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> Vec n b
- postscanr :: forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> Vec n b
- mapAccumL :: forall acc x y (n :: Nat). (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y)
- mapAccumR :: forall acc x y (n :: Nat). (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y)
- stencil1d :: forall (n :: Nat) (stX :: Natural) a b. KnownNat n => SNat (stX + 1) -> (Vec (stX + 1) a -> b) -> Vec ((stX + n) + 1) a -> Vec (n + 1) b
- stencil2d :: forall (n :: Nat) (m :: Nat) (stY :: Natural) (stX :: Natural) a b. (KnownNat n, KnownNat m) => SNat (stY + 1) -> SNat (stX + 1) -> (Vec (stY + 1) (Vec (stX + 1) a) -> b) -> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a) -> Vec (m + 1) (Vec (n + 1) b)
- windows1d :: forall (n :: Nat) (stX :: Natural) a. KnownNat n => SNat (stX + 1) -> Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a)
- windows2d :: forall (n :: Nat) (m :: Nat) (stY :: Natural) (stX :: Natural) a. (KnownNat n, KnownNat m) => SNat (stY + 1) -> SNat (stX + 1) -> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a) -> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
- toList :: forall (n :: Nat) a. Vec n a -> [a]
- fromList :: forall (n :: Nat) a. KnownNat n => [a] -> Maybe (Vec n a)
- unsafeFromList :: forall (n :: Nat) a. KnownNat n => [a] -> Vec n a
- bv2v :: forall (n :: Nat). KnownNat n => BitVector n -> Vec n Bit
- v2bv :: forall (n :: Nat). KnownNat n => Vec n Bit -> BitVector n
- lazyV :: forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a
- data VCons a (f :: TyFun Nat Type)
- asNatProxy :: forall (n :: Nat) a. Vec n a -> Proxy n
- seqV :: forall (n :: Nat) a b. KnownNat n => Vec n a -> b -> b
- forceV :: forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a
- seqVX :: forall (n :: Nat) a b. KnownNat n => Vec n a -> b -> b
- forceVX :: forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a
- traverse# :: forall a f b (n :: Nat). Applicative f => (a -> f b) -> Vec n a -> f (Vec n b)
- concatBitVector# :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) => Vec n (BitVector m) -> BitVector (n * m)
- unconcatBitVector# :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) => BitVector (n * m) -> Vec n (BitVector m)

# `Vec`tor data type

data Vec (a :: Nat) b where Source #

Fixed size vectors.

- Lists with their length encoded in their type
- `Vec`tor elements have an ASCENDING subscript starting from 0 and ending at ``length` - 1`.

Constructors

Nil :: forall b. Vec 0 b |
Cons :: forall b (n :: Natural). b -> Vec n b -> Vec (n + 1) b infixr 5 |

Bundled Patterns

pattern (:>) :: a -> Vec n a -> Vec (n + 1) a infixr 5

Add an element to the head of a vector.

    >>> 3:>4:>5:>Nil
    3 :> 4 :> 5 :> Nil
    >>> let x = 3:>4:>5:>Nil
    >>> :t x
    x :: Num a => Vec 3 a

Can be used as a pattern:

    >>> let f (x :> y :> _) = x + y
    >>> :t f
    f :: Num a => Vec ((n + 1) + 1) a -> a
    >>> f (3:>4:>5:>6:>7:>Nil)
    7

Also in conjunctions with (`:<`):

    >>> let g (a :> b :> (_ :< y :< x)) = a + b +  x + y
    >>> :t g
    g :: Num a => Vec ((((n + 1) + 1) + 1) + 1) a -> a
    >>> g (1:>2:>3:>4:>5:>Nil)
    12

pattern (:<) :: Vec n a -> a -> Vec (n + 1) a infixl 5

Add an element to the tail of a vector.

    >>> (3:>4:>5:>Nil) :< 1
    3 :> 4 :> 5 :> 1 :> Nil
    >>> let x = (3:>4:>5:>Nil) :< 1
    >>> :t x
    x :: Num a => Vec 4 a

Can be used as a pattern:

    >>> let f (_ :< y :< x) = y + x
    >>> :t f
    f :: Num a => Vec ((n + 1) + 1) a -> a
    >>> f (3:>4:>5:>6:>7:>Nil)
    13

Also in conjunctions with (`:>`):

    >>> let g (a :> b :> (_ :< y :< x)) = a + b +  x + y
    >>> :t g
    g :: Num a => Vec ((((n + 1) + 1) + 1) + 1) a -> a
    >>> g (1:>2:>3:>4:>5:>Nil)
    12

#### Instances

Instances details

Lift a => Lift (Vec n a :: Type) Source # |
Instance details Defined in Clash.Sized.Vector Methods lift :: Quote m => Vec n a -> m Exp Source # liftTyped :: forall (m :: Type -> Type). Quote m => Vec n a -> Code m (Vec n a) Source #
(KnownNat n, 1 <= n) => Foldable1 (Vec n) Source # |

Instance details

Defined in Clash.Sized.Vector

Methods

fold1 :: Semigroup m => Vec n m -> m Source #

foldMap1 :: Semigroup m => (a -> m) -> Vec n a -> m Source #

foldMap1' :: Semigroup m => (a -> m) -> Vec n a -> m Source #

toNonEmpty :: Vec n a -> NonEmpty a Source #

maximum :: Ord a => Vec n a -> a Source #

minimum :: Ord a => Vec n a -> a Source #

head :: Vec n a -> a Source #

last :: Vec n a -> a Source #

foldrMap1 :: (a -> b) -> (a -> b -> b) -> Vec n a -> b Source #

foldlMap1' :: (a -> b) -> (b -> a -> b) -> Vec n a -> b Source #

foldlMap1 :: (a -> b) -> (b -> a -> b) -> Vec n a -> b Source #

foldrMap1' :: (a -> b) -> (a -> b -> b) -> Vec n a -> b Source #

KnownNat n => Applicative (Vec n) Source # |
Instance details Defined in Clash.Sized.Vector Methods pure :: a -> Vec n a Source # (<*>) :: Vec n (a -> b) -> Vec n a -> Vec n b Source # liftA2 :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c Source # (*>) :: Vec n a -> Vec n b -> Vec n b Source # (<*) :: Vec n a -> Vec n b -> Vec n a Source #
Functor (Vec n) Source # |
Instance details Defined in Clash.Sized.Vector Methods fmap :: (a -> b) -> Vec n a -> Vec n b Source # (<$) :: a -> Vec n b -> Vec n a Source #
KnownNat n => Foldable (Vec n) Source # |

Instance details

Defined in Clash.Sized.Vector

Methods

fold :: Monoid m => Vec n m -> m Source #

foldMap :: Monoid m => (a -> m) -> Vec n a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Vec n a -> m Source #

foldr :: (a -> b -> b) -> b -> Vec n a -> b Source #

foldr' :: (a -> b -> b) -> b -> Vec n a -> b Source #

foldl :: (b -> a -> b) -> b -> Vec n a -> b Source #

foldl' :: (b -> a -> b) -> b -> Vec n a -> b Source #

foldr1 :: (a -> a -> a) -> Vec n a -> a Source #

foldl1 :: (a -> a -> a) -> Vec n a -> a Source #

toList :: Vec n a -> [a] Source #

null :: Vec n a -> Bool Source #

length :: Vec n a -> Int Source #

elem :: Eq a => a -> Vec n a -> Bool Source #

maximum :: Ord a => Vec n a -> a Source #

minimum :: Ord a => Vec n a -> a Source #

sum :: Num a => Vec n a -> a Source #

product :: Num a => Vec n a -> a Source #

KnownNat n => Traversable (Vec n) Source # |
Instance details Defined in Clash.Sized.Vector Methods traverse :: Applicative f => (a -> f b) -> Vec n a -> f (Vec n b) Source # sequenceA :: Applicative f => Vec n (f a) -> f (Vec n a) Source # mapM :: Monad m => (a -> m b) -> Vec n a -> m (Vec n b) Source # sequence :: Monad m => Vec n (m a) -> m (Vec n a) Source #
(KnownNat n, Arbitrary a) => Arbitrary (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector Methods arbitrary :: Gen (Vec n a) Source # shrink :: Vec n a -> [Vec n a] Source #
CoArbitrary a => CoArbitrary (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector Methods coarbitrary :: Vec n a -> Gen b -> Gen b Source #
(KnownNat n, AutoReg a) => AutoReg (Vec n a) Source # |
Instance details Defined in Clash.Class.AutoReg.Internal Methods autoReg :: forall (dom :: Domain). (HasCallStack, KnownDomain dom) => Clock dom -> Reset dom -> Enable dom -> Vec n a -> Signal dom (Vec n a) -> Signal dom (Vec n a) Source #
(KnownNat n, BitPack a) => BitPack (Vec n a) Source # |

Instance details

Defined in Clash.Sized.Vector

Associated Types

type BitSize (Vec n a) |
Instance details Defined in Clash.Sized.Vector type BitSize (Vec n a) = n * BitSize a

Methods

pack :: Vec n a -> BitVector (BitSize (Vec n a)) Source #

unpack :: BitVector (BitSize (Vec n a)) -> Vec n a Source #

KnownNat n => Bundle (Vec n a) Source # |
Instance details Defined in Clash.Signal.Bundle Methods bundle :: forall (dom :: Domain). Unbundled dom (Vec n a) -> Signal dom (Vec n a) Source # unbundle :: forall (dom :: Domain). Signal dom (Vec n a) -> Unbundled dom (Vec n a) Source #
KnownNat n => Bundle (Vec n a) Source # |
Instance details Defined in Clash.Signal.Delayed.Bundle Methods bundle :: forall (dom :: Domain) (d :: Nat). Unbundled dom d (Vec n a) -> DSignal dom d (Vec n a) Source # unbundle :: forall (dom :: Domain) (d :: Nat). DSignal dom d (Vec n a) -> Unbundled dom d (Vec n a) Source #
VecToTuple (Vec 0 a) Source # |

Instance details

Defined in Clash.Sized.Vector.ToTuple

Associated Types

type TupType (Vec 0 a) |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 0 a) = Tagged a ()

Methods

vecToTuple :: Vec 0 a -> TupType (Vec 0 a) Source #

VecToTuple (Vec 1 a) Source # | Instead of using `vecToTuple` for `Vec 1 _`, you could also consider using `head`

Instance details

Defined in Clash.Sized.Vector.ToTuple

Associated Types

type TupType (Vec 1 a) |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 1 a) = Solo a

Methods

vecToTuple :: Vec 1 a -> TupType (Vec 1 a) Source #

VecToTuple (Vec 2 a) Source # | NB: The documentation only shows instances up to 3-tuples. By default, instances up to and including 12-tuples will exist. If the flag `large-tuples` is set instances up to the GHC imposed limit will exist. The GHC imposed limit is either 62 or 64 depending on the GHC version.

Instance details

Defined in Clash.Sized.Vector.ToTuple

Associated Types

type TupType (Vec 2 a) |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 2 a) = (a, a)

Methods

vecToTuple :: Vec 2 a -> TupType (Vec 2 a) Source #

VecToTuple (Vec 3 a) Source # |

Instance details

Defined in Clash.Sized.Vector.ToTuple

Associated Types

type TupType (Vec 3 a) |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 3 a) = (a, a, a)

Methods

vecToTuple :: Vec 3 a -> TupType (Vec 3 a) Source #

VecToTuple (Vec 4 a) Source # |

Instance details

Defined in Clash.Sized.Vector.ToTuple

Associated Types

type TupType (Vec 4 a) |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 4 a) = (a, a, a, a)

Methods

vecToTuple :: Vec 4 a -> TupType (Vec 4 a) Source #

VecToTuple (Vec 5 a) Source # |

Instance details

Defined in Clash.Sized.Vector.ToTuple

Associated Types

type TupType (Vec 5 a) |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 5 a) = (a, a, a, a, a)

Methods

vecToTuple :: Vec 5 a -> TupType (Vec 5 a) Source #

VecToTuple (Vec 6 a) Source # |

Instance details

Defined in Clash.Sized.Vector.ToTuple

Associated Types

type TupType (Vec 6 a) |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 6 a) = (a, a, a, a, a, a)

Methods

vecToTuple :: Vec 6 a -> TupType (Vec 6 a) Source #

VecToTuple (Vec 7 a) Source # |

Instance details

Defined in Clash.Sized.Vector.ToTuple

Associated Types

type TupType (Vec 7 a) |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 7 a) = (a, a, a, a, a, a, a)

Methods

vecToTuple :: Vec 7 a -> TupType (Vec 7 a) Source #

VecToTuple (Vec 8 a) Source # |

Instance details

Defined in Clash.Sized.Vector.ToTuple

Associated Types

type TupType (Vec 8 a) |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 8 a) = (a, a, a, a, a, a, a, a)

Methods

vecToTuple :: Vec 8 a -> TupType (Vec 8 a) Source #

VecToTuple (Vec 9 a) Source # |

Instance details

Defined in Clash.Sized.Vector.ToTuple

Associated Types

type TupType (Vec 9 a) |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 9 a) = (a, a, a, a, a, a, a, a, a)

Methods

vecToTuple :: Vec 9 a -> TupType (Vec 9 a) Source #

VecToTuple (Vec 10 a) Source # |

Instance details

Defined in Clash.Sized.Vector.ToTuple

Associated Types

type TupType (Vec 10 a) |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 10 a) = (a, a, a, a, a, a, a, a, a, a)

Methods

vecToTuple :: Vec 10 a -> TupType (Vec 10 a) Source #

VecToTuple (Vec 11 a) Source # |

Instance details

Defined in Clash.Sized.Vector.ToTuple

Associated Types

type TupType (Vec 11 a) |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 11 a) = (a, a, a, a, a, a, a, a, a, a, a)

Methods

vecToTuple :: Vec 11 a -> TupType (Vec 11 a) Source #

VecToTuple (Vec 12 a) Source # |

Instance details

Defined in Clash.Sized.Vector.ToTuple

Associated Types

type TupType (Vec 12 a) |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 12 a) = (a, a, a, a, a, a, a, a, a, a, a, a)

Methods

vecToTuple :: Vec 12 a -> TupType (Vec 12 a) Source #

(NFDataX a, KnownNat n) => NFDataX (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector Methods deepErrorX :: String -> Vec n a Source # hasUndefined :: Vec n a -> Bool Source # ensureSpine :: Vec n a -> Vec n a Source # rnfX :: Vec n a -> () Source #
ShowX a => ShowX (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector Methods showsPrecX :: Int -> Vec n a -> ShowS Source # showX :: Vec n a -> String Source # showListX :: [Vec n a] -> ShowS Source #
(Default a, KnownNat n) => Default (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector Methods def :: Vec n a #
NFData a => NFData (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector Methods rnf :: Vec n a -> () Source #
(KnownNat n, Monoid a) => Monoid (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector Methods mempty :: Vec n a Source # mappend :: Vec n a -> Vec n a -> Vec n a Source # mconcat :: [Vec n a] -> Vec n a Source #
(KnownNat n, Semigroup a) => Semigroup (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector Methods (<>) :: Vec n a -> Vec n a -> Vec n a Source # sconcat :: NonEmpty (Vec n a) -> Vec n a Source # stimes :: Integral b => b -> Vec n a -> Vec n a Source #
(KnownNat n, Typeable a, Data a) => Data (Vec n a) Source # |

Instance details

Defined in Clash.Sized.Vector

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Vec n a -> c (Vec n a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Vec n a) Source #

toConstr :: Vec n a -> Constr Source #

dataTypeOf :: Vec n a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Vec n a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Vec n a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Vec n a -> Vec n a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Vec n a -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Vec n a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Vec n a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Vec n a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Vec n a -> m (Vec n a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Vec n a -> m (Vec n a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Vec n a -> m (Vec n a) Source #

KnownNat n => Generic (Vec n a) Source # | In many cases, this Generic instance only allows generic functions/instances over vectors of at least size 1, due to the n-1 in the Rep (Vec n a) definition. We'll have to wait for things like https://ryanglscott.github.io/2018/02/11/how-to-derive-generic-for-some-gadts/ before we can work around this limitation

Instance details

Defined in Clash.Sized.Vector

Associated Types

type Rep (Vec n a) |

Instance details

Defined in Clash.Sized.Vector

type Rep (Vec n a) = D1 ('MetaData "Vec" "Clash.Data.Vector" "clash-prelude" 'False) (C1 ('MetaCons "Nil" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Cons" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Vec (n - 1) a))))

Methods

from :: Vec n a -> Rep (Vec n a) x Source #

to :: Rep (Vec n a) x -> Vec n a Source #

Show a => Show (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector Methods showsPrec :: Int -> Vec n a -> ShowS Source # show :: Vec n a -> String Source # showList :: [Vec n a] -> ShowS Source #
(KnownNat n, Eq a) => Eq (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector Methods (==) :: Vec n a -> Vec n a -> Bool Source # (/=) :: Vec n a -> Vec n a -> Bool Source #
(KnownNat n, Ord a) => Ord (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector Methods compare :: Vec n a -> Vec n a -> Ordering Source # (<) :: Vec n a -> Vec n a -> Bool Source # (<=) :: Vec n a -> Vec n a -> Bool Source # (>) :: Vec n a -> Vec n a -> Bool Source # (>=) :: Vec n a -> Vec n a -> Bool Source # max :: Vec n a -> Vec n a -> Vec n a Source # min :: Vec n a -> Vec n a -> Vec n a Source #
KnownNat n => Ixed (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector Methods ix :: Index (Vec n a) -> Traversal' (Vec n a) (IxValue (Vec n a)) Source #
(LockStep en a, KnownNat n) => LockStep (Vec n en) (Vec n a) Source # |
Instance details Defined in Clash.Prelude.DataFlow Methods lockStep :: forall (dom :: Domain). DataFlow dom (Vec n en) Bool (Vec n a) (Vec n a) Source # stepLock :: forall (dom :: Domain). DataFlow dom Bool (Vec n en) (Vec n a) (Vec n a) Source #
type Unbundled t d (Vec n a) Source # |
Instance details Defined in Clash.Signal.Delayed.Bundle type Unbundled t d (Vec n a) = Vec n (DSignal t d a)
type TryDomain t (Vec n a) Source # |
Instance details Defined in Clash.Class.HasDomain.HasSingleDomain type TryDomain t (Vec n a) = TryDomain t a
type HasDomain dom (Vec n a) Source # |
Instance details Defined in Clash.Class.HasDomain.HasSpecificDomain type HasDomain dom (Vec n a) = HasDomain dom a
type Unbundled t (Vec n a) Source # |
Instance details Defined in Clash.Signal.Bundle type Unbundled t (Vec n a) = Vec n (Signal t a)
type BitSize (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector type BitSize (Vec n a) = n * BitSize a
type TupType (Vec 0 a) Source # |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 0 a) = Tagged a ()
type TupType (Vec 1 a) Source # |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 1 a) = Solo a
type TupType (Vec 2 a) Source # |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 2 a) = (a, a)
type TupType (Vec 3 a) Source # |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 3 a) = (a, a, a)
type TupType (Vec 4 a) Source # |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 4 a) = (a, a, a, a)
type TupType (Vec 5 a) Source # |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 5 a) = (a, a, a, a, a)
type TupType (Vec 6 a) Source # |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 6 a) = (a, a, a, a, a, a)
type TupType (Vec 7 a) Source # |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 7 a) = (a, a, a, a, a, a, a)
type TupType (Vec 8 a) Source # |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 8 a) = (a, a, a, a, a, a, a, a)
type TupType (Vec 9 a) Source # |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 9 a) = (a, a, a, a, a, a, a, a, a)
type TupType (Vec 10 a) Source # |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 10 a) = (a, a, a, a, a, a, a, a, a, a)
type TupType (Vec 11 a) Source # |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 11 a) = (a, a, a, a, a, a, a, a, a, a, a)
type TupType (Vec 12 a) Source # |
Instance details Defined in Clash.Sized.Vector.ToTuple type TupType (Vec 12 a) = (a, a, a, a, a, a, a, a, a, a, a, a)
type Rep (Vec n a) Source # |

Instance details

Defined in Clash.Sized.Vector

type Rep (Vec n a) = D1 ('MetaData "Vec" "Clash.Data.Vector" "clash-prelude" 'False) (C1 ('MetaCons "Nil" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Cons" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Vec (n - 1) a))))

type Index (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector type Index (Vec n a) = Index n
type IxValue (Vec n a) Source # |
Instance details Defined in Clash.Sized.Vector type IxValue (Vec n a) = a

# Accessors

## Length information

length :: forall (n :: Nat) a. KnownNat n => Vec n a -> Int Source #

The length of a `Vec`tor as an `Int` value.

    >>> length (6 :> 7 :> 8 :> Nil)
    3

lengthS :: forall (n :: Nat) a. KnownNat n => Vec n a -> SNat n Source #

Length of a `Vec`tor as an `SNat` value

## Indexing

(!!) :: forall (n :: Nat) i a. (KnownNat n, Enum i) => Vec n a -> i -> a Source #

"`xs` `!!` `n`" returns the n'th element of xs.

NB: Vector elements have an ASCENDING subscript starting from 0 and ending at ``length` - 1`.

    >>> (1:>2:>3:>4:>5:>Nil) !! 4
    5
    >>> (1:>2:>3:>4:>5:>Nil) !! (length (1:>2:>3:>4:>5:>Nil) - 1)
    5
    >>> (1:>2:>3:>4:>5:>Nil) !! 1
    2
    >>> (1:>2:>3:>4:>5:>Nil) !! 14
    *** Exception: Clash.Sized.Vector.(!!): index 14 is larger than maximum index 4
    ...

head :: forall (n :: Natural) a. Vec (n + 1) a -> a Source #

Extract the first element of a vector

    >>> head (1:>2:>3:>Nil)
    1

    >>> head Nil
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected: Vec (0 + 1) a
            Actual: Vec 0 a
        • In the first argument of ‘head’, namely ‘Nil’
          In the expression: head Nil
          In an equation for ‘it’: it = head Nil

# 448 "srcClashSized/Vector.hs"

last :: forall (n :: Natural) a. Vec (n + 1) a -> a Source #

Extract the last element of a vector

    >>> last (1:>2:>3:>Nil)
    3

    >>> last Nil
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected: Vec (0 + 1) a
            Actual: Vec 0 a
        • In the first argument of ‘last’, namely ‘Nil’
          In the expression: last Nil
          In an equation for ‘it’: it = last Nil

# 540 "srcClashSized/Vector.hs"

at :: forall (m :: Nat) (n :: Natural) a. SNat m -> Vec (m + (n + 1)) a -> a Source #

"`at` `n xs`" returns n'th element of xs

NB: Vector elements have an ASCENDING subscript starting from 0 and ending at ``length` - 1`.

    >>> at (SNat :: SNat 1) (1:>2:>3:>4:>5:>Nil)
    2
    >>> at d1               (1:>2:>3:>4:>5:>Nil)
    2

indices :: forall (n :: Nat). KnownNat n => SNat n -> Vec n (Index n) Source #

Generate a vector of indices.

    >>> indices d4
    0 :> 1 :> 2 :> 3 :> Nil

indicesI :: forall (n :: Nat). KnownNat n => Vec n (Index n) Source #

Generate a vector of indices, where the length of the vector is determined by the context.

    >>> indicesI :: Vec 4 (Index 4)
    0 :> 1 :> 2 :> 3 :> Nil

findIndex :: forall (n :: Nat) a. KnownNat n => (a -> Bool) -> Vec n a -> Maybe (Index n) Source #

"`findIndex` `p xs`" returns the index of the first element of xs satisfying the predicate p, or `Nothing` if there is no such element.

    >>> findIndex (> 3) (1:>3:>2:>4:>3:>5:>6:>Nil)
    Just 3
    >>> findIndex (> 8) (1:>3:>2:>4:>3:>5:>6:>Nil)
    Nothing

elemIndex :: forall (n :: Nat) a. (KnownNat n, Eq a) => a -> Vec n a -> Maybe (Index n) Source #

"`elemIndex` `a xs`" returns the index of the first element which is equal (by `==`) to the query element a, or `Nothing` if there is no such element.

    >>> elemIndex 3 (1:>3:>2:>4:>3:>5:>6:>Nil)
    Just 1
    >>> elemIndex 8 (1:>3:>2:>4:>3:>5:>6:>Nil)
    Nothing

## Extracting sub-vectors (slicing)

tail :: forall (n :: Natural) a. Vec (n + 1) a -> Vec n a Source #

Extract the elements after the head of a vector

    >>> tail (1:>2:>3:>Nil)
    2 :> 3 :> Nil

    >>> tail Nil
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected: Vec (0 + 1) a
            Actual: Vec 0 a
        • In the first argument of ‘tail’, namely ‘Nil’
          In the expression: tail Nil
          In an equation for ‘it’: it = tail Nil

# 494 "srcClashSized/Vector.hs"

init :: forall (n :: Natural) a. Vec (n + 1) a -> Vec n a Source #

Extract all the elements of a vector except the last element

    >>> init (1:>2:>3:>Nil)
    1 :> 2 :> Nil

    >>> init Nil
    <interactive>:...
        • Couldn't match type ‘1’ with ‘0’
          Expected: Vec (0 + 1) a
            Actual: Vec 0 a
        • In the first argument of ‘init’, namely ‘Nil’
          In the expression: init Nil
          In an equation for ‘it’: it = init Nil

# 587 "srcClashSized/Vector.hs"

take :: forall (m :: Nat) (n :: Natural) a. SNat m -> Vec (m + n) a -> Vec m a Source #

"`take` `n xs`" returns the n-length prefix of xs.

    >>> take (SNat :: SNat 3) (1:>2:>3:>4:>5:>Nil)
    1 :> 2 :> 3 :> Nil
    >>> take d3               (1:>2:>3:>4:>5:>Nil)
    1 :> 2 :> 3 :> Nil
    >>> take d0               (1:>2:>Nil)
    Nil

    >>> take d4               (1:>2:>Nil)
    <interactive>:...
        • Couldn't match type ‘4 + n0’ with ‘2’
          Expected: Vec (4 + n0) a
            Actual: Vec (1 + 1) a
          The type variable ‘n0’ is ambiguous
        • In the second argument of ‘take’, namely ‘(1 :> 2 :> Nil)’
          In the expression: take d4 (1 :> 2 :> Nil)
          In an equation for ‘it’: it = take d4 (1 :> 2 :> Nil)

# 1632 "srcClashSized/Vector.hs"

takeI :: forall (m :: Nat) (n :: Natural) a. KnownNat m => Vec (m + n) a -> Vec m a Source #

"`takeI` `xs`" returns the prefix of xs as demanded by the context.

    >>> takeI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
    1 :> 2 :> Nil

drop :: forall (m :: Nat) (n :: Natural) a. SNat m -> Vec (m + n) a -> Vec n a Source #

"`drop` `n xs`" returns the suffix of xs after the first n elements.

    >>> drop (SNat :: SNat 3) (1:>2:>3:>4:>5:>Nil)
    4 :> 5 :> Nil
    >>> drop d3               (1:>2:>3:>4:>5:>Nil)
    4 :> 5 :> Nil
    >>> drop d0               (1:>2:>Nil)
    1 :> 2 :> Nil

    >>> drop d4               (1:>2:>Nil)
    <interactive>:...: error:...
        • Couldn't match...type ‘4 + n0...
          The type variable ‘n0’ is ambiguous
        • In the first argument of ‘print’, namely ‘it’
          In a stmt of an interactive GHCi command: print it

# 1682 "srcClashSized/Vector.hs"

dropI :: forall (m :: Nat) (n :: Natural) a. KnownNat m => Vec (m + n) a -> Vec n a Source #

"`dropI` `xs`" returns the suffix of xs as demanded by the context.

    >>> dropI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
    4 :> 5 :> Nil

select :: forall (i :: Natural) (s :: Natural) (n :: Natural) (f :: Nat) a. CmpNat (i + s) (s * n) ~ 'GT => SNat f -> SNat s -> SNat n -> Vec (f + i) a -> Vec n a Source #

"`select` `f s n xs`" selects n elements with step-size s and offset `f` from xs.

    >>> select (SNat :: SNat 1) (SNat :: SNat 2) (SNat :: SNat 3) (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
    2 :> 4 :> 6 :> Nil
    >>> select d1 d2 d3 (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
    2 :> 4 :> 6 :> Nil

selectI :: forall (i :: Natural) (s :: Natural) (n :: Natural) (f :: Nat) a. (CmpNat (i + s) (s * n) ~ 'GT, KnownNat n) => SNat f -> SNat s -> Vec (f + i) a -> Vec n a Source #

"`selectI` `f s xs`" selects as many elements as demanded by the context with step-size s and offset f from xs.

    >>> selectI d1 d2 (1:>2:>3:>4:>5:>6:>7:>8:>Nil) :: Vec 2 Int
    2 :> 4 :> Nil

### Splitting

splitAt :: forall (m :: Nat) (n :: Natural) a. SNat m -> Vec (m + n) a -> (Vec m a, Vec n a) Source #

Split a vector into two vectors at the given point.

    >>> splitAt (SNat :: SNat 3) (1:>2:>3:>7:>8:>Nil)
    (1 :> 2 :> 3 :> Nil,7 :> 8 :> Nil)
    >>> splitAt d3 (1:>2:>3:>7:>8:>Nil)
    (1 :> 2 :> 3 :> Nil,7 :> 8 :> Nil)

splitAtI :: forall (m :: Nat) (n :: Natural) a. KnownNat m => Vec (m + n) a -> (Vec m a, Vec n a) Source #

Split a vector into two vectors where the length of the two is determined by the context.

    >>> splitAtI (1:>2:>3:>7:>8:>Nil) :: (Vec 2 Int, Vec 3 Int)
    (1 :> 2 :> Nil,3 :> 7 :> 8 :> Nil)

unconcat :: forall (n :: Nat) (m :: Nat) a. KnownNat n => SNat m -> Vec (n * m) a -> Vec n (Vec m a) Source #

Split a vector of (n * m) elements into a vector of "vectors of length m", where the length m is given.

    >>> unconcat d4 (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)
    (1 :> 2 :> 3 :> 4 :> Nil) :> (5 :> 6 :> 7 :> 8 :> Nil) :> (9 :> 10 :> 11 :> 12 :> Nil) :> Nil

unconcatI :: forall (n :: Nat) (m :: Nat) a. (KnownNat n, KnownNat m) => Vec (n * m) a -> Vec n (Vec m a) Source #

Split a vector of (n * m) elements into a vector of "vectors of length m", where the length m is determined by the context.

    >>> unconcatI (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil) :: Vec 2 (Vec 6 Int)
    (1 :> 2 :> 3 :> 4 :> 5 :> 6 :> Nil) :> (7 :> 8 :> 9 :> 10 :> 11 :> 12 :> Nil) :> Nil

# Construction

## Initialization

singleton :: a -> Vec 1 a Source #

Create a vector of one element

    >>> singleton 5
    5 :> Nil

replicate :: forall (n :: Nat) a. SNat n -> a -> Vec n a Source #

"`replicate` `n a`" returns a vector that has n copies of a.

    >>> replicate (SNat :: SNat 3) 6
    6 :> 6 :> 6 :> Nil
    >>> replicate d3 6
    6 :> 6 :> 6 :> Nil

repeat :: forall (n :: Nat) a. KnownNat n => a -> Vec n a Source #

"`repeat` `a`" creates a vector with as many copies of a as demanded by the context.

    >>> repeat 6 :: Vec 5 Int
    6 :> 6 :> 6 :> 6 :> 6 :> Nil

iterate :: forall (n :: Nat) a. SNat n -> (a -> a) -> a -> Vec n a Source #

"`iterate` `n f x`" returns a vector starting with x followed by n repeated applications of f to x.

    iterate (SNat :: SNat 4) f x == (x :> f x :> f (f x) :> f (f (f x)) :> Nil)
    iterate d4 f x               == (x :> f x :> f (f x) :> f (f (f x)) :> Nil)

    >>> iterate d4 (+1) 1
    1 :> 2 :> 3 :> 4 :> Nil

"`iterate` `n f z`" corresponds to the following circuit layout:

iterateI :: forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a Source #

"`iterateI` `f x`" returns a vector starting with `x` followed by `n` repeated applications of `f` to `x`, where `n` is determined by the context.

    iterateI f x :: Vec 3 a == (x :> f x :> f (f x) :> Nil)

    >>> iterateI (+1) 1 :: Vec 3 Int
    1 :> 2 :> 3 :> Nil

"`iterateI` `f z`" corresponds to the following circuit layout:

generate :: forall (n :: Nat) a. SNat n -> (a -> a) -> a -> Vec n a Source #

"`generate` `n f x`" returns a vector with `n` repeated applications of `f` to `x`.

    generate (SNat :: SNat 4) f x == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil)
    generate d4 f x               == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil)

    >>> generate d4 (+1) 1
    2 :> 3 :> 4 :> 5 :> Nil

"`generate` `n f z`" corresponds to the following circuit layout:

generateI :: forall (n :: Nat) a. KnownNat n => (a -> a) -> a -> Vec n a Source #

"`generateI` `f x`" returns a vector with `n` repeated applications of `f` to `x`, where `n` is determined by the context.

    generateI f x :: Vec 3 a == (f x :> f (f x) :> f (f (f x)) :> Nil)

    >>> generateI (+1) 1 :: Vec 3 Int
    2 :> 3 :> 4 :> Nil

"`generateI` `f z`" corresponds to the following circuit layout:

unfoldr :: forall (n :: Nat) s a. SNat n -> (s -> (a, s)) -> s -> Vec n a Source #

"`unfoldr` `n f s`" builds a vector of length `n` from a seed value `s`, where every element `a` is created by successive calls of `f` on `s`. Unlike `unfoldr` from Data.List the generating function `f` cannot dictate the length of the resulting vector, it must be statically known.

a simple use of `unfoldr`:

    >>> unfoldr d10 (\s -> (s,s-1)) 10
    10 :> 9 :> 8 :> 7 :> 6 :> 5 :> 4 :> 3 :> 2 :> 1 :> Nil

unfoldrI :: forall (n :: Nat) s a. KnownNat n => (s -> (a, s)) -> s -> Vec n a Source #

"`unfoldrI` `f s`" builds a vector from a seed value `s`, where every element `a` is created by successive calls of `f` on `s`; the length of the vector is inferred from the context. Unlike `unfoldr` from Data.List the generating function `f` cannot dictate the length of the resulting vector, it must be statically known.

a simple use of `unfoldrI`:

    >>> unfoldrI (\s -> (s,s-1)) 10 :: Vec 10 Int
    10 :> 9 :> 8 :> 7 :> 6 :> 5 :> 4 :> 3 :> 2 :> 1 :> Nil

### Initialization from a list

listToVecTH :: Lift a => [a] -> ExpQ Source #

Create a vector literal from a list literal.

    $(listToVecTH [1::Signed 8,2,3,4,5]) == (8:>2:>3:>4:>5:>Nil) :: Vec 5 (Signed 8)

    >>> [1 :: Signed 8,2,3,4,5]
    [1,2,3,4,5]
    >>> $(listToVecTH [1::Signed 8,2,3,4,5])
    1 :> 2 :> 3 :> 4 :> 5 :> Nil

## Concatenation

(++) :: forall (n :: Nat) a (m :: Nat). Vec n a -> Vec m a -> Vec (n + m) a infixr 5 Source #

Append two vectors.

    >>> (1:>2:>3:>Nil) ++ (7:>8:>Nil)
    1 :> 2 :> 3 :> 7 :> 8 :> Nil

(+>>) :: forall (n :: Nat) a. KnownNat n => a -> Vec n a -> Vec n a infixr 4 Source #

Add an element to the head of a vector, and extract all but the last element.

    >>> 1 +>> (3:>4:>5:>Nil)
    1 :> 3 :> 4 :> Nil
    >>> 1 +>> Nil
    Nil

(<<+) :: forall (n :: Nat) a. Vec n a -> a -> Vec n a infixl 4 Source #

Add an element to the tail of a vector, and extract all but the first element.

    >>> (3:>4:>5:>Nil) <<+ 1
    4 :> 5 :> 1 :> Nil
    >>> Nil <<+ 1
    Nil

concat :: forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (n * m) a Source #

Concatenate a vector of vectors.

    >>> concat ((1:>2:>3:>Nil) :> (4:>5:>6:>Nil) :> (7:>8:>9:>Nil) :> (10:>11:>12:>Nil) :> Nil)
    1 :> 2 :> 3 :> 4 :> 5 :> 6 :> 7 :> 8 :> 9 :> 10 :> 11 :> 12 :> Nil

concatMap :: forall a (m :: Nat) b (n :: Nat). (a -> Vec m b) -> Vec n a -> Vec (n * m) b Source #

Map a function over all the elements of a vector and concatentate the resulting vectors.

    >>> concatMap (replicate d3) (1:>2:>3:>Nil)
    1 :> 1 :> 1 :> 2 :> 2 :> 2 :> 3 :> 3 :> 3 :> Nil

shiftInAt0 Source #

Arguments

:: forall (n :: Nat) a (m :: Nat). KnownNat n |
=> Vec n a | The old vector
-> Vec m a | The elements to shift in at the head
-> (Vec n a, Vec m a) | (The new vector, shifted out elements)

Shift in elements to the head of a vector, bumping out elements at the tail. The result is a tuple containing:

- The new vector
- The shifted out elements

    >>> shiftInAt0 (1 :> 2 :> 3 :> 4 :> Nil) ((-1) :> 0 :> Nil)
    (-1 :> 0 :> 1 :> 2 :> Nil,3 :> 4 :> Nil)
    >>> shiftInAt0 (1 :> Nil) ((-1) :> 0 :> Nil)
    (-1 :> Nil,0 :> 1 :> Nil)

shiftInAtN Source #

Arguments

:: forall (m :: Nat) (n :: Nat) a. KnownNat m |
=> Vec n a | The old vector
-> Vec m a | The elements to shift in at the tail
-> (Vec n a, Vec m a) | (The new vector, shifted out elements)

Shift in element to the tail of a vector, bumping out elements at the head. The result is a tuple containing:

- The new vector
- The shifted out elements

    >>> shiftInAtN (1 :> 2 :> 3 :> 4 :> Nil) (5 :> 6 :> Nil)
    (3 :> 4 :> 5 :> 6 :> Nil,1 :> 2 :> Nil)
    >>> shiftInAtN (1 :> Nil) (2 :> 3 :> Nil)
    (3 :> Nil,1 :> 2 :> Nil)

shiftOutFrom0 Source #

Arguments

:: forall a (m :: Nat) (n :: Natural). (Default a, KnownNat m) |
=> SNat m | `m`, the number of elements to shift out
-> Vec (m + n) a | The old vector
-> (Vec (m + n) a, Vec m a) | (The new vector, shifted out elements)

Shift m elements out from the head of a vector, filling up the tail with `Default` values. The result is a tuple containing:

- The new vector
- The shifted out values

    >>> shiftOutFrom0 d2 ((1 :> 2 :> 3 :> 4 :> 5 :> Nil) :: Vec 5 Integer)
    (3 :> 4 :> 5 :> 0 :> 0 :> Nil,1 :> 2 :> Nil)

shiftOutFromN Source #

Arguments

:: forall a (n :: Nat) (m :: Nat). (Default a, KnownNat n) |
=> SNat m | `m`, the number of elements to shift out
-> Vec (m + n) a | The old vector
-> (Vec (m + n) a, Vec m a) | (The new vector, shifted out elements)

Shift m elements out from the tail of a vector, filling up the head with `Default` values. The result is a tuple containing:

- The new vector
- The shifted out values

    >>> shiftOutFromN d2 ((1 :> 2 :> 3 :> 4 :> 5 :> Nil) :: Vec 5 Integer)
    (0 :> 0 :> 1 :> 2 :> 3 :> Nil,4 :> 5 :> Nil)

merge :: forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a -> Vec (2 * n) a Source #

Merge two vectors, alternating their elements, i.e.,

    >>> merge (1 :> 2 :> 3 :> 4 :> Nil) (5 :> 6 :> 7 :> 8 :> Nil)
    1 :> 5 :> 2 :> 6 :> 3 :> 7 :> 4 :> 8 :> Nil

# Modifying vectors

replace :: forall (n :: Nat) i a. (KnownNat n, Enum i) => i -> a -> Vec n a -> Vec n a Source #

"`replace` `n a xs`" returns the vector xs where the n'th element is replaced by a.

NB: Vector elements have an ASCENDING subscript starting from 0 and ending at ``length` - 1`.

    >>> replace 3 7 (1:>2:>3:>4:>5:>Nil)
    1 :> 2 :> 3 :> 7 :> 5 :> Nil
    >>> replace 0 7 (1:>2:>3:>4:>5:>Nil)
    7 :> 2 :> 3 :> 4 :> 5 :> Nil
    >>> replace 9 7 (1:>2:>3:>4:>5:>Nil)
    1 :> 2 :> 3 :> 4 :> 5 :> *** Exception: Clash.Sized.Vector.replace: index 9 is larger than maximum index 4
    ...

## Permutations

permute Source #

Arguments

:: forall i (n :: Nat) (m :: Nat) a (k :: Natural). (Enum i, KnownNat n, KnownNat m) |
=> (a -> a -> a) | Combination function, f
-> Vec n a | Default values, def
-> Vec m i | Index mapping, is
-> Vec (m + k) a | Vector to be permuted, xs
-> Vec n a |

Forward permutation specified by an index mapping, ix. The result vector is initialized by the given defaults, def, and an further values that are permuted into the result are added to the current value using the given combination function, f.

The combination function must be associative and commutative.

backpermute Source #

Arguments

:: forall i (n :: Nat) a (m :: Nat). (Enum i, KnownNat n) |
=> Vec n a | Source vector, xs
-> Vec m i | Index mapping, is
-> Vec m a |

Backwards permutation specified by an index mapping, is, from the destination vector specifying which element of the source vector xs to read.

"`backpermute` `xs is`" is equivalent to "`map` `(xs `!!`) is`".

For example:

    >>> let input = 1:>9:>6:>4:>4:>2:>0:>1:>2:>Nil
    >>> let from  = 1:>3:>7:>2:>5:>3:>Nil
    >>> backpermute input from
    9 :> 4 :> 1 :> 6 :> 2 :> 4 :> Nil

scatter Source #

Arguments

:: forall i (n :: Nat) (m :: Nat) a (k :: Natural). (Enum i, KnownNat n, KnownNat m) |
=> Vec n a | Default values, def
-> Vec m i | Index mapping, is
-> Vec (m + k) a | Vector to be scattered, xs
-> Vec n a |

Copy elements from the source vector, xs, to the destination vector according to an index mapping is. This is a forward permute operation where a to vector encodes an input to output index mapping. Output elements for indices that are not mapped assume the value in the default vector def.

For example:

    >>> let defVec = 0:>0:>0:>0:>0:>0:>0:>0:>0:>Nil
    >>> let to = 1:>3:>7:>2:>5:>8:>Nil
    >>> let input = 1:>9:>6:>4:>4:>2:>5:>Nil
    >>> scatter defVec to input
    0 :> 1 :> 4 :> 9 :> 0 :> 4 :> 0 :> 6 :> 2 :> Nil

NB: If the same index appears in the index mapping more than once, the latest mapping is chosen.

gather Source #

Arguments

:: forall i (n :: Nat) a (m :: Nat). (Enum i, KnownNat n) |
=> Vec n a | Source vector, xs
-> Vec m i | Index mapping, is
-> Vec m a |

Backwards permutation specified by an index mapping, is, from the destination vector specifying which element of the source vector xs to read.

"`gather` `xs is`" is equivalent to "`map` `(xs `!!`) is`".

For example:

    >>> let input = 1:>9:>6:>4:>4:>2:>0:>1:>2:>Nil
    >>> let from  = 1:>3:>7:>2:>5:>3:>Nil
    >>> gather input from
    9 :> 4 :> 1 :> 6 :> 2 :> 4 :> Nil

### Specialized permutations

reverse :: forall (n :: Nat) a. Vec n a -> Vec n a Source #

The elements in a vector in reverse order.

    >>> reverse (1:>2:>3:>4:>Nil)
    4 :> 3 :> 2 :> 1 :> Nil

transpose :: forall (n :: Nat) (m :: Nat) a. KnownNat n => Vec m (Vec n a) -> Vec n (Vec m a) Source #

Transpose a matrix: go from row-major to column-major

    >>> let xss = (1:>2:>Nil):>(3:>4:>Nil):>(5:>6:>Nil):>Nil
    >>> xss
    (1 :> 2 :> Nil) :> (3 :> 4 :> Nil) :> (5 :> 6 :> Nil) :> Nil
    >>> transpose xss
    (1 :> 3 :> 5 :> Nil) :> (2 :> 4 :> 6 :> Nil) :> Nil

interleave Source #

Arguments

:: forall (n :: Nat) (d :: Nat) a. (KnownNat n, KnownNat d) |
=> SNat d | Interleave step, d
-> Vec (n * d) a |
-> Vec (d * n) a |

"`interleave` `d xs`" creates a vector:

    <x_0,x_d,x_(2d),...,x_1,x_(d+1),x_(2d+1),...,x_(d-1),x_(2d-1),x_(3d-1)>

    >>> let xs = 1 :> 2 :> 3 :> 4 :> 5 :> 6 :> 7 :> 8 :> 9 :> Nil
    >>> interleave d3 xs
    1 :> 4 :> 7 :> 2 :> 5 :> 8 :> 3 :> 6 :> 9 :> Nil

rotateLeft :: forall i (n :: Nat) a. (Enum i, KnownNat n) => Vec n a -> i -> Vec n a Source #

Dynamically rotate a `Vec`tor to the left:

    >>> let xs = 1 :> 2 :> 3 :> 4 :> Nil
    >>> rotateLeft xs 1
    2 :> 3 :> 4 :> 1 :> Nil
    >>> rotateLeft xs 2
    3 :> 4 :> 1 :> 2 :> Nil
    >>> rotateLeft xs (-1)
    4 :> 1 :> 2 :> 3 :> Nil

NB: Use `rotateLeftS` if you want to rotate left by a static amount.

rotateRight :: forall i (n :: Nat) a. (Enum i, KnownNat n) => Vec n a -> i -> Vec n a Source #

Dynamically rotate a `Vec`tor to the right:

    >>> let xs = 1 :> 2 :> 3 :> 4 :> Nil
    >>> rotateRight xs 1
    4 :> 1 :> 2 :> 3 :> Nil
    >>> rotateRight xs 2
    3 :> 4 :> 1 :> 2 :> Nil
    >>> rotateRight xs (-1)
    2 :> 3 :> 4 :> 1 :> Nil

NB: Use `rotateRightS` if you want to rotate right by a static amount.

rotateLeftS :: forall (n :: Nat) a (d :: Nat). KnownNat n => Vec n a -> SNat d -> Vec n a Source #

Statically rotate a `Vec`tor to the left:

    >>> let xs = 1 :> 2 :> 3 :> 4 :> Nil
    >>> rotateLeftS xs d1
    2 :> 3 :> 4 :> 1 :> Nil

NB: Use `rotateLeft` if you want to rotate left by a dynamic amount.

rotateRightS :: forall (n :: Nat) a (d :: Nat). KnownNat n => Vec n a -> SNat d -> Vec n a Source #

Statically rotate a `Vec`tor to the right:

    >>> let xs = 1 :> 2 :> 3 :> 4 :> Nil
    >>> rotateRightS xs d1
    4 :> 1 :> 2 :> 3 :> Nil

NB: Use `rotateRight` if you want to rotate right by a dynamic amount.

# Element-wise operations

## Mapping

map :: forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b Source #

"`map` `f xs`" is the vector obtained by applying f to each element of xs, i.e.,

    map f (x1 :> x2 :>  ... :> xn :> Nil) == (f x1 :> f x2 :> ... :> f xn :> Nil)

and corresponds to the following circuit layout:

imap :: forall (n :: Nat) a b. KnownNat n => (Index n -> a -> b) -> Vec n a -> Vec n b Source #

Apply a function of every element of a vector and its index.

    >>> :t imap (+) (2 :> 2 :> 2 :> 2 :> Nil)
    imap (+) (2 :> 2 :> 2 :> 2 :> Nil) :: Vec 4 (Index 4)
    >>> imap (+) (2 :> 2 :> 2 :> 2 :> Nil)
    2 :> 3 :> *** Exception: X: Clash.Sized.Index: result 4 is out of bounds: [0..3]
    ...
    >>> imap (\i a -> extend (bitCoerce i) + a) (2 :> 2 :> 2 :> 2 :> Nil) :: Vec 4 (Unsigned 8)
    2 :> 3 :> 4 :> 5 :> Nil

"`imap` `f xs`" corresponds to the following circuit layout:

smap :: forall (k :: Nat) a b. KnownNat k => (forall (l :: Nat). SNat l -> a -> b) -> Vec k a -> Vec k b Source #

Apply a function to every element of a vector and the element's position (as an `SNat` value) in the vector.

    >>> let rotateMatrix = smap (flip rotateRightS)
    >>> let xss = (1:>2:>3:>Nil):>(1:>2:>3:>Nil):>(1:>2:>3:>Nil):>Nil
    >>> xss
    (1 :> 2 :> 3 :> Nil) :> (1 :> 2 :> 3 :> Nil) :> (1 :> 2 :> 3 :> Nil) :> Nil
    >>> rotateMatrix xss
    (1 :> 2 :> 3 :> Nil) :> (3 :> 1 :> 2 :> Nil) :> (2 :> 3 :> 1 :> Nil) :> Nil

## Zipping

zipWith :: forall a b c (n :: Nat). (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c Source #

`zipWith` generalizes `zip` by zipping with the function given as the first argument, instead of a tupling function. For example, "`zipWith` `(+)`" applied to two vectors produces the vector of corresponding sums.

    zipWith f (x1 :> x2 :> ... xn :> Nil) (y1 :> y2 :> ... :> yn :> Nil) == (f x1 y1 :> f x2 y2 :> ... :> f xn yn :> Nil)

"`zipWith` `f xs ys`" corresponds to the following circuit layout:

NB: `zipWith` is strict in its second argument, and lazy in its third. This matters when `zipWith` is used in a recursive setting. See `lazyV` for more information.

zipWith3 :: forall a b c d (n :: Nat). (a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n d Source #

`zipWith3` generalizes `zip3` by zipping with the function given as the first argument, instead of a tupling function.

    zipWith3 f (x1 :> x2 :> ... xn :> Nil) (y1 :> y2 :> ... :> yn :> Nil) (z1 :> z2 :> ... :> zn :> Nil) == (f x1 y1 z1 :> f x2 y2 z2 :> ... :> f xn yn zn :> Nil)

"`zipWith3` `f xs ys zs`" corresponds to the following circuit layout:

NB: `zipWith3` is strict in its second argument, and lazy in its third and fourth. This matters when `zipWith3` is used in a recursive setting. See `lazyV` for more information.

zipWith4 :: forall a b c d e (n :: Nat). (a -> b -> c -> d -> e) -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e Source #

zipWith5 :: forall a b c d e f (n :: Nat). (a -> b -> c -> d -> e -> f) -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n f Source #

zipWith6 :: forall a b c d e f g (n :: Nat). (a -> b -> c -> d -> e -> f -> g) -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n f -> Vec n g Source #

zipWith7 :: forall a b c d e f g h (n :: Nat). (a -> b -> c -> d -> e -> f -> g -> h) -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n f -> Vec n g -> Vec n h Source #

zip :: forall (n :: Nat) a b. Vec n a -> Vec n b -> Vec n (a, b) Source #

`zip` takes two vectors and returns a vector of corresponding pairs.

    >>> zip (1:>2:>3:>4:>Nil) (4:>3:>2:>1:>Nil)
    (1,4) :> (2,3) :> (3,2) :> (4,1) :> Nil

zip3 :: forall (n :: Nat) a b c. Vec n a -> Vec n b -> Vec n c -> Vec n (a, b, c) Source #

`zip3` takes three vectors and returns a vector of corresponding triplets.

    >>> zip3 (1:>2:>3:>4:>Nil) (4:>3:>2:>1:>Nil) (5:>6:>7:>8:>Nil)
    (1,4,5) :> (2,3,6) :> (3,2,7) :> (4,1,8) :> Nil

zip4 :: forall (n :: Nat) a b c d. Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n (a, b, c, d) Source #

`zip4` takes four vectors and returns a list of quadruples, analogous to `zip`.

zip5 :: forall (n :: Nat) a b c d e. Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n (a, b, c, d, e) Source #

`zip5` takes five vectors and returns a list of five-tuples, analogous to `zip`.

zip6 :: forall (n :: Nat) a b c d e f. Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n f -> Vec n (a, b, c, d, e, f) Source #

`zip6` takes six vectors and returns a list of six-tuples, analogous to `zip`.

zip7 :: forall (n :: Nat) a b c d e f g. Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n f -> Vec n g -> Vec n (a, b, c, d, e, f, g) Source #

`zip7` takes seven vectors and returns a list of seven-tuples, analogous to `zip`.

izipWith :: forall (n :: Nat) a b c. KnownNat n => (Index n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c Source #

Zip two vectors with a functions that also takes the elements' indices.

    >>> izipWith (\i a b -> i + a + b) (2 :> 2 :> Nil)  (3 :> 3:> Nil)
    *** Exception: X: Clash.Sized.Index: result 2 is out of bounds: [0..1]
    ...
    >>> izipWith (\i a b -> extend (bitCoerce i) + a + b) (2 :> 2 :> Nil) (3 :> 3 :> Nil) :: Vec 2 (Unsigned 8)
    5 :> 6 :> Nil

"`imap` `f xs`" corresponds to the following circuit layout:

NB: `izipWith` is strict in its second argument, and lazy in its third. This matters when `izipWith` is used in a recursive setting. See `lazyV` for more information.

## Unzipping

unzip :: forall (n :: Nat) a b. Vec n (a, b) -> (Vec n a, Vec n b) Source #

`unzip` transforms a vector of pairs into a vector of first components and a vector of second components.

    >>> unzip ((1,4):>(2,3):>(3,2):>(4,1):>Nil)
    (1 :> 2 :> 3 :> 4 :> Nil,4 :> 3 :> 2 :> 1 :> Nil)

unzip3 :: forall (n :: Nat) a b c. Vec n (a, b, c) -> (Vec n a, Vec n b, Vec n c) Source #

`unzip3` transforms a vector of triplets into a vector of first components, a vector of second components, and a vector of third components.

    >>> unzip3 ((1,4,5):>(2,3,6):>(3,2,7):>(4,1,8):>Nil)
    (1 :> 2 :> 3 :> 4 :> Nil,4 :> 3 :> 2 :> 1 :> Nil,5 :> 6 :> 7 :> 8 :> Nil)

unzip4 :: forall (n :: Nat) a b c d. Vec n (a, b, c, d) -> (Vec n a, Vec n b, Vec n c, Vec n d) Source #

`unzip4` takes a vector of quadruples and returns four vectors, analogous to `unzip`.

unzip5 :: forall (n :: Nat) a b c d e. Vec n (a, b, c, d, e) -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e) Source #

`unzip5` takes a vector of five-tuples and returns five vectors, analogous to `unzip`.

unzip6 :: forall (n :: Nat) a b c d e f. Vec n (a, b, c, d, e, f) -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f) Source #

`unzip6` takes a vector of six-tuples and returns six vectors, analogous to `unzip`.

unzip7 :: forall (n :: Nat) a b c d e f g. Vec n (a, b, c, d, e, f, g) -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e, Vec n f, Vec n g) Source #

`unzip7` takes a vector of seven-tuples and returns seven vectors, analogous to `unzip`.

# Folding

foldr :: forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> b Source #

`foldr`, applied to a binary operator, a starting value (typically the right-identity of the operator), and a vector, reduces the vector using the binary operator, from right to left:

    foldr f z (x1 :> ... :> xn1 :> xn :> Nil) == x1 `f` (... (xn1 `f` (xn `f` z))...)
    foldr r z Nil                             == z

    >>> foldr (/) 1 (5 :> 4 :> 3 :> 2 :> Nil)
    1.875

"`foldr` `f z xs`" corresponds to the following circuit layout:

NB: `"`foldr` f z xs"` produces a linear structure, which has a depth, or delay, of O(``length` xs`). Use `fold` if your binary operator `f` is associative, as `"`fold` f xs"` produces a structure with a depth of O(log_2(``length` xs`)).

foldl :: forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> b Source #

`foldl`, applied to a binary operator, a starting value (typically the left-identity of the operator), and a vector, reduces the vector using the binary operator, from left to right:

    foldl f z (x1 :> x2 :> ... :> xn :> Nil) == (...((z `f` x1) `f` x2) `f`...) `f` xn
    foldl f z Nil                            == z

    >>> foldl (/) 1 (5 :> 4 :> 3 :> 2 :> Nil)
    8.333333333333333e-3

"`foldl` `f z xs`" corresponds to the following circuit layout:

NB: `"`foldl` f z xs"` produces a linear structure, which has a depth, or delay, of O(``length` xs`). Use `fold` if your binary operator `f` is associative, as `"`fold` f xs"` produces a structure with a depth of O(log_2(``length` xs`)).

foldr1 :: forall a (n :: Natural). (a -> a -> a) -> Vec (n + 1) a -> a Source #

`foldr1` is a variant of `foldr` that has no starting value argument, and thus must be applied to non-empty vectors.

    foldr1 f (x1 :> ... :> xn2 :> xn1 :> xn :> Nil) == x1 `f` (... (xn2 `f` (xn1 `f` xn))...)
    foldr1 f (x1 :> Nil)                            == x1
    foldr1 f Nil                                    == TYPE ERROR

    >>> foldr1 (/) (5 :> 4 :> 3 :> 2 :> 1 :> Nil)
    1.875

"`foldr1` `f xs`" corresponds to the following circuit layout:

NB: `"`foldr1` f z xs"` produces a linear structure, which has a depth, or delay, of O(``length` xs`). Use `fold` if your binary operator `f` is associative, as `"`fold` f xs"` produces a structure with a depth of O(log_2(``length` xs`)).

foldl1 :: forall a (n :: Natural). (a -> a -> a) -> Vec (n + 1) a -> a Source #

`foldl1` is a variant of `foldl` that has no starting value argument, and thus must be applied to non-empty vectors.

    foldl1 f (x1 :> x2 :> x3 :> ... :> xn :> Nil) == (...((x1 `f` x2) `f` x3) `f`...) `f` xn
    foldl1 f (x1 :> Nil)                          == x1
    foldl1 f Nil                                  == TYPE ERROR

    >>> foldl1 (/) (1 :> 5 :> 4 :> 3 :> 2 :> Nil)
    8.333333333333333e-3

"`foldl1` `f xs`" corresponds to the following circuit layout:

NB: `"`foldl1` f z xs"` produces a linear structure, which has a depth, or delay, of O(``length` xs`). Use `fold` if your binary operator `f` is associative, as `"`fold` f xs"` produces a structure with a depth of O(log_2(``length` xs`)).

fold :: forall (n :: Natural) a. (a -> a -> a) -> Vec (n + 1) a -> a Source #

`fold` is a variant of `foldr1` and `foldl1`, but instead of reducing from right to left, or left to right, it reduces a vector using a tree-like structure. The depth, or delay, of the structure produced by "``fold` f xs`", is hence `O(log_2(`length` xs))`, and not `O(`length` xs)`.

NB: The binary operator "`f`" in "``fold` f xs`" must be associative.

    fold f (x1 :> x2 :> ... :> xn1 :> xn :> Nil) == ((x1 `f` x2) `f` ...) `f` (... `f` (xn1 `f` xn))
    fold f (x1 :> Nil)                           == x1
    fold f Nil                                   == TYPE ERROR

    >>> fold (+) (5 :> 4 :> 3 :> 2 :> 1 :> Nil)
    15

"`fold` `f xs`" corresponds to the following circuit layout:

ifoldr :: forall (n :: Nat) a b. KnownNat n => (Index n -> a -> b -> b) -> b -> Vec n a -> b Source #

Right fold (function applied to each element and its index)

    >>> let findLeftmost x xs = ifoldr (\i a b -> if a == x then Just i else b) Nothing xs
    >>> findLeftmost 3 (1:>3:>2:>4:>3:>5:>6:>Nil)
    Just 1
    >>> findLeftmost 8 (1:>3:>2:>4:>3:>5:>6:>Nil)
    Nothing

"`ifoldr` `f z xs`" corresponds to the following circuit layout:

ifoldl :: forall (n :: Nat) a b. KnownNat n => (a -> Index n -> b -> a) -> a -> Vec n b -> a Source #

Left fold (function applied to each element and its index)

    >>> let findRightmost x xs = ifoldl (\a i b -> if b == x then Just i else a) Nothing xs
    >>> findRightmost 3 (1:>3:>2:>4:>3:>5:>6:>Nil)
    Just 4
    >>> findRightmost 8 (1:>3:>2:>4:>3:>5:>6:>Nil)
    Nothing

"`ifoldl` `f z xs`" corresponds to the following circuit layout:

## Specialized folds

dfold Source #

Arguments

:: forall (p :: TyFun Nat Type -> Type) (k :: Nat) a. KnownNat k |
=> Proxy p | The motive
-> (forall (l :: Nat). SNat l -> a -> (p @@ l) -> p @@ (l + 1)) | Function to fold. NB: The `SNat l` is not the index (see (`!!`)) to the element a. `SNat l` is the number of elements that occur to the right of a.
-> (p @@ 0) | Initial element
-> Vec k a | Vector to fold over
-> p @@ k |

A dependently typed fold.

### doctests setup

Expand

    >>> :seti -fplugin GHC.TypeLits.Normalise
    >>> import Data.Singletons (Apply, Proxy (..), TyFun)
    >>> data Append (m :: Nat) (a :: Type) (f :: TyFun Nat Type) :: Type
    >>> type instance Apply (Append m a) l = Vec (l + m) a
    >>> let append' xs ys = dfold (Proxy :: Proxy (Append m a)) (const (:>)) ys xs

### Example usage

Using lists, we can define append (a.k.a. `Data.List.``++`) in terms of `Data.List.``foldr`:

    >>> import qualified Data.List
    >>> let append xs ys = Data.List.foldr (:) ys xs
    >>> append [1,2] [3,4]
    [1,2,3,4]

However, when we try to do the same for `Vec`, by defining append' in terms of `Clash.Sized.Vector.``foldr`:

    append' xs ys = foldr (:>) ys xs

we get a type error:

    >>> let append' xs ys = foldr (:>) ys xs

    <interactive>:...
        • Occurs check: cannot construct the infinite type: ... ~ ... + 1
          Expected type: a -> Vec ... a -> Vec ... a
            Actual type: a -> Vec ... a -> Vec (... + 1) a
        • In the first argument of ‘foldr’, namely ‘(:>)’
          In the expression: foldr (:>) ys xs
          In an equation for ‘append'’: append' xs ys = foldr (:>) ys xs
        • Relevant bindings include
            ys :: Vec ... a (bound at ...)
            append' :: Vec n a -> Vec ... a -> Vec ... a
              (bound at ...)

The reason is that the type of `foldr` is:

    >>> :t foldr
    foldr :: (a -> b -> b) -> b -> Vec n a -> b

While the type of (`:>`) is:

    >>> :t (:>)
    (:>) :: a -> Vec n a -> Vec (n + 1) a

We thus need a `fold` function that can handle the growing vector type: `dfold`. Compared to `foldr`, `dfold` takes an extra parameter, called the motive, that allows the folded function to have an argument and result type that depends on the current length of the vector. Using `dfold`, we can now correctly define append':

    import Data.Singletons
    import Data.Proxy

    data Append (m :: Nat) (a :: Type) (f :: TyFun Nat Type) :: Type
    type instance Apply (Append m a) l = Vec (l + m) a

    append' xs ys = dfold (Proxy :: Proxy (Append m a)) (const (:>)) ys xs

We now see that append' has the appropriate type:

    >>> :t append'
    append' :: KnownNat k => Vec k a -> Vec m a -> Vec (k + m) a

And that it works:

    >>> append' (1 :> 2 :> Nil) (3 :> 4 :> Nil)
    1 :> 2 :> 3 :> 4 :> Nil

NB: "``dfold` m f z xs`" creates a linear structure, which has a depth, or delay, of O(``length` xs`). Look at `dtfold` for a dependently typed fold that produces a structure with a depth of O(log_2(``length` xs`)).

dtfold Source #

Arguments

:: forall (p :: TyFun Nat Type -> Type) (k :: Nat) a. KnownNat k |
=> Proxy p | The motive
-> (a -> p @@ 0) | Function to apply to every element
-> (forall (l :: Nat). SNat l -> (p @@ l) -> (p @@ l) -> p @@ (l + 1)) | Function to combine results. NB: The `SNat l` indicates the depth/height of the node in the tree that is created by applying this function. The leafs of the tree have depth/height 0, and the root of the tree has height k.
-> Vec (2 ^ k) a | Vector to fold over. NB: Must have a length that is a power of 2.
-> p @@ k |

A combination of `dfold` and `fold`: a dependently typed fold that reduces a vector in a tree-like structure.

### doctests setup

Expand

    >>> :seti -XUndecidableInstances
    >>> import Data.Singletons (Apply, Proxy (..), TyFun)
    >>> data IIndex (f :: TyFun Nat Type) :: Type
    >>> type instance Apply IIndex l = Index ((2^l)+1)
    >>> :{
    let populationCount' :: (KnownNat k, KnownNat (2^k)) => BitVector (2^k) -> Index ((2^k)+1)
        populationCount' bv = dtfold (Proxy @IIndex)
                                     fromIntegral
                                     (\_ x y -> add x y)
                                     (bv2v bv)
    :}

### Example usage

As an example of when you might want to use `dtfold` we will build a population counter: a circuit that counts the number of bits set to '1' in a `BitVector`. Given a vector of n bits, we only need we need a data type that can represent the number n: `Index` `(n+1)`. `Index` `k` has a range of `[0 .. k-1]` (using `ceil(log2(k))` bits), hence we need `Index` `n+1`. As an initial attempt we will use `sum`, because it gives a nice (`log2(n)`) tree-structure of adders:

    populationCount :: (KnownNat (n+1), KnownNat (n+2))
                    => BitVector (n+1) -> Index (n+2)
    populationCount = sum . map fromIntegral . bv2v

The "problem" with this description is that all adders have the same bit-width, i.e. all adders are of the type:

    (+) :: Index (n+2) -> Index (n+2) -> Index (n+2).

This is a "problem" because we could have a more efficient structure: one where each layer of adders is precisely wide enough to count the number of bits at that layer. That is, at height d we want the adder to be of type:

    Index ((2^d)+1) -> Index ((2^d)+1) -> Index ((2^(d+1))+1)

We have such an adder in the form of the `add` function, as defined in the instance `ExtendingNum` instance of `Index`. However, we cannot simply use `fold` to create a tree-structure of `add`es:

    >>> :{
    let populationCount' :: (KnownNat (n+1), KnownNat (n+2))
                         => BitVector (n+1) -> Index (n+2)
        populationCount' = fold add . map fromIntegral . bv2v
    :}
    <interactive>:...
        • Couldn't match type: ((n + 2) + (n + 2)) - 1
                         with: n + 2
          Expected: Index (n + 2) -> Index (n + 2) -> Index (n + 2)
            Actual: Index (n + 2)
                    -> Index (n + 2) -> AResult (Index (n + 2)) (Index (n + 2))
        • In the first argument of ‘fold’, namely ‘add’
          In the first argument of ‘(.)’, namely ‘fold add’
          In the expression: fold add . map fromIntegral . bv2v
        • Relevant bindings include
            populationCount' :: BitVector (n + 1) -> Index (n + 2)
              (bound at ...)

# 2539 "srcClashSized/Vector.hs"

because `fold` expects a function of type "`a -> a -> a`", i.e. a function where the arguments and result all have exactly the same type.

In order to accommodate the type of our `add`, where the result is larger than the arguments, we must use a dependently typed fold in the form of `dtfold`:

    {-# LANGUAGE UndecidableInstances #-}
    import Data.Singletons
    import Data.Proxy

    data IIndex (f :: TyFun Nat Type) :: Type
    type instance Apply IIndex l = Index ((2^l)+1)

    populationCount' :: (KnownNat k, KnownNat (2^k))
                     => BitVector (2^k) -> Index ((2^k)+1)
    populationCount' bv = dtfold (Proxy @IIndex)
                                 fromIntegral
                                 (\_ x y -> add x y)
                                 (bv2v bv)

And we can test that it works:

    >>> :t populationCount' (7 :: BitVector 16)
    populationCount' (7 :: BitVector 16) :: Index 17
    >>> populationCount' (7 :: BitVector 16)
    3

Some final remarks:

- By using `dtfold` instead of `fold`, we had to restrict our `BitVector` argument to have bit-width that is a power of 2.
- Even though our original populationCount function specified a structure where all adders had the same width. Most VHDL/(System)Verilog synthesis tools will create a more efficient circuit, i.e. one where the adders have an increasing bit-width for every layer, from the VHDL/(System)Verilog produced by the Clash compiler.

NB: The depth, or delay, of the structure produced by "``dtfold` m f g xs`" is O(log_2(``length` xs`)).

vfold :: forall (k :: Nat) a b. KnownNat k => (forall (l :: Nat). SNat l -> a -> Vec l b -> Vec (l + 1) b) -> Vec k a -> Vec k b Source #

Specialised version of `dfold` that builds a triangular computational structure.

### doctests setup

Expand

    >>> let compareSwap a b = if a > b then (a,b) else (b,a)
    >>> let insert y xs = let (y',xs') = mapAccumL compareSwap y xs in xs' :< y'
    >>> let insertionSort = vfold (const insert)

### Example usage

    compareSwap a b = if a > b then (a,b) else (b,a)
    insert y xs     = let (y',xs') = mapAccumL compareSwap y xs in xs' :< y'
    insertionSort   = vfold (const insert)

Builds a triangular structure of compare and swaps to sort a row.

    >>> insertionSort (7 :> 3 :> 9 :> 1 :> Nil)
    1 :> 3 :> 7 :> 9 :> Nil

The circuit layout of `insertionSort`, build using `vfold`, is:

maximum :: forall a (n :: Natural). Ord a => Vec (n + 1) a -> a Source #

The largest element of a non-empty vector

minimum :: forall a (n :: Natural). Ord a => Vec (n + 1) a -> a Source #

The least element of a non-empty vector

# Prefix sums (scans)

scanl :: forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b Source #

`scanl` is similar to `foldl`, but returns a vector of successive reduced values from the left:

    scanl f z (x1 :> x2 :> ... :> Nil) == z :> (z `f` x1) :> ((z `f` x1) `f` x2) :> ... :> Nil

    >>> scanl (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
    0 :> 5 :> 9 :> 12 :> 14 :> Nil

"`scanl` `f z xs`" corresponds to the following circuit layout:

- NB:

      last (scanl f z xs) == foldl f z xs

- For a different trade-off between circuit size and logic depth for associative operators, see Clash.Sized.RTree

scanl1 :: forall (n :: Nat) a. KnownNat n => (a -> a -> a) -> Vec (n + 1) a -> Vec (n + 1) a Source #

`scanl` with no seed value

    >>> scanl1 (-) (1 :> 2 :> 3 :> 4 :> Nil)
    1 :> -1 :> -4 :> -8 :> Nil

scanr :: forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> Vec (n + 1) b Source #

`scanr` is similar to `foldr`, but returns a vector of successive reduced values from the right:

    scanr f z (... :> xn1 :> xn :> Nil) == ... :> (xn1 `f` (xn `f` z)) :> (xn `f` z) :> z :> Nil

    >>> scanr (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
    14 :> 9 :> 5 :> 2 :> 0 :> Nil

"`scanr` `f z xs`" corresponds to the following circuit layout:

- NB:

      head (scanr f z xs) == foldr f z xs

- For a different trade-off between circuit size and logic depth for associative operators, see Clash.Sized.RTree

scanr1 :: forall (n :: Nat) a. KnownNat n => (a -> a -> a) -> Vec (n + 1) a -> Vec (n + 1) a Source #

`scanr` with no seed value

    >>> scanr1 (-) (1 :> 2 :> 3 :> 4 :> Nil)
    -2 :> 3 :> -1 :> 4 :> Nil

postscanl :: forall b a (n :: Nat). (b -> a -> b) -> b -> Vec n a -> Vec n b Source #

`postscanl` is a variant of `scanl` where the first result is dropped:

    postscanl f z (x1 :> x2 :> ... :> Nil) == (z `f` x1) :> ((z `f` x1) `f` x2) :> ... :> Nil

    >>> postscanl (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
    5 :> 9 :> 12 :> 14 :> Nil

"`postscanl` `f z xs`" corresponds to the following circuit layout:

postscanr :: forall a b (n :: Nat). (a -> b -> b) -> b -> Vec n a -> Vec n b Source #

`postscanr` is a variant of `scanr` that where the last result is dropped:

    postscanr f z (... :> xn1 :> xn :> Nil) == ... :> (xn1 `f` (xn `f` z)) :> (xn `f` z) :> Nil

    >>> postscanr (+) 0 (5 :> 4 :> 3 :> 2 :> Nil)
    14 :> 9 :> 5 :> 2 :> Nil

"`postscanr` `f z xs`" corresponds to the following circuit layout:

mapAccumL :: forall acc x y (n :: Nat). (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y) Source #

The `mapAccumL` function behaves like a combination of `map` and `foldl`; it applies a function to each element of a vector, passing an accumulating parameter from left to right, and returning a final value of this accumulator together with the new vector.

    >>> mapAccumL (\acc x -> (acc + x,acc + 1)) 0 (1 :> 2 :> 3 :> 4 :> Nil)
    (10,1 :> 2 :> 4 :> 7 :> Nil)

"`mapAccumL` `f acc xs`" corresponds to the following circuit layout:

mapAccumR :: forall acc x y (n :: Nat). (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y) Source #

The `mapAccumR` function behaves like a combination of `map` and `foldr`; it applies a function to each element of a vector, passing an accumulating parameter from right to left, and returning a final value of this accumulator together with the new vector.

    >>> mapAccumR (\acc x -> (acc + x,acc + 1)) 0 (1 :> 2 :> 3 :> 4 :> Nil)
    (10,10 :> 8 :> 5 :> 1 :> Nil)

"`mapAccumR` `f acc xs`" corresponds to the following circuit layout:

# Stencil computations

stencil1d Source #

Arguments

:: forall (n :: Nat) (stX :: Natural) a b. KnownNat n |
=> SNat (stX + 1) | Windows length stX, at least size 1
-> (Vec (stX + 1) a -> b) | The stencil (function)
-> Vec ((stX + n) + 1) a |
-> Vec (n + 1) b |

1-dimensional stencil computations

"`stencil1d` `stX f xs`", where xs has stX + n elements, applies the stencil computation f on: n + 1 overlapping (1D) windows of length stX, drawn from xs. The resulting vector has n + 1 elements.

    >>> let xs = (1:>2:>3:>4:>5:>6:>Nil)
    >>> :t xs
    xs :: Num a => Vec 6 a
    >>> :t stencil1d d2 sum xs
    stencil1d d2 sum xs :: Num b => Vec 5 b
    >>> stencil1d d2 sum xs
    3 :> 5 :> 7 :> 9 :> 11 :> Nil

stencil2d Source #

Arguments

:: forall (n :: Nat) (m :: Nat) (stY :: Natural) (stX :: Natural) a b. (KnownNat n, KnownNat m) |
=> SNat (stY + 1) | Window hight stY, at least size 1
-> SNat (stX + 1) | Window width stX, at least size 1
-> (Vec (stY + 1) (Vec (stX + 1) a) -> b) | The stencil (function)
-> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a) |
-> Vec (m + 1) (Vec (n + 1) b) |

2-dimensional stencil computations

"`stencil2d` `stY stX f xss`", where xss is a matrix of stY + m rows of stX + n elements, applies the stencil computation f on: (m + 1) * (n + 1) overlapping (2D) windows of stY rows of stX elements, drawn from xss. The result matrix has m + 1 rows of n + 1 elements.

    >>> let xss = ((1:>2:>3:>4:>Nil):>(5:>6:>7:>8:>Nil):>(9:>10:>11:>12:>Nil):>(13:>14:>15:>16:>Nil):>Nil)
    >>> :t xss
    xss :: Num a => Vec 4 (Vec 4 a)

    >>> :t stencil2d d2 d2 (sum . map sum) xss
    stencil2d d2 d2 (sum . map sum) xss :: Num a => Vec 3 (Vec 3 a)

    >>> stencil2d d2 d2 (sum . map sum) xss
    (14 :> 18 :> 22 :> Nil) :> (30 :> 34 :> 38 :> Nil) :> (46 :> 50 :> 54 :> Nil) :> Nil

windows1d Source #

Arguments

:: forall (n :: Nat) (stX :: Natural) a. KnownNat n |
=> SNat (stX + 1) | Length of the window, at least size 1
-> Vec ((stX + n) + 1) a |
-> Vec (n + 1) (Vec (stX + 1) a) |

"`windows1d` `stX xs`", where the vector xs has stX + n elements, returns a vector of n + 1 overlapping (1D) windows of xs of length stX.

    >>> let xs = (1:>2:>3:>4:>5:>6:>Nil)
    >>> :t xs
    xs :: Num a => Vec 6 a
    >>> :t windows1d d2 xs
    windows1d d2 xs :: Num a => Vec 5 (Vec 2 a)
    >>> windows1d d2 xs
    (1 :> 2 :> Nil) :> (2 :> 3 :> Nil) :> (3 :> 4 :> Nil) :> (4 :> 5 :> Nil) :> (5 :> 6 :> Nil) :> Nil

windows2d Source #

Arguments

:: forall (n :: Nat) (m :: Nat) (stY :: Natural) (stX :: Natural) a. (KnownNat n, KnownNat m) |
=> SNat (stY + 1) | Window hight stY, at least size 1
-> SNat (stX + 1) | Window width stX, at least size 1
-> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a) |
-> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a))) |

"`windows2d` `stY stX xss`", where matrix xss has stY + m rows of stX + n, returns a matrix of m+1 rows of n+1 elements. The elements of this new matrix are the overlapping (2D) windows of xss, where every window has stY rows of stX elements.

    >>> let xss = ((1:>2:>3:>4:>Nil):>(5:>6:>7:>8:>Nil):>(9:>10:>11:>12:>Nil):>(13:>14:>15:>16:>Nil):>Nil)
    >>> :t xss
    xss :: Num a => Vec 4 (Vec 4 a)
    >>> :t windows2d d2 d2 xss
    windows2d d2 d2 xss :: Num a => Vec 3 (Vec 3 (Vec 2 (Vec 2 a)))
    >>> windows2d d2 d2 xss
    (((1 :> 2 :> Nil) :> (5 :> 6 :> Nil) :> Nil) :> ((2 :> 3 :> Nil) :> (6 :> 7 :> Nil) :> Nil) :> ((3 :> 4 :> Nil) :> (7 :> 8 :> Nil) :> Nil) :> Nil) :> (((5 :> 6 :> Nil) :> (9 :> 10 :> Nil) :> Nil) :> ((6 :> 7 :> Nil) :> (10 :> 11 :> Nil) :> Nil) :> ((7 :> 8 :> Nil) :> (11 :> 12 :> Nil) :> Nil) :> Nil) :> (((9 :> 10 :> Nil) :> (13 :> 14 :> Nil) :> Nil) :> ((10 :> 11 :> Nil) :> (14 :> 15 :> Nil) :> Nil) :> ((11 :> 12 :> Nil) :> (15 :> 16 :> Nil) :> Nil) :> Nil) :> Nil

# Conversions

toList :: forall (n :: Nat) a. Vec n a -> [a] Source #

Convert a vector to a list.

    >>> toList (1:>2:>3:>Nil)
    [1,2,3]

NB: This function is not synthesizable

fromList :: forall (n :: Nat) a. KnownNat n => [a] -> Maybe (Vec n a) Source #

Convert a list to a vector. This function returns Nothing if the size of the list is not equal to the size of the resulting vector.

    >>> Vec.fromList [1,2,3,4,5] :: Maybe (Vec 5 Int)
    Just (1 :> 2 :> 3 :> 4 :> 5 :> Nil)

    >>> Vec.fromList [1,2,3,4,5] :: Maybe (Vec 3 Int)
    Nothing

    >>> Vec.fromList [1,2,3,4,5] :: Maybe (Vec 10 Int)
    Nothing

- NB: Use `listToVecTH` if you want to make a statically known vector
- NB: This function is not synthesizable

unsafeFromList :: forall (n :: Nat) a. KnownNat n => [a] -> Vec n a Source #

Convert a list to a vector. This function always returns a vector of the desired length, by either truncating the list or padding the vector with undefined elements.

    >>> Vec.unsafeFromList [1,2,3,4,5] :: Vec 5 Int
    1 :> 2 :> 3 :> 4 :> 5 :> Nil

    >>> Vec.unsafeFromList [1,2,3,4,5] :: Vec 3 Int
    1 :> 2 :> 3 :> Nil

    >>> Vec.unsafeFromList [1,2,3,4,5] :: Vec 10 Int
    1 :> 2 :> 3 :> 4 :> 5 :> *** Exception: Clash.Sized.Vector.unsafeFromList: vector larger than list
    ...

- NB: Use `listToVecTH` if you want to make a statically known vector
- NB: This function is not synthesizable

bv2v :: forall (n :: Nat). KnownNat n => BitVector n -> Vec n Bit Source #

Convert a `BitVector` to a `Vec` of `Bit`s.

    >>> let x = 6 :: BitVector 8
    >>> x
    0b0000_0110
    >>> bv2v x
    0 :> 0 :> 0 :> 0 :> 0 :> 1 :> 1 :> 0 :> Nil

v2bv :: forall (n :: Nat). KnownNat n => Vec n Bit -> BitVector n Source #

Convert a `Vec` of `Bit`s to a `BitVector`.

    >>> let x = (0:>0:>0:>1:>0:>0:>1:>0:>Nil) :: Vec 8 Bit
    >>> x
    0 :> 0 :> 0 :> 1 :> 0 :> 0 :> 1 :> 0 :> Nil
    >>> v2bv x
    0b0001_0010

# Misc

lazyV :: forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a Source #

What you should use when your vector functions are too strict in their arguments.

### doctests setup

Expand

    >>> let compareSwapL a b = if a < b then (a,b) else (b,a)
    >>> :{
    let sortVL :: (Ord a, KnownNat (n + 1)) => Vec ((n + 1) + 1) a -> Vec ((n + 1) + 1) a
        sortVL xs = map fst sorted :< (snd (last sorted))
          where
            lefts  = head xs :> map snd (init sorted)
            rights = tail xs
            sorted = zipWith compareSwapL (lazyV lefts) rights
    :}

    >>> :{
    let sortV_flip xs = map fst sorted :< (snd (last sorted))
          where
            lefts  = head xs :> map snd (init sorted)
            rights = tail xs
            sorted = zipWith (flip compareSwapL) rights lefts
    :}

### Example usage

For example:

    -- Bubble sort for 1 iteration
    sortV xs = map fst sorted :< (snd (last sorted))
     where
       lefts  = head xs :> map snd (init sorted)
       rights = tail xs
       sorted = zipWith compareSwapL lefts rights

    -- Compare and swap
    compareSwapL a b = if a < b then (a,b)
                                else (b,a)

Will not terminate because `zipWith` is too strict in its second argument.

In this case, adding `lazyV` on `zipWith`s second argument:

    sortVL xs = map fst sorted :< (snd (last sorted))
     where
       lefts  = head xs :> map snd (init sorted)
       rights = tail xs
       sorted = zipWith compareSwapL (lazyV lefts) rights

Results in a successful computation:

    >>> sortVL (4 :> 1 :> 2 :> 3 :> Nil)
    1 :> 2 :> 3 :> 4 :> Nil

NB: There is also a solution using `flip`, but it slightly obfuscates the meaning of the code:

    sortV_flip xs = map fst sorted :< (snd (last sorted))
     where
       lefts  = head xs :> map snd (init sorted)
       rights = tail xs
       sorted = zipWith (flip compareSwapL) rights lefts

    >>> sortV_flip (4 :> 1 :> 2 :> 3 :> Nil)
    1 :> 2 :> 3 :> 4 :> Nil

data VCons a (f :: TyFun Nat Type) Source #

To be used as the motive p for `dfold`, when the f in "`dfold` `p f`" is a variation on (`:>`), e.g.:

    map' :: forall n a b . KnownNat n => (a -> b) -> Vec n a -> Vec n b
    map' f = dfold (Proxy @(VCons b)) (_ x xs -> f x :> xs)

#### Instances

Instances details

type Apply (VCons a :: TyFun Nat Type -> Type) (l :: Nat) Source # |
Instance details Defined in Clash.Sized.Vector type Apply (VCons a :: TyFun Nat Type -> Type) (l :: Nat) = Vec l a

asNatProxy :: forall (n :: Nat) a. Vec n a -> Proxy n Source #

`Vec`tor as a `Proxy` for `Nat`

seqV :: forall (n :: Nat) a b. KnownNat n => Vec n a -> b -> b infixr 0 Source #

Evaluate all elements of a vector to WHNF, returning the second argument

forceV :: forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a Source #

Evaluate all elements of a vector to WHNF

seqVX :: forall (n :: Nat) a b. KnownNat n => Vec n a -> b -> b infixr 0 Source #

Evaluate all elements of a vector to WHNF, returning the second argument. Does not propagate `XException`s.

forceVX :: forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a Source #

Evaluate all elements of a vector to WHNF. Does not propagate `XException`s.

# Primitives

## `Traversable` instance

traverse# :: forall a f b (n :: Nat). Applicative f => (a -> f b) -> Vec n a -> f (Vec n b) Source #

## `BitPack` instance

concatBitVector# :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) => Vec n (BitVector m) -> BitVector (n * m) Source #

unconcatBitVector# :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) => BitVector (n * m) -> Vec n (BitVector m) Source #