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

import qualified Data.List as L

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

mac
  :: KnownDomain dom
  => Clock dom
  -> Reset dom
  -> Enable dom
  -> Signal dom (Int, Int)
  -> Signal dom Int
mac clk rst en = mealy clk rst en macT 0

>>> simulate (mac systemClockGen systemResetGen enableGen) [(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
  :: KnownDomain dom
  => Clock dom
  -> Reset dom
  -> Enable dom
  -> (Signal dom Int, Signal dom Int)
  -> (Signal dom Int, Signal dom Int)
  -> Signal dom Int
dualMac clk rst en (a,b) (x,y) = s1 + s2
  where
    s1 = mealy clk rst en macT 0 (bundle (a,x))
    s2 = mealy clk rst en macT 0 (bundle (b,y))

Create a synchronous function from a combinational function describing a mealy machine using the state monad. This can be particularly useful when combined with lenses or optics to replicate imperative algorithms.

data DelayState = DelayState
  { _history    :: Vec 4 Int
  , _untilValid :: Index 4
  }
  deriving (Generic, NFDataX)
makeLenses ''DelayState

initialDelayState = DelayState (repeat 0) maxBound

delayS :: Int -> State DelayState (Maybe Int)
delayS n = do
  history   %= (n +>>)
  remaining <- use untilValid
  if remaining > 0
  then do
     untilValid -= 1
     return Nothing
   else do
     out <- uses history last
     return (Just out)

delayTop ::KnownDomain dom
  => Clock dom
  -> Reset dom
  -> Enable dom
  -> (Signal dom Int -> Signal dom (Maybe Int))
delayTop clk rst en = mealyS clk rst en delayS initialDelayState

>>> L.take 7 $ simulate (delayTop systemClockGen systemResetGen enableGen) [-100,1,2,3,4,5,6,7,8]
[Nothing,Nothing,Nothing,Nothing,Just 1,Just 2,Just 3]

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 clk rst en a b c = (b1,b2,i2)
  where
    (i1,b1) = unbundle (mealy clk rst en f 0 (bundle (a,b)))
    (i2,b2) = unbundle (mealy clk rst en f 3 (bundle (c,i1)))

Using mealyB however we can write:

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

A version of mealyS that does automatic Bundleing, see mealyB for details.

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

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

mac
  :: KnownDomain dom
  => Clock dom
  -> Reset dom
  -> Enable dom
  -> Signal dom (Int, Int)
  -> Signal dom Int
mac clk rst en = moore clk rst en macT id 0

>>> simulate (mac systemClockGen systemResetGen enableGen) [(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
  :: KnownDomain dom
  => Clock dom
  -> Reset dom
  -> Enable dom
  -> (Signal dom Int, Signal dom Int)
  -> (Signal dom Int, Signal dom Int)
  -> Signal dom Int
dualMac clk rst en (a,b) (x,y) = s1 + s2
  where
    s1 = moore clk rst en macT id 0 (bundle (a,x))
    s2 = moore clk rst en macT id 0 (bundle (b,y))

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 clk rst en a b c = (b1,b2,i2)
  where
    (i1,b1) = unbundle (moore clk rst en t o 0 (bundle (a,b)))
    (i2,b2) = unbundle (moore clk rst en t o 3 (bundle (c,i1)))

Using mooreB however we can write:

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

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

rP :: Clock dom -> Reset dom -> Enable dom
   -> (Signal dom Int, Signal dom Int)
   -> (Signal dom Int, Signal dom Int)
rP clk rst en = registerB clk rst en (8,8)

>>> simulateB (rP systemClockGen systemResetGen enableGen) [(1,1),(1,1),(2,2),(3,3)] :: [(Int,Int)]
[(8,8),(8,8),(1,1),(2,2),(3,3)...
...

Synchronizer based on two sequentially connected flip-flops.

• NB: This synchronizer can be used for bit-synchronization.

• NB: Although this synchronizer does reduce metastability, it does not guarantee the proper synchronization of a whole word. For example, given that the output is sampled twice as fast as the input is running, and we have two samples in the input stream that look like:

  [0111,1000]

  But the circuit driving the input stream has a longer propagation delay on msb compared to the lsbs. What can happen is an output stream that looks like this:

  [0111,0111,0000,1000]

  Where the level-change of the msb was not captured, but the level change of the lsbs were.

  If you want to have safe word-synchronization use asyncFIFOSynchronizer.

Synchronizer implemented as a FIFO around a synchronous RAM. Based on the design described in Clash.Tutorial, which is itself based on the design described in http://www.sunburst-design.com/papers/CummingsSNUG2002SJ_FIFO1.pdf. However, this FIFO uses a synchronous dual-ported RAM which, unlike those designs using RAM with an asynchronous read port, is nearly guaranteed to actually synthesize into one of the dual-ported RAMs found on most FPGAs.

NB: This synchronizer can be used for word-synchronization. NB: This synchronizer will only work safely when you set up the proper bus skew and maximum delay constraints inside your synthesis tool for the clock domain crossings of the gray pointers.

An asynchronous/combinational ROM with space for n elements

See also:

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

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

See also:

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

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

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

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

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

An asynchronous/combinational ROM with space for n elements

See also:

• See Clash.Sized.Fixed and Clash.Prelude.BlockRam for ideas on how to use ROMs and RAMs.

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

See also:

• See Clash.Sized.Fixed and Clash.Prelude.BlockRam for ideas on how to use ROMs and RAMs.

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

• See Clash.Sized.Fixed and Clash.Explicit.BlockRam for ideas on how to use ROMs and RAMs.

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

• See Clash.Sized.Fixed and Clash.Explicit.BlockRam for ideas on how to use ROMs and RAMs.

An asynchronous/combinational ROM with space for n elements

• NB: This function might not work for specific combinations of code-generation backends and hardware targets. Please check the support table below:

See also:

• See Clash.Prelude.ROM.File for more information on how to instantiate a ROM with the contents of a data file.
• See Clash.Sized.Fixed for ideas on how to create your own data files.

• When you notice that asyncRomFile is significantly slowing down your simulation, give it a monomorphic type signature. So instead of leaving the type to be inferred:

  myRomData = asyncRomFile d512 "memory.bin"
  

  or giving it a polymorphic type signature:

  myRomData :: Enum addr => addr -> BitVector 16
  myRomData = asyncRomFile d512 "memory.bin"
  

  you should give it a monomorphic type signature:

  myRomData :: Unsigned 9 -> BitVector 16
  myRomData = asyncRomFile d512 "memory.bin"
  

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

• NB: This function might not work for specific combinations of code-generation backends and hardware targets. Please check the support table below:

See also:

• See Clash.Prelude.ROM.File for more information on how to instantiate a ROM with the contents of a data file.
• See Clash.Sized.Fixed for ideas on how to create your own data files.

• When you notice that asyncRomFilePow2 is significantly slowing down your simulation, give it a monomorphic type signature. So instead of leaving the type to be inferred:

  myRomData = asyncRomFilePow2 "memory.bin"
  

  you should give it a monomorphic type signature:

  myRomData :: Unsigned 9 -> BitVector 16
  myRomData = asyncRomFilePow2 "memory.bin"
  

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
• NB: This function might not work for specific combinations of code-generation backends and hardware targets. Please check the support table below:

See also:

• See Clash.Explicit.ROM.File for more information on how to instantiate a ROM with the contents of a data file.
• See memFile for creating a data file with Clash.
• See Clash.Sized.Fixed for ideas on how to create your own data files.

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
• NB: This function might not work for specific combinations of code-generation backends and hardware targets. Please check the support table below:

See also:

• See Clash.Explicit.ROM.File for more information on how to instantiate a ROM with the contents of a data file.
• See memFile for creating a data file with Clash.
• See Clash.Sized.Fixed for more ideas on how to create your own data files.

Create a RAM with space for n elements

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

See also:

• See Clash.Explicit.BlockRam for more information on how to use a RAM.

Create a RAM with space for 2^n elements

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

See also:

• See Clash.Prelude.BlockRam for more information on how to use a RAM.

Create a block RAM 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 also:

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

Example

bram40
  :: Clock  dom
  -> Enable  dom
  -> Signal dom (Unsigned 6)
  -> Signal dom (Maybe (Unsigned 6, Bit))
  -> Signal dom Bit
bram40 clk en = blockRam clk en (replicate d40 1)

Create a block RAM 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 also:

• 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 clk rst en (blockRamPow2 clk inits) rd wrM.
• A large Vec for the initial content may be too inefficient, depending on how it is constructed. See blockRamFilePow2 and blockRamBlobPow2 for different approaches that scale well.

Example

bram32
  :: Clock dom
  -> Enable dom
  -> Signal dom (Unsigned 5)
  -> Signal dom (Maybe (Unsigned 5, Bit))
  -> Signal dom Bit
bram32 clk en = blockRamPow2 clk en (replicate d32 1)

A version of blockRam that has no default values set. May be cleared to an arbitrary state using a reset function.

A version of blockRam that is initialized with the same value on all memory positions

Create a block RAM 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 also:

• 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 clk rst en (blockRamBlob clk en content) rd wrM.

Create a block RAM 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 also:

• 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 clk rst en (blockRamBlobPow2 clk en content) rd wrM.

Efficient storage of memory content

It holds n words of BitVector m.

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

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

ram clk en = blockRamBlob clk en content

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

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

ram clk en = blockRamBlob clk en $(memBlobTH Nothing [15 :: Unsigned 8 .. 17])

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

Convert a MemBlob back to a list

NB: Not synthesizable

Create a block RAM 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
• NB: This function might not work for specific combinations of code-generation backends and hardware targets. Please check the support table below:

See also:

• See Clash.Explicit.BlockRam for more information on how to use a block RAM.
• Use the adapter readNew for obtaining write-before-read semantics like this: readNew clk rst en (blockRamFile clk en size file) rd wrM.
• See Clash.Explicit.BlockRam.File for more information on how to instantiate a block RAM with the contents of a data file.
• See memFile for creating a data file with Clash.
• See Clash.Sized.Fixed for more ideas on how to create your own data files.

Create a block RAM 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
• NB: This function might not work for specific combinations of code-generation backends and hardware targets. Please check the support table below:

See also:

• 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 clk rst en (blockRamFilePow2' clk en file) rd wrM.
• See Clash.Explicit.BlockRam.File for more information on how to instantiate a block RAM with the contents of a data file.
• See memFile for creating a data file with Clash.
• See Clash.Explicit.Fixed for more ideas on how to create your own data files.

Create a read-after-write block RAM from a read-before-write one

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.

Port operation

Give a window over a Signal

@ window4

Give a delayed window over a Signal

windowD3
  :: KnownDomain dom
  -> Clock dom
  -> Enable dom
  -> Reset dom
  -> Signal dom Int
  -> Vec 3 (Signal dom Int)
windowD3 = windowD

>>> simulateB (windowD3 systemClockGen resetGen enableGen) [1::Int,1,2,3,4] :: [Vec 3 Int]
[0 :> 0 :> 0 :> Nil,0 :> 0 :> 0 :> Nil,1 :> 0 :> 0 :> Nil,2 :> 1 :> 0 :> Nil,3 :> 2 :> 1 :> Nil,4 :> 3 :> 2 :> Nil,...
...

Give a pulse when the Signal goes from minBound to maxBound

Give a pulse when the Signal goes from maxBound to minBound

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.

Oscillate a Bool for a given number of cycles, given the starting state.

Compares the first two Signals for equality and logs a warning when they are not equal. The second Signal is considered the expected value. This function simply returns the third Signal unaltered as its result. This function is used by outputVerifier.

Usage in clashi

NB: When simulating a component that uses assert in clashi, usually, the warnings are only logged the first time the component is simulated. Issuing :reload in clashi will discard the cached result of the computation, and warnings will once again be emitted.

NB: This function can be used in synthesizable designs.

Example:

testInput
  :: KnownDomain dom
  => Clock dom
  -> Reset dom
  -> Signal dom Int
testInput clk rst = stimuliGenerator clk rst $(listToVecTH [(1::Int),3..21])

>>> sampleN 14 (testInput systemClockGen resetGen)
[1,1,3,5,7,9,11,13,15,17,19,21,21,21]

Same as outputVerifier but used in cases where the test bench domain and the domain of the circuit under test are the same.

Trace a single signal. Will emit an error if a signal with the same name was previously registered.

NB: Associates the traced signal with a clock period of 1, which results in incorrect VCD files when working with circuits that have multiple clocks. Use traceSignal when working with circuits that have multiple clocks.

Trace a single vector signal: each element in the vector will show up as a different trace. If the trace name already exists, this function will emit an error.

NB: Associates the traced signal with a clock period of 1, which results in incorrect VCD files when working with circuits that have multiple clocks. Use traceSignal when working with circuits that have multiple clocks.

Trace a single signal. Will emit an error if a signal with the same name was previously registered.

NB: Works correctly when creating VCD files from traced signal in multi-clock circuits. However traceSignal1 might be more convenient to use when the domain of your circuit is polymorphic.

Trace a single vector signal: each element in the vector will show up as a different trace. If the trace name already exists, this function will emit an error.

NB: Works correctly when creating VCD files from traced signal in multi-clock circuits. However traceSignal1 might be more convenient to use when the domain of your circuit is polymorphic.

Produce a four-state VCD (Value Change Dump) according to IEEE 1364-{1995,2001}. This function fails if a trace name contains either non-printable or non-VCD characters.

Due to lazy evaluation, the created VCD files might not contain all the traces you were expecting. You therefore have to provide a list of names you definately want to be dumped in the VCD file.

For example:

vcd <- dumpVCD (0, 100) cntrOut ["main", "sub"]

Evaluates cntrOut long enough in order for to guarantee that the main, and sub traces end up in the generated VCD file.

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.

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

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

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)

Create a vector of one element

>>> singleton 5
5 :> Nil

Extract the first element of a vector

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

>>> head Nil

<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

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

Extract the last element of a vector

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

>>> last Nil

<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

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

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)

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)

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

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

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)

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)

Append two vectors.

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

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)

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)

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

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

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

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

The elements in a vector in reverse order.

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

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:

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

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:

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:

Generate a vector of indices.

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

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

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