Add Safe vector indexing

clash-lang / clash-prelude

CLaSH prelude library containing datatypes and functions for circuit design

http://www.clash-lang.org/

Other

31 stars 27 forks source link

Add Safe vector indexing #17

Open Ericson2314 opened 9 years ago

Ericson2314 commented 9 years ago

Just as we have pow2 block ram, etc, it would be nice if we had safe pow2 vector indexing.

I was just refactoring one of my processors to change the word size, and some bugs got caught with my tests instead of the type checker because I was using !!.

Maybe something like

(!!!) :: Integral i
      => KnownNat (2 ^ BitSize i)
      => Vec (2 ^ BitSize i) a
      -> i -> a
(!!!) = (CL.!!)

should go in CLaSH.Sized.Vector?

Feel free to suggest a different identifier if you like the idea, of course.

christiaanb commented 9 years ago

Perhaps call it safeIndex? I mean... there are already: at (!) (!!)

I feel adding another indexing operator is going to make things more confusing, so I prefer a normal name.

Ericson2314 commented 9 years ago

Sure, that makes sense.

bgamari commented 8 years ago

What remains to be done on this?

christiaanb commented 8 years ago

Well, mostly we need to decide if we need more indexing operations than we already have for Vec: http://hackage.haskell.org/package/clash-prelude-0.10.10/docs/CLaSH-Sized-Vector.html#g:4, and then decide on a type signature.

As we currently have:

(!!) :: (KnownNat n, Enum i) => Vec n a -> i -> a
at :: SNat m -> Vec (m + (n + 1)) a -> a