Switch forall to ranges/sets

[Timmmm]

There are a lot of type declarations using e.g. forall 'n, 0 < 'n <= 8 . that could be using the range(0, 8), and some that could be switched to the set notation {1, 2, 3}. This would be simpler and easier to read, and we can use type aliases, e.g. instead of

type regno ('n : Int), 0 <= 'n < 32 = atom('n)

val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits
function rX r = {

we can do

type regno = range(0, 31)

function rX(r : regno) -> xlenbits = {

which is much simpler and clearer (especially to people unfamiliar with fancy existential types, which is approximately everyone!).

[martinberger]

Agreed, range(...) is more readable.

[ShivangMishra]

@Timmmm @martinberger I want to work on this issue. I've found most such lines in this codebase using a couple of regex patterns. Now just need to replace them and raise a PR. Does this approach sound ok, or are we looking for some other advanced method ?

[martinberger]

@ShivangMishra If you can convince the type-checker to accept your changes, that would be a good start.

[Timmmm]

Note, not all instances of this can be replaced by range(). Any where the type variable appears more than once, or has some maths done to it (usually 8 * 'n) will have to stay as-is.

I searched for forall and from my brief skim it looks like we could change:

• Register access functions rX, wX, rF, wF
• is_aligned_addr - I'm not sure why this uses a type variable in the first place
• within_* in riscv_platform.sail
• pmpCheck
• Technically the memory write functions could use range() but the read functions can't (because they use 8 * ) and I think it makes sense to keep them symmetric.

I would maybe start with a PR that just the register access functions.

[jordancarlin]

@ShivangMishra Is this still something you're planning to work on? If not I would be interested in giving it a go.

[ShivangMishra]

@ShivangMishra Is this still something you're planning to work on? If not I would be interested in giving it a go.

Hi, yes I'm working on it... Will hopefully raise a PR this weekend.