clash-prelude-1.6.4: Clash: a functional hardware description language - Prelude library
Copyright (C) 2016 University of Twente2022 QBayLogic B.V. BSD2 (see the file LICENSE) QBayLogic B.V. Trustworthy Haskell2010

Clash.Sized.RTree

Description

Synopsis

# RTree data type

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

Perfect depth binary tree.

• Only has elements at the leaf of the tree
• A tree of depth d has 2^d elements.

Constructors

 RLeaf :: a -> RTree 0 a RBranch :: RTree d a -> RTree d a -> RTree (d + 1) a

Bundled Patterns

 pattern LR :: a -> RTree 0 a RLeaf of a perfect depth tree>>> LR 1 1 >>> let x = LR 1 >>> :t x x :: Num a => RTree 0 a Can be used as a pattern:>>> let f (LR a) (LR b) = a + b >>> :t f f :: Num a => RTree 0 a -> RTree 0 a -> a >>> f (LR 1) (LR 2) 3  pattern BR :: RTree d a -> RTree d a -> RTree (d + 1) a RBranch of a perfect depth tree>>> BR (LR 1) (LR 2) <1,2> >>> let x = BR (LR 1) (LR 2) >>> :t x x :: Num a => RTree 1 a Case be used a pattern:>>> let f (BR (LR a) (LR b)) = LR (a + b) >>> :t f f :: Num a => RTree 1 a -> RTree 0 a >>> f (BR (LR 1) (LR 2)) 3 

#### Instances

Instances details
 Lift a => Lift (RTree d a :: Type) Source # Instance detailsDefined in Clash.Sized.RTree Methodslift :: RTree d a -> Q Exp #liftTyped :: RTree d a -> Q (TExp (RTree d a)) # KnownNat d => Functor (RTree d) Source # Instance detailsDefined in Clash.Sized.RTree Methodsfmap :: (a -> b) -> RTree d a -> RTree d b #(<$) :: a -> RTree d b -> RTree d a # KnownNat d => Applicative (RTree d) Source # Instance detailsDefined in Clash.Sized.RTree Methodspure :: a -> RTree d a #(<*>) :: RTree d (a -> b) -> RTree d a -> RTree d b #liftA2 :: (a -> b -> c) -> RTree d a -> RTree d b -> RTree d c #(*>) :: RTree d a -> RTree d b -> RTree d b #(<*) :: RTree d a -> RTree d b -> RTree d a # KnownNat d => Foldable (RTree d) Source # Instance detailsDefined in Clash.Sized.RTree Methodsfold :: Monoid m => RTree d m -> m #foldMap :: Monoid m => (a -> m) -> RTree d a -> m #foldMap' :: Monoid m => (a -> m) -> RTree d a -> m #foldr :: (a -> b -> b) -> b -> RTree d a -> b #foldr' :: (a -> b -> b) -> b -> RTree d a -> b #foldl :: (b -> a -> b) -> b -> RTree d a -> b #foldl' :: (b -> a -> b) -> b -> RTree d a -> b #foldr1 :: (a -> a -> a) -> RTree d a -> a #foldl1 :: (a -> a -> a) -> RTree d a -> a #toList :: RTree d a -> [a] #null :: RTree d a -> Bool #length :: RTree d a -> Int #elem :: Eq a => a -> RTree d a -> Bool #maximum :: Ord a => RTree d a -> a #minimum :: Ord a => RTree d a -> a #sum :: Num a => RTree d a -> a #product :: Num a => RTree d a -> a # KnownNat d => Traversable (RTree d) Source # Instance detailsDefined in Clash.Sized.RTree Methodstraverse :: Applicative f => (a -> f b) -> RTree d a -> f (RTree d b) #sequenceA :: Applicative f => RTree d (f a) -> f (RTree d a) #mapM :: Monad m => (a -> m b) -> RTree d a -> m (RTree d b) #sequence :: Monad m => RTree d (m a) -> m (RTree d a) # (KnownNat d, Eq a) => Eq (RTree d a) Source # Instance detailsDefined in Clash.Sized.RTree Methods(==) :: RTree d a -> RTree d a -> Bool #(/=) :: RTree d a -> RTree d a -> Bool # (KnownNat d, Ord a) => Ord (RTree d a) Source # Instance detailsDefined in Clash.Sized.RTree Methodscompare :: RTree d a -> RTree d a -> Ordering #(<) :: RTree d a -> RTree d a -> Bool #(<=) :: RTree d a -> RTree d a -> Bool #(>) :: RTree d a -> RTree d a -> Bool #(>=) :: RTree d a -> RTree d a -> Bool #max :: RTree d a -> RTree d a -> RTree d a #min :: RTree d a -> RTree d a -> RTree d a # Show a => Show (RTree n a) Source # Instance detailsDefined in Clash.Sized.RTree MethodsshowsPrec :: Int -> RTree n a -> ShowS #show :: RTree n a -> String #showList :: [RTree n a] -> ShowS # (KnownNat d, Arbitrary a) => Arbitrary (RTree d a) Source # Instance detailsDefined in Clash.Sized.RTree Methodsarbitrary :: Gen (RTree d a) #shrink :: RTree d a -> [RTree d a] # (KnownNat d, CoArbitrary a) => CoArbitrary (RTree d a) Source # Instance detailsDefined in Clash.Sized.RTree Methodscoarbitrary :: RTree d a -> Gen b -> Gen b # (KnownNat d, Default a) => Default (RTree d a) Source # Instance detailsDefined in Clash.Sized.RTree Methodsdef :: RTree d a # NFData a => NFData (RTree d a) Source # Instance detailsDefined in Clash.Sized.RTree Methodsrnf :: RTree d a -> () # KnownNat d => Ixed (RTree d a) Source # Instance detailsDefined in Clash.Sized.RTree Methodsix :: Index (RTree d a) -> Traversal' (RTree d a) (IxValue (RTree d a)) # (KnownNat d, NFDataX a) => NFDataX (RTree d a) Source # Instance detailsDefined in Clash.Sized.RTree MethodsdeepErrorX :: String -> RTree d a Source #hasUndefined :: RTree d a -> Bool Source #ensureSpine :: RTree d a -> RTree d a Source #rnfX :: RTree d a -> () Source # ShowX a => ShowX (RTree n a) Source # Instance detailsDefined in Clash.Sized.RTree MethodsshowsPrecX :: Int -> RTree n a -> ShowS Source #showX :: RTree n a -> String Source #showListX :: [RTree n a] -> ShowS Source # (KnownNat d, BitPack a) => BitPack (RTree d a) Source # Instance detailsDefined in Clash.Sized.RTree Associated Typestype BitSize (RTree d a) :: Nat Source # Methodspack :: RTree d a -> BitVector (BitSize (RTree d a)) Source #unpack :: BitVector (BitSize (RTree d a)) -> RTree d a Source # KnownNat d => Bundle (RTree d a) Source # Instance detailsDefined in Clash.Signal.Bundle Associated Typestype Unbundled dom (RTree d a) = (res :: Type) Source # Methodsbundle :: forall (dom :: Domain). Unbundled dom (RTree d a) -> Signal dom (RTree d a) Source #unbundle :: forall (dom :: Domain). Signal dom (RTree d a) -> Unbundled dom (RTree d a) Source # KnownNat d => Bundle (RTree d a) Source # Instance detailsDefined in Clash.Signal.Delayed.Bundle Associated Typestype Unbundled dom d (RTree d a) = (res :: Type) Source # Methodsbundle :: forall (dom :: Domain) (d0 :: Nat). Unbundled dom d0 (RTree d a) -> DSignal dom d0 (RTree d a) Source #unbundle :: forall (dom :: Domain) (d0 :: Nat). DSignal dom d0 (RTree d a) -> Unbundled dom d0 (RTree d a) Source # (KnownNat d, AutoReg a) => AutoReg (RTree d a) Source # Instance detailsDefined in Clash.Class.AutoReg.Internal MethodsautoReg :: forall (dom :: Domain). (HasCallStack, KnownDomain dom) => Clock dom -> Reset dom -> Enable dom -> RTree d a -> Signal dom (RTree d a) -> Signal dom (RTree d a) Source # type Unbundled t delay (RTree d a) Source # Instance detailsDefined in Clash.Signal.Delayed.Bundle type Unbundled t delay (RTree d a) = RTree d (DSignal t delay a) type Unbundled t (RTree d a) Source # Instance detailsDefined in Clash.Signal.Bundle type Unbundled t (RTree d a) = RTree d (Signal t a) type TryDomain t (RTree d a) Source # Instance detailsDefined in Clash.Class.HasDomain.HasSingleDomain type TryDomain t (RTree d a) = TryDomain t a type Index (RTree d a) Source # Instance detailsDefined in Clash.Sized.RTree type Index (RTree d a) = Int type IxValue (RTree d a) Source # Instance detailsDefined in Clash.Sized.RTree type IxValue (RTree d a) = a type BitSize (RTree d a) Source # Instance detailsDefined in Clash.Sized.RTree type BitSize (RTree d a) = (2 ^ d) * BitSize a # Construction treplicate :: forall d a. SNat d -> a -> RTree d a Source # "treplicate d a" returns a tree of depth d, and has 2^d copies of a. >>> treplicate (SNat :: SNat 3) 6 <<<6,6>,<6,6>>,<<6,6>,<6,6>>> >>> treplicate d3 6 <<<6,6>,<6,6>>,<<6,6>,<6,6>>>  trepeat :: KnownNat d => a -> RTree d a Source # "trepeat a" creates a tree with as many copies of a as demanded by the context. >>> trepeat 6 :: RTree 2 Int <<6,6>,<6,6>>  # Accessors thead :: RTree n a -> a Source # Extract the first element of a tree The first element is defined to be the bottom-left leaf. >>> thead$ BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4))
1


tlast :: RTree n a -> a Source #

Extract the last element of a tree

The last element is defined to be the bottom-right leaf.

>>> tlast \$ BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4))
4


## Indexing

indexTree :: (KnownNat d, Enum i) => RTree d a -> i -> a Source #

"indexTree t n" returns the n'th element of t.

The bottom-left leaf had index 0, and the bottom-right leaf has index 2^d-1, where d is the depth of the tree

>>> indexTree (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4))) 0
1
>>> indexTree (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4))) 2
3
>>> indexTree (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4))) 14
*** Exception: Clash.Sized.Vector.(!!): index 14 is larger than maximum index 3
...


tindices :: forall d. KnownNat d => RTree d (Index (2 ^ d)) Source #

Generate a tree of indices, where the depth of the tree is determined by the context.

>>> tindices :: RTree 3 (Index 8)
<<<0,1>,<2,3>>,<<4,5>,<6,7>>>


# Modifying trees

replaceTree :: (KnownNat d, Enum i) => i -> a -> RTree d a -> RTree d a Source #

"replaceTree n a t" returns the tree t where the n'th element is replaced by a.

The bottom-left leaf had index 0, and the bottom-right leaf has index 2^d-1, where d is the depth of the tree

>>> replaceTree 0 5 (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4)))
<<5,2>,<3,4>>
>>> replaceTree 2 7 (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4)))
<<1,2>,<7,4>>
>>> replaceTree 9 6 (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4)))
<<1,2>,<3,*** Exception: Clash.Sized.Vector.replace: index 9 is larger than maximum index 3
...


# Element-wise operations

## Mapping

tmap :: forall d a b. KnownNat d => (a -> b) -> RTree d a -> RTree d b Source #

"tmap f t" is the tree obtained by apply f to each element of t, i.e.,

tmap f (BR (LR a) (LR b)) == BR (LR (f a)) (LR (f b))

tzipWith :: forall a b c d. KnownNat d => (a -> b -> c) -> RTree d a -> RTree d b -> RTree d c Source #

tzipWith generalizes tzip by zipping with the function given as the first argument, instead of a tupling function. For example, "tzipWith (+)" applied to two trees produces the tree of corresponding sums.

tzipWith f (BR (LR a1) (LR b1)) (BR (LR a2) (LR b2)) == BR (LR (f a1 a2)) (LR (f b1 b2))

## Zipping

tzip :: KnownNat d => RTree d a -> RTree d b -> RTree d (a, b) Source #

tzip takes two trees and returns a tree of corresponding pairs.

## Unzipping

tunzip :: forall d a b. KnownNat d => RTree d (a, b) -> (RTree d a, RTree d b) Source #

tunzip transforms a tree of pairs into a tree of first components and a tree of second components.

# Folding

Arguments

 :: forall d a b. KnownNat d => (a -> b) Function to apply to the leaves -> (b -> b -> b) Function to combine the results of the reduction of two branches -> RTree d a Tree to fold reduce -> b

Reduce a tree to a single element

## Specialised folds

Arguments

 :: forall p k a. KnownNat k => Proxy (p :: TyFun Nat Type -> Type) The motive -> (a -> p @@ 0) Function to apply to the elements on the leafs -> (forall l. SNat l -> (p @@ l) -> (p @@ l) -> p @@ (l + 1)) Function to fold the branches with.NB: SNat l is the depth of the two sub-branches. -> RTree k a Tree to fold over. -> p @@ k

A dependently typed fold over trees.

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 tfold, because it gives a nice (log2(n)) tree-structure of adders:

populationCount :: (KnownNat (2^d), KnownNat d, KnownNat (2^d+1))
=> BitVector (2^d) -> Index (2^d+1)
populationCount = tfold (resize . bv2i . pack) (+) . v2t . bv2v


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

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


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 adds: >>> :{ let populationCount' :: (KnownNat (2^d), KnownNat d, KnownNat (2^d+1)) => BitVector (2^d) -> Index (2^d+1) populationCount' = tfold (resize . bv2i . pack) add . v2t . bv2v :} BLANKLINE interactive:... • Couldn't match type ‘(((2 ^ d) + 1) + ((2 ^ d) + 1)) - 1’ with ‘(2 ^ d) + 1’ Expected type: Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1) Actual type: Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1) -> AResult (Index ((2 ^ d) + 1)) (Index ((2 ^ d) + 1)) • In the second argument of ‘tfold’, namely ‘add’ In the first argument of ‘(.)’, namely ‘tfold (resize . bv2i . pack) add’ In the expression: tfold (resize . bv2i . pack) add . v2t . bv2v • Relevant bindings include populationCount' :: BitVector (2 ^ d) -> Index ((2 ^ d) + 1) (bound at ...)

because tfold expects a function of type "b -> b -> b", 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

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

populationCount' :: (KnownNat k, KnownNat (2^k))
=> BitVector (2^k) -> Index ((2^k)+1)
populationCount' bv = tdfold (Proxy @IIndex)
(resize . bv2i . pack)
(\_ x y -> add x y)
(v2t (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


## Prefix sums (scans)

Scans (scanl, scanr) are similar to folds (foldl, foldr) but return a list of successive reduced values. When the binary reduction operator f is associative, the scan functions in this module can be characterized as follows:

tscanl f [x1, x2, x3, ...] == [x1, x1 f x2, x1 f x2 f x3, ...]
tscanr f [..., xn2, xn1, xn] == [..., xn2 f xn1 f xn, xn1 f xn, xn]

The scan functions in this module provide a different trade-off between circuit size and logic depth than the default scanl and scanr functions. When $$n$$ is the number of elements, circuit size is $$\mathcal{O}(n \cdot \log n)$$, but logic depth is $$\mathcal{O}(\log n)$$. This means the resource usage will likely increase, but the maximum clock frequency also increases due to the reduced logic depth. The exact amount of instantiations of f given a tree of depth d is:

work 0 = 0
work d = 2 ^ (d - 1) + 2 * work (d - 1)

Arguments

 :: KnownNat n => (a -> a -> a) Must be associative -> Vec (2 ^ n) a -> Vec (2 ^ n) a

tscanl applied to Vec

>>> scanlPar (+) (1 :> 2 :> 3 :> 4 :> Nil)
1 :> 3 :> 6 :> 10 :> Nil


Arguments

 :: forall a n. KnownNat n => (a -> a -> a) Must be associative -> RTree n a -> RTree n a

Low-depth left scan

tscanl is similar to foldl, but returns a tree of successive reduced values from the left:

tscanl f [x1, x2, x3, ...] == [x1, x1 f x2, x1 f x2 f x3, ...]
>>> tscanl (+) (v2t (1 :> 2 :> 3 :> 4 :> Nil))
<<1,3>,<6,10>>


Arguments

 :: KnownNat n => (a -> a -> a) Must be associative -> Vec (2 ^ n) a -> Vec (2 ^ n) a

tscanr applied to Vec

>>> scanrPar (+) (1 :> 2 :> 3 :> 4 :> Nil)
10 :> 9 :> 7 :> 4 :> Nil


tscanr :: forall a n. KnownNat n => (a -> a -> a) -> RTree n a -> RTree n a Source #

Low-depth right scan

tscanr is similar to foldr, but returns a tree of successive reduced values from the left:

tscanr f [..., xn2, xn1, xn] == [..., xn2 f xn1 f xn, xn1 f xn, xn]
>>> tscanr (+) (v2t (1 :> 2 :> 3 :> 4 :> Nil))
<<10,9>,<7,4>>


# Conversions

v2t :: forall d a. KnownNat d => Vec (2 ^ d) a -> RTree d a Source #

Convert a vector with 2^d elements to a tree of depth d.

>>> v2t (1 :> 2 :> 3 :> 4:> Nil)
<<1,2>,<3,4>>


t2v :: forall d a. KnownNat d => RTree d a -> Vec (2 ^ d) a Source #

Convert a tree of depth d to a vector of 2^d elements

>>> (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4)))
<<1,2>,<3,4>>
>>> t2v (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4)))
1 :> 2 :> 3 :> 4 :> Nil


# Misc

lazyT :: KnownNat d => RTree d a -> RTree d a Source #

Given a function f that is strict in its nth RTree argument, make it lazy by applying lazyT to this argument:

f x0 x1 .. (lazyT xn) .. xn_plus_k