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_include2 番目のパラメーターが空のコマンド ( "") です。より長い 2 番目のパラメーターを選択すると、Efficient_Nat理論は最初にそのコードを発行します。ただし、ファイルの先頭に書き込む必要があります。

code_include Scala ""
{*package GENERATED

// Code generated by Isabelle
*}

この解決策はどれほど悪いですか？それほど悪くない場合、現在の日付、現在のあなたのファイル、および発生した行などをどのように追加できますexport_codeか。エクスポートしたコード方程式を追加することはできますが、それらの品位は追加できませんか?

4

1 に答える 1

3

code_includeあなたが望むもののための正しいことです。2 番目のパラメーターはインクルードを識別し、コード ジェネレーターが異なる を出力する順序を決定しますcode_include。空の identifier を選択したため""、テキストは常に最初に来ますが、同じ識別子を持つ複数の を使用することはできません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 ^ "\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 に答える