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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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