scala - Scalaのexport_codeの醜い文字列エクスポートを修正

Question

私fooはそのstring型で機能する関数を持っています。export_code foo in Scala file -非常に醜いScalaコードを入手したとき。

このように見える非常に長いリストが作成されます

abstract sealed class nibble
final case class Nibble0() extends nibble
final case class Nibble1() extends nibble
final case class Nibble2() extends nibble
...

Answer 1

Code_CharIsabelle定義をデータ型として変換する代わりに、ターゲット言語でchar / stringの既存の実装を使用するようにコード生成に指示するには、理論をインポートする必要があります。

理論のインポート句に追加"~~/src/HOL/Library/Code_Char"すると、すべてが正常に機能するはずです。

また、これを確認することはできませんでしたが、これは常にインポート句の最後にある必要があると言われています。そうしないと、コードジェネレーターに面白いことが起こるからです。

乾杯、マヌエル