Open fgdorais opened 4 days ago
This proposal would bypass the remainder step
Surely this step is optimized out by LLVM anyway?
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.
Proposal
I propose to add
Array.usize
to get theUSize
size of an array, without going throughNat
.Currently, to get the
USize
of an array, one needs to useArray.size
and thenNat.toUSize
. The latter takes the return value ofArray.size
and calculates the remainder moduloUSize.size
. This is not optimal since arrays are stored in memory and therefore cannot exceedUSize.size
. This proposal would bypass the remainder step and return the correct array size as anUSize
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 :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.