How can I specify a header and the package of generated code?

Question

I'm generating Scala code with Isabelle. How can I specify a header for my Scala file? For example, I'd like to have something like this:

// Generated code. Generated with Isabelle/HOL
// File: blubb.thy line:1234
// Date: Wed, 27.03.2013
// exported code equations: bla blub blob ...

How can I specify the package to use? For example, to use the package GENERATED, the file should begin with the words package GENERATED.

The best idea I got so far is the code_include command with an empty second parameter (""). If I choose a longer second parameter, the Efficient_Nat theory first emits its code. But I must write to the beginning of the file.

code_include Scala ""
{*package GENERATED

// Code generated by Isabelle
*}

How evil is this solution? If it is not that evil, how can I add things like the current date, the current thy file, and the line in which the export_code happens. Can I also add the code equations I exported but not their decencies?

Andreas Lochbihler Andreas Lochbihler · Accepted Answer · 2013-03-28T07:43:58

code_include is the right thing for what you want. The second parameter identifies the includes and determines the order in which the code generator outputs different code_includes. As you have picked the empty identifier "", your text will always come first, but you cannot have multiple code_includes with the same identifier (the latter overwrites the former).

The text that you give to code_include inside {* and *} is not interpreted, so you cannot have dynamic parts there. However, if you use the ML interface of the code generator, you can generate the string just before invoking export_code. This might look as follows:

ML {*
val scala_header =
  let
    val package = "package GENERATED";   
    val date = Date.toString (Date.fromTimeLocal (Time.now ()))
    val header = package ^ "\n\n" ^ "// Generated by Isabelle on " ^ date ^ "\n"
  in
    Code_Target.add_include "Scala" ("", SOME (header, []))
  end
*}

Now, you just have to call scala_header before export_code:

setup {* scala_header *}
export_code ... in Scala file ...

This gives you roughly the correct generation date. In detail, the time will be the one when setup {* scala_header *} executes, which can be (due to multithreading) some time before export_code actually executes. Even in sequential mode, when you generate lots of code or do much preprocessing of the code equations, the gap may be several minutes.

How can I specify a header and the package of generated code?

1 Answers