Hi Florian and Lukas, Am 04.05.2013 um 09:07 schrieb Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de> > I am curious to to see the already existing and emerging changes. Maybe > there are already some things to point out then. The attached small patch is used in our setting: - every target language has so-called "interface" functions, which are the ones to be exported (i.e. with a "public" modifier) by the target language.
So instead of >> export_code List.sublists in Scala you would have to write something like code_interfaces Scala "List.sublists" export_code List.sublists in Scala There are several shortcomings that should be addressed for applications in more general settings: - the serializer should check wether the "interface" functions are actually used in the module - usually, one probably wants the functions that are exported to be the ones that were declared in the export_code statement For conceptual advances, there has also been the idea of providing a slot for "pragmas" for serializers: One use-case is the need to add pragmas for the target language in the generated code, but they could also be used to advise a serializer to export only specific constants -- and these pragmas could be generated e.g. by the export_code statement. Cheers, Fabian
interfaces
Description: Binary data
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
