Copyright  (C) 20132016 University of Twente 20172019 Myrtle Software Ltd 2017 Google Inc. 20212022 QBayLogic B.V. 

License  BSD2 (see the file LICENSE) 
Maintainer  QBayLogic B.V. <devops@qbaylogic.com> 
Safe Haskell  Safe 
Language  Haskell2010 
Extensions 

This is the Safe API only of Clash.Prelude
Clash is a functional hardware description language that borrows both its syntax and semantics from the functional programming language Haskell. The merits of using a functional language to describe hardware comes from the fact that combinational circuits can be directly modeled as mathematical functions and that functional languages lend themselves very well at describing and (de)composing mathematical functions.
This package provides:
 Prelude library containing datatypes and functions for circuit design
To use the library:
 Import Clash.Prelude
 Additionally import Clash.Explicit.Prelude if you want to design explicitly clocked circuits in a multiclock setting
For now, Clash.Prelude is also the best starting point for exploring the library. A preliminary version of a tutorial can be found in Clash.Tutorial. Some circuit examples can be found in Clash.Examples.
Synopsis
 mealy :: (HiddenClockResetEnable dom, NFDataX s) => (s > i > (s, o)) > s > Signal dom i > Signal dom o
 mealyB :: (HiddenClockResetEnable dom, NFDataX s, Bundle i, Bundle o) => (s > i > (s, o)) > s > Unbundled dom i > Unbundled dom o
 (<^>) :: (HiddenClockResetEnable dom, NFDataX s, Bundle i, Bundle o) => (s > i > (s, o)) > s > Unbundled dom i > Unbundled dom o
 moore :: (HiddenClockResetEnable dom, NFDataX s) => (s > i > s) > (s > o) > s > Signal dom i > Signal dom o
 mooreB :: (HiddenClockResetEnable dom, NFDataX s, Bundle i, Bundle o) => (s > i > s) > (s > o) > s > Unbundled dom i > Unbundled dom o
 registerB :: (HiddenClockResetEnable dom, NFDataX a, Bundle a) => a > Unbundled dom a > Unbundled dom a
 asyncRom :: (KnownNat n, Enum addr) => Vec n a > addr > a
 asyncRomPow2 :: KnownNat n => Vec (2 ^ n) a > Unsigned n > a
 rom :: forall dom n m a. (NFDataX a, KnownNat n, KnownNat m, HiddenClock dom, HiddenEnable dom) => Vec n a > Signal dom (Unsigned m) > Signal dom a
 romPow2 :: forall dom n a. (KnownNat n, NFDataX a, HiddenClock dom, HiddenEnable dom) => Vec (2 ^ n) a > Signal dom (Unsigned n) > Signal dom a
 asyncRomBlob :: Enum addr => MemBlob n m > addr > BitVector m
 asyncRomBlobPow2 :: KnownNat n => MemBlob (2 ^ n) m > Unsigned n > BitVector m
 romBlob :: forall dom addr m n. (HiddenClock dom, HiddenEnable dom, Enum addr) => MemBlob n m > Signal dom addr > Signal dom (BitVector m)
 romBlobPow2 :: forall dom m n. (HiddenClock dom, HiddenEnable dom, KnownNat n) => MemBlob (2 ^ n) m > Signal dom (Unsigned n) > Signal dom (BitVector m)
 asyncRam :: (Enum addr, HiddenClock dom, HiddenEnable dom, HasCallStack, NFDataX a) => SNat n > Signal dom addr > Signal dom (Maybe (addr, a)) > Signal dom a
 asyncRamPow2 :: (KnownNat n, HiddenClock dom, HiddenEnable dom, HasCallStack, NFDataX a) => Signal dom (Unsigned n) > Signal dom (Maybe (Unsigned n, a)) > Signal dom a
 blockRam :: (HasCallStack, HiddenClock dom, HiddenEnable dom, NFDataX a, Enum addr) => Vec n a > Signal dom addr > Signal dom (Maybe (addr, a)) > Signal dom a
 blockRamPow2 :: (HasCallStack, HiddenClock dom, HiddenEnable dom, NFDataX a, KnownNat n) => Vec (2 ^ n) a > Signal dom (Unsigned n) > Signal dom (Maybe (Unsigned n, a)) > Signal dom a
 blockRamBlob :: forall dom addr m n. (HiddenClock dom, HiddenEnable dom, Enum addr) => MemBlob n m > Signal dom addr > Signal dom (Maybe (addr, BitVector m)) > Signal dom (BitVector m)
 blockRamBlobPow2 :: forall dom m n. (HiddenClock dom, HiddenEnable dom, KnownNat n) => MemBlob (2 ^ n) m > Signal dom (Unsigned n) > Signal dom (Maybe (Unsigned n, BitVector m)) > Signal dom (BitVector m)
 data MemBlob (n :: Nat) (m :: Nat)
 createMemBlob :: forall a f. (Foldable f, BitPack a) => String > Maybe Bit > f a > DecsQ
 memBlobTH :: forall a f. (Foldable f, BitPack a) => Maybe Bit > f a > ExpQ
 unpackMemBlob :: forall n m. MemBlob n m > [BitVector m]
 readNew :: (HiddenClockResetEnable dom, NFDataX a, Eq addr) => (Signal dom addr > Signal dom (Maybe (addr, a)) > Signal dom a) > Signal dom addr > Signal dom (Maybe (addr, a)) > Signal dom a
 trueDualPortBlockRam :: forall nAddrs dom1 dom2 a. (HasCallStack, KnownNat nAddrs, HiddenClock dom1, HiddenClock dom2, NFDataX a) => Signal dom1 (RamOp nAddrs a) > Signal dom2 (RamOp nAddrs a) > (Signal dom1 a, Signal dom2 a)
 data RamOp n a
 isRising :: (HiddenClockResetEnable dom, NFDataX a, Bounded a, Eq a) => a > Signal dom a > Signal dom Bool
 isFalling :: (HiddenClockResetEnable dom, NFDataX a, Bounded a, Eq a) => a > Signal dom a > Signal dom Bool
 riseEvery :: HiddenClockResetEnable dom => SNat n > Signal dom Bool
 oscillate :: HiddenClockResetEnable dom => Bool > SNat n > Signal dom Bool
 module Clash.Signal
 module Clash.Signal.Delayed
 module Clash.Sized.BitVector
 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.Hidden
 module Clash.HaskellPrelude
Creating synchronous sequential circuits
:: (HiddenClockResetEnable dom, NFDataX s)  
=> (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
macT :: Int  Current state > (Int,Int)  Input > (Int,Int)  (Updated state, output) macT s (x,y) = (s',s) where s' = x * y + s mac :: HiddenClockResetEnable dom =>Signal
dom (Int, Int) >Signal
dom Int mac =mealy
macT 0
>>>
simulate @System mac [(0,0),(1,1),(2,2),(3,3),(4,4)]
[0,0,1,5,14... ...
Synchronous sequential functions can be composed just like their combinational counterpart:
dualMac :: HiddenClockResetEnable dom => (Signal
dom Int,Signal
dom Int) > (Signal
dom Int,Signal
dom Int) >Signal
dom Int dualMac (a,b) (x,y) = s1 + s2 where s1 =mealy
mac 0 (bundle
(a,x)) s2 =mealy
mac 0 (bundle
(b,y))
:: (HiddenClockResetEnable dom, NFDataX s, Bundle i, Bundle o)  
=> (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 Bundle
ing
Given a function f
of type:
f :: Int > (Bool, Int) > (Int, (Int, Bool))
When we want to make compositions of f
in g
using mealy
, we have to
write:
g a b c = (b1,b2,i2) where (i1,b1) =unbundle
(mealy
f 0 (bundle
(a,b))) (i2,b2) =unbundle
(mealy
f 3 (bundle
(c,i1)))
Using mealyB
however we can write:
g a b c = (b1,b2,i2) where (i1,b1) =mealyB
f 0 (a,b) (i2,b2) =mealyB
f 3 (c,i1)
:: (HiddenClockResetEnable dom, NFDataX s, Bundle i, Bundle o)  
=> (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 
Infix version of mealyB
:: (HiddenClockResetEnable dom, NFDataX s)  
=> (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  Updated state macT s (x,y) = x * y + s mac :: HiddenClockResetEnable dom =>Signal
dom (Int, Int) >Signal
dom Int mac =moore
mac id 0
>>>
simulate @System mac [(0,0),(1,1),(2,2),(3,3),(4,4)]
[0,0,1,5,14,30,... ...
Synchronous sequential functions can be composed just like their combinational counterpart:
dualMac :: HiddenClockResetEnable dom => (Signal
dom Int,Signal
dom Int) > (Signal
dom Int,Signal
dom Int) >Signal
dom Int dualMac (a,b) (x,y) = s1 + s2 where s1 =moore
mac id 0 (bundle
(a,x)) s2 =moore
mac id 0 (bundle
(b,y))
:: (HiddenClockResetEnable dom, NFDataX s, Bundle i, Bundle o)  
=> (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 Bundle
ing
Given a functions t
and o
of types:
t :: Int > (Bool, Int) > Int o :: Int > (Int, Bool)
When we want to make compositions of t
and o
in g
using moore
, we have to
write:
g a b c = (b1,b2,i2) where (i1,b1) =unbundle
(moore
t o 0 (bundle
(a,b))) (i2,b2) =unbundle
(moore
t o 3 (bundle
(c,i1)))
Using mooreB
however we can write:
g a b c = (b1,b2,i2) where (i1,b1) =mooreB
t o 0 (a,b) (i2,b2) =mooreB
t o 3 (c,i1)
registerB :: (HiddenClockResetEnable dom, NFDataX a, Bundle a) => a > Unbundled dom a > Unbundled dom a infixr 3 Source #
Create a register
function for producttype like signals (e.g. '(Signal a, Signal b)')
rP :: HiddenClockResetEnable dom => (Signal dom Int, Signal dom Int) > (Signal dom Int, Signal dom Int) rP = registerB (8,8)
>>>
simulateB @System rP [(1,1),(2,2),(3,3)] :: [(Int,Int)]
[(8,8),(1,1),(2,2),(3,3)... ...
ROMs
:: (KnownNat n, Enum addr)  
=> Vec n a  ROM content, also determines the size, 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
 A large
Vec
for the content might be too inefficient, depending on how it is constructed. SeeasyncRomFile
andasyncRomBlob
for different approaches that scale well.
:: 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
 A large
Vec
for the content might be too inefficient, depending on how it is constructed. SeeasyncRomFilePow2
andasyncRomBlobPow2
for different approaches that scale well.
:: forall dom n m a. (NFDataX a, KnownNat n, KnownNat m, HiddenClock dom, HiddenEnable dom)  
=> Vec n a  ROM content, also determines the size, NB: must be a constant 
> Signal dom (Unsigned m)  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, reading it will throw an
XException
Additional helpful information:
 See Clash.Sized.Fixed and Clash.Prelude.BlockRam for ideas on how to use ROMs and RAMs
 A large
Vec
for the content might be too inefficient, depending on how it is constructed. SeeromFile
andromBlob
for different approaches that scale well.
:: forall dom n a. (KnownNat n, NFDataX a, HiddenClock dom, HiddenEnable dom)  
=> 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, reading it will throw an
XException
Additional helpful information:
 See Clash.Sized.Fixed and Clash.Prelude.BlockRam for ideas on how to use ROMs and RAMs
 A large
Vec
for the content might be too inefficient, depending on how it is constructed. SeeromFilePow2
andromBlobPow2
for different approaches that scale well.
ROMs defined by a MemBlob
:: Enum addr  
=> MemBlob n m  ROM content, also determines the size, NB: MUST be a constant 
> addr  Read address 
> BitVector m  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.
:: KnownNat n  
=> MemBlob (2 ^ n) m  ROM content, also determines the size, 2^ NB: MUST be a constant 
> Unsigned n  Read address 
> BitVector m  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.
:: forall dom addr m n. (HiddenClock dom, HiddenEnable dom, Enum addr)  
=> MemBlob n m  ROM content, also determines the size, NB: MUST be a constant 
> Signal dom addr  Read address 
> Signal dom (BitVector m)  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, reading it will throw an
XException
Additional helpful information:
 See Clash.Sized.Fixed and Clash.Explicit.BlockRam for ideas on how to use ROMs and RAMs.
:: forall dom m n. (HiddenClock dom, HiddenEnable dom, KnownNat n)  
=> MemBlob (2 ^ n) m  ROM content, also determines the size, 2^ NB: MUST be a constant 
> Signal dom (Unsigned n)  Read address 
> Signal dom (BitVector m)  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, reading it will throw an
XException
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
:: (Enum addr, HiddenClock dom, HiddenEnable dom, HasCallStack, NFDataX a)  
=> SNat n  Size 
> Signal dom addr  Read address 
> Signal dom (Maybe (addr, a))  (write address 
> Signal dom a  Value of the 
Create a RAM with space for n
elements.
 NB: Initial content of the RAM is undefined, reading it will throw an
XException
Additional helpful information:
 See Clash.Prelude.BlockRam for more information on how to use a RAM.
:: (KnownNat n, HiddenClock dom, HiddenEnable dom, HasCallStack, NFDataX a)  
=> Signal dom (Unsigned n)  Read address 
> Signal dom (Maybe (Unsigned n, a))  (write address 
> Signal dom a  Value of the 
Create a RAM with space for 2^n
elements
 NB: Initial content of the RAM is undefined, reading it will throw an
XException
Additional helpful information:
 See Clash.Prelude.BlockRam for more information on how to use a RAM.
BlockRAM primitives
:: (HasCallStack, HiddenClock dom, HiddenEnable dom, NFDataX a, Enum addr)  
=> 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, reading it will throw an
XException
bram40 ::HiddenClock
dom =>Signal
dom (Unsigned
6) >Signal
dom (Maybe (Unsigned
6,Bit
)) >Signal
domBit
bram40 =blockRam
(replicate
d40 1)
Additional helpful information:
 See Clash.Prelude.BlockRam for more information on how to use a Block RAM.
 Use the adapter
readNew
for obtaining writebeforeread semantics like this:readNew (blockRam inits) rd wrM
.  A large
Vec
for the initial content might be too inefficient, depending on how it is constructed. SeeblockRamFile
andblockRamBlob
for different approaches that scale well.
:: (HasCallStack, HiddenClock dom, HiddenEnable dom, NFDataX a, KnownNat n)  
=> Vec (2 ^ n) a  Initial content of the BRAM 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, reading it will throw an
XException
bram32 ::HiddenClock
dom =>Signal
dom (Unsigned
5) >Signal
dom (Maybe (Unsigned
5,Bit
)) >Signal
domBit
bram32 =blockRamPow2
(replicate
d32 1)
Additional helpful information:
 See Clash.Prelude.BlockRam for more information on how to use a Block RAM.
 Use the adapter
readNew
for obtaining writebeforeread semantics like this:readNew (blockRamPow2 inits) rd wrM
.  A large
Vec
for the initial content might be too inefficient, depending on how it is constructed. SeeblockRamFilePow2
andblockRamBlobPow2
for different approaches that scale well.
BlockRAM primitives initialized with a MemBlob
:: forall dom addr m n. (HiddenClock dom, HiddenEnable dom, Enum addr)  
=> MemBlob n m  Initial content of the RAM, also determines the size, NB: MUST be a constant 
> Signal dom addr  Read address 
> Signal dom (Maybe (addr, BitVector m))  (write address 
> Signal dom (BitVector m)  Value of the blockRAM at address 
Create a blockRAM with space for n
elements
 NB: Read value is delayed by 1 cycle
 NB: Initial output value is undefined, reading it will throw an
XException
Additional helpful information:
 See Clash.Prelude.BlockRam for more information on how to use a Block RAM.
 Use the adapter
readNew
for obtaining writebeforeread semantics like this:
.readNew
(blockRamBlob
content) rd wrM
:: forall dom m n. (HiddenClock dom, HiddenEnable dom, KnownNat n)  
=> MemBlob (2 ^ n) m  Initial content of the RAM, also determines the size, 2^ NB: MUST be a constant 
> Signal dom (Unsigned n)  Read address 
> Signal dom (Maybe (Unsigned n, BitVector m))  (write address 
> Signal dom (BitVector m)  Value of the blockRAM at address 
Create a blockRAM with space for 2^n
elements
 NB: Read value is delayed by 1 cycle
 NB: Initial output value is undefined, reading it will throw an
XException
Additional helpful information:
 See Clash.Prelude.BlockRam for more information on how to use a Block RAM.
 Use the adapter
readNew
for obtaining writebeforeread semantics like this:
.readNew
(blockRamBlobPow2
content) rd wrM
Creating and inspecting MemBlob
data MemBlob (n :: Nat) (m :: Nat) Source #
Efficient storage of memory content
It holds n
words of
.BitVector
m
:: forall a f. (Foldable f, BitPack a)  
=> String  Name of the binding to generate 
> Maybe Bit  Value to map don't care bits to. 
> f a  The content for the 
> DecsQ 
Create a MemBlob
binding from a list of values
Since this uses Template Haskell, nothing in the arguments given to
createMemBlob
can refer to something defined in the same module.
Example
createMemBlob
"content"Nothing
[15 :: Unsigned 8 .. 17] ram clk en =blockRamBlob
clk en content
The Maybe
datatype has don't care bits, where the actual value
does not matter. But the bits need a defined value in the memory. Either 0 or
1 can be used, and both are valid representations of the data.
>>>
import qualified Prelude as P
>>>
let es = [ Nothing, Just (7 :: Unsigned 8), Just 8 ]
>>>
:{
createMemBlob "content0" (Just 0) es createMemBlob "content1" (Just 1) es x = 1 :}
>>>
let pr = mapM_ (putStrLn . show)
>>>
pr $ P.map pack es
0b0_...._.... 0b1_0000_0111 0b1_0000_1000>>>
pr $ unpackMemBlob content0
0b0_0000_0000 0b1_0000_0111 0b1_0000_1000>>>
pr $ unpackMemBlob content1
0b0_1111_1111 0b1_0000_0111 0b1_0000_1000>>>
:{
createMemBlob "contentN" Nothing es x = 1 :} <interactive>:...: error: packBVs: cannot convert don't care values. Please specify a mapping to a definite value.
Note how we hinted to clashi
that our multiline command was a list of
declarations by including a dummy declaration x = 1
. Without this trick,
clashi
would expect an expression and the Template Haskell would not work.
:: forall a f. (Foldable f, BitPack a)  
=> Maybe Bit  Value to map don't care bits to. 
> f a  The content for the 
> ExpQ 
Create a MemBlob
from a list of values
Since this uses Template Haskell, nothing in the arguments given to
memBlobTH
can refer to something defined in the same module.
Example
ram clk en = blockRamBlob
clk en $(memBlobTH Nothing [15 :: Unsigned 8 .. 17])
The Maybe
datatype has don't care bits, where the actual value
does not matter. But the bits need a defined value in the memory. Either 0 or
1 can be used, and both are valid representations of the data.
>>>
import qualified Prelude as P
>>>
let es = [ Nothing, Just (7 :: Unsigned 8), Just 8 ]
>>>
content0 = $(memBlobTH (Just 0) es)
>>>
content1 = $(memBlobTH (Just 1) es)
>>>
let pr = mapM_ (putStrLn . show)
>>>
pr $ P.map pack es
0b0_...._.... 0b1_0000_0111 0b1_0000_1000>>>
pr $ unpackMemBlob content0
0b0_0000_0000 0b1_0000_0111 0b1_0000_1000>>>
pr $ unpackMemBlob content1
0b0_1111_1111 0b1_0000_0111 0b1_0000_1000>>>
$(memBlobTH Nothing es)
<interactive>:...: error: • packBVs: cannot convert don't care values. Please specify a mapping to a definite value. • In the untyped splice: $(memBlobTH Nothing es)
unpackMemBlob :: forall n m. MemBlob n m > [BitVector m] Source #
Convert a MemBlob
back to a list
NB: Not synthesizable
BlockRAM read/write conflict resolution
:: (HiddenClockResetEnable dom, NFDataX a, Eq addr)  
=> (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 readafterwrite blockRAM from a readbeforewrite one (synchronized to system clock)
>>>
import Clash.Prelude
>>>
:t readNew (blockRam (0 :> 1 :> Nil))
readNew (blockRam (0 :> 1 :> Nil)) :: ... ... ... ... ... => Signal dom addr > Signal dom (Maybe (addr, a)) > Signal dom a
True dualport block RAM
:: forall nAddrs dom1 dom2 a. (HasCallStack, KnownNat nAddrs, HiddenClock dom1, HiddenClock dom2, NFDataX a)  
=> Signal dom1 (RamOp nAddrs a)  RAM operation for port A 
> Signal dom2 (RamOp nAddrs a)  RAM operation for port B 
> (Signal dom1 a, Signal dom2 a)  Outputs data on next cycle. When writing, the data written will be echoed. When reading, the read data is returned. 
Produces vendoragnostic HDL that will be inferred as a true dualport 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 sameport read/write behavior is: WriteFirst. For mixedport 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
Instances
Show a => Show (RamOp n a) Source #  
Generic (RamOp n a) Source #  
NFDataX a => NFDataX (RamOp n a) Source #  
Defined in Clash.Explicit.BlockRam  
type Rep (RamOp n a) Source #  
Defined in Clash.Explicit.BlockRam type Rep (RamOp n a) = D1 ('MetaData "RamOp" "Clash.Explicit.BlockRam" "clashprelude1.5.0inplace" 'False) (C1 ('MetaCons "RamRead" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Index n))) :+: (C1 ('MetaCons "RamWrite" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Index n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "RamNoOp" 'PrefixI 'False) (U1 :: Type > Type))) 
Utility functions
riseEvery :: HiddenClockResetEnable dom => SNat n > Signal dom Bool Source #
Give a pulse every n
clock cycles. This is a useful helper function when
combined with functions like
or regEn
,
in order to delay a register by a known amount.mux
To be precise: the given signal will be
for the next False
n1
cycles,
followed by a single
value:True
>>>
Prelude.last (sampleN @System 1025 (riseEvery d1024)) == True
True>>>
Prelude.or (sampleN @System 1024 (riseEvery d1024)) == False
True
For example, to update a counter once every 10 million cycles:
counter =regEn
0 (riseEvery
(SNat
::SNat
10000000)) (counter + 1)
oscillate :: HiddenClockResetEnable dom => Bool > SNat n > Signal dom Bool Source #
Oscillate a
for a given number of cycles. This is a convenient
function when combined with something like Bool
, as it allows you to
easily hold a register value for a given number of cycles. The input regEn
determines what the initial value is.Bool
To oscillate on an interval of 5 cycles:
>>>
sampleN @System 11 (oscillate False d5)
[False,False,False,False,False,False,True,True,True,True,True]
To oscillate between
and True
:False
>>>
sampleN @System 11 (oscillate False d1)
[False,False,True,False,True,False,True,False,True,False,True]
An alternative definition for the above could be:
>>>
let osc' = register False (not <$> osc')
>>>
sampleN @System 200 (oscillate False d1) == sampleN @System 200 osc'
True
Exported modules
Synchronous signals
module Clash.Signal
module Clash.Signal.Delayed
Datatypes
Bit vectors
module Clash.Sized.BitVector
Arbitrarywidth 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.
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 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 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 n1 in the Rep (Vec n a) definition. We'll have to wait for things like https://ryanglscott.github.io/2018/02/11/howtoderivegenericforsomegadts/ 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 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" "clashprelude" '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 leftidentity 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.333333333333333e3
"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 rightidentity 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
# 391 "srcClashSized/Vector.hs" >>> head Nil BLANKLINE interactive:... • Couldn't match type ‘1’ with ‘0’ Expected type: Vec (0 + 1) a Actual type: Vec 0 a • In the first argument of ‘head’, namely ‘Nil’ In the expression: head Nil In an equation for ‘it’: it = head Nil
tail :: Vec (n + 1) a > Vec n a Source #
Extract the elements after the head of a vector
>>>
tail (1:>2:>3:>Nil)
2 :> 3 :> Nil
# 425 "srcClashSized/Vector.hs" >>> tail Nil BLANKLINE interactive:... • Couldn't match type ‘1’ with ‘0’ Expected type: Vec (0 + 1) a Actual type: Vec 0 a • In the first argument of ‘tail’, namely ‘Nil’ In the expression: tail Nil In an equation for ‘it’: it = tail Nil
last :: Vec (n + 1) a > a Source #
Extract the last element of a vector
>>>
last (1:>2:>3:>Nil)
3
# 459 "srcClashSized/Vector.hs" >>> last Nil BLANKLINE interactive:... • Couldn't match type ‘1’ with ‘0’ Expected type: Vec (0 + 1) a Actual type: Vec 0 a • In the first argument of ‘last’, namely ‘Nil’ In the expression: last Nil In an equation for ‘it’: it = last Nil
init :: Vec (n + 1) a > Vec n a Source #
Extract all the elements of a vector except the last element
>>>
init (1:>2:>3:>Nil)
1 :> 2 :> Nil
# 494 "srcClashSized/Vector.hs" >>> init Nil BLANKLINE interactive:... • Couldn't match type ‘1’ with ‘0’ Expected type: Vec (0 + 1) a Actual type: Vec 0 a • In the first argument of ‘init’, namely ‘Nil’ In the expression: init Nil In an equation for ‘it’: it = init Nil
:: KnownNat n  
=> Vec n a  The old vector 
> Vec m a  The elements to shift in at the head 
> (Vec n a, Vec m a)  (The new vector, shifted out elements) 
Shift in elements to the head of a vector, bumping out elements at the tail. The result is a tuple containing:
 The new vector
 The shifted out elements
>>>
shiftInAt0 (1 :> 2 :> 3 :> 4 :> Nil) ((1) :> 0 :> Nil)
(1 :> 0 :> 1 :> 2 :> Nil,3 :> 4 :> Nil)>>>
shiftInAt0 (1 :> Nil) ((1) :> 0 :> Nil)
(1 :> Nil,0 :> 1 :> Nil)
:: KnownNat m  
=> Vec n a  The old vector 
> Vec m a  The elements to shift in at the tail 
> (Vec n a, Vec m a)  (The new vector, shifted out elements) 
Shift in element to the tail of a vector, bumping out elements at the head. The result is a tuple containing:
 The new vector
 The shifted out elements
>>>
shiftInAtN (1 :> 2 :> 3 :> 4 :> Nil) (5 :> 6 :> Nil)
(3 :> 4 :> 5 :> 6 :> Nil,1 :> 2 :> Nil)>>>
shiftInAtN (1 :> Nil) (2 :> 3 :> Nil)
(3 :> Nil,1 :> 2 :> Nil)
(+>>) :: KnownNat n => a > Vec n a > Vec n a infixr 4 Source #
Add an element to the head of a vector, and extract all but the last element.
>>>
1 +>> (3:>4:>5:>Nil)
1 :> 3 :> 4 :> Nil>>>
1 +>> Nil
Nil
(<<+) :: Vec n a > a > Vec n a infixl 4 Source #
Add an element to the tail of a vector, and extract all but the first element.
>>>
(3:>4:>5:>Nil) <<+ 1
4 :> 5 :> 1 :> Nil>>>
Nil <<+ 1
Nil
:: (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 :> Nil,1 :> 2 :> Nil)
:: (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 :> Nil,4 :> 5 :> Nil)
(++) :: Vec n a > Vec m a > Vec (n + m) a infixr 5 Source #
Append two vectors.
>>>
(1:>2:>3:>Nil) ++ (7:>8:>Nil)
1 :> 2 :> 3 :> 7 :> 8 :> Nil
splitAt :: SNat m > Vec (m + n) a > (Vec m a, Vec n a) Source #
Split a vector into two vectors at the given point.
>>>
splitAt (SNat :: SNat 3) (1:>2:>3:>7:>8:>Nil)
(1 :> 2 :> 3 :> Nil,7 :> 8 :> Nil)>>>
splitAt d3 (1:>2:>3:>7:>8:>Nil)
(1 :> 2 :> 3 :> Nil,7 :> 8 :> Nil)
splitAtI :: KnownNat m => Vec (m + n) a > (Vec m a, Vec n a) Source #
Split a vector into two vectors where the length of the two is determined by the context.
>>>
splitAtI (1:>2:>3:>7:>8:>Nil) :: (Vec 2 Int, Vec 3 Int)
(1 :> 2 :> Nil,3 :> 7 :> 8 :> Nil)
concat :: Vec n (Vec m a) > Vec (n * m) a Source #
Concatenate a vector of vectors.
>>>
concat ((1:>2:>3:>Nil) :> (4:>5:>6:>Nil) :> (7:>8:>9:>Nil) :> (10:>11:>12:>Nil) :> Nil)
1 :> 2 :> 3 :> 4 :> 5 :> 6 :> 7 :> 8 :> 9 :> 10 :> 11 :> 12 :> Nil
concatMap :: (a > Vec m b) > Vec n a > Vec (n * m) b Source #
Map a function over all the elements of a vector and concatentate the resulting vectors.
>>>
concatMap (replicate d3) (1:>2:>3:>Nil)
1 :> 1 :> 1 :> 2 :> 2 :> 2 :> 3 :> 3 :> 3 :> Nil
unconcat :: KnownNat n => SNat m > Vec (n * m) a > Vec n (Vec m a) Source #
Split a vector of (n * m) elements into a vector of "vectors of length m", where the length m is given.
>>>
unconcat d4 (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)
(1 :> 2 :> 3 :> 4 :> Nil) :> (5 :> 6 :> 7 :> 8 :> Nil) :> (9 :> 10 :> 11 :> 12 :> Nil) :> Nil
unconcatI :: (KnownNat n, KnownNat m) => Vec (n * m) a > Vec n (Vec m a) Source #
Split a vector of (n * m) elements into a vector of "vectors of length m", where the length m is determined by the context.
>>>
unconcatI (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil) :: Vec 2 (Vec 6 Int)
(1 :> 2 :> 3 :> 4 :> 5 :> 6 :> Nil) :> (7 :> 8 :> 9 :> 10 :> 11 :> 12 :> Nil) :> Nil
merge :: KnownNat n => Vec n a > Vec n a > Vec (2 * n) a Source #
Merge two vectors, alternating their elements, i.e.,
>>>
merge (1 :> 2 :> 3 :> 4 :> Nil) (5 :> 6 :> 7 :> 8 :> Nil)
1 :> 5 :> 2 :> 6 :> 3 :> 7 :> 4 :> 8 :> Nil
reverse :: Vec n a > Vec n a Source #
The elements in a vector in reverse order.
>>>
reverse (1:>2:>3:>4:>Nil)
4 :> 3 :> 2 :> 1 :> Nil
imap :: forall n a b. KnownNat n => (Index n > a > b) > Vec n a > Vec n b Source #
Apply a function of every element of a vector and its index.
>>>
:t imap (+) (2 :> 2 :> 2 :> 2 :> Nil)
imap (+) (2 :> 2 :> 2 :> 2 :> Nil) :: Vec 4 (Index 4)>>>
imap (+) (2 :> 2 :> 2 :> 2 :> Nil)
2 :> 3 :> *** Exception: X: Clash.Sized.Index: result 4 is out of bounds: [0..3] ...>>>
imap (\i a > fromIntegral i + a) (2 :> 2 :> 2 :> 2 :> Nil) :: Vec 4 (Unsigned 8)
2 :> 3 :> 4 :> 5 :> Nil
"imap
f xs
" corresponds to the following circuit layout:
izipWith :: KnownNat n => (Index n > a > b > c) > Vec n a > Vec n b > Vec n c Source #
Zip two vectors with a functions that also takes the elements' indices.
>>>
izipWith (\i a b > i + a + b) (2 :> 2 :> Nil) (3 :> 3:> Nil)
*** Exception: X: Clash.Sized.Index: result 3 is out of bounds: [0..1] ...
>>>
izipWith (\i a b > fromIntegral i + a + b) (2 :> 2 :> Nil) (3 :> 3 :> Nil) :: Vec 2 (Unsigned 8)
5 :> 6 :> Nil
"imap
f xs
" corresponds to the following circuit layout:
NB: izipWith
is strict in its second argument, and lazy in its
third. This matters when izipWith
is used in a recursive setting. See
lazyV
for more information.
ifoldr :: KnownNat n => (Index n > a > b > b) > b > Vec n a > b Source #
Right fold (function applied to each element and its index)
>>>
let findLeftmost x xs = ifoldr (\i a b > if a == x then Just i else b) Nothing xs
>>>
findLeftmost 3 (1:>3:>2:>4:>3:>5:>6:>Nil)
Just 1>>>
findLeftmost 8 (1:>3:>2:>4:>3:>5:>6:>Nil)
Nothing
"ifoldr
f z xs
" corresponds to the following circuit layout:
ifoldl :: KnownNat n => (a > Index n > b > a) > a > Vec n b > a Source #
Left fold (function applied to each element and its index)
>>>
let findRightmost x xs = ifoldl (\a i b > if b == x then Just i else a) Nothing xs
>>>
findRightmost 3 (1:>3:>2:>4:>3:>5:>6:>Nil)
Just 4>>>
findRightmost 8 (1:>3:>2:>4:>3:>5:>6:>Nil)
Nothing
"ifoldl
f z xs
" corresponds to the following circuit layout:
indices :: KnownNat n => SNat n > Vec n (Index n) Source #
Generate a vector of indices.
>>>
indices d4
0 :> 1 :> 2 :> 3 :> Nil
indicesI :: KnownNat n => Vec n (Index n) Source #
Generate a vector of indices, where the length of the vector is determined by the context.
>>>
indicesI :: Vec 4 (Index 4)
0 :> 1 :> 2 :> 3 :> Nil
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 nonempty 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 nonempty 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.333333333333333e3
"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 treelike
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 :> Nil
"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 :> Nil
"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 :> Nil)
"mapAccumL
f acc xs
" corresponds to the following circuit layout:
mapAccumR :: (acc > x > (acc, y)) > acc > Vec n x > (acc, Vec n y) Source #
The mapAccumR
function behaves like a combination of map
and foldr
;
it applies a function to each element of a vector, passing an accumulating
parameter from right to left, and returning a final value of this accumulator
together with the new vector.
>>>
mapAccumR (\acc x > (acc + x,acc + 1)) 0 (1 :> 2 :> 3 :> 4 :> Nil)
(10,10 :> 8 :> 5 :> 1 :> Nil)
"mapAccumR
f acc xs
" corresponds to the following circuit layout:
zip :: Vec n a > Vec n b > Vec n (a, b) Source #
zip
takes two vectors and returns a vector of corresponding pairs.
>>>
zip (1:>2:>3:>4:>Nil) (4:>3:>2:>1:>Nil)
(1,4) :> (2,3) :> (3,2) :> (4,1) :> Nil
zip3 :: Vec n a > Vec n b > Vec n c > Vec n (a, b, c) Source #
zip3
takes three vectors and returns a vector of corresponding triplets.
>>>
zip3 (1:>2:>3:>4:>Nil) (4:>3:>2:>1:>Nil) (5:>6:>7:>8:>Nil)
(1,4,5) :> (2,3,6) :> (3,2,7) :> (4,1,8) :> Nil
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 :> Nil,4 :> 3 :> 2 :> 1 :> Nil)
unzip3 :: Vec n (a, b, c) > (Vec n a, Vec n b, Vec n c) Source #
unzip3
transforms a vector of triplets into a vector of first components,
a vector of second components, and a vector of third components.
>>>
unzip3 ((1,4,5):>(2,3,6):>(3,2,7):>(4,1,8):>Nil)
(1 :> 2 :> 3 :> 4 :> Nil,4 :> 3 :> 2 :> 1 :> Nil,5 :> 6 :> 7 :> 8 :> Nil)
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) !! 4
5>>>
(1:>2:>3:>4:>5:>Nil) !! (length (1:>2:>3:>4:>5:>Nil)  1)
5>>>
(1:>2:>3:>4:>5:>Nil) !! 1
2>>>
(1:>2:>3:>4:>5:>Nil) !! 14
*** Exception: Clash.Sized.Vector.(!!): index 14 is larger than maximum index 4 ...
replace :: (KnownNat n, Enum i) => i > a > Vec n a > Vec n a Source #
"replace
n a xs
" returns the vector xs where the n'th element is
replaced by a.
NB: vector elements have an ASCENDING subscript starting from 0 and
ending at
.length
 1
>>>
replace 3 7 (1:>2:>3:>4:>5:>Nil)
1 :> 2 :> 3 :> 7 :> 5 :> Nil>>>
replace 0 7 (1:>2:>3:>4:>5:>Nil)
7 :> 2 :> 3 :> 4 :> 5 :> Nil>>>
replace 9 7 (1:>2:>3:>4:>5:>Nil)
1 :> 2 :> 3 :> 4 :> 5 :> *** Exception: Clash.Sized.Vector.replace: index 9 is larger than maximum index 4 ...
take :: SNat m > Vec (m + n) a > Vec m a Source #
"take
n xs
" returns the nlength prefix of xs.
>>>
take (SNat :: SNat 3) (1:>2:>3:>4:>5:>Nil)
1 :> 2 :> 3 :> Nil>>>
take d3 (1:>2:>3:>4:>5:>Nil)
1 :> 2 :> 3 :> Nil>>>
take d0 (1:>2:>Nil)
Nil
# 1432 "srcClashSized/Vector.hs" >>> take d4 (1:>2:>Nil) BLANKLINE interactive:... • Couldn't match type ‘4 + n0’ with ‘2’ Expected type: Vec (4 + n0) a Actual type: Vec (1 + 1) a The type variable ‘n0’ is ambiguous • In the second argument of ‘take’, namely ‘(1 :> 2 :> Nil)’ In the expression: take d4 (1 :> 2 :> Nil) In an equation for ‘it’: it = take d4 (1 :> 2 :> Nil)
takeI :: KnownNat m => Vec (m + n) a > Vec m a Source #
"takeI
xs
" returns the prefix of xs as demanded by the context.
>>>
takeI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
1 :> 2 :> Nil
drop :: SNat m > Vec (m + n) a > Vec n a Source #
"drop
n xs
" returns the suffix of xs after the first n elements.
>>>
drop (SNat :: SNat 3) (1:>2:>3:>4:>5:>Nil)
4 :> 5 :> Nil>>>
drop d3 (1:>2:>3:>4:>5:>Nil)
4 :> 5 :> Nil>>>
drop d0 (1:>2:>Nil)
1 :> 2 :> Nil>>>
drop d4 (1:>2:>Nil)
<interactive>:...: error: • Couldn't match...type ‘4 + n0... The type variable ‘n0’ is ambiguous • In the first argument of ‘print’, namely ‘it’ In a stmt of an interactive GHCi command: print it
dropI :: KnownNat m => Vec (m + n) a > Vec n a Source #
"dropI
xs
" returns the suffix of xs as demanded by the context.
>>>
dropI (1:>2:>3:>4:>5:>Nil) :: Vec 2 Int
4 :> 5 :> Nil
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 stepsize s and
offset f
from xs.
>>>
select (SNat :: SNat 1) (SNat :: SNat 2) (SNat :: SNat 3) (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
2 :> 4 :> 6 :> Nil>>>
select d1 d2 d3 (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
2 :> 4 :> 6 :> Nil
selectI :: (CmpNat (i + s) (s * n) ~ 'GT, KnownNat n) => SNat f > SNat s > Vec (f + i) a > Vec n a Source #
"selectI
f s xs
" selects as many elements as demanded by the context
with stepsize s and offset f from xs.
>>>
selectI d1 d2 (1:>2:>3:>4:>5:>6:>7:>8:>Nil) :: Vec 2 Int
2 :> 4 :> Nil
replicate :: SNat n > a > Vec n a Source #
"replicate
n a
" returns a vector that has n copies of a.
>>>
replicate (SNat :: SNat 3) 6
6 :> 6 :> 6 :> Nil>>>
replicate d3 6
6 :> 6 :> 6 :> Nil
repeat :: KnownNat n => a > Vec n a Source #
"repeat
a
" creates a vector with as many copies of a as demanded
by the context.
>>>
repeat 6 :: Vec 5 Int
6 :> 6 :> 6 :> 6 :> 6 :> Nil
iterate :: SNat n > (a > a) > a > Vec n a Source #
"iterate
n f x
" returns a vector starting with x followed by
n repeated applications of f to x.
iterate (SNat :: SNat 4) f x == (x :> f x :> f (f x) :> f (f (f x)) :> Nil) iterate d4 f x == (x :> f x :> f (f x) :> f (f (f x)) :> Nil)
>>>
iterate d4 (+1) 1
1 :> 2 :> 3 :> 4 :> Nil
"iterate
n f z
" corresponds to the following circuit layout:
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,s1)) 10
10 :> 9 :> 8 :> 7 :> 6 :> 5 :> 4 :> 3 :> 2 :> 1 :> Nil
unfoldrI :: KnownNat n => (s > (a, s)) > s > Vec n a Source #
"'unfoldr f s
" builds a vector from a seed value s
, where every
element a
is created by successive calls of f
on s
; the length of the
vector is inferred from the context. Unlike unfoldr
from
Data.List the generating function f
cannot dictate the length of the
resulting vector, it must be statically known.
a simple use of unfoldrI
:
>>>
unfoldrI (\s > (s,s1)) 10 :: Vec 10 Int
10 :> 9 :> 8 :> 7 :> 6 :> 5 :> 4 :> 3 :> 2 :> 1 :> Nil
generate :: SNat n > (a > a) > a > Vec n a Source #
"generate
n f x
" returns a vector with n
repeated applications of
f
to x
.
generate (SNat :: SNat 4) f x == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil) generate d4 f x == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil)
>>>
generate d4 (+1) 1
2 :> 3 :> 4 :> 5 :> Nil
"generate
n f z
" corresponds to the following circuit layout:
transpose :: KnownNat n => Vec m (Vec n a) > Vec n (Vec m a) Source #
Transpose a matrix: go from rowmajor to columnmajor
>>>
let xss = (1:>2:>Nil):>(3:>4:>Nil):>(5:>6:>Nil):>Nil
>>>
xss
(1 :> 2 :> Nil) :> (3 :> 4 :> Nil) :> (5 :> 6 :> Nil) :> Nil>>>
transpose xss
(1 :> 3 :> 5 :> Nil) :> (2 :> 4 :> 6 :> Nil) :> Nil
:: 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 
1dimensional stencil computations
"stencil1d
stX f xs
", where xs has stX + n elements, applies the
stencil computation f on: n + 1 overlapping (1D) windows of length stX,
drawn from xs. The resulting vector has n + 1 elements.
>>>
let xs = (1:>2:>3:>4:>5:>6:>Nil)
>>>
:t xs
xs :: Num a => Vec 6 a>>>
:t stencil1d d2 sum xs
stencil1d d2 sum xs :: Num b => Vec 5 b>>>
stencil1d d2 sum xs
3 :> 5 :> 7 :> 9 :> 11 :> Nil
:: (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) 
2dimensional stencil computations
"stencil2d
stY stX f xss
", where xss is a matrix of stY + m rows
of stX + n elements, applies the stencil computation f on:
(m + 1) * (n + 1) overlapping (2D) windows of stY rows of stX elements,
drawn from xss. The result matrix has m + 1 rows of n + 1 elements.
>>>
let xss = ((1:>2:>3:>4:>Nil):>(5:>6:>7:>8:>Nil):>(9:>10:>11:>12:>Nil):>(13:>14:>15:>16:>Nil):>Nil)
>>>
:t xss
xss :: Num a => Vec 4 (Vec 4 a)>>>
:t stencil2d d2 d2 (sum . map sum) xss
stencil2d d2 d2 (sum . map sum) xss :: Num b => Vec 3 (Vec 3 b)>>>
stencil2d d2 d2 (sum . map sum) xss
(14 :> 18 :> 22 :> Nil) :> (30 :> 34 :> 38 :> Nil) :> (46 :> 50 :> 54 :> Nil) :> Nil
:: KnownNat n  
=> SNat (stX + 1)  Length of the window, at least size 1 
> Vec ((stX + n) + 1) a  
> Vec (n + 1) (Vec (stX + 1) a) 
"windows1d
stX xs
", where the vector xs has stX + n elements,
returns a vector of n + 1 overlapping (1D) windows of xs of length stX.
>>>
let xs = (1:>2:>3:>4:>5:>6:>Nil)
>>>
:t xs
xs :: Num a => Vec 6 a>>>
:t windows1d d2 xs
windows1d d2 xs :: Num a => Vec 5 (Vec 2 a)>>>
windows1d d2 xs
(1 :> 2 :> Nil) :> (2 :> 3 :> Nil) :> (3 :> 4 :> Nil) :> (4 :> 5 :> Nil) :> (5 :> 6 :> Nil) :> Nil
:: (KnownNat n, KnownNat m)  
=> SNat (stY + 1)  Window hight stY, at least size 1 
> SNat (stX + 1)  Window width stX, at least size 1 
> Vec ((stY + m) + 1) (Vec ((stX + n) + 1) a)  
> Vec (m + 1) (Vec (n + 1) (Vec (stY + 1) (Vec (stX + 1) a))) 
"windows2d
stY stX xss
", where matrix xss has stY + m rows of
stX + n, returns a matrix of m+1 rows of n+1 elements. The elements
of this new matrix are the overlapping (2D) windows of xss, where every
window has stY rows of stX elements.
>>>
let xss = ((1:>2:>3:>4:>Nil):>(5:>6:>7:>8:>Nil):>(9:>10:>11:>12:>Nil):>(13:>14:>15:>16:>Nil):>Nil)
>>>
:t xss
xss :: Num a => Vec 4 (Vec 4 a)>>>
:t windows2d d2 d2 xss
windows2d d2 d2 xss :: Num a => Vec 3 (Vec 3 (Vec 2 (Vec 2 a)))>>>
windows2d d2 d2 xss
(((1 :> 2 :> Nil) :> (5 :> 6 :> Nil) :> Nil) :> ((2 :> 3 :> Nil) :> (6 :> 7 :> Nil) :> Nil) :> ((3 :> 4 :> Nil) :> (7 :> 8 :> Nil) :> Nil) :> Nil) :> (((5 :> 6 :> Nil) :> (9 :> 10 :> Nil) :> Nil) :> ((6 :> 7 :> Nil) :> (10 :> 11 :> Nil) :> Nil) :> ((7 :> 8 :> Nil) :> (11 :> 12 :> Nil) :> Nil) :> Nil) :> (((9 :> 10 :> Nil) :> (13 :> 14 :> Nil) :> Nil) :> ((10 :> 11 :> Nil) :> (14 :> 15 :> Nil) :> Nil) :> ((11 :> 12 :> Nil) :> (15 :> 16 :> Nil) :> Nil) :> Nil) :> Nil
:: (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 :> Nil
:: (Enum i, KnownNat n, KnownNat m)  
=> Vec n a  Default values, def 
> Vec m i  Index mapping, is 
> Vec (m + k) a  Vector to be scattered, xs 
> Vec n a 
Copy elements from the source vector, xs, to the destination vector according to an index mapping is. This is a forward permute operation where a to vector encodes an input to output index mapping. Output elements for indices that are not mapped assume the value in the default vector def.
For example:
>>>
let defVec = 0:>0:>0:>0:>0:>0:>0:>0:>0:>Nil
>>>
let to = 1:>3:>7:>2:>5:>8:>Nil
>>>
let input = 1:>9:>6:>4:>4:>2:>5:>Nil
>>>
scatter defVec to input
0 :> 1 :> 4 :> 9 :> 0 :> 4 :> 0 :> 6 :> 2 :> Nil
NB: If the same index appears in the index mapping more than once, the latest mapping is chosen.
Backwards permutation specified by an index mapping, is, from the destination vector specifying which element of the source vector xs to read.
"gather
xs is
" is equivalent to "map
(xs
".!!
) is
For example:
>>>
let input = 1:>9:>6:>4:>4:>2:>0:>1:>2:>Nil
>>>
let from = 1:>3:>7:>2:>5:>3:>Nil
>>>
gather input from
9 :> 4 :> 1 :> 6 :> 2 :> 4 :> Nil
"interleave
d xs
" creates a vector:
<x_0,x_d,x_(2d),...,x_1,x_(d+1),x_(2d+1),...,x_(d1),x_(2d1),x_(3d1)>
>>>
let xs = 1 :> 2 :> 3 :> 4 :> 5 :> 6 :> 7 :> 8 :> 9 :> Nil
>>>
interleave d3 xs
1 :> 4 :> 7 :> 2 :> 5 :> 8 :> 3 :> 6 :> 9 :> Nil
rotateLeft :: (Enum i, KnownNat n) => Vec n a > i > Vec n a Source #
Dynamically rotate a Vec
tor to the left:
>>>
let xs = 1 :> 2 :> 3 :> 4 :> Nil
>>>
rotateLeft xs 1
2 :> 3 :> 4 :> 1 :> Nil>>>
rotateLeft xs 2
3 :> 4 :> 1 :> 2 :> Nil>>>
rotateLeft xs (1)
4 :> 1 :> 2 :> 3 :> Nil
NB: use rotateLeftS
if you want to rotate left by a static amount.
rotateRight :: (Enum i, KnownNat n) => Vec n a > i > Vec n a Source #
Dynamically rotate a Vec
tor to the right:
>>>
let xs = 1 :> 2 :> 3 :> 4 :> Nil
>>>
rotateRight xs 1
4 :> 1 :> 2 :> 3 :> Nil>>>
rotateRight xs 2
3 :> 4 :> 1 :> 2 :> Nil>>>
rotateRight xs (1)
2 :> 3 :> 4 :> 1 :> Nil
NB: use rotateRightS
if you want to rotate right by a static amount.
rotateLeftS :: KnownNat n => Vec n a > SNat d > Vec n a Source #
Statically rotate a Vec
tor to the left:
>>>
let xs = 1 :> 2 :> 3 :> 4 :> Nil
>>>
rotateLeftS xs d1
2 :> 3 :> 4 :> 1 :> Nil
NB: use rotateLeft
if you want to rotate left by a dynamic amount.
rotateRightS :: KnownNat n => Vec n a > SNat d > Vec n a Source #
Statically rotate a Vec
tor to the right:
>>>
let xs = 1 :> 2 :> 3 :> 4 :> Nil
>>>
rotateRightS xs d1
4 :> 1 :> 2 :> 3 :> Nil
NB: use rotateRight
if you want to rotate right by a dynamic amount.
toList :: Vec n a > [a] Source #
Convert a vector to a list.
>>>
toList (1:>2:>3:>Nil)
[1,2,3]
NB: this function is not synthesizable
listToVecTH :: Lift a => [a] > ExpQ Source #
Create a vector literal from a list literal.
$(listToVecTH [1::Signed 8,2,3,4,5]) == (8:>2:>3:>4:>5:>Nil) :: Vec 5 (Signed 8)
>>>
[1 :: Signed 8,2,3,4,5]
[1,2,3,4,5]>>>
$(listToVecTH [1::Signed 8,2,3,4,5])
1 :> 2 :> 3 :> 4 :> 5 :> Nil
lazyV :: KnownNat n => Vec n a > Vec n a Source #
What you should use when your vector functions are too strict in their arguments.
doctests setup
>>>
let compareSwapL a b = if a < b then (a,b) else (b,a)
>>>
:{
let sortVL :: (Ord a, KnownNat (n + 1)) => Vec ((n + 1) + 1) a > Vec ((n + 1) + 1) a sortVL xs = map fst sorted :< (snd (last sorted)) where lefts = head xs :> map snd (init sorted) rights = tail xs sorted = zipWith compareSwapL (lazyV lefts) rights :}
>>>
:{
let sortV_flip xs = map fst sorted :< (snd (last sorted)) where lefts = head xs :> map snd (init sorted) rights = tail xs sorted = zipWith (flip compareSwapL) rights lefts :}
Example usage
For example:
 Bubble sort for 1 iteration sortV xs =map
fst sorted:<
(snd (last
sorted)) where lefts =head
xs :>map
snd (init
sorted) rights =tail
xs sorted =zipWith
compareSwapL lefts rights  Compare and swap compareSwapL a b = if a < b then (a,b) else (b,a)
Will not terminate because zipWith
is too strict in its second argument.
In this case, adding lazyV
on zipWith
s second argument:
sortVL xs =map
fst sorted:<
(snd (last
sorted)) where lefts =head
xs :> map snd (init
sorted) rights =tail
xs sorted =zipWith
compareSwapL (lazyV
lefts) rights
Results in a successful computation:
>>>
sortVL (4 :> 1 :> 2 :> 3 :> Nil)
1 :> 2 :> 3 :> 4 :> Nil
NB: There is also a solution using flip
, but it slightly obfuscates the
meaning of the code:
sortV_flip xs =map
fst sorted:<
(snd (last
sorted)) where lefts =head
xs :>map
snd (init
sorted) rights =tail
xs sorted =zipWith
(flip
compareSwapL) rights lefts
>>>
sortV_flip (4 :> 1 :> 2 :> 3 :> Nil)
1 :> 2 :> 3 :> 4 :> Nil
:: 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.
doctests setup
>>>
:seti fplugin GHC.TypeLits.Normalise
>>>
import Data.Singletons (Apply, Proxy (..), TyFun)
>>>
data Append (m :: Nat) (a :: Type) (f :: TyFun Nat Type) :: Type
>>>
type instance Apply (Append m a) l = Vec (l + m) a
>>>
let append' xs ys = dfold (Proxy :: Proxy (Append m a)) (const (:>)) ys xs
Example usage
Using lists, we can define append (a.k.a. Data.List.
++
) in
terms of Data.List.
foldr
:
>>>
import qualified Data.List
>>>
let append xs ys = Data.List.foldr (:) ys xs
>>>
append [1,2] [3,4]
[1,2,3,4]
However, when we try to do the same for Vec
, by defining append' in terms
of Clash.Sized.Vector.
foldr
:
append' xs ys = foldr
(:>) ys xs
we get a type error:
>>> let append' xs ys = foldr (:>) ys xs <interactive>:... • Occurs check: cannot construct the infinite type: ... ~ ... + 1 Expected type: a > Vec ... a > Vec ... a Actual type: a > Vec ... a > Vec (... + 1) a • In the first argument of ‘foldr’, namely ‘(:>)’ In the expression: foldr (:>) ys xs In an equation for ‘append'’: append' xs ys = foldr (:>) ys xs • Relevant bindings include ys :: Vec ... a (bound at ...) append' :: Vec n a > Vec ... a > Vec ... a (bound at ...)
The reason is that the type of foldr
is:
>>>
:t foldr
foldr :: (a > b > b) > b > Vec n a > b
While the type of (:>
) is:
>>>
:t (:>)
(:>) :: a > Vec n a > Vec (n + 1) a
We thus need a fold
function that can handle the growing vector type:
dfold
. Compared to foldr
, dfold
takes an extra parameter, called the
motive, that allows the folded function to have an argument and result type
that depends on the current length of the vector. Using dfold
, we can
now correctly define append':
import Data.Singletons import Data.Proxy data Append (m :: Nat) (a :: Type) (f ::TyFun
Nat Type) :: Type type 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 :> Nil
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
:: 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 treelike structure.
doctests setup
>>>
:seti XUndecidableInstances
>>>
import Data.Singletons (Apply, Proxy (..), TyFun)
>>>
data IIndex (f :: TyFun Nat Type) :: Type
>>>
type instance Apply IIndex l = Index ((2^l)+1)
>>>
:{
let populationCount' :: (KnownNat k, KnownNat (2^k)) => BitVector (2^k) > Index ((2^k)+1) populationCount' bv = dtfold (Proxy @IIndex) fromIntegral (\_ x y > add x y) (bv2v bv) :}
Example usage
As an example of when you might want to use dtfold
we will build a
population counter: a circuit that counts the number of bits set to '1' in
a BitVector
. Given a vector of n bits, we only need we need a data type
that can represent the number n: Index
(n+1)
. Index
k
has a range
of [0 .. k1]
(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)
)
treestructure 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 bitwidth, 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 treestructure of
add
es:
# 2271 "srcClashSized/Vector.hs" >>> :{ let populationCount' :: (KnownNat (n+1), KnownNat (n+2)) => BitVector (n+1) > Index (n+2) populationCount' = fold add . map fromIntegral . bv2v :} BLANKLINE interactive:... • Couldn't match type ‘((n + 2) + (n + 2))  1’ with ‘n + 2’ Expected type: Index (n + 2) > Index (n + 2) > Index (n + 2) Actual type: Index (n + 2) > Index (n + 2) > AResult (Index (n + 2)) (Index (n + 2)) • In the first argument of ‘fold’, namely ‘add’ In the first argument of ‘(.)’, namely ‘fold add’ In the expression: fold add . map fromIntegral . bv2v • Relevant bindings include populationCount' :: BitVector (n + 1) > Index (n + 2) (bound at ...)
because fold
expects a function of type "a > a > a
", i.e. a function
where the arguments and result all have exactly the same type.
In order to accommodate the type of our add
, where the
result is larger than the arguments, we must use a dependently typed fold in
the form of dtfold
:
{# LANGUAGE UndecidableInstances #} import Data.Singletons import Data.Proxy data IIndex (f ::TyFun
Nat Type) :: Type type instanceApply
IIndex l =Index
((2^l)+1) populationCount' :: (KnownNat k, KnownNat (2^k)) => BitVector (2^k) > Index ((2^k)+1) populationCount' bv =dtfold
(Proxy @IIndex) fromIntegral (\_ x y >add
x y) (bv2v
bv)
And we can test that it works:
>>>
:t populationCount' (7 :: BitVector 16)
populationCount' (7 :: BitVector 16) :: Index 17>>>
populationCount' (7 :: BitVector 16)
3
Some final remarks:
 By using
dtfold
instead offold
, we had to restrict ourBitVector
argument to have bitwidth 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 bitwidth 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.
doctests setup
>>>
let compareSwap a b = if a > b then (a,b) else (b,a)
>>>
let insert y xs = let (y',xs') = mapAccumL compareSwap y xs in xs' :< y'
>>>
let insertionSort = vfold (const insert)
Example usage
compareSwap a b = if a > b then (a,b) else (b,a) insert y xs = let (y',xs') =mapAccumL
compareSwap y xs in xs':<
y' insertionSort =vfold
(const insert)
Builds a triangular structure of compare and swaps to sort a row.
>>>
insertionSort (7 :> 3 :> 9 :> 1 :> Nil)
1 :> 3 :> 7 :> 9 :> Nil
The circuit layout of insertionSort
, build using vfold
, is:
smap :: forall k a b. KnownNat k => (forall l. SNat l > a > b) > Vec k a > Vec k b Source #
Apply a function to every element of a vector and the element's position
(as an SNat
value) in the vector.
>>>
let rotateMatrix = smap (flip rotateRightS)
>>>
let xss = (1:>2:>3:>Nil):>(1:>2:>3:>Nil):>(1:>2:>3:>Nil):>Nil
>>>
xss
(1 :> 2 :> 3 :> Nil) :> (1 :> 2 :> 3 :> Nil) :> (1 :> 2 :> 3 :> Nil) :> Nil>>>
rotateMatrix xss
(1 :> 2 :> 3 :> Nil) :> (3 :> 1 :> 2 :> Nil) :> (2 :> 3 :> 1 :> Nil) :> Nil
concatBitVector# :: forall n m. (KnownNat n, KnownNat m) => Vec n (BitVector m) > BitVector (n * m) Source #
unconcatBitVector# :: forall n m. (KnownNat n, KnownNat m) => BitVector (n * m) > Vec n (BitVector m) Source #
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 XException
s.
forceVX :: KnownNat n => Vec n a > Vec n a Source #
Evaluate all elements of a vector to WHNF. Does not propagate
XException
s.
Perfect depth trees
module Clash.Sized.RTree
Annotations
module Clash.Annotations.TopEntity
Generics typeclasses
Representable types of kind *
.
This class is derivable in GHC with the DeriveGeneric
flag on.
A Generic
instance must satisfy the following laws:
from
.to
≡id
to
.from
≡id