[isabelle-dev] NEWS: generated code as proper theory export

[Florian Haftmann]

>> Maybe the »checking« should just be a variant of the regular export.
>>
>> Hence the modification could be quite conservative:
>>
>> 	export_code CONSTS in LANGUAGE ( '(' OPTIONS ')' ) ( module_name NAME )
>> ( file … | ( prefix … ) ( checked ) )
>>
>> where »file« denotes a relative root in the file system and »checked«
>> indicated that the generated code will be checked implicitly.
> 
> I have looked around at typical uses of 'export_code' in AFP. Most of
> the time it is just informative: writing a file and looking at it in the
> editor (or via the command-line!?), or doing that on the output channel.
> The isabelle-export: file-system covers that already, i.e. we should be
> able to eliminate almost all generated files from the AFP repository.
> 
> So "export_code .. file" should just disappear -- it is semantically
> illtyped in PIDE: editing the "file" argument will leave a trace of
> machine oil spilled to the physical file-system.
> 
> 
> We do need an explicit prefix and an internal check for duplicates, e.g.
> as in the command 'generated_file'.
> 
> That should be really just a prefix for the exported artifact, not the
> name itself: each language processor should be smart enough to derive
> file or directory names from it as required.  Thus the prefix locally
> belongs in front of the arguments.
> 
> Here is an example from AFP/160ac13cdc05
> SATSolverVerification/SatSolverCode.thy:
> 
>   export_code solve
>     in OCaml file "code/solve.ML"
>     in SML file "code/solve.ocaml
>     in Haskell file "code/"
> 
> It could be turned into something like this:
> 
>   export_code "code/" = solve in OCaml SML Haskell
> 
> Some details about the automatic name derivation scheme still need to be
> sorted out -- or 'file' remains as an option to specify the suffix for
> effective name (without writing anything to the file-system).

Some further round of thinking.  Indeed, naming files is a little bit
delicate since there are two classes of target languages here: Haskell
with its strict one module – one file approach and ML where source code
is conceptually just a stream.  Hence in the current implementation the
exact interpretation of the »file« argument is up to the target language.

To make this more fitting, at the moment I am thinking about something like

> export_code [ ( NAME | PREFIX._ ) = ] CONSTS in LANGUAGE [ '(' OPTIONS ')' ] [ file_prefix PATH ] [ checked ] 

* »checked« is just an aside to regular code generation, no distinctive
variant

* A mere prefix for the relative location can be given after »file_prefix«.

* Language-specific options remain as they are.

* The module naming schema gets more sophisticated: default, name or
prefix.  The key point is that this naming schema is again
target-language specific.

  For ML:
           code                                           file name
  default  multiple structures                            theory name
  name     one structure NAME                             NAME
  prefix   one structure PREFIX with multiple structures  PREFIX

  For Haskell:
           code                                    file name
  default  multiple modules                        module name
  name     one module NAME                         NAME
  prefix   multiple modules beneath PREFIX         PREFIX module name

This should cover all application cases.

It will take further rounds of refinement to actually get there.

At the moment I am still in favour of a diagnostic command to emit sth
ad-hoc into the file system -- but this could be something separate from
export_code and maybe just use $ISABELLE_TMP_PREFIX/… as destination.

Just an aside: with the current tool support in Isabelle/jEdit I
consider the auxiliary construct »file ‹›« obsolete – the regular
exports are just two clicks away.

Cheers,
	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190202/af8f0d27/attachment.sig>