如何指定头文件和生成的代码包

Question

我正在与Isabelle生成Scala代码。我如何为我的Scala文件指定一个头?例如，我希望有这样的内容:

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

如何指定要使用的包?例如，要使用包GENERATED，文件应该以单词package GENERATED开头。

---

到目前为止，我得到的最好的想法是code_include命令与一个空的第二个参数("")。如果我选择一个更长的第二个参数，Efficient_Nat理论首先发出它的代码。但是我必须写到文件的开头。

code_include Scala ""
{*package GENERATED
// Code generated by Isabelle
*}

这个解决方案有多邪恶?如果它不是那么邪恶，我如何添加诸如当前日期，当前文件和export_code发生的行之类的东西。我也可以添加我导出的代码方程，但不是他们的礼仪?

Answer 1

code_include是你想要的。第二个参数标识包含并确定代码生成器输出不同code_include的顺序。由于您选择了空标识符""，您的文本将始终放在第一位，但是您不能有多个具有相同标识符的code_include(后者覆盖前者)。

在{*和*}中给code_include的文本不被解释，所以你不能在那里有动态部分。但是，如果使用代码生成器的ML接口，则可以在调用export_code之前生成字符串。可能如下所示:

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

现在，你只需要在export_code之前调用scala_header:

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

这给出了大致正确的生成日期。详细地说，这个时间将是setup {* scala_header *}执行的时间，这可能是export_code实际执行之前的一段时间(由于多线程)。即使在顺序模式下，当您生成大量代码或对代码方程进行大量预处理时，间隔也可能是几分钟。