| Copyright | (C) 2013-2016 University of Twente 2017 Google Inc. 2019 Myrtle Software Ltd |
|---|---|
| License | BSD2 (see the file LICENSE) |
| Maintainer | Christiaan Baaij <christiaan.baaij@gmail.com> |
| Safe Haskell | Safe |
| Language | Haskell2010 |
| Extensions |
|
Clash.Explicit.Prelude.Safe
Description
This is the Safe API only of Clash.Explicit.Prelude
This module defines the explicitly clocked counterparts of the functions defined in Clash.Prelude.
Synopsis
- mealy :: (KnownDomain dom, NFDataX s) => Clock dom -> Reset dom -> Enable dom -> (s -> i -> (s, o)) -> s -> Signal dom i -> Signal dom o
- mealyB :: (KnownDomain dom, NFDataX s, Bundle i, Bundle o) => Clock dom -> Reset dom -> Enable dom -> (s -> i -> (s, o)) -> s -> Unbundled dom i -> Unbundled dom o
- moore :: (KnownDomain dom, NFDataX s) => Clock dom -> Reset dom -> Enable dom -> (s -> i -> s) -> (s -> o) -> s -> Signal dom i -> Signal dom o
- mooreB :: (KnownDomain dom, NFDataX s, Bundle i, Bundle o) => Clock dom -> Reset dom -> Enable dom -> (s -> i -> s) -> (s -> o) -> s -> Unbundled dom i -> Unbundled dom o
- registerB :: (KnownDomain dom, NFDataX a, Bundle a) => Clock dom -> Reset dom -> Enable dom -> a -> Unbundled dom a -> Unbundled dom a
- dualFlipFlopSynchronizer :: (NFDataX a, KnownDomain dom1, KnownDomain dom2) => Clock dom1 -> Clock dom2 -> Reset dom2 -> Enable dom2 -> a -> Signal dom1 a -> Signal dom2 a
- asyncFIFOSynchronizer :: (KnownDomain wdom, KnownDomain rdom, 2 <= addrSize) => SNat addrSize -> Clock wdom -> Clock rdom -> Reset wdom -> Reset rdom -> Enable wdom -> Enable rdom -> Signal rdom Bool -> Signal wdom (Maybe a) -> (Signal rdom a, Signal rdom Bool, Signal wdom Bool)
- asyncRom :: (KnownNat n, Enum addr) => Vec n a -> addr -> a
- asyncRomPow2 :: KnownNat n => Vec (2 ^ n) a -> Unsigned n -> a
- rom :: (KnownDomain dom, KnownNat n, NFDataX a, Enum addr) => Clock dom -> Enable dom -> Vec n a -> Signal dom addr -> Signal dom a
- romPow2 :: (KnownDomain dom, KnownNat n, NFDataX a) => Clock dom -> Enable dom -> Vec (2 ^ n) a -> Signal dom (Unsigned n) -> Signal dom a
- asyncRam :: (Enum addr, HasCallStack, KnownDomain wdom, KnownDomain rdom) => Clock wdom -> Clock rdom -> Enable wdom -> SNat n -> Signal rdom addr -> Signal wdom (Maybe (addr, a)) -> Signal rdom a
- asyncRamPow2 :: forall wdom rdom n a. (KnownNat n, HasCallStack, KnownDomain wdom, KnownDomain rdom) => Clock wdom -> Clock rdom -> Enable wdom -> Signal rdom (Unsigned n) -> Signal wdom (Maybe (Unsigned n, a)) -> Signal rdom a
- blockRam :: (KnownDomain dom, HasCallStack, NFDataX a, Enum addr) => Clock dom -> Enable dom -> Vec n a -> Signal dom addr -> Signal dom (Maybe (addr, a)) -> Signal dom a
- blockRamPow2 :: (KnownDomain dom, HasCallStack, NFDataX a, KnownNat n) => Clock dom -> Enable dom -> Vec (2 ^ n) a -> Signal dom (Unsigned n) -> Signal dom (Maybe (Unsigned n, a)) -> Signal dom a
- readNew :: (KnownDomain dom, NFDataX a, Eq addr) => Clock dom -> Reset dom -> Enable dom -> (Signal dom addr -> Signal dom (Maybe (addr, a)) -> Signal dom a) -> Signal dom addr -> Signal dom (Maybe (addr, a)) -> Signal dom a
- isRising :: (KnownDomain dom, NFDataX a, Bounded a, Eq a) => Clock dom -> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom Bool
- isFalling :: (KnownDomain dom, NFDataX a, Bounded a, Eq a) => Clock dom -> Reset dom -> Enable dom -> a -> Signal dom a -> Signal dom Bool
- riseEvery :: forall dom n. KnownDomain dom => Clock dom -> Reset dom -> Enable dom -> SNat n -> Signal dom Bool
- oscillate :: forall dom n. KnownDomain dom => Clock dom -> Reset dom -> Enable dom -> Bool -> SNat n -> Signal dom Bool
- module Clash.Explicit.Signal
- module Clash.Explicit.Signal.Delayed
- module Clash.Sized.BitVector
- module Clash.Prelude.BitIndex
- module Clash.Prelude.BitReduction
- module Clash.Sized.Signed
- module Clash.Sized.Unsigned
- module Clash.Sized.Index
- module Clash.Sized.Fixed
- data Vec :: Nat -> Type -> Type where
- foldl :: (b -> a -> b) -> b -> Vec n a -> b
- foldr :: (a -> b -> b) -> b -> Vec n a -> b
- map :: (a -> b) -> Vec n a -> Vec n b
- bv2v :: KnownNat n => BitVector n -> Vec n Bit
- data VCons (a :: Type) (f :: TyFun Nat Type) :: Type
- traverse# :: forall a f b n. Applicative f => (a -> f b) -> Vec n a -> f (Vec n b)
- singleton :: a -> Vec 1 a
- head :: Vec (n + 1) a -> a
- tail :: Vec (n + 1) a -> Vec n a
- last :: Vec (n + 1) a -> a
- init :: Vec (n + 1) a -> Vec n a
- shiftInAt0 :: KnownNat n => Vec n a -> Vec m a -> (Vec n a, Vec m a)
- shiftInAtN :: KnownNat m => Vec n a -> Vec m a -> (Vec n a, Vec m a)
- (+>>) :: KnownNat n => a -> Vec n a -> Vec n a
- (<<+) :: Vec n a -> a -> Vec n a
- shiftOutFrom0 :: (Default a, KnownNat m) => SNat m -> Vec (m + n) a -> (Vec (m + n) a, Vec m a)
- shiftOutFromN :: (Default a, KnownNat n) => SNat m -> Vec (m + n) a -> (Vec (m + n) a, Vec m a)
- (++) :: Vec n a -> Vec m a -> Vec (n + m) a
- splitAt :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
- splitAtI :: KnownNat m => Vec (m + n) a -> (Vec m a, Vec n a)
- concat :: Vec n (Vec m a) -> Vec (n * m) a
- concatMap :: (a -> Vec m b) -> Vec n a -> Vec (n * m) b
- unconcat :: KnownNat n => SNat m -> Vec (n * m) a -> Vec n (Vec m a)
- unconcatI :: (KnownNat n, KnownNat m) => Vec (n * m) a -> Vec n (Vec m a)
- merge :: KnownNat n => Vec n a -> Vec n a -> Vec (2 * n) a
- reverse :: Vec n a -> Vec n a
- imap :: forall n a b. KnownNat n => (Index n -> a -> b) -> Vec n a -> Vec n b
- izipWith :: KnownNat n => (Index n -> a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
- ifoldr :: KnownNat n => (Index n -> a -> b -> b) -> b -> Vec n a -> b
- ifoldl :: KnownNat n => (a -> Index n -> b -> a) -> a -> Vec n b -> a
- indices :: KnownNat n => SNat n -> Vec n (Index n)
- indicesI :: KnownNat n => Vec n (Index n)
- findIndex :: KnownNat n => (a -> Bool) -> Vec n a -> Maybe (Index n)
- elemIndex :: (KnownNat n, Eq a) => a -> Vec n a -> Maybe (Index n)
- zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
- zipWith3 :: (a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n d
- zipWith4 :: (a -> b -> c -> d -> e) -> Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e
- 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
- 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
- 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
- foldr1 :: (a -> a -> a) -> Vec (n + 1) a -> a
- foldl1 :: (a -> a -> a) -> Vec (n + 1) a -> a
- fold :: forall n a. (a -> a -> a) -> Vec (n + 1) a -> a
- scanl :: (b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
- postscanl :: (b -> a -> b) -> b -> Vec n a -> Vec n b
- scanr :: (a -> b -> b) -> b -> Vec n a -> Vec (n + 1) b
- postscanr :: (a -> b -> b) -> b -> Vec n a -> Vec n b
- mapAccumL :: (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y)
- mapAccumR :: (acc -> x -> (acc, y)) -> acc -> Vec n x -> (acc, Vec n y)
- zip :: Vec n a -> Vec n b -> Vec n (a, b)
- zip3 :: Vec n a -> Vec n b -> Vec n c -> Vec n (a, b, c)
- zip4 :: Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n (a, b, c, d)
- zip5 :: Vec n a -> Vec n b -> Vec n c -> Vec n d -> Vec n e -> Vec n (a, b, c, d, e)
- 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)
- 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)
- unzip :: Vec n (a, b) -> (Vec n a, Vec n b)
- unzip3 :: Vec n (a, b, c) -> (Vec n a, Vec n b, Vec n c)
- unzip4 :: Vec n (a, b, c, d) -> (Vec n a, Vec n b, Vec n c, Vec n d)
- unzip5 :: Vec n (a, b, c, d, e) -> (Vec n a, Vec n b, Vec n c, Vec n d, Vec n e)
- 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)
- 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)
- (!!) :: (KnownNat n, Enum i) => Vec n a -> i -> a
- length :: KnownNat n => Vec n a -> Int
- replace :: (KnownNat n, Enum i) => i -> a -> Vec n a -> Vec n a
- take :: SNat m -> Vec (m + n) a -> Vec m a
- takeI :: KnownNat m => Vec (m + n) a -> Vec m a
- drop :: SNat m -> Vec (m + n) a -> Vec n a
- dropI :: KnownNat m => Vec (m + n) a -> Vec n a
- at :: SNat m -> Vec (m + (n + 1)) a -> a
- select :: CmpNat (i + s) (s * n) ~ 'GT => SNat f -> SNat s -> SNat n -> Vec (f + i) a -> Vec n a
- selectI :: (CmpNat (i + s) (s * n) ~ 'GT, KnownNat n) => SNat f -> SNat s -> Vec (f + i) a -> Vec n a
- replicate :: SNat n -> a -> Vec n a
- repeat :: KnownNat n => a -> Vec n a
- iterate :: SNat n -> (a -> a) -> a -> Vec n a
- iterateI :: forall n a. KnownNat n => (a -> a) -> a -> Vec n a
- unfoldr :: SNat n -> (s -> (a, s)) -> s -> Vec n a
- unfoldrI :: KnownNat n => (s -> (a, s)) -> s -> Vec n a
- generate :: SNat n -> (a -> a) -> a -> Vec n a
- generateI :: KnownNat n => (a -> a) -> a -> Vec n a
- transpose :: KnownNat n => Vec m (Vec n a) -> Vec n (Vec m a)
- stencil1d :: KnownNat n => SNat (stX + 1) -> (Vec (stX + 1) a -> b) -> Vec ((stX + n) + 1) a -> Vec (n + 1) b
- stencil2d :: (KnownNat n, KnownNat m) => SNat (stY + 1) -> SNat (stX + 1) -> (Vec (stY + 1) (Vec (stX + 1) a) -> b) -> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a) -> Vec (m + 1) (Vec (n + 1) b)
- windows1d :: KnownNat n => SNat (stX + 1) -> Vec ((stX + n) + 1) a -> Vec (n + 1) (Vec (stX + 1) a)
- windows2d :: (KnownNat n, KnownNat m) => SNat (stY + 1) -> SNat (stX + 1) -> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a) -> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a)))
- permute :: (Enum i, KnownNat n, KnownNat m) => (a -> a -> a) -> Vec n a -> Vec m i -> Vec (m + k) a -> Vec n a
- backpermute :: (Enum i, KnownNat n) => Vec n a -> Vec m i -> Vec m a
- scatter :: (Enum i, KnownNat n, KnownNat m) => Vec n a -> Vec m i -> Vec (m + k) a -> Vec n a
- gather :: (Enum i, KnownNat n) => Vec n a -> Vec m i -> Vec m a
- interleave :: (KnownNat n, KnownNat d) => SNat d -> Vec (n * d) a -> Vec (d * n) a
- rotateLeft :: (Enum i, KnownNat n) => Vec n a -> i -> Vec n a
- rotateRight :: (Enum i, KnownNat n) => Vec n a -> i -> Vec n a
- rotateLeftS :: KnownNat n => Vec n a -> SNat d -> Vec n a
- rotateRightS :: KnownNat n => Vec n a -> SNat d -> Vec n a
- toList :: Vec n a -> [a]
- listToVecTH :: Lift a => [a] -> ExpQ
- asNatProxy :: Vec n a -> Proxy n
- lengthS :: KnownNat n => Vec n a -> SNat n
- lazyV :: KnownNat n => Vec n a -> Vec n a
- dfold :: forall p k a. KnownNat k => Proxy (p :: TyFun Nat Type -> Type) -> (forall l. SNat l -> a -> (p @@ l) -> p @@ (l + 1)) -> (p @@ 0) -> Vec k a -> p @@ k
- dtfold :: forall p k a. KnownNat k => Proxy (p :: TyFun Nat Type -> Type) -> (a -> p @@ 0) -> (forall l. SNat l -> (p @@ l) -> (p @@ l) -> p @@ (l + 1)) -> Vec (2 ^ k) a -> p @@ k
- 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
- smap :: forall k a b. KnownNat k => (forall l. SNat l -> a -> b) -> Vec k a -> Vec k b
- concatBitVector# :: forall n m. (KnownNat n, KnownNat m) => Vec n (BitVector m) -> BitVector (n * m)
- unconcatBitVector# :: forall n m. (KnownNat n, KnownNat m) => BitVector (n * m) -> Vec n (BitVector m)
- v2bv :: KnownNat n => Vec n Bit -> BitVector n
- seqV :: KnownNat n => Vec n a -> b -> b
- forceV :: KnownNat n => Vec n a -> Vec n a
- seqVX :: KnownNat n => Vec n a -> b -> b
- forceVX :: KnownNat n => Vec n a -> Vec n a
- module Clash.Sized.RTree
- module Clash.Annotations.TopEntity
- class Generic a
- class Generic1 (f :: k -> Type)
- module GHC.TypeLits
- module GHC.TypeLits.Extra
- module Clash.Promoted.Nat
- module Clash.Promoted.Nat.Literals
- module Clash.Promoted.Nat.TH
- module Clash.Promoted.Symbol
- module Clash.Class.BitPack
- module Clash.Class.Num
- module Clash.Class.Resize
- module Control.Applicative
- module Data.Bits
- module Clash.XException
- module Clash.NamedTypes
- module Clash.HaskellPrelude
Creating synchronous sequential circuits
Arguments
| :: (KnownDomain dom, NFDataX s) | |
| => Clock dom |
|
| -> Reset dom | |
| -> Enable dom | Global enable |
| -> (s -> i -> (s, o)) | Transfer function in mealy machine form: |
| -> 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
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 ::KnownDomaindom =>Clockdom ->Resetdom ->Enabledom -> (Signaldom Int,Signaldom Int) -> (Signaldom Int,Signaldom Int) ->Signaldom Int dualMac clk rst en (a,b) (x,y) = s1 + s2 where s1 =mealyclk rst en mac 0 (bundle(a,x)) s2 =mealyclk rst en mac 0 (bundle(b,y))
Arguments
| :: (KnownDomain dom, NFDataX s, Bundle i, Bundle o) | |
| => Clock dom | |
| -> Reset dom | |
| -> Enable dom | |
| -> (s -> i -> (s, o)) | Transfer function in mealy machine form: |
| -> 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 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)
Arguments
| :: (KnownDomain dom, NFDataX s) | |
| => Clock dom |
|
| -> Reset dom | |
| -> Enable dom | |
| -> (s -> i -> s) | Transfer function in moore machine form: |
| -> (s -> o) | Output function in moore machine form: |
| -> 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,Int) -- Updated state macT s (x,y) = x * y + s mac ::KnownDomaindom =>Clockdom ->Resetdom ->Enabledom ->Signaldom (Int, Int) ->Signaldom Int mac clk rst en =mooreclk 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 ::KnownDomaindom =>Clockdom ->Resetdom ->Enabledom -> (Signaldom Int,Signaldom Int) -> (Signaldom Int,Signaldom Int) ->Signaldom Int dualMac clk rst en (a,b) (x,y) = s1 + s2 where s1 =mooreclk rst en mac id 0 (bundle(a,x)) s2 =mooreclk rst en mac id 0 (bundle(b,y))
Arguments
| :: (KnownDomain dom, NFDataX s, Bundle i, Bundle o) | |
| => Clock dom | |
| -> Reset dom | |
| -> Enable dom | |
| -> (s -> i -> s) | Transfer function in moore machine form:
|
| -> (s -> o) | Output function in moore machine form:
|
| -> 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 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)
registerB :: (KnownDomain dom, NFDataX a, Bundle a) => Clock dom -> Reset dom -> Enable dom -> a -> Unbundled dom a -> Unbundled dom a Source #
Create a register function for product-type like signals (e.g.
()Signal a, Signal b)
rP :: Clock dom -> Reset dom -> Enable dom -> (Signaldom Int,Signaldom Int) -> (Signaldom Int,Signaldom Int) rP clk rst en =registerBclk 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 circuits for safe clock domain crossing
dualFlipFlopSynchronizer Source #
Arguments
| :: (NFDataX a, KnownDomain dom1, KnownDomain dom2) | |
| => Clock dom1 |
|
| -> Clock dom2 |
|
| -> Reset dom2 |
|
| -> Enable dom2 |
|
| -> a | Initial value of the two synchronization registers |
| -> Signal dom1 a | Incoming data |
| -> Signal dom2 a | Outgoing, synchronized, data |
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.
asyncFIFOSynchronizer Source #
Arguments
| :: (KnownDomain wdom, KnownDomain rdom, 2 <= addrSize) | |
| => SNat addrSize | Size of the internally used addresses, the FIFO contains |
| -> Clock wdom |
|
| -> Clock rdom |
|
| -> Reset wdom | |
| -> Reset rdom | |
| -> Enable wdom | |
| -> Enable rdom | |
| -> Signal rdom Bool | Read request |
| -> Signal wdom (Maybe a) | Element to insert |
| -> (Signal rdom a, Signal rdom Bool, Signal wdom Bool) | (Oldest element in the FIFO, |
Synchronizer implemented as a FIFO around an asynchronous 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.
NB: This synchronizer can be used for word-synchronization.
ROMs
Arguments
| :: (KnownNat n, Enum addr) | |
| => Vec n a | ROM content NB: must be a constant |
| -> addr | Read address |
| -> a | The value of the ROM at address |
An asynchronous/combinational ROM with space for n elements
Additional helpful information:
- See Clash.Sized.Fixed and Clash.Prelude.BlockRam for ideas on how to use ROMs and RAMs
Arguments
| :: KnownNat n | |
| => Vec (2 ^ n) a | ROM content NB: must be a constant |
| -> Unsigned n | Read address |
| -> a | The value of the ROM at address |
An asynchronous/combinational ROM with space for 2^n elements
Additional helpful information:
- See Clash.Sized.Fixed and Clash.Prelude.BlockRam for ideas on how to use ROMs and RAMs
Arguments
| :: (KnownDomain dom, KnownNat n, NFDataX a, Enum addr) | |
| => Clock dom |
|
| -> Enable dom | Global enable |
| -> Vec n a | ROM content NB: must be a constant |
| -> Signal dom addr | Read address |
| -> Signal dom a | The value of the ROM at address |
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
Additional helpful information:
- See Clash.Sized.Fixed and Clash.Explicit.BlockRam for ideas on how to use ROMs and RAMs
Arguments
| :: (KnownDomain dom, KnownNat n, NFDataX a) | |
| => Clock dom |
|
| -> Enable dom | Global enable |
| -> Vec (2 ^ n) a | ROM content NB: must be a constant |
| -> Signal dom (Unsigned n) | Read address |
| -> Signal dom a | The value of the ROM at address |
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
Additional helpful information:
- See Clash.Sized.Fixed and Clash.Explicit.BlockRam for ideas on how to use ROMs and RAMs
RAM primitives with a combinational read port
Arguments
| :: (Enum addr, HasCallStack, KnownDomain wdom, KnownDomain rdom) | |
| => Clock wdom |
|
| -> Clock rdom |
|
| -> Enable wdom | Global enable |
| -> SNat n | Size |
| -> Signal rdom addr | Read address |
| -> Signal wdom (Maybe (addr, a)) | (write address |
| -> Signal rdom a | Value of the |
Create a RAM with space for n elements
- NB: Initial content of the RAM is
undefined
Additional helpful information:
- See Clash.Explicit.BlockRam for more information on how to use a RAM.
Arguments
| :: forall wdom rdom n a. (KnownNat n, HasCallStack, KnownDomain wdom, KnownDomain rdom) | |
| => Clock wdom |
|
| -> Clock rdom |
|
| -> Enable wdom | Global enable |
| -> Signal rdom (Unsigned n) | Read address |
| -> Signal wdom (Maybe (Unsigned n, a)) | (write address |
| -> Signal rdom a | Value of the |
Create a RAM with space for 2^n elements
- NB: Initial content of the RAM is
undefined
Additional helpful information:
- See Clash.Prelude.BlockRam for more information on how to use a RAM.
BlockRAM primitives
Arguments
| :: (KnownDomain dom, HasCallStack, NFDataX a, Enum addr) | |
| => Clock dom |
|
| -> Enable dom | Global enable |
| -> Vec n a | Initial content of the BRAM, also determines the size, NB: MUST be a constant. |
| -> Signal dom addr | Read address |
| -> Signal dom (Maybe (addr, a)) | (write address |
| -> Signal dom a | Value of the |
Create a blockRAM with space for n elements
- NB: Read value is delayed by 1 cycle
- NB: Initial output value is undefined
bram40 ::Clockdom ->Enabledom ->Signaldom (Unsigned6) ->Signaldom (Maybe (Unsigned6,Bit)) ->SignaldomBitbram40 clk en =blockRamclk en (replicated40 1)
Additional helpful information:
- See Clash.Explicit.BlockRam for more information on how to use a Block RAM.
- Use the adapter
readNewfor obtaining write-before-read semantics like this:.readNewclk rst (blockRamclk inits) rd wrM
Arguments
| :: (KnownDomain dom, HasCallStack, NFDataX a, KnownNat n) | |
| => Clock dom |
|
| -> Enable dom | Global enable |
| -> Vec (2 ^ n) a | Initial content of the BRAM, also
determines the size, NB: MUST be a constant. |
| -> Signal dom (Unsigned n) | Read address |
| -> Signal dom (Maybe (Unsigned n, a)) | (Write address |
| -> Signal dom a | Value of the |
Create a blockRAM with space for 2^n elements
- NB: Read value is delayed by 1 cycle
- NB: Initial output value is undefined
bram32 ::Clockdom ->Enabledom ->Signaldom (Unsigned5) ->Signaldom (Maybe (Unsigned5,Bit)) ->SignaldomBitbram32 clk en =blockRamPow2clk en (replicated32 1)
Additional helpful information:
- See Clash.Prelude.BlockRam for more information on how to use a Block RAM.
- Use the adapter
readNewfor obtaining write-before-read semantics like this:.readNewclk rst (blockRamPow2clk inits) rd wrM
BlockRAM read/write conflict resolution
Arguments
| :: (KnownDomain dom, NFDataX a, Eq addr) | |
| => Clock dom | |
| -> Reset dom | |
| -> Enable dom | |
| -> (Signal dom addr -> Signal dom (Maybe (addr, a)) -> Signal dom a) | The |
| -> Signal dom addr | Read address |
| -> Signal dom (Maybe (addr, a)) | (Write address |
| -> Signal dom a | Value of the |
Create read-after-write blockRAM from a read-before-write one
Utility functions
riseEvery :: forall dom n. KnownDomain dom => Clock dom -> Reset dom -> Enable dom -> SNat n -> Signal dom Bool Source #
oscillate :: forall dom n. KnownDomain dom => Clock dom -> Reset dom -> Enable dom -> Bool -> SNat n -> Signal dom Bool Source #
Oscillate a for a given number of cycles, given the starting state.Bool
Exported modules
Synchronous signals
module Clash.Explicit.Signal
Datatypes
Bit vectors
module Clash.Sized.BitVector
module Clash.Prelude.BitIndex
module Clash.Prelude.BitReduction
Arbitrary-width numbers
module Clash.Sized.Signed
module Clash.Sized.Unsigned
module Clash.Sized.Index
Fixed point numbers
module Clash.Sized.Fixed
Fixed size vectors
data Vec :: Nat -> Type -> Type where Source #
Fixed size vectors.
Bundled Patterns
| pattern (:<) :: Vec n a -> a -> Vec (n + 1) a infixl 5 | Add an element to the tail of a vector.
Can be used as a pattern:
Also in conjunctions with (
|
| pattern (:>) :: a -> Vec n a -> Vec (n + 1) a infixr 5 | Add an element to the head of a vector.
Can be used as a pattern:
Also in conjunctions with (
|
Instances
| Lift a => Lift (Vec n a :: Type) Source # | |
| Functor (Vec n) Source # | |
| KnownNat n => Applicative (Vec n) Source # | |
| (KnownNat n, 1 <= n) => Foldable (Vec n) Source # | |
Defined in Clash.Sized.Vector Methods fold :: 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 # elem :: Eq a => a -> Vec n a -> Bool # maximum :: Ord a => Vec n a -> a # minimum :: Ord a => Vec n a -> a # | |
| (KnownNat n, 1 <= n) => Traversable (Vec n) Source # | |
| (KnownNat n, Eq a) => Eq (Vec n a) Source # | |
| (KnownNat n, Typeable a, Data a) => Data (Vec n a) Source # | |
Defined in Clash.Sized.Vector Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Vec n a -> c (Vec n a) # 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 # | |
| Show a => Show (Vec n a) Source # | |
| KnownNat n => Generic (Vec n a) Source # | In many cases, this Generic instance only allows generic functions/instances over vectors of at least size 1, due to the n-1 in the Rep (Vec n a) definition. We'll have to wait for things like https://ryanglscott.github.io/2018/02/11/how-to-derive-generic-for-some-gadts/ before we can work around this limitation |
| (KnownNat n, Semigroup a) => Semigroup (Vec n a) Source # | |
| (KnownNat n, Monoid a) => Monoid (Vec n a) Source # | |
| (KnownNat n, Arbitrary a) => Arbitrary (Vec n a) Source # | |
| CoArbitrary a => CoArbitrary (Vec n a) Source # | |
Defined in Clash.Sized.Vector Methods coarbitrary :: Vec n a -> Gen b -> Gen b # | |
| (Default a, KnownNat n) => Default (Vec n a) Source # | |
Defined in Clash.Sized.Vector | |
| NFData a => NFData (Vec n a) Source # | |
Defined in Clash.Sized.Vector | |
| KnownNat n => Ixed (Vec n a) Source # | |
Defined in Clash.Sized.Vector | |
| (NFDataX a, KnownNat n) => NFDataX (Vec n a) Source # | |
Defined in Clash.Sized.Vector | |
| ShowX a => ShowX (Vec n a) Source # | |
| (KnownNat n, BitPack a) => BitPack (Vec n a) Source # | |
| KnownNat n => Bundle (Vec n a) Source # | |
| KnownNat n => Bundle (Vec n a) Source # | |
Defined in Clash.Signal.Delayed.Bundle | |
| (KnownNat n, AutoReg a) => AutoReg (Vec n a) Source # | |
Defined in Clash.Class.AutoReg.Internal | |
| (LockStep en a, KnownNat n) => LockStep (Vec n en) (Vec n a) Source # | |
| type Unbundled t d (Vec n a) Source # | |
Defined in Clash.Signal.Delayed.Bundle | |
| type HasDomain dom (Vec n a) Source # | |
Defined in Clash.Class.HasDomain.HasSpecificDomain | |
| type TryDomain t (Vec n a) Source # | |
Defined in Clash.Class.HasDomain.HasSingleDomain | |
| type Unbundled t (Vec n a) Source # | |
Defined in Clash.Signal.Bundle | |
| type Rep (Vec n a) Source # | |
Defined in Clash.Sized.Vector type Rep (Vec n a) = D1 ('MetaData "Vec" "Clash.Data.Vector" "clash-prelude" 'False) (C1 ('MetaCons "Nil" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Cons" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Vec (n - 1) a)))) | |
| type Index (Vec n a) Source # | |
Defined in Clash.Sized.Vector | |
| type IxValue (Vec n a) Source # | |
Defined in Clash.Sized.Vector | |
| type BitSize (Vec n a) Source # | |
Defined in Clash.Sized.Vector | |
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: " produces a linear structure, which has a depth, or
delay, of O(foldl f z xs"). Use length xsfold if your binary operator f is
associative, as " produces a structure with a depth of
O(log_2(fold f xs")).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: " produces a linear structure, which has a depth, or
delay, of O(foldr f z xs"). Use length xsfold if your binary operator f is
associative, as " produces a structure with a depth of
O(log_2(fold f xs")).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:
data VCons (a :: Type) (f :: TyFun Nat Type) :: Type Source #
head :: Vec (n + 1) a -> a Source #
Extract the first element of a vector
>>>head (1:>2:>3:>Nil)1
# 421 "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>
# 454 "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
# 487 "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>
# 521 "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>,<3,4>)>>>shiftInAt0 (1 :> Nil) ((-1) :> 0 :> Nil)(<-1>,<0,1>)
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>,<1,2>)>>>shiftInAtN (1 :> Nil) (2 :> 3 :> Nil)(<3>,<1,2>)
(+>>) :: 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>>>>1 +>> 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 <<+ 1<>
Arguments
| :: (Default a, KnownNat m) | |
| => SNat m |
|
| -> 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>,<1,2>)
Arguments
| :: (Default a, KnownNat n) | |
| => SNat m |
|
| -> 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>,<4,5>)
(++) :: 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>
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>,<7,8>)>>>splitAt d3 (1:>2:>3:>7:>8:>Nil)(<1,2,3>,<7,8>)
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>,<3,7,8>)
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>
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>
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>,<5,6,7,8>,<9,10,11,12>>
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>,<7,8,9,10,11,12>>
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>
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>
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>
"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>
"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>
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>
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.
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: " produces a linear structure, which has a depth,
or delay, of O(foldr1 f z xs"). Use length xsfold if your binary operator f is
associative, as " produces a structure with a depth of
O(log_2(fold f xs")).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: " produces a linear structure, which has a depth,
or delay, of O(foldl1 f z xs"). Use length xsfold if your binary operator f is
associative, as " produces a structure with a depth of
O(log_2(fold f xs")).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
"", is hence fold f xsO(log_2(, and not
length xs))O(.length xs)
NB: The binary operator "f" in "" must be associative.fold f xs
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>
"scanl f z xs" corresponds to the following circuit layout:
NB:
last (scanl f z xs) == foldl f z xs
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>
"scanr f z xs" corresponds to the following circuit layout:
NB:
head (scanr f z xs) == foldr f z xs
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>)
"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>)
"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)>
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)>
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 #
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 #
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>,<4,3,2,1>)
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>,<4,3,2,1>,<5,6,7,8>)
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 #
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 #
(!!) :: (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) !! 45>>>(1:>2:>3:>4:>5:>Nil) !! (length (1:>2:>3:>4:>5:>Nil) - 1)5>>>(1:>2:>3:>4:>5:>Nil) !! 12>>>(1:>2:>3:>4:>5:>Nil) !! 14*** Exception: Clash.Sized.Vector.(!!): index 14 is larger than maximum index 4 ...
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>>>>replace 0 7 (1:>2:>3:>4:>5:>Nil)<7,2,3,4,5>>>>replace 9 7 (1:>2:>3:>4:>5:>Nil)<1,2,3,4,*** 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>>>>take d3 (1:>2:>3:>4:>5:>Nil)<1,2,3>>>>take d0 (1:>2:>Nil)<>
# 1446 "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>
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>>>>drop d3 (1:>2:>3:>4:>5:>Nil)<4,5>>>>drop d0 (1:>2:>Nil)<1,2>>>>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>
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>>>>select d1 d2 d3 (1:>2:>3:>4:>5:>6:>7:>8:>Nil)<2,4,6>
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>
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>>>>replicate d3 6<6,6,6>
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>
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>
"iterate n 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>
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>
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>
"generate n 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>,<3,4>,<5,6>>>>>transpose xss<<1,3,5>,<2,4,6>>
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 xsxs :: Num a => Vec 6 a>>>:t stencil1d d2 sum xsstencil1d d2 sum xs :: Num b => Vec 5 b>>>stencil1d d2 sum xs<3,5,7,9,11>
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 xssxss :: Num a => Vec 4 (Vec 4 a)>>>:t stencil2d d2 d2 (sum . map sum) xssstencil2d d2 d2 (sum . map sum) xss :: Num b => Vec 3 (Vec 3 b)>>>stencil2d d2 d2 (sum . map sum) xss<<14,18,22>,<30,34,38>,<46,50,54>>
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 xsxs :: Num a => Vec 6 a>>>:t windows1d d2 xswindows1d d2 xs :: Num a => Vec 5 (Vec 2 a)>>>windows1d d2 xs<<1,2>,<2,3>,<3,4>,<4,5>,<5,6>>
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 xssxss :: Num a => Vec 4 (Vec 4 a)>>>:t windows2d d2 d2 xsswindows2d d2 d2 xss :: Num a => Vec 3 (Vec 3 (Vec 2 (Vec 2 a)))>>>windows2d d2 d2 xss<<<<1,2>,<5,6>>,<<2,3>,<6,7>>,<<3,4>,<7,8>>>,<<<5,6>,<9,10>>,<<6,7>,<10,11>>,<<7,8>,<11,12>>>,<<<9,10>,<13,14>>,<<10,11>,<14,15>>,<<11,12>,<15,16>>>>
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.
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>
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>
NB: If the same index appears in the index mapping more than once, the latest mapping is chosen.
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>
"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>
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>>>>rotateLeft xs 2<3,4,1,2>>>>rotateLeft xs (-1)<4,1,2,3>
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>>>>rotateRight xs 2<3,4,1,2>>>>rotateRight xs (-1)<2,3,4,1>
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>
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>
NB: use rotateRight if you want to rotate right by a dynamic amount.
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>
lazyV :: KnownNat n => Vec n a -> Vec n a Source #
What you should use when your vector functions are too strict in their arguments.
For example:
-- Bubble sort for 1 iteration sortV xs =mapfst sorted:<(snd (lastsorted)) where lefts =headxs :>mapsnd (initsorted) rights =tailxs sorted =zipWithcompareSwapL 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 =mapfst sorted:<(snd (lastsorted)) where lefts =headxs :> map snd (initsorted) rights =tailxs sorted =zipWithcompareSwapL (lazyVlefts) rights
Results in a successful computation:
>>>sortVL (4 :> 1 :> 2 :> 3 :> Nil)<1,2,3,4>
NB: There is also a solution using flip, but it slightly obfuscates the
meaning of the code:
sortV_flip xs =mapfst sorted:<(snd (lastsorted)) where lefts =headxs :>mapsnd (initsorted) rights =tailxs sorted =zipWith(flipcompareSwapL) rights lefts
>>>sortV_flip (4 :> 1 :> 2 :> 3 :> Nil)<1,2,3,4>
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 |
| -> (p @@ 0) | Initial element |
| -> Vec k a | Vector to fold over |
| -> p @@ k |
A dependently typed fold.
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 foldrfoldr :: (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 :: *) (f ::TyFunNat *) :: * type instanceApply(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>
NB: "" creates a linear structure, which has a depth,
or delay, of O(dfold m f z xs). Look at length xsdtfold 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 |
| -> 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.
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:
# 2231 "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 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
dtfoldinstead offold, we had to restrict ourBitVectorargument 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
"" is O(log_2(dtfold m f g xs)).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.
Example:
compareSwap a b = if a > b then (a,b) else (b,a) insert y xs = let (y',xs') =mapAccumLcompareSwap 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>
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>,<1,2,3>,<1,2,3>>>>>rotateMatrix xss<<1,2,3>,<3,1,2>,<2,3,1>>
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 #
seqV :: KnownNat n => Vec n a -> b -> b infixr 0 Source #
Evaluate all elements of a vector to WHNF, returning the second argument
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.
Perfect depth trees
module Clash.Sized.RTree
Annotations
module Clash.Annotations.TopEntity
Generics type-classes
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≡idto.from≡id
Instances
class Generic1 (f :: k -> Type) #
Representable types of kind * -> * (or kind k -> *, when PolyKinds
is enabled).
This class is derivable in GHC with the DeriveGeneric flag on.
A Generic1 instance must satisfy the following laws:
from1.to1≡idto1.from1≡id
Instances
| Generic1 (V1 :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (U1 :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (Proxy :: k -> Type) | Since: base-4.6.0.0 |
| Generic1 (FromTextShow1 f :: k -> Type) | |
Defined in TextShow.FromStringTextShow Associated Types type Rep1 (FromTextShow1 f) :: k -> Type # Methods from1 :: forall (a :: k0). FromTextShow1 f a -> Rep1 (FromTextShow1 f) a # to1 :: forall (a :: k0). Rep1 (FromTextShow1 f) a -> FromTextShow1 f a # | |
| Generic1 (FromStringShow1 f :: k -> Type) | |
Defined in TextShow.FromStringTextShow Associated Types type Rep1 (FromStringShow1 f) :: k -> Type # Methods from1 :: forall (a :: k0). FromStringShow1 f a -> Rep1 (FromStringShow1 f) a # to1 :: forall (a :: k0). Rep1 (FromStringShow1 f) a -> FromStringShow1 f a # | |
| Generic1 (FromGeneric1 f :: k -> Type) | |
Defined in TextShow.Generic Associated Types type Rep1 (FromGeneric1 f) :: k -> Type # Methods from1 :: forall (a :: k0). FromGeneric1 f a -> Rep1 (FromGeneric1 f) a # to1 :: forall (a :: k0). Rep1 (FromGeneric1 f) a -> FromGeneric1 f a # | |
| Generic1 (Alt f :: k -> Type) | Since: base-4.8.0.0 |
| Generic1 (Ap f :: k -> Type) | Since: base-4.12.0.0 |
| Generic1 (Const a :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (URec (Ptr ()) :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (URec Char :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (URec Double :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (URec Float :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (URec Int :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (URec Word :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (Rec1 f :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (Sum f g :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (Product f g :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (K1 i c :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (f :+: g :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (f :*: g :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (WrappedBifunctor p a :: k1 -> Type) | |
Defined in Data.Bifunctor.Wrapped Associated Types type Rep1 (WrappedBifunctor p a) :: k -> Type # Methods from1 :: forall (a0 :: k). WrappedBifunctor p a a0 -> Rep1 (WrappedBifunctor p a) a0 # to1 :: forall (a0 :: k). Rep1 (WrappedBifunctor p a) a0 -> WrappedBifunctor p a a0 # | |
| Generic1 (Joker g a :: k1 -> Type) | |
| Generic1 (Clown f a :: k1 -> Type) | |
| Generic1 (FromTextShow2 f a :: k1 -> Type) | |
Defined in TextShow.FromStringTextShow Associated Types type Rep1 (FromTextShow2 f a) :: k -> Type # Methods from1 :: forall (a0 :: k). FromTextShow2 f a a0 -> Rep1 (FromTextShow2 f a) a0 # to1 :: forall (a0 :: k). Rep1 (FromTextShow2 f a) a0 -> FromTextShow2 f a a0 # | |
| Generic1 (FromStringShow2 f a :: k1 -> Type) | |
Defined in TextShow.FromStringTextShow Associated Types type Rep1 (FromStringShow2 f a) :: k -> Type # Methods from1 :: forall (a0 :: k). FromStringShow2 f a a0 -> Rep1 (FromStringShow2 f a) a0 # to1 :: forall (a0 :: k). Rep1 (FromStringShow2 f a) a0 -> FromStringShow2 f a a0 # | |
| Functor f => Generic1 (Compose f g :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (M1 i c f :: k -> Type) | Since: base-4.9.0.0 |
| Functor f => Generic1 (f :.: g :: k -> Type) | Since: base-4.9.0.0 |
| Generic1 (Sum p q a :: k1 -> Type) | |
| Generic1 (Product f g a :: k1 -> Type) | |
| Functor f => Generic1 (Tannen f p a :: k2 -> Type) | |
| Functor (p (f a)) => Generic1 (Biff p f g a :: k3 -> Type) | |
| Generic1 [] | Since: base-4.6.0.0 |
| Generic1 Maybe | Since: base-4.6.0.0 |
| Generic1 Par1 | Since: base-4.9.0.0 |
| Generic1 Complex | Since: base-4.9.0.0 |
| Generic1 Min | Since: base-4.9.0.0 |
| Generic1 Max | Since: base-4.9.0.0 |
| Generic1 First | Since: base-4.9.0.0 |
| Generic1 Last | Since: base-4.9.0.0 |
| Generic1 WrappedMonoid | Since: base-4.9.0.0 |
Defined in Data.Semigroup Associated Types type Rep1 WrappedMonoid :: k -> Type # Methods from1 :: forall (a :: k). WrappedMonoid a -> Rep1 WrappedMonoid a # to1 :: forall (a :: k). Rep1 WrappedMonoid a -> WrappedMonoid a # | |
| Generic1 Option | Since: base-4.9.0.0 |
| Generic1 ZipList | Since: base-4.7.0.0 |
| Generic1 Identity | Since: base-4.8.0.0 |
| Generic1 First | Since: base-4.7.0.0 |
| Generic1 Last | Since: base-4.7.0.0 |
| Generic1 Dual | Since: base-4.7.0.0 |
| Generic1 Sum | Since: base-4.7.0.0 |
| Generic1 Product | Since: base-4.7.0.0 |
| Generic1 Down | Since: base-4.12.0.0 |
| Generic1 NonEmpty | Since: base-4.6.0.0 |
| Generic1 Tree | Since: containers-0.5.8 |
| Generic1 FingerTree | Since: containers-0.6.1 |
Defined in Data.Sequence.Internal Associated Types type Rep1 FingerTree :: k -> Type # Methods from1 :: forall (a :: k). FingerTree a -> Rep1 FingerTree a # to1 :: forall (a :: k). Rep1 FingerTree a -> FingerTree a # | |
| Generic1 Digit | Since: containers-0.6.1 |
| Generic1 Node | Since: containers-0.6.1 |
| Generic1 Elem | Since: containers-0.6.1 |
| Generic1 ViewL | Since: containers-0.5.8 |
| Generic1 ViewR | Since: containers-0.5.8 |
| Generic1 Maybe | |
| Generic1 FromGeneric | |
Defined in TextShow.Generic Associated Types type Rep1 FromGeneric :: k -> Type # Methods from1 :: forall (a :: k). FromGeneric a -> Rep1 FromGeneric a # to1 :: forall (a :: k). Rep1 FromGeneric a -> FromGeneric a # | |
| Generic1 FromStringShow | |
Defined in TextShow.FromStringTextShow Associated Types type Rep1 FromStringShow :: k -> Type # Methods from1 :: forall (a :: k). FromStringShow a -> Rep1 FromStringShow a # to1 :: forall (a :: k). Rep1 FromStringShow a -> FromStringShow a # | |
| Generic1 FromTextShow | |
Defined in TextShow.FromStringTextShow Associated Types type Rep1 FromTextShow :: k -> Type # Methods from1 :: forall (a :: k). FromTextShow a -> Rep1 FromTextShow a # to1 :: forall (a :: k). Rep1 FromTextShow a -> FromTextShow a # | |
| Generic1 (Either a :: Type -> Type) | Since: base-4.6.0.0 |
| Generic1 ((,) a :: Type -> Type) | Since: base-4.6.0.0 |
| Generic1 (Arg a :: Type -> Type) | Since: base-4.9.0.0 |
| Generic1 (WrappedMonad m :: Type -> Type) | Since: base-4.7.0.0 |
Defined in Control.Applicative Associated Types type Rep1 (WrappedMonad m) :: k -> Type # Methods from1 :: forall (a :: k). WrappedMonad m a -> Rep1 (WrappedMonad m) a # to1 :: forall (a :: k). Rep1 (WrappedMonad m) a -> WrappedMonad m a # | |
| Functor f => Generic1 (Cofree f :: Type -> Type) | |
| Functor f => Generic1 (Free f :: Type -> Type) | |
| Generic1 (ListF a :: Type -> Type) | |
| Generic1 (NonEmptyF a :: Type -> Type) | |
| Generic1 (TreeF a :: Type -> Type) | |
| Generic1 (Pair a :: Type -> Type) | |
| Generic1 (These a :: Type -> Type) | |
| Generic1 (Either a :: Type -> Type) | |
| Generic1 (These a :: Type -> Type) | |
| Generic1 ((,,) a b :: Type -> Type) | Since: base-4.6.0.0 |
| Generic1 (Kleisli m a :: Type -> Type) | Since: base-4.14.0.0 |
| Generic1 (WrappedArrow a b :: Type -> Type) | Since: base-4.7.0.0 |
Defined in Control.Applicative Associated Types type Rep1 (WrappedArrow a b) :: k -> Type # Methods from1 :: forall (a0 :: k). WrappedArrow a b a0 -> Rep1 (WrappedArrow a b) a0 # to1 :: forall (a0 :: k). Rep1 (WrappedArrow a b) a0 -> WrappedArrow a b a0 # | |
| Generic1 (FreeF f a :: Type -> Type) | |
| Generic1 (CofreeF f a :: Type -> Type) | |
| Generic1 (Tagged s :: Type -> Type) | |
| Generic1 ((,,,) a b c :: Type -> Type) | Since: base-4.6.0.0 |
| Generic1 ((,,,,) a b c d :: Type -> Type) | Since: base-4.6.0.0 |
| Generic1 ((,,,,,) a b c d e :: Type -> Type) | Since: base-4.6.0.0 |
| Generic1 ((,,,,,,) a b c d e f :: Type -> Type) | Since: base-4.6.0.0 |
Type-level natural numbers
module GHC.TypeLits
module GHC.TypeLits.Extra
module Clash.Promoted.Nat
module Clash.Promoted.Nat.Literals
module Clash.Promoted.Nat.TH
Type-level strings
module Clash.Promoted.Symbol
Type classes
Clash
module Clash.Class.BitPack
module Clash.Class.Num
module Clash.Class.Resize
Other
module Control.Applicative
module Data.Bits
Exceptions
module Clash.XException
Named types
module Clash.NamedTypes
Haskell Prelude
module Clash.HaskellPrelude