[isabelle-dev] Announcing Isabelle work: Access Modifiers for Scala Code Generator
immler at in.tum.de
Tue May 7 09:59:55 CEST 2013
Hi Florian and Lukas,
Am 04.05.2013 um 09:07 schrieb Florian Haftmann <florian.haftmann at 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 10970 bytes
Desc: not available
More information about the isabelle-dev