clash-prelude-1.5.0: Clash: a functional hardware description language - Prelude library
Copyright (C) 2013-2016 University of Twente2017-2019 Myrtle Software Ltd2017 Google Inc.2021-2022 QBayLogic B.V. BSD2 (see the file LICENSE) QBayLogic B.V. Safe Haskell2010 ScopedTypeVariablesBangPatternsViewPatternsDataKindsInstanceSigsStandaloneDerivingDeriveDataTypeableDeriveFunctorDeriveTraversableDeriveFoldableDeriveGenericDefaultSignaturesDeriveLiftDerivingStrategiesFlexibleContextsMagicHashKindSignaturesTupleSectionsTypeOperatorsExplicitNamespacesExplicitForAllBinaryLiteralsTypeApplications

Clash.Prelude.Safe

Description

This is the Safe API only of Clash.Prelude

Clash is a functional hardware description language that borrows both its syntax and semantics from the functional programming language Haskell. The merits of using a functional language to describe hardware comes from the fact that combinational circuits can be directly modeled as mathematical functions and that functional languages lend themselves very well at describing and (de-)composing mathematical functions.

This package provides:

• Prelude library containing datatypes and functions for circuit design

To use the library:

For now, Clash.Prelude is also the best starting point for exploring the library. A preliminary version of a tutorial can be found in Clash.Tutorial. Some circuit examples can be found in Clash.Examples.

Synopsis

# Creating synchronous sequential circuits

Arguments

 :: (HiddenClockResetEnable dom, NFDataX s) => (s -> i -> (s, o)) Transfer function in mealy machine form: state -> input -> (newstate,output) -> s Initial state -> Signal dom i -> Signal dom o Synchronous sequential function with input and output matching that of the mealy machine

Create a synchronous function from a combinational function describing a mealy machine

macT
:: Int        -- Current state
-> (Int,Int)  -- Input
-> (Int,Int)  -- (Updated state, output)
macT s (x,y) = (s',s)
where
s' = x * y + s

mac :: HiddenClockResetEnable dom  => Signal dom (Int, Int) -> Signal dom Int
mac = mealy macT 0

>>> simulate @System mac [(0,0),(1,1),(2,2),(3,3),(4,4)]
[0,0,1,5,14...
...


Synchronous sequential functions can be composed just like their combinational counterpart:

dualMac
:: HiddenClockResetEnable dom
=> (Signal dom Int, Signal dom Int)
-> (Signal dom Int, Signal dom Int)
-> Signal dom Int
dualMac (a,b) (x,y) = s1 + s2
where
s1 = mealy mac 0 (bundle (a,x))
s2 = mealy mac 0 (bundle (b,y))


Arguments

 :: (HiddenClockResetEnable dom, NFDataX s, Bundle i, Bundle o) => (s -> i -> (s, o)) Transfer function in mealy machine form: state -> input -> (newstate,output) -> s Initial state -> Unbundled dom i -> Unbundled dom o Synchronous sequential function with input and output matching that of the mealy machine

A version of mealy that does automatic Bundleing

Given a function f of type:

f :: Int -> (Bool, Int) -> (Int, (Int, Bool))


When we want to make compositions of f in g using mealy, we have to write:

g a b c = (b1,b2,i2)
where
(i1,b1) = unbundle (mealy f 0 (bundle (a,b)))
(i2,b2) = unbundle (mealy f 3 (bundle (c,i1)))


Using mealyB however we can write:

g a b c = (b1,b2,i2)
where
(i1,b1) = mealyB f 0 (a,b)
(i2,b2) = mealyB f 3 (c,i1)


Arguments

 :: (HiddenClockResetEnable dom, NFDataX s, Bundle i, Bundle o) => (s -> i -> (s, o)) Transfer function in mealy machine form: state -> input -> (newstate,output) -> s Initial state -> Unbundled dom i -> Unbundled dom o Synchronous sequential function with input and output matching that of the mealy machine

Infix version of mealyB

Arguments

 :: (HiddenClockResetEnable dom, NFDataX s) => (s -> i -> s) Transfer function in moore machine form: state -> input -> newstate -> (s -> o) Output function in moore machine form: state -> output -> s Initial state -> Signal dom i -> Signal dom o Synchronous sequential function with input and output matching that of the moore machine

Create a synchronous function from a combinational function describing a moore machine

macT
:: Int        -- Current state
-> (Int,Int)  -- Input
-> Int        -- Updated state
macT s (x,y) = x * y + s

mac
:: HiddenClockResetEnable dom
=> Signal dom (Int, Int)
-> Signal dom Int
mac = moore mac id 0

>>> simulate @System mac [(0,0),(1,1),(2,2),(3,3),(4,4)]
[0,0,1,5,14,30,...
...


Synchronous sequential functions can be composed just like their combinational counterpart:

dualMac
:: HiddenClockResetEnable dom
=> (Signal dom Int, Signal dom Int)
-> (Signal dom Int, Signal dom Int)
-> Signal dom Int
dualMac (a,b) (x,y) = s1 + s2
where
s1 = moore mac id 0 (bundle (a,x))
s2 = moore mac id 0 (bundle (b,y))


Arguments

 :: (HiddenClockResetEnable dom, NFDataX s, Bundle i, Bundle o) => (s -> i -> s) Transfer function in moore machine form: state -> input -> newstate -> (s -> o) Output function in moore machine form: state -> output -> s Initial state -> Unbundled dom i -> Unbundled dom o Synchronous sequential function with input and output matching that of the moore machine

A version of moore that does automatic Bundleing

Given a functions t and o of types:

t :: Int -> (Bool, Int) -> Int
o :: Int -> (Int, Bool)


When we want to make compositions of t and o in g using moore, we have to write:

g a b c = (b1,b2,i2)
where
(i1,b1) = unbundle (moore t o 0 (bundle (a,b)))
(i2,b2) = unbundle (moore t o 3 (bundle (c,i1)))


Using mooreB however we can write:

g a b c = (b1,b2,i2)
where
(i1,b1) = mooreB t o 0 (a,b)
(i2,b2) = mooreB t o 3 (c,i1)


registerB :: (HiddenClockResetEnable dom, NFDataX a, Bundle a) => a -> Unbundled dom a -> Unbundled dom a infixr 3 Source #

Create a register function for product-type like signals (e.g. '(Signal a, Signal b)')

rP :: HiddenClockResetEnable dom
=> (Signal dom Int, Signal dom Int)
-> (Signal dom Int, Signal dom Int)
rP = registerB (8,8)
>>> simulateB @System rP [(1,1),(2,2),(3,3)] :: [(Int,Int)]
[(8,8),(1,1),(2,2),(3,3)...
...


# ROMs

Arguments

 :: (KnownNat n, Enum addr) => Vec n a ROM content, also determines the size, n, of the ROMNB: must be a constant -> addr Read address rd -> a The value of the ROM at address rd

An asynchronous/combinational ROM with space for n elements

• See Clash.Sized.Fixed and Clash.Prelude.BlockRam for ideas on how to use ROMs and RAMs
• A large Vec for the content might be too inefficient, depending on how it is constructed. See asyncRomFile and asyncRomBlob for different approaches that scale well.

Arguments

 :: KnownNat n => Vec (2 ^ n) a ROM contentNB: must be a constant -> Unsigned n Read address rd -> a The value of the ROM at address rd

An asynchronous/combinational ROM with space for 2^n elements

• See Clash.Sized.Fixed and Clash.Prelude.BlockRam for ideas on how to use ROMs and RAMs
• A large Vec for the content might be too inefficient, depending on how it is constructed. See asyncRomFilePow2 and asyncRomBlobPow2 for different approaches that scale well.

Arguments

 :: forall dom n m a. (NFDataX a, KnownNat n, KnownNat m, HiddenClock dom, HiddenEnable dom) => Vec n a ROM content, also determines the size, n, of the ROMNB: must be a constant -> Signal dom (Unsigned m) Read address rd -> Signal dom a The value of the ROM at address rd

A ROM with a synchronous read port, with space for n elements

• NB: Read value is delayed by 1 cycle
• NB: Initial output value is undefined, reading it will throw an XException

• See Clash.Sized.Fixed and Clash.Prelude.BlockRam for ideas on how to use ROMs and RAMs
• A large Vec for the content might be too inefficient, depending on how it is constructed. See romFile and romBlob for different approaches that scale well.

Arguments

 :: forall dom n a. (KnownNat n, NFDataX a, HiddenClock dom, HiddenEnable dom) => Vec (2 ^ n) a ROM contentNB: must be a constant -> Signal dom (Unsigned n) Read address rd -> Signal dom a The value of the ROM at address rd

A ROM with a synchronous read port, with space for 2^n elements

• NB: Read value is delayed by 1 cycle
• NB: Initial output value is undefined, reading it will throw an XException

• See Clash.Sized.Fixed and Clash.Prelude.BlockRam for ideas on how to use ROMs and RAMs
• A large Vec for the content might be too inefficient, depending on how it is constructed. See romFilePow2 and romBlobPow2 for different approaches that scale well.

## ROMs defined by a MemBlob

Arguments

 :: Enum addr => MemBlob n m ROM content, also determines the size, n, of the ROMNB: MUST be a constant -> addr Read address r -> BitVector m The value of the ROM at address r

An asynchronous/combinational ROM with space for n elements

Arguments

 :: KnownNat n => MemBlob (2 ^ n) m ROM content, also determines the size, 2^n, of the ROMNB: MUST be a constant -> Unsigned n Read address r -> BitVector m The value of the ROM at address r

An asynchronous/combinational ROM with space for 2^n elements

Arguments

 :: forall dom addr m n. (HiddenClock dom, HiddenEnable dom, Enum addr) => MemBlob n m ROM content, also determines the size, n, of the ROMNB: MUST be a constant -> Signal dom addr Read address r -> Signal dom (BitVector m) The value of the ROM at address r from the previous clock cycle

A ROM with a synchronous read port, with space for n elements

• NB: Read value is delayed by 1 cycle
• NB: Initial output value is undefined, reading it will throw an XException

Arguments

 :: forall dom m n. (HiddenClock dom, HiddenEnable dom, KnownNat n) => MemBlob (2 ^ n) m ROM content, also determines the size, 2^n, of the ROMNB: MUST be a constant -> Signal dom (Unsigned n) Read address r -> Signal dom (BitVector m) The value of the ROM at address r from the previous clock cycle

A ROM with a synchronous read port, with space for 2^n elements

• NB: Read value is delayed by 1 cycle
• NB: Initial output value is undefined, reading it will throw an XException

# RAM primitives with a combinational read port

Arguments

 :: (Enum addr, HiddenClock dom, HiddenEnable dom, HasCallStack, NFDataX a) => SNat n Size n of the RAM -> Signal dom addr Read address r -> Signal dom (Maybe (addr, a)) (write address w, value to write) -> Signal dom a Value of the RAM at address r

Create a RAM with space for n elements.

• NB: Initial content of the RAM is undefined, reading it will throw an XException

Arguments

 :: (KnownNat n, HiddenClock dom, HiddenEnable dom, HasCallStack, NFDataX a) => Signal dom (Unsigned n) Read address r -> Signal dom (Maybe (Unsigned n, a)) (write address w, value to write) -> Signal dom a Value of the RAM at address r

Create a RAM with space for 2^n elements

• NB: Initial content of the RAM is undefined, reading it will throw an XException

# BlockRAM primitives

Arguments

 :: (HasCallStack, HiddenClock dom, HiddenEnable dom, NFDataX a, Enum addr) => Vec n a Initial content of the BRAM, also determines the size, n, of the BRAM.NB: MUST be a constant. -> Signal dom addr Read address r -> Signal dom (Maybe (addr, a)) (write address w, value to write) -> Signal dom a Value of the blockRAM at address r from the previous clock cycle

Create a blockRAM with space for n elements.

• NB: Read value is delayed by 1 cycle
• NB: Initial output value is undefined, reading it will throw an XException
bram40
:: HiddenClock dom
=> Signal dom (Unsigned 6)
-> Signal dom (Maybe (Unsigned 6, Bit))
-> Signal dom Bit
bram40 = blockRam (replicate d40 1)


• See Clash.Prelude.BlockRam for more information on how to use a Block RAM.
• Use the adapter readNew for obtaining write-before-read semantics like this: readNew (blockRam inits) rd wrM.
• A large Vec for the initial content might be too inefficient, depending on how it is constructed. See blockRamFile and blockRamBlob for different approaches that scale well.

Arguments

 :: (HasCallStack, HiddenClock dom, HiddenEnable dom, NFDataX a, KnownNat n) => Vec (2 ^ n) a Initial content of the BRAMNB: MUST be a constant. -> Signal dom (Unsigned n) Read address r -> Signal dom (Maybe (Unsigned n, a)) (write address w, value to write) -> Signal dom a Value of the blockRAM at address r from the previous clock cycle

Create a blockRAM with space for 2^n elements

• NB: Read value is delayed by 1 cycle
• NB: Initial output value is undefined, reading it will throw an XException
bram32
:: HiddenClock dom
=> Signal dom (Unsigned 5)
-> Signal dom (Maybe (Unsigned 5, Bit))
-> Signal dom Bit
bram32 = blockRamPow2 (replicate d32 1)


• See Clash.Prelude.BlockRam for more information on how to use a Block RAM.
• Use the adapter readNew for obtaining write-before-read semantics like this: readNew (blockRamPow2 inits) rd wrM.
• A large Vec for the initial content might be too inefficient, depending on how it is constructed. See blockRamFilePow2 and blockRamBlobPow2 for different approaches that scale well.

## BlockRAM primitives initialized with a MemBlob

Arguments

 :: forall dom addr m n. (HiddenClock dom, HiddenEnable dom, Enum addr) => MemBlob n m Initial content of the RAM, also determines the size, n, of the RAMNB: MUST be a constant -> Signal dom addr Read address r -> Signal dom (Maybe (addr, BitVector m)) (write address w, value to write) -> Signal dom (BitVector m) Value of the blockRAM at address r from the previous clock cycle

Create a blockRAM with space for n elements

• NB: Read value is delayed by 1 cycle
• NB: Initial output value is undefined, reading it will throw an XException

• See Clash.Prelude.BlockRam for more information on how to use a Block RAM.
• Use the adapter readNew for obtaining write-before-read semantics like this: readNew (blockRamBlob content) rd wrM.

Arguments

 :: forall dom m n. (HiddenClock dom, HiddenEnable dom, KnownNat n) => MemBlob (2 ^ n) m Initial content of the RAM, also determines the size, 2^n, of the RAMNB: MUST be a constant -> Signal dom (Unsigned n) Read address r -> Signal dom (Maybe (Unsigned n, BitVector m)) (write address w, value to write) -> Signal dom (BitVector m) Value of the blockRAM at address r from the previous clock cycle

Create a blockRAM with space for 2^n elements

• NB: Read value is delayed by 1 cycle
• NB: Initial output value is undefined, reading it will throw an XException

• See Clash.Prelude.BlockRam for more information on how to use a Block RAM.
• Use the adapter readNew for obtaining write-before-read semantics like this: readNew (blockRamBlobPow2 content) rd wrM.

### Creating and inspecting MemBlob

data MemBlob (n :: Nat) (m :: Nat) Source #

Efficient storage of memory content

It holds n words of BitVector m.

#### Instances

Instances details
 Show (MemBlob n m) Source # Instance detailsDefined in Clash.Explicit.BlockRam.Internal MethodsshowsPrec :: Int -> MemBlob n m -> ShowS #show :: MemBlob n m -> String #showList :: [MemBlob n m] -> ShowS #

Arguments

 :: forall a f. (Foldable f, BitPack a) => String Name of the binding to generate -> Maybe Bit Value to map don't care bits to. Nothing means throwing an error on don't care bits. -> f a The content for the MemBlob -> DecsQ

Create a MemBlob binding from a list of values

Since this uses Template Haskell, nothing in the arguments given to createMemBlob can refer to something defined in the same module.

### Example

Expand
createMemBlob "content" Nothing [15 :: Unsigned 8 .. 17]

ram clk en = blockRamBlob clk en content


The Maybe datatype has don't care bits, where the actual value does not matter. But the bits need a defined value in the memory. Either 0 or 1 can be used, and both are valid representations of the data.

>>> import qualified Prelude as P
>>> let es = [ Nothing, Just (7 :: Unsigned 8), Just 8 ]
>>> :{
createMemBlob "content0" (Just 0) es
createMemBlob "content1" (Just 1) es
x = 1
:}

>>> let pr = mapM_ (putStrLn . show)
>>> pr $P.map pack es 0b0_...._.... 0b1_0000_0111 0b1_0000_1000 >>> pr$ unpackMemBlob content0
0b0_0000_0000
0b1_0000_0111
0b1_0000_1000
>>> pr $unpackMemBlob content1 0b0_1111_1111 0b1_0000_0111 0b1_0000_1000 >>> :{ createMemBlob "contentN" Nothing es x = 1 :} <interactive>:...: error: packBVs: cannot convert don't care values. Please specify a mapping to a definite value.  Note how we hinted to clashi that our multi-line command was a list of declarations by including a dummy declaration x = 1. Without this trick, clashi would expect an expression and the Template Haskell would not work. Arguments  :: forall a f. (Foldable f, BitPack a) => Maybe Bit Value to map don't care bits to. Nothing means throwing an error on don't care bits. -> f a The content for the MemBlob -> ExpQ Create a MemBlob from a list of values Since this uses Template Haskell, nothing in the arguments given to memBlobTH can refer to something defined in the same module. ### Example Expand ram clk en = blockRamBlob clk en$(memBlobTH Nothing [15 :: Unsigned 8 .. 17])


The Maybe datatype has don't care bits, where the actual value does not matter. But the bits need a defined value in the memory. Either 0 or 1 can be used, and both are valid representations of the data.

>>> import qualified Prelude as P
>>> let es = [ Nothing, Just (7 :: Unsigned 8), Just 8 ]
>>> content0 = $(memBlobTH (Just 0) es) >>> content1 =$(memBlobTH (Just 1) es)
>>> let pr = mapM_ (putStrLn . show)
>>> pr $P.map pack es 0b0_...._.... 0b1_0000_0111 0b1_0000_1000 >>> pr$ unpackMemBlob content0
0b0_0000_0000
0b1_0000_0111
0b1_0000_1000
>>> pr $unpackMemBlob content1 0b0_1111_1111 0b1_0000_0111 0b1_0000_1000 >>> $(memBlobTH Nothing es)

<interactive>:...: error:
• packBVs: cannot convert don't care values. Please specify a mapping to a definite value.
• In the untyped splice: $(memBlobTH Nothing es)  unpackMemBlob :: forall n m. MemBlob n m -> [BitVector m] Source # Convert a MemBlob back to a list NB: Not synthesizable ## BlockRAM read/write conflict resolution Arguments  :: (HiddenClockResetEnable dom, NFDataX a, Eq addr) => (Signal dom addr -> Signal dom (Maybe (addr, a)) -> Signal dom a) The ram component -> Signal dom addr Read address r -> Signal dom (Maybe (addr, a)) (Write address w, value to write) -> Signal dom a Value of the ram at address r from the previous clock cycle Create read-after-write blockRAM from a read-before-write one (synchronized to system clock) >>> import Clash.Prelude >>> :t readNew (blockRam (0 :> 1 :> Nil)) readNew (blockRam (0 :> 1 :> Nil)) :: ... ... ... ... ... => Signal dom addr -> Signal dom (Maybe (addr, a)) -> Signal dom a  ## True dual-port block RAM Arguments  :: forall nAddrs dom1 dom2 a. (HasCallStack, KnownNat nAddrs, HiddenClock dom1, HiddenClock dom2, NFDataX a) => Signal dom1 (RamOp nAddrs a) RAM operation for port A -> Signal dom2 (RamOp nAddrs a) RAM operation for port B -> (Signal dom1 a, Signal dom2 a) Outputs data on next cycle. When writing, the data written will be echoed. When reading, the read data is returned. Produces vendor-agnostic HDL that will be inferred as a true dual-port block RAM Any value that is being written on a particular port is also the value that will be read on that port, i.e. the same-port read/write behavior is: WriteFirst. For mixed-port read/write, when port A writes to the address port B reads from, the output of port B is undefined, and vice versa. data RamOp n a Source # Port operation Constructors  RamRead (Index n) Read from address RamWrite (Index n) a Write data to address RamNoOp No operation #### Instances Instances details  Show a => Show (RamOp n a) Source # Instance detailsDefined in Clash.Explicit.BlockRam MethodsshowsPrec :: Int -> RamOp n a -> ShowS #show :: RamOp n a -> String #showList :: [RamOp n a] -> ShowS # Generic (RamOp n a) Source # Instance detailsDefined in Clash.Explicit.BlockRam Associated Typestype Rep (RamOp n a) :: Type -> Type # Methodsfrom :: RamOp n a -> Rep (RamOp n a) x #to :: Rep (RamOp n a) x -> RamOp n a # NFDataX a => NFDataX (RamOp n a) Source # Instance detailsDefined in Clash.Explicit.BlockRam MethodsdeepErrorX :: String -> RamOp n a Source #hasUndefined :: RamOp n a -> Bool Source #ensureSpine :: RamOp n a -> RamOp n a Source #rnfX :: RamOp n a -> () Source # type Rep (RamOp n a) Source # Instance detailsDefined in Clash.Explicit.BlockRam type Rep (RamOp n a) = D1 ('MetaData "RamOp" "Clash.Explicit.BlockRam" "clash-prelude-1.5.0-inplace" 'False) (C1 ('MetaCons "RamRead" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Index n))) :+: (C1 ('MetaCons "RamWrite" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Index n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "RamNoOp" 'PrefixI 'False) (U1 :: Type -> Type))) # Utility functions Arguments  :: (HiddenClockResetEnable dom, NFDataX a, Bounded a, Eq a) => a Starting value -> Signal dom a -> Signal dom Bool Give a pulse when the Signal goes from minBound to maxBound Arguments  :: (HiddenClockResetEnable dom, NFDataX a, Bounded a, Eq a) => a Starting value -> Signal dom a -> Signal dom Bool Give a pulse when the Signal goes from maxBound to minBound riseEvery :: HiddenClockResetEnable dom => SNat n -> Signal dom Bool Source # Give a pulse every n clock cycles. This is a useful helper function when combined with functions like regEn or mux, in order to delay a register by a known amount. To be precise: the given signal will be False for the next n-1 cycles, followed by a single True value: >>> Prelude.last (sampleN @System 1025 (riseEvery d1024)) == True True >>> Prelude.or (sampleN @System 1024 (riseEvery d1024)) == False True  For example, to update a counter once every 10 million cycles: counter = regEn 0 (riseEvery (SNat :: SNat 10000000)) (counter + 1)  oscillate :: HiddenClockResetEnable dom => Bool -> SNat n -> Signal dom Bool Source # Oscillate a Bool for a given number of cycles. This is a convenient function when combined with something like regEn, as it allows you to easily hold a register value for a given number of cycles. The input Bool determines what the initial value is. To oscillate on an interval of 5 cycles: >>> sampleN @System 11 (oscillate False d5) [False,False,False,False,False,False,True,True,True,True,True]  To oscillate between True and False: >>> sampleN @System 11 (oscillate False d1) [False,False,True,False,True,False,True,False,True,False,True]  An alternative definition for the above could be: >>> let osc' = register False (not <$> osc')
>>> sampleN @System 200 (oscillate False d1) == sampleN @System 200 osc'
True


# Exported modules

## Datatypes

### Fixed size vectors

data Vec :: Nat -> Type -> Type where Source #

Fixed size vectors.

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

Constructors

 Nil :: Vec 0 a Cons :: a -> Vec n a -> Vec (n + 1) a infixr 5

Bundled Patterns

 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  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 

#### Instances

Instances details
 Lift a => Lift (Vec n a :: Type) Source # Instance detailsDefined in Clash.Sized.Vector Methodslift :: Vec n a -> Q Exp #liftTyped :: Vec n a -> Q (TExp (Vec n a)) # Functor (Vec n) Source # Instance detailsDefined in Clash.Sized.Vector Methodsfmap :: (a -> b) -> Vec n a -> Vec n b #(<$) :: a -> Vec n b -> Vec n a # KnownNat n => Applicative (Vec n) Source # Instance detailsDefined in Clash.Sized.Vector Methodspure :: a -> Vec n a #(<*>) :: Vec n (a -> b) -> Vec n a -> Vec n b #liftA2 :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c #(*>) :: Vec n a -> Vec n b -> Vec n b #(<*) :: Vec n a -> Vec n b -> Vec n a # (KnownNat n, 1 <= n) => Foldable (Vec n) Source # Instance detailsDefined in Clash.Sized.Vector Methodsfold :: Monoid m => Vec n m -> m #foldMap :: Monoid m => (a -> m) -> Vec n a -> m #foldMap' :: Monoid m => (a -> m) -> Vec n a -> m #foldr :: (a -> b -> b) -> b -> Vec n a -> b #foldr' :: (a -> b -> b) -> b -> Vec n a -> b #foldl :: (b -> a -> b) -> b -> Vec n a -> b #foldl' :: (b -> a -> b) -> b -> Vec n a -> b #foldr1 :: (a -> a -> a) -> Vec n a -> a #foldl1 :: (a -> a -> a) -> Vec n a -> a #toList :: Vec n a -> [a] #null :: Vec n a -> Bool #length :: Vec n a -> Int #elem :: Eq a => a -> Vec n a -> Bool #maximum :: Ord a => Vec n a -> a #minimum :: Ord a => Vec n a -> a #sum :: Num a => Vec n a -> a #product :: Num a => Vec n a -> a # (KnownNat n, 1 <= n) => Traversable (Vec n) Source # Instance detailsDefined in Clash.Sized.Vector Methodstraverse :: Applicative f => (a -> f b) -> Vec n a -> f (Vec n b) #sequenceA :: Applicative f => Vec n (f a) -> f (Vec n a) #mapM :: Monad m => (a -> m b) -> Vec n a -> m (Vec n b) #sequence :: Monad m => Vec n (m a) -> m (Vec n a) # (KnownNat n, Eq a) => Eq (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector Methods(==) :: Vec n a -> Vec n a -> Bool #(/=) :: Vec n a -> Vec n a -> Bool # (KnownNat n, Typeable a, Data a) => Data (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Vec n a -> c (Vec n a) #gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Vec n a) #toConstr :: Vec n a -> Constr #dataTypeOf :: Vec n a -> DataType #dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Vec n a)) #dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Vec n a)) #gmapT :: (forall b. Data b => b -> b) -> Vec n a -> Vec n a #gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Vec n a -> r #gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Vec n a -> r #gmapQ :: (forall d. Data d => d -> u) -> Vec n a -> [u] #gmapQi :: Int -> (forall d. Data d => d -> u) -> Vec n a -> u #gmapM :: Monad m => (forall d. Data d => d -> m d) -> Vec n a -> m (Vec n a) #gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Vec n a -> m (Vec n a) #gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Vec n a -> m (Vec n a) # (KnownNat n, Ord a) => Ord (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector Methodscompare :: Vec n a -> Vec n a -> Ordering #(<) :: Vec n a -> Vec n a -> Bool #(<=) :: Vec n a -> Vec n a -> Bool #(>) :: Vec n a -> Vec n a -> Bool #(>=) :: Vec n a -> Vec n a -> Bool #max :: Vec n a -> Vec n a -> Vec n a #min :: Vec n a -> Vec n a -> Vec n a # Show a => Show (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector MethodsshowsPrec :: Int -> Vec n a -> ShowS #show :: Vec n a -> String #showList :: [Vec n a] -> ShowS # 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 detailsDefined in Clash.Sized.Vector Associated Typestype Rep (Vec n a) :: Type -> Type # Methodsfrom :: Vec n a -> Rep (Vec n a) x #to :: Rep (Vec n a) x -> Vec n a # (KnownNat n, Semigroup a) => Semigroup (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector Methods(<>) :: Vec n a -> Vec n a -> Vec n a #sconcat :: NonEmpty (Vec n a) -> Vec n a #stimes :: Integral b => b -> Vec n a -> Vec n a # (KnownNat n, Monoid a) => Monoid (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector Methodsmempty :: Vec n a #mappend :: Vec n a -> Vec n a -> Vec n a #mconcat :: [Vec n a] -> Vec n a # (KnownNat n, Arbitrary a) => Arbitrary (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector Methodsarbitrary :: Gen (Vec n a) #shrink :: Vec n a -> [Vec n a] # CoArbitrary a => CoArbitrary (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector Methodscoarbitrary :: Vec n a -> Gen b -> Gen b # (Default a, KnownNat n) => Default (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector Methodsdef :: Vec n a # NFData a => NFData (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector Methodsrnf :: Vec n a -> () # KnownNat n => Ixed (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector Methodsix :: Index (Vec n a) -> Traversal' (Vec n a) (IxValue (Vec n a)) # (NFDataX a, KnownNat n) => NFDataX (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector MethodsdeepErrorX :: 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 detailsDefined in Clash.Sized.Vector MethodsshowsPrecX :: Int -> Vec n a -> ShowS Source #showX :: Vec n a -> String Source #showListX :: [Vec n a] -> ShowS Source # (KnownNat n, BitPack a) => BitPack (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector Associated Typestype BitSize (Vec n a) :: Nat Source # Methodspack :: 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 detailsDefined in Clash.Signal.Bundle Associated Typestype Unbundled dom (Vec n a) = (res :: Type) Source # Methodsbundle :: 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 detailsDefined in Clash.Signal.Delayed.Bundle Associated Typestype Unbundled dom d (Vec n a) = (res :: Type) Source # Methodsbundle :: 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 # (KnownNat n, AutoReg a) => AutoReg (Vec n a) Source # Instance detailsDefined in Clash.Class.AutoReg.Internal MethodsautoReg :: 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 # (LockStep en a, KnownNat n) => LockStep (Vec n en) (Vec n a) Source # Instance detailsDefined in Clash.Prelude.DataFlow MethodslockStep :: 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 detailsDefined in Clash.Signal.Delayed.Bundle type Unbundled t d (Vec n a) = Vec n (DSignal t d a) type HasDomain dom (Vec n a) Source # Instance detailsDefined in Clash.Class.HasDomain.HasSpecificDomain type HasDomain dom (Vec n a) = HasDomain dom a type TryDomain t (Vec n a) Source # Instance detailsDefined in Clash.Class.HasDomain.HasSingleDomain type TryDomain t (Vec n a) = TryDomain t a type Unbundled t (Vec n a) Source # Instance detailsDefined in Clash.Signal.Bundle type Unbundled t (Vec n a) = Vec n (Signal t a) type Rep (Vec n a) Source # Instance detailsDefined 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 detailsDefined in Clash.Sized.Vector type Index (Vec n a) = Index n type IxValue (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector type IxValue (Vec n a) = a type BitSize (Vec n a) Source # Instance detailsDefined in Clash.Sized.Vector type BitSize (Vec n a) = n * BitSize a foldl :: (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)). foldr :: (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)). map :: (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: bv2v :: KnownNat n => BitVector n -> Vec n Bit Source # Convert a BitVector to a Vec of Bits. >>> let x = 6 :: BitVector 8 >>> x 0b0000_0110 >>> bv2v x 0 :> 0 :> 0 :> 0 :> 0 :> 1 :> 1 :> 0 :> Nil  data VCons (a :: Type) (f :: TyFun Nat Type) :: 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 detailsDefined in Clash.Sized.Vector type Apply (VCons a :: TyFun Nat Type -> Type) (l :: Nat) = Vec l a traverse# :: forall a f b n. Applicative f => (a -> f b) -> Vec n a -> f (Vec n b) Source # singleton :: a -> Vec 1 a Source # Create a vector of one element >>> singleton 5 5 :> Nil  head :: Vec (n + 1) a -> a Source # Extract the first element of a vector >>> head (1:>2:>3:>Nil) 1  # 391 "srcClashSized/Vector.hs" >>> head Nil BLANKLINE interactive:... • Couldn't match type ‘1’ with ‘0’ Expected type: Vec (0 + 1) a Actual type: Vec 0 a • In the first argument of ‘head’, namely ‘Nil’ In the expression: head Nil In an equation for ‘it’: it = head Nil tail :: 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  # 425 "srcClashSized/Vector.hs" >>> tail Nil BLANKLINE interactive:... • Couldn't match type ‘1’ with ‘0’ Expected type: Vec (0 + 1) a Actual type: Vec 0 a • In the first argument of ‘tail’, namely ‘Nil’ In the expression: tail Nil In an equation for ‘it’: it = tail Nil last :: Vec (n + 1) a -> a Source # Extract the last element of a vector >>> last (1:>2:>3:>Nil) 3  # 459 "srcClashSized/Vector.hs" >>> last Nil BLANKLINE interactive:... • Couldn't match type ‘1’ with ‘0’ Expected type: Vec (0 + 1) a Actual type: Vec 0 a • In the first argument of ‘last’, namely ‘Nil’ In the expression: last Nil In an equation for ‘it’: it = last Nil init :: 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  # 494 "srcClashSized/Vector.hs" >>> init Nil BLANKLINE interactive:... • Couldn't match type ‘1’ with ‘0’ Expected type: Vec (0 + 1) a Actual type: Vec 0 a • In the first argument of ‘init’, namely ‘Nil’ In the expression: init Nil In an equation for ‘it’: it = init Nil Arguments  :: 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)  Arguments  :: 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)  (+>>) :: 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  (<<+) :: 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  Arguments  :: (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)  Arguments  :: (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)  (++) :: 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  splitAt :: 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 :: 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)  concat :: 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 :: (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  unconcat :: 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 :: (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  merge :: 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  reverse :: 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  imap :: forall n 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 -> fromIntegral 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: izipWith :: 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 3 is out of bounds: [0..1] ...  >>> izipWith (\i a b -> fromIntegral 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. ifoldr :: 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 :: 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: indices :: KnownNat n => SNat n -> Vec n (Index n) Source # Generate a vector of indices. >>> indices d4 0 :> 1 :> 2 :> 3 :> Nil  indicesI :: 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 :: 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 :: (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  zipWith :: (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 :: (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 :: (a -> b -> c -> d -> e) -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e Source # zipWith5 :: (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 :: (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 :: (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 # foldr1 :: (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 :: (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 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: scanl :: (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 postscanl :: (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: scanr :: (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 postscanr :: (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 :: (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 :: (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: zip :: 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 :: 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 :: 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 :: 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 :: 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 :: 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. unzip :: 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 :: 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 :: 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 :: 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 :: 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 :: 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. (!!) :: (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 ...  length :: KnownNat n => Vec n a -> Int Source # The length of a Vector as an Int value. >>> length (6 :> 7 :> 8 :> Nil) 3  replace :: (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 ...  take :: 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  # 1432 "srcClashSized/Vector.hs" >>> take d4 (1:>2:>Nil) BLANKLINE interactive:... • Couldn't match type ‘4 + n0’ with ‘2’ Expected type: Vec (4 + n0) a Actual type: 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) takeI :: 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 :: 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  dropI :: 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  at :: 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  select :: 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 :: (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  replicate :: 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 :: 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 :: 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 a. KnownNat n => (a -> a) -> a -> Vec n a Source # "iterate 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: unfoldr :: 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 :: KnownNat n => (s -> (a, s)) -> s -> Vec n a Source # "'unfoldr 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  generate :: 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 :: 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: transpose :: 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  Arguments  :: 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  Arguments  :: (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 b => Vec 3 (Vec 3 b) >>> stencil2d d2 d2 (sum . map sum) xss (14 :> 18 :> 22 :> Nil) :> (30 :> 34 :> 38 :> Nil) :> (46 :> 50 :> 54 :> Nil) :> Nil  Arguments  :: 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  Arguments  :: (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  Arguments  :: (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. Arguments  :: (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  Arguments  :: (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. Arguments  :: (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  Arguments  :: (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 :: (Enum i, KnownNat n) => Vec n a -> i -> Vec n a Source # Dynamically rotate a Vector 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 :: (Enum i, KnownNat n) => Vec n a -> i -> Vec n a Source # Dynamically rotate a Vector 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 :: KnownNat n => Vec n a -> SNat d -> Vec n a Source # Statically rotate a Vector 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 :: KnownNat n => Vec n a -> SNat d -> Vec n a Source # Statically rotate a Vector 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. toList :: 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 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


asNatProxy :: Vec n a -> Proxy n Source #

Vector as a Proxy for Nat

lengthS :: KnownNat n => Vec n a -> SNat n Source #

Length of a Vector as an SNat value

lazyV :: 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 zipWiths 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


Arguments

 :: forall p k a. KnownNat k => Proxy (p :: TyFun Nat Type -> Type) The motive -> (forall l. 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)).

Arguments

 :: forall p k a. KnownNat k => Proxy (p :: TyFun Nat Type -> Type) The motive -> (a -> p @@ 0) Function to apply to every element -> (forall l. 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 addes:

# 2271 "srcClashSized/Vector.hs" >>> :{ let populationCount' :: (KnownNat (n+1), KnownNat (n+2)) => BitVector (n+1) -> Index (n+2) populationCount' = fold add . map fromIntegral . bv2v :} BLANKLINE interactive:... • Couldn't match type ‘((n + 2) + (n + 2)) - 1’ with ‘n + 2’ Expected type: Index (n + 2) -> Index (n + 2) -> Index (n + 2) Actual type: 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 ...)

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 a b. KnownNat k => (forall l. 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:

smap :: forall k a b. KnownNat k => (forall l. 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


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

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

v2bv :: KnownNat n => Vec n Bit -> BitVector n Source #

Convert a Vec of Bits 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


seqV :: KnownNat n => Vec n a -> b -> b infixr 0 Source #

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

forceV :: KnownNat n => Vec n a -> Vec n a Source #

Evaluate all elements of a vector to WHNF

seqVX :: 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 XExceptions.

forceVX :: KnownNat n => Vec n a -> Vec n a Source #

Evaluate all elements of a vector to WHNF. Does not propagate XExceptions.

## Generics type-classes

class Generic a #

Representable types of kind *. This class is derivable in GHC with the DeriveGeneric flag on.

A Generic instance must satisfy the following laws:

from . to ≡ id
to . from ≡ id


Minimal complete definition

#### Instances

Instances details