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_Char理论以告诉代码生成使用目标语言中现有的 char/string 实现，而不是将 Isabelle 定义翻译为数据类型。

添加"~~/src/HOL/Library/Code_Char"到您的理论的导入子句中，一切都应该正常工作。

另外，有人告诉我——但到目前为止还无法验证——这应该总是在你的 import 子句的末尾，否则，代码生成器会发生有趣的事情。

干杯，曼努埃尔