[isabelle-dev] Theories Code_*Int* in AFP entry Native_Word

[Andreas Lochbihler]

Hi Florian,

Thanks a lot for cleaning up all the things around bits, also in my AFP 
entries.

IIRC the int / integer bit operation material in Native_Word ended up in 
the entry because I needed them for implementing a symbolic execution 
strategy that works with the code generator setup in Native_Word. As 
such, the two setups were originally coupled fairly tightly. I do not 
know whether that's still the case, but I would suspect so as I haven't 
noticed any big changes in this direction. So from a maintenance 
perspective, it makes sense to me to keep them in the same place.

Best,
Andreas

Am 26.02.2022 um 20:36 schrieb Florian Haftmann:
> Hi Andreas,
> 
> after the substantial »disentangling« of bit operations and word types
> in the last Isabelle release, I went through the theories in Native_Word
> concerning code generation for int / integer to clarify the historically
> grown theory names following the naming convention of theories
> Code_*.thy from HOL-Library (hg id 700323b3c105).
> 
> The situation is still not 100% convincing since – despite the session
> name – those theories refer to bit operations on int / integer, not
> word, but I do not see an alternative which would be worth the effort,
> e. g. moving to the distribution or separating into a dedicated AFP
> entry Native_Bit or similar.
> 
> What could still be done is to eliminate some reminiscences e. g. to the
> now discontinued ancient signed numeral representation, but this will
> not be a game changer either.
> 
> But maybe you want to have a look at the current matter of affairs which
> to your eyes might suggest improvements.  No urgency.
> 
> Cheers,
> 	Florian
>