Re: [isabelle] Word32/64 ?


This topic is of interest to me. At the isabelle users workshop in Munich last year I had a long discussion with Florian about precisely this. The answer seemed to be "not with the current code generator", and his argument felt convincing enough for me to leave that approach alone.

One approach for high-performance code seems to be going in reverse, i.e. parsing annotated SML/C/Haskell/whatever into Isabelle, where you can pick your own translation, but have to pay by having to specify the semantics also.

That or trying to write your own code generator, which might be... interesting.


Rafal Kolanski.

Peter Lammich wrote:
Hi all,

Is there any code-generator setup to generate 32/(64) bit integers with modulo-arithmetic, mapped on the corresponding SML type (Word32) ? In the logic, the type Word.word has the intended behaviour, but how to get,e.g., "32 word", mapped to SML's "Word32" ?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.