clash-prelude-1.8.4: Clash: a functional hardware description language - Prelude library

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

Contents

- `RTree` data type
- Construction
- Accessors
  - Indexing
- Modifying trees
- Element-wise operations
  - Mapping
  - Zipping
  - Unzipping
- Folding
  - Specialised folds
  - Prefix sums (scans)
- Conversions
- Misc
- Internal

Description

Synopsis

- data RTree (a :: Nat) b where
  - RLeaf :: forall b. b -> RTree 0 b
  - RBranch :: forall (d :: Natural) b. RTree d b -> RTree d b -> RTree (d + 1) b
  - pattern LR :: a -> RTree 0 a
  - pattern BR :: RTree d a -> RTree d a -> RTree (d + 1) a
- treplicate :: forall (d :: Nat) a. SNat d -> a -> RTree d a
- trepeat :: forall (d :: Nat) a. KnownNat d => a -> RTree d a
- thead :: forall (n :: Nat) a. RTree n a -> a
- tlast :: forall (n :: Nat) a. RTree n a -> a
- indexTree :: forall (d :: Nat) i a. (KnownNat d, Enum i) => RTree d a -> i -> a
- tindices :: forall (d :: Nat). KnownNat d => RTree d (Index (2 ^ d))
- replaceTree :: forall (d :: Nat) i a. (KnownNat d, Enum i) => i -> a -> RTree d a -> RTree d a
- tmap :: forall (d :: Nat) a b. KnownNat d => (a -> b) -> RTree d a -> RTree d b
- tzipWith :: forall a b c (d :: Nat). KnownNat d => (a -> b -> c) -> RTree d a -> RTree d b -> RTree d c
- tzip :: forall (d :: Nat) a b. KnownNat d => RTree d a -> RTree d b -> RTree d (a, b)
- tunzip :: forall (d :: Nat) a b. KnownNat d => RTree d (a, b) -> (RTree d a, RTree d b)
- tfold :: forall (d :: Nat) a b. KnownNat d => (a -> b) -> (b -> b -> b) -> RTree d a -> b
- tdfold :: forall (p :: TyFun Nat Type -> Type) (k :: Nat) a. KnownNat k => Proxy p -> (a -> p @@ 0) -> (forall (l :: Nat). SNat l -> (p @@ l) -> (p @@ l) -> p @@ (l + 1)) -> RTree k a -> p @@ k
- scanlPar :: forall (n :: Nat) a. KnownNat n => (a -> a -> a) -> Vec (2 ^ n) a -> Vec (2 ^ n) a
- tscanl :: forall a (n :: Nat). KnownNat n => (a -> a -> a) -> RTree n a -> RTree n a
- scanrPar :: forall (n :: Nat) a. KnownNat n => (a -> a -> a) -> Vec (2 ^ n) a -> Vec (2 ^ n) a
- tscanr :: forall a (n :: Nat). KnownNat n => (a -> a -> a) -> RTree n a -> RTree n a
- v2t :: forall (d :: Nat) a. KnownNat d => Vec (2 ^ d) a -> RTree d a
- t2v :: forall (d :: Nat) a. KnownNat d => RTree d a -> Vec (2 ^ d) a
- lazyT :: forall (d :: Nat) a. KnownNat d => RTree d a -> RTree d a
- textract :: RTree 0 a -> a
- tsplit :: forall (d :: Natural) a. RTree (d + 1) a -> (RTree d a, RTree d a)

# `RTree` data type

data RTree (a :: Nat) b 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 :: forall b. b -> RTree 0 b |
RBranch :: forall (d :: Natural) b. RTree d b -> RTree d b -> RTree (d + 1) b |

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 details Defined in Clash.Sized.RTree Methods lift :: Quote m => RTree d a -> m Exp Source # liftTyped :: forall (m :: Type -> Type). Quote m => RTree d a -> Code m (RTree d a) Source #
KnownNat d => Applicative (RTree d) Source # |
Instance details Defined in Clash.Sized.RTree Methods pure :: a -> RTree d a Source # (<*>) :: RTree d (a -> b) -> RTree d a -> RTree d b Source # liftA2 :: (a -> b -> c) -> RTree d a -> RTree d b -> RTree d c Source # (*>) :: RTree d a -> RTree d b -> RTree d b Source # (<*) :: RTree d a -> RTree d b -> RTree d a Source #
KnownNat d => Functor (RTree d) Source # |
Instance details Defined in Clash.Sized.RTree Methods fmap :: (a -> b) -> RTree d a -> RTree d b Source # (<$) :: a -> RTree d b -> RTree d a Source #
KnownNat d => Foldable (RTree d) Source # |

Instance details

Defined in Clash.Sized.RTree

Methods

fold :: Monoid m => RTree d m -> m Source #

foldMap :: Monoid m => (a -> m) -> RTree d a -> m Source #

foldMap' :: Monoid m => (a -> m) -> RTree d a -> m Source #

foldr :: (a -> b -> b) -> b -> RTree d a -> b Source #

foldr' :: (a -> b -> b) -> b -> RTree d a -> b Source #

foldl :: (b -> a -> b) -> b -> RTree d a -> b Source #

foldl' :: (b -> a -> b) -> b -> RTree d a -> b Source #

foldr1 :: (a -> a -> a) -> RTree d a -> a Source #

foldl1 :: (a -> a -> a) -> RTree d a -> a Source #

toList :: RTree d a -> [a] Source #

null :: RTree d a -> Bool Source #

length :: RTree d a -> Int Source #

elem :: Eq a => a -> RTree d a -> Bool Source #

maximum :: Ord a => RTree d a -> a Source #

minimum :: Ord a => RTree d a -> a Source #

sum :: Num a => RTree d a -> a Source #

product :: Num a => RTree d a -> a Source #

KnownNat d => Traversable (RTree d) Source # |
Instance details Defined in Clash.Sized.RTree Methods traverse :: Applicative f => (a -> f b) -> RTree d a -> f (RTree d b) Source # sequenceA :: Applicative f => RTree d (f a) -> f (RTree d a) Source # mapM :: Monad m => (a -> m b) -> RTree d a -> m (RTree d b) Source # sequence :: Monad m => RTree d (m a) -> m (RTree d a) Source #
(KnownNat d, Arbitrary a) => Arbitrary (RTree d a) Source # |
Instance details Defined in Clash.Sized.RTree Methods arbitrary :: Gen (RTree d a) Source # shrink :: RTree d a -> [RTree d a] Source #
(KnownNat d, CoArbitrary a) => CoArbitrary (RTree d a) Source # |
Instance details Defined in Clash.Sized.RTree Methods coarbitrary :: RTree d a -> Gen b -> Gen b Source #
(KnownNat d, AutoReg a) => AutoReg (RTree d a) Source # |
Instance details Defined in Clash.Class.AutoReg.Internal Methods autoReg :: 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 #
(KnownNat d, BitPack a) => BitPack (RTree d a) Source # |

Instance details

Defined in Clash.Sized.RTree

Associated Types

type BitSize (RTree d a) |
Instance details Defined in Clash.Sized.RTree type BitSize (RTree d a) = (2 ^ d) * BitSize a

Methods

pack :: 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 details Defined in Clash.Signal.Bundle Methods bundle :: 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 details Defined in Clash.Signal.Delayed.Bundle Methods bundle :: 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, NFDataX a) => NFDataX (RTree d a) Source # |
Instance details Defined in Clash.Sized.RTree Methods deepErrorX :: 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 details Defined in Clash.Sized.RTree Methods showsPrecX :: Int -> RTree n a -> ShowS Source # showX :: RTree n a -> String Source # showListX :: [RTree n a] -> ShowS Source #
(KnownNat d, Default a) => Default (RTree d a) Source # |
Instance details Defined in Clash.Sized.RTree Methods def :: RTree d a #
NFData a => NFData (RTree d a) Source # |
Instance details Defined in Clash.Sized.RTree Methods rnf :: RTree d a -> () Source #
Show a => Show (RTree n a) Source # |
Instance details Defined in Clash.Sized.RTree Methods showsPrec :: Int -> RTree n a -> ShowS Source # show :: RTree n a -> String Source # showList :: [RTree n a] -> ShowS Source #
(KnownNat d, Eq a) => Eq (RTree d a) Source # |
Instance details Defined in Clash.Sized.RTree Methods (==) :: RTree d a -> RTree d a -> Bool Source # (/=) :: RTree d a -> RTree d a -> Bool Source #
(KnownNat d, Ord a) => Ord (RTree d a) Source # |

Instance details

Defined in Clash.Sized.RTree

Methods

compare :: RTree d a -> RTree d a -> Ordering Source #

(<) :: RTree d a -> RTree d a -> Bool Source #

(<=) :: RTree d a -> RTree d a -> Bool Source #

(>) :: RTree d a -> RTree d a -> Bool Source #

(>=) :: RTree d a -> RTree d a -> Bool Source #

max :: RTree d a -> RTree d a -> RTree d a Source #

min :: RTree d a -> RTree d a -> RTree d a Source #

KnownNat d => Ixed (RTree d a) Source # |
Instance details Defined in Clash.Sized.RTree Methods ix :: Index (RTree d a) -> Traversal' (RTree d a) (IxValue (RTree d a)) Source #
type Unbundled t delay (RTree d a) Source # |
Instance details Defined in Clash.Signal.Delayed.Bundle type Unbundled t delay (RTree d a) = RTree d (DSignal t delay a)
type TryDomain t (RTree d a) Source # |
Instance details Defined in Clash.Class.HasDomain.HasSingleDomain type TryDomain t (RTree d a) = TryDomain t a
type Unbundled t (RTree d a) Source # |
Instance details Defined in Clash.Signal.Bundle type Unbundled t (RTree d a) = RTree d (Signal t a)
type BitSize (RTree d a) Source # |
Instance details Defined in Clash.Sized.RTree type BitSize (RTree d a) = (2 ^ d) * BitSize a
type Index (RTree d a) Source # |
Instance details Defined in Clash.Sized.RTree type Index (RTree d a) = Int
type IxValue (RTree d a) Source # |
Instance details Defined in Clash.Sized.RTree type IxValue (RTree d a) = a

# Construction

treplicate :: forall (d :: Nat) 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 :: forall (d :: Nat) a. 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 :: forall (n :: Nat) a. 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 :: forall (n :: Nat) a. 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 :: forall (d :: Nat) i a. (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 :: Nat). 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 :: forall (d :: Nat) i a. (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 :: Nat) 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 :: Nat). 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 :: forall (d :: Nat) a b. 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 :: Nat) 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

tfold Source #

Arguments

:: forall (d :: Nat) 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 Source #

Arguments

:: forall (p :: TyFun Nat Type -> Type) (k :: Nat) a. KnownNat k |
=> Proxy p | The motive
-> (a -> p @@ 0) | Function to apply to the elements on the leafs
-> (forall (l :: Nat). 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 `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: Index ((2 ^ d) + 1)
                    -> Index ((2 ^ d) + 1) -> Index ((2 ^ d) + 1)
            Actual: 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 ...)

# 376 "srcClashSized/RTree.hs"

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)

scanlPar Source #

Arguments

:: forall (n :: Nat) a. 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

tscanl Source #

Arguments

:: forall a (n :: Nat). 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>>

scanrPar Source #

Arguments

:: forall (n :: Nat) a. 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 :: Nat). 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 :: Nat) 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 :: Nat) 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 :: forall (d :: Nat) a. 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

# Internal

textract :: RTree 0 a -> a Source #

tsplit :: forall (d :: Natural) a. RTree (d + 1) a -> (RTree d a, RTree d a) Source #