Clash.Sized.RTree

RTree data type

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

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

Leaf 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

Branch 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

KnownNat d => Functor (RTree d)

Defined in Clash.Sized.RTree

Methods

fmap :: (a -> b) -> RTree d a -> RTree d b

(<$) :: a -> RTree d b -> RTree d a

KnownNat d => Applicative (RTree d)

Defined in Clash.Sized.RTree

Methods

pure :: 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)

Defined in Clash.Sized.RTree

Methods

fold :: 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)

Defined in Clash.Sized.RTree

Methods

traverse :: 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)

Defined 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)

Defined in Clash.Sized.RTree

Methods

compare :: 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)

Defined in Clash.Sized.RTree

Methods

showsPrec :: Int -> RTree n a -> ShowS

show :: RTree n a -> String

showList :: [RTree n a] -> ShowS

Lift a => Lift (RTree d a)

Defined in Clash.Sized.RTree

Methods

lift :: RTree d a -> Q Exp

(KnownNat d, Arbitrary a) => Arbitrary (RTree d a)

Defined in Clash.Sized.RTree

Methods

arbitrary :: Gen (RTree d a)

shrink :: RTree d a -> [RTree d a]

(KnownNat d, CoArbitrary a) => CoArbitrary (RTree d a)

Defined in Clash.Sized.RTree

Methods

coarbitrary :: RTree d a -> Gen b -> Gen b

(KnownNat d, Default a) => Default (RTree d a)

Defined in Clash.Sized.RTree

Methods

def :: RTree d a

NFData a => NFData (RTree d a)

Defined in Clash.Sized.RTree

Methods

rnf :: RTree d a -> ()

KnownNat d => Ixed (RTree d a)

Defined in Clash.Sized.RTree

Methods

ix :: Index (RTree d a) -> Traversal' (RTree d a) (IxValue (RTree d a))

(KnownNat d, Undefined a) => Undefined (RTree d a)

Defined in Clash.Sized.RTree

Methods

deepErrorX :: String -> RTree d a

rnfX :: RTree d a -> ()

ShowX a => ShowX (RTree n a)

Defined in Clash.Sized.RTree

Methods

showsPrecX :: Int -> RTree n a -> ShowS

showX :: RTree n a -> String

showListX :: [RTree n a] -> ShowS

(KnownNat d, KnownNat (BitSize a), BitPack a) => BitPack (RTree d a)

Defined in Clash.Sized.RTree

Associated Types

type BitSize (RTree d a) :: Nat

Methods

pack :: RTree d a -> BitVector (BitSize (RTree d a))

unpack :: BitVector (BitSize (RTree d a)) -> RTree d a

KnownNat d => Bundle (RTree d a)

Defined in Clash.Signal.Bundle

Associated Types

type Unbundled dom (RTree d a) = (res :: Type)

Methods

bundle :: forall (dom :: Domain). Unbundled dom (RTree d a) -> Signal dom (RTree d a)

unbundle :: forall (dom :: Domain). Signal dom (RTree d a) -> Unbundled dom (RTree d a)

KnownNat d => Bundle (RTree d a)

Defined in Clash.Signal.Delayed.Bundle

Associated Types

type Unbundled dom d (RTree d a) = (res :: Type)

Methods

bundle :: forall (dom :: Domain) (d0 :: Nat). Unbundled dom d0 (RTree d a) -> DSignal dom d0 (RTree d a)

unbundle :: forall (dom :: Domain) (d0 :: Nat). DSignal dom d0 (RTree d a) -> Unbundled dom d0 (RTree d a)

type Unbundled t delay (RTree d a)

Defined in Clash.Signal.Delayed.Bundle

type Unbundled t delay (RTree d a) = RTree d (DSignal t delay a)

type Unbundled t (RTree d a)

Defined in Clash.Signal.Bundle

type Unbundled t (RTree d a) = RTree d (Signal t a)

type TryDomain t (RTree d a)

Defined in Clash.Class.HasDomain.HasSingleDomain

type TryDomain t (RTree d a) = TryDomain t a

type Index (RTree d a)

Defined in Clash.Sized.RTree

type Index (RTree d a) = Int

type IxValue (RTree d a)

Defined in Clash.Sized.RTree

type IxValue (RTree d a) = a

type BitSize (RTree d a)

Defined in Clash.Sized.RTree

type BitSize (RTree d a) = (2 ^ d) * BitSize a

Construction

treplicate :: forall d a. SNat d -> a -> RTree d a

"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

"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

Indexing

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

"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))

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

"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

"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

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)

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)

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

Folding

tfold

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

tdfold

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 fromIntegral (+) . 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 addes:

>>> :{
let populationCount' :: (KnownNat (2^d), KnownNat d, KnownNat (2^d+1))
                     => BitVector (2^d) -> Index (2^d+1)
    populationCount' = tfold fromIntegral 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 fromIntegral add’
      In the expression: tfold fromIntegral 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.Prelude
import Data.Proxy

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

populationCount' :: (KnownNat k, KnownNat (2^k))
                 => BitVector (2^k) -> Index ((2^k)+1)
populationCount' bv = tdfold (Proxy @IIndex)
                             fromIntegral
                             (\_ 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

Conversions

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

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

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

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

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>

Misc

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

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