Problem with polyml-e266a93fe8fe and Generate_Target_Bit_Operations

[Florian Haftmann]

> I have tested a recent repository version of Poly/ML https://github.com/ 
> polyml/polyml/commit/e266a93fe8fe with current Isabelle/9e5f645d6000.
> 
> This causes a problem in line 83 of theory 
> "Codegenerator_Test.Generate_Target_Bit_Operations.thy":
> 
> *** Evaluation for PolyML failed:
> *** exception Fail raised (line 5): Bad max
> 
> Looking only superficially, I don't quite understand what is the 
> intention of the test.
> 
> Note that there have been recent changes in Poly/ML on word arithmetic.

The explanation for this test can be found (admittedly, very indirect 
and implicit) at

https://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Code_Numeral.thy#l1014

reading

val max_index = pow (fromInt 2, Int.- (Word.wordSize, 3)) - fromInt 1; 
(*experimentally determined*)

This is the maximum value usable as index in bit shifts.

The check in Generate_Target_Bit_Operations.thy then asserts that this 
is really the maximum.

I am uncertain where to proceed from here. If this max_index is no 
longer unique across different ML versions, it is maybe best to drop the 
line

https://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy#l76

Ie. just assert that the index is small enough.

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/20250415/963aaa38/attachment.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/20250415/963aaa38/attachment.sig>