代码之家 › 专栏 › 技术社区 › corny

如何指定生成代码的标头和包?

isabelle code-generation scala

1

corny · 技术社区 · 13 年前

我正在与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 发生。我还可以添加我导出的代码方程,但不能添加它们的小数吗?

1 回复 | 直到 13 年前

1

3

Andreas Lochbihler 13 年前

code_include 是你想要的合适的东西。第二个参数标识包含并确定代码生成器输出不同代码的顺序 代码_包含 s.由于您选择了空标识符 "" ,您的文本总是排在第一位,但不能有多个 代码_包含 s具有相同的标识符(后者覆盖前者)。

你给的文本 代码_包含 在…内 {* 和 *} 未被解释,因此不能在那里有动态部件。但是,如果使用代码生成器的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 之前 导出代码 :

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

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