Email Gateway (Aug 18 2022 at 15:23): Email Gateway (Aug 18 2022 at 15:23):From: Tjark Weber <webertj@in.tum.de>
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?
Tjark
Email Gateway (Aug 18 2022 at 15:24):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Tjark,
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
signature.asc
Last updated: Apr 25 2024 at 08:20 UTC