[isabelle-dev] Announcing Isabelle work: Access Modifiers for Scala Code Generator

[Fabian Immler]

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.

Cheers,
Fabian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: interfaces
Type: application/octet-stream
Size: 10970 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130507/3facab07/attachment-0002.obj>