什么时候我应该使用Rosette的浅嵌入和深嵌入来进行程序综合？

Question

花环的一些教程介绍使用浅埋的程序综合，还有一些使用深埋。

在阅读了Torlak et Bodik的“成长中的解决方案辅助语言与玫瑰花”之后，浅层嵌入似乎有利于快速原型化(因为它不需要定义DSL和解释器)，而且深度嵌入有利于提供更强的正确性保证的查询。这是一个很好的经验法则来决定使用哪一个嵌入？

有什么好的理由使用Rosette的浅嵌入和深嵌入程序综合？

Answer 1

作为一般的经验法则，浅嵌入最适合于使用求解器搜索程序处理的值的应用程序，这在程序验证和天使执行中是典型的。

如果您正在进行程序综合和搜索(表示代码的值)，那么深度嵌入是最好的选择。

如果您的应用程序只需要搜索常量，那么浅层嵌入可能是一个很好的程序综合选择。但是，如果你在寻找任何更复杂的东西(例如表达式或语句)，那么深层嵌入就是最好的选择。

浅嵌入，你有有限的控制空间的程序，罗塞特将搜索。基本上，您仅限于使用Rosette的基于宏的草图构造进行编码。这些允许您定义基本的搜索空间并编写快速原型，但是如果您想要构建一个扩展的工具，您将需要严格控制搜索空间。

通过深度嵌入，您可以完全控制将要搜索的程序空间。本质上，您可以编写任意的Rosette / Racket函数来生成表示要搜索的所有具体程序的符号程序。然后，您还可以完全控制最后一步，即代码生成。一旦Rosette返回一个表示深度嵌入中的程序的值(例如AST)，您就可以任意处理它。对于浅嵌入，您只限于使用Rosette的内置代码生成器。

因此，最后，如果你正在做或计划做合成，使用深埋。对于其他一切(验证和天使般的执行)，浅嵌入将更容易和更快。