1

我正在用 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发生的行之类的东西。我还可以添加我导出的代码方程式但不添加它们的体面吗？

4

1 回答 1

3

code_include是你想要的正确的东西。第二个参数标识包含并确定代码生成器输出不同code_includes 的顺序。当您选择了空标识符""时，您的文本将始终排在第一位，但您不能有多个code_include具有相同标识符的 s（后者会覆盖前者）。

你给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 ^ "\n\n" ^ "// Generated by Isabelle on " ^ date ^ "\n"
  in
    Code_Target.add_include "Scala" ("", SOME (header, []))
  end
*}

现在，您只需要在scala_header之前调用export_code：

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

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

于 2013-03-28T07:43:58.653 回答