Using numeric bounds with `Vec` functions, going from `1 <= n => Vec n a` to `Vec (m + 1) a`

Clash Help
1

I’m writing an interconnect that selects which subordinate to route a request to. For that I want to select which one to use based on an address.

For that I have a vector that contains the (ascending) starting addresses of the components addresses :: Vec n (BitVector 32), to make selecting which component to route the request to I want to calculate a addressRange :: Vec n (BitVector 32, BitVector 32) that contains the lower and upper bound of every subordinate.

My idea was to use the start addresses, remove the first element and append maxBound at the end, then zip the start and end addresses together

Ideally I want to have code like this

addrRange :: forall a n . (Bounded a, 1 <= n) => Vec n a -> Vec n (a, a)
addrRange startAddrs = zip startAddrs bounds
  where
    bounds = tail startAddrs <<+ maxBound

For that I’m getting

    • Could not deduce: (n + 1) ~ n
      from the context: (Bounded a, 1 <= n)
        bound by the type signature for:
                   addrRange :: forall a (n :: Nat).
                                (Bounded a, 1 <= n) =>
                                Vec n a -> Vec n (a, a)
        at src/Protocols/MemoryMap.hs:244:1-72
      Expected: Vec (n + 1) a
        Actual: Vec n a

I have a workaround that uses bounds = replace maxBound maxBound $ rotateLeft startAddrs 1 (that doesn’t need a 1 <= n bound or have size n + 1), but I wonder how I could make it work with tail

2

Huh <<+ already does exactly what I want for bounded, I didn’t read the description properly and thought it would append :woozy_face:

If I still wanted to do this manually I could use leToPlus like this

where
    bounds = leToPlus @1 @n $ tail startAddrs ++ singleton maxBound
2 Likes
3

You were thinking of :<, which can be used to append a single element to the end of a vector.
Which could simplify your manual example to

where
    bounds = leToPlus @1 @n $ tail startAddrs :< maxBound

But indeed <<+ does it all for you, adding an element on the end and dropping one from the start.
And its mirror image +>> also exists.

2 Likes