在export_code for Scala中修复丑陋的字符串导出

Question

我有一个在string类型上工作的函数foo。当我使用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理论，以便告诉代码生成使用目标语言中已有的字符/字符串实现，而不是将Isabelle定义转换为数据类型。

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

此外，我被告知-但到目前为止无法验证-这应该总是在您的导入子句的末尾，因为否则，有趣的事情会发生在代码生成器上。

干杯，曼纽尔