A lot of performance critical CakeML code is doing simple calculations with array indices, which are currently compiled to general-purpose integer operations. Such integer operations need to deal with tests for bignums and conditional jumps to the bignum library.
This issue is about implementing unsafe arithmetic (operations +, -, ... and comparisons <, =, ...) with witnesses that guarantee the integers are smallnums. The idea can be explained with an example: instead of doing
App (Arith Add IntT) [arg1; arg2]
we do:
App (UnsafeIndexArith Add) [arg1; arg2; witness]
where the semantics is the following:
- get integers
i1 and i2 from arg1 and arg2
- read length
len of vector / array / byte array or even list from witness
- perform the arithmetic operation (in this case
Add) on i1 and i2
- check that all numbers involved (
i1 and i2 and i1 + i2) satisfy -256 * len ≤ ... ≤ 256 * len, if not then type error
The cool thing is that operations such as Add then compile to a single (add) instruction.
This can be seen as a manual version of #367
A lot of performance critical CakeML code is doing simple calculations with array indices, which are currently compiled to general-purpose integer operations. Such integer operations need to deal with tests for bignums and conditional jumps to the bignum library.
This issue is about implementing unsafe arithmetic (operations
+,-, ... and comparisons<,=, ...) with witnesses that guarantee the integers are smallnums. The idea can be explained with an example: instead of doingwe do:
where the semantics is the following:
i1andi2fromarg1andarg2lenof vector / array / byte array or even list fromwitnessAdd) oni1andi2i1andi2andi1 + i2) satisfy-256 * len ≤ ... ≤ 256 * len, if not then type errorThe cool thing is that operations such as
Addthen compile to a single (add) instruction.This can be seen as a manual version of #367