Copyright | (C) 2016 University of Twente 2022-2024 QBayLogic B.V. |
---|---|
License | BSD2 (see the file LICENSE) |
Maintainer | QBayLogic B.V. <devops@qbaylogic.com> |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
Clash.Sized.RTree
Description
Synopsis
- data RTree :: Nat -> Type -> Type where
- treplicate :: forall d a. SNat d -> a -> RTree d a
- trepeat :: KnownNat d => a -> RTree d a
- thead :: RTree n a -> a
- tlast :: RTree n a -> a
- indexTree :: (KnownNat d, Enum i) => RTree d a -> i -> a
- tindices :: forall d. KnownNat d => RTree d (Index (2 ^ d))
- replaceTree :: (KnownNat d, Enum i) => i -> a -> RTree d a -> RTree d a
- tmap :: forall d a b. KnownNat d => (a -> b) -> RTree d a -> RTree d b
- tzipWith :: forall a b c d. KnownNat d => (a -> b -> c) -> RTree d a -> RTree d b -> RTree d c
- tzip :: KnownNat d => RTree d a -> RTree d b -> RTree d (a, b)
- tunzip :: forall d a b. KnownNat d => RTree d (a, b) -> (RTree d a, RTree d b)
- tfold :: forall d a b. KnownNat d => (a -> b) -> (b -> b -> b) -> RTree d a -> b
- tdfold :: 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)) -> RTree k a -> p @@ k
- scanlPar :: KnownNat n => (a -> a -> a) -> Vec (2 ^ n) a -> Vec (2 ^ n) a
- tscanl :: forall a n. KnownNat n => (a -> a -> a) -> RTree n a -> RTree n a
- scanrPar :: KnownNat n => (a -> a -> a) -> Vec (2 ^ n) a -> Vec (2 ^ n) a
- tscanr :: forall a n. KnownNat n => (a -> a -> a) -> RTree n a -> RTree n a
- v2t :: forall d a. KnownNat d => Vec (2 ^ d) a -> RTree d a
- t2v :: forall d a. KnownNat d => RTree d a -> Vec (2 ^ d) a
- lazyT :: KnownNat d => RTree d a -> RTree d a
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.
Bundled Patterns
pattern LR :: a -> RTree 0 a | RLeaf of a perfect depth tree
Can be used as a pattern:
|
pattern BR :: RTree d a -> RTree d a -> RTree (d + 1) a | RBranch of a perfect depth tree
Case be used a pattern:
|
Instances
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 #
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: |
-> 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
add
s:
>>>
:{
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 :} <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 instanceApply
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 O(n⋅logn), but logic depth is O(logn).
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)
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