RFC: Array.usize

[fgdorais]

Proposal

I propose to add Array.usize to get the USize size of an array, without going through Nat.

Currently, to get the USize of an array, one needs to use Array.size and then Nat.toUSize. The latter takes the return value of Array.size and calculates the remainder modulo USize.size. This is not optimal since arrays are stored in memory and therefore cannot exceed USize.size. This proposal would bypass the remainder step and return the correct array size as an USize scalar (which is trivial to access in the current array implementation).

Other array operations have optimizations that bypass this trivial size check for the sake of nearly matching C-language performance. Some of my code at UnicodeBasic and elsewhere could benefit a lot from this nearly trivial improvement to the array API.

The drawback is that this adds one more unsafe implementation. So this request needs some careful consideration.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[Kha]

This proposal would bypass the remainder step

Surely this step is optimized out by LLVM anyway?

[fgdorais]

Of course, no actual division is done but it's not quite optimized out. The issue is that the m_size component of a lean_array_object cannot be larger than LEAN_MAX_SMALL_NAT but LLVM doesn't know that which leads to overly complex code. On the small branch, the only one actually used, LLVM does optimize the box/unbox to an (unnecessary!) and to clear the top bit. Anyway, the end result much more complex than what should simply return the m_size component of the array.