在导出代码中为Scala修复丑陋的字符串导出

我有一个功能foo，它可以在string类型上工作。当我export_code foo in Scala file -我得到一个非常丑陋的Scala代码。在导出代码中为Scala修复丑陋的字符串导出

一个很长的列表，看起来像这样创建

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

来源

2013-03-07 corny

伊莎贝尔/ HOL？！？哇。 – 2013-03-07 16:13:19

Isabelle拥有多种语言的代码生成功能，包括Scala和Haskell – 2013-03-07 21:32:41

你需要导入Code_Char理论，以告诉代码生成使用字符/字符串的现有实现在目标语言，而不是将Isabelle定义翻译为数据类型。

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

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

干杯，曼努埃尔·斯卡拉

来源

2013-03-07 12:31:01

在导出代码中为Scala修复丑陋的字符串导出

回答

相关问题