在使用完整的Rosette语言时，有哪些方法可以识别未提升的球拍结构？

Question

在用花环实现程序合成器时，最常见的错误之一是不安全地使用无吊装球拍结构，从而使合成器输出(unsat)。

事实上，作为一个初学者Rosette程序员，很难找到可能导致问题的未解除的球拍结构。我认为DrRacket可能可以帮助，例如，通过不将箭头从#lang rosette线显示到未提升的球拍结构(如assv )，但情况并非如此，也就是说，它向未解除的(例如assv)和向提升的操作符(例如first)显示箭头。

我一直在使用两种策略，(i)在rosette/safe中构建合成代码，直到我能够切换到完整的语言，这是不方便的，因为我不能使用更新的、更高级的Racker结构；(ii)浏览我在代码中使用的结构，并检查它们是否由rosette/base/base.rkt“提供”，这是令人厌烦的。

经验丰富的Rosette程序员有什么建议吗？

Answer 1

一种方法是在rosette/safe中开始编程，然后根据需要显式地从and中要求所需的构造。那么，如果事情出了问题，就更容易找出他们在哪里和什么时候做了。

因此，例如，您的代码应该如下所示：

   #lang rosette/safe

   (require (only-in racket for assv))

随着代码库的增长，还可以将所有这些导入收集到一个导出它们的模块中。然后，您的其余代码将需要该模块，该模块将充当您自定义的rosette/safe版本以及您所需的最小数量的that结构。