The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 24/03/2014 07:10, Moshe Tenenbaum wrote:
> Gabriel and Enrico, thank you very much for your responses! Good step
> forward for me.
>
> My next question regards if there is any possible way to go a bit
> further with the code. FOr example, in the coq_interp.c code you
> mention, on line 1300, there is an instruction that looks like this:
>
> Instruct (TAIL0INT31) {
>      int r = 0;
>          uint32 x;
>          print_instr("TAIL0INT31");
>      x = (((uint32) accu >> 1) | 0x80000000);
>          if (!(x & 0xFFFF)) { x >>= 16; r += 16; }
>          if (!(x & 0x00FF)) { x >>= 8;  r += 8; }
>          if (!(x & 0x000F)) { x >>= 4;  r += 4; }
>          if (!(x & 0x0003)) { x >>= 2;  r += 2; }
>          if (!(x & 0x0001)) { x >>=1;   r += 1; }
>          if (!(x & 0x0001)) {           r += 1; }
>          accu = value_of_uint32(r);
>          Next;
>        }
>
> Can this be transformed using mnemonics like uint64 instead of uint32?

Sure, you can declare x of static type uint64. But presumably, any 
optimizing compiler is already doing this transformation behind the 
scenes when it is beneficial for performances.

You can even go further with mnemonics and substitute all of this code 
with __builtin_ctz(x) (assuming this construct is portable enough) and 
let the compiler do its black magic. That said, I doubt that it would 
bring any noticeable speed-up.

(By the way, I am noticing that the last test is pointless, since it 
always evaluates to false.)

> And can it be extended for TAIL0INT63 for proper memory allocation?

No, it can't. Keep in mind that this is just the tiny C part of a huge 
Coq development about 31-bit integers. If you change the width of 
integers there, you will have to modify some Coq theories in depth and 
deal with the fallout of breaking user formalizations.

I am not saying it is a bad idea. In fact, I whole-heartedly support 
switching Coq native integer from 31 bits to 63 bits in the long run. I 
am just saying that this is a much more massive endeavor than the code 
might suggest.

Best regards,

Guillaume