Re: [isabelle] Code Generation for Records



Hi Tjark,

> I noticed that the (SML/OCaml) code generator translates Isabelle/HOL
> record types into tuple-based data types.  This works reasonably well
> (and is understandable, given the internal representation of records in
> Isabelle/HOL).  Still, it would be nicer if the code generator instead
> used SML/OCaml records where possible.  There is no easy way to achieve
> this, is there?

you are touching a couple of issues here.

The deeper reason why there is no record-specific support in the code
generator is that, given HOL, SML, OCaml, Haskell, the concept of
records is very different, prohibiting a faithful translation except on
the foundational level (I still hope to come up with a better naming
scheme which makes the internal record identifiers less cryptic,
though).  Maybe for SML in there is a quick-and-dirty solution using
code_type and code_const.

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.