Copyright | (C) 2016 University of Twente 2022 QBayLogic B.V. |
---|---|
License | BSD2 (see the file LICENSE) |
Maintainer | QBayLogic B.V. <devops@qbaylogic.com> |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
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.
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
:: 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
:: 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 \(\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)
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