Noteble slowdown of AFP/Native_Word

[Florian Haftmann]

> There is a notable slowdown AFP/Native_Word:
> 
> Isabelle/e4207dfa36b5 AFP/16cb1cb993ae
> Finished HOL (0:01:46 elapsed time, 0:05:36 cpu time, factor 3.16)
> Finished Word_Lib (0:00:26 elapsed time, 0:01:37 cpu time, factor 3.70)
> Finished Native_Word (0:01:36 elapsed time, 0:01:23 cpu time, factor 0.86)
> 
> Isabelle/3704717ed7bf AFP/ccc0b8182357
> Finished HOL (0:01:47 elapsed time, 0:05:41 cpu time, factor 3.17)
> Finished Word_Lib (0:00:25 elapsed time, 0:01:36 cpu time, factor 3.81)
> Finished Native_Word (0:03:27 elapsed time, 0:03:16 cpu time, factor 0.94)
> 
> 
> In the above changeset intervals, I see many changes on words and code 
> generation setup by Florian Haftmann, both in Isabelle and AFP.
> 
> He needs to say if the effect on Native_Word is to be expected, or if 
> this a problem that has been overlooked.

This decay stems from calls to code_simp.

The deviation comes from the code equations for int_of_integer: in the 
previous situations, there was a compromise in the code setup which used 
a variant of int_of_integer to speed up execution of code_simp in trade 
for that the code setup would not be executable stand-alone in a plain 
target language built would need additional modifications of the code setup.

The equations in question are
   ‹int_of_integer 0 = 0›
   ‹int_of_integer (Code_Numeral.Pos n) = Int.Pos n›
   ‹int_of_integer (Code_Numeral.Neg n) = Int.Neg n›
   ‹int_of_integer k = …› (*)
where for real target languages only the last one is used (*), where the 
conversion happens by explicit binary cuts, which is fine for an unknown 
representation, but does not compute that well in the logic.
The first three equations are fine for abstract representations (Pure, 
NBE). For NBE there is no decay, so it seems to work as intended there.

But for some unknown reason, the simplifier prefers the last equation, 
as can be seen in HOL-Main:
	
declare int_of_integer_code_nbe [code nbe]
declare int_of_integer_code [code]
declare [[code_simp_trace]]

lemma
   ‹P (int_of_integer (Code_Numeral.Pos Num.One))›
   apply code_simp

Can anybody familiar with the simplifier explain what is going on?

Bzw. the timing panel in Isabelle/jEdit is an excellent tool to pin down 
such things.

Cheers,
	Florian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 22777 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250731/c700e212/attachment-0001.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250731/c700e212/attachment-0001.sig>