Re: [isabelle] Word32/64 ?



Hi Peter,

> 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" ?

there is, as far as I remember, a default setup for code generation for
type 'a word, but no mapping to any target-language-specific types.  If
this is desired, it would be required to wrap up type expressions like
e.g. "64 word" into a dedicated type, say, "word64", to have dedicated
types for all the different 'a word instances.  This wrapping is simple
but cumbersome to do.

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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