我希望在 Rosette 中编写一个 DSL，目的是合成一个函数。DSL 基于一个非常小的 Haskell 子集，并且是强类型的。因此，我想确保 Rosette 生成的任何内容都是正确类型的。
我可以考虑解决这个问题的一种方法是编写一个“is-well-typed-code”函数（这是我在 Julia 中已经做过的事情，我正在从中移植），然后断言它必须适用于综合函数。但是，我没有看到define-synthax以及synthesize如何将代码视为句法对象（即，可以应用任何函数的 S-expr）和在合成时作为语义函数。
我还可以想象cond在模块内部使用define-synthax所有可能类型的参数（这是这个小型 DSL 的有限集），并为每种类型分别定义可能的形式。define-synthax但是，似乎不可能在里面包含 conds 。
有任何想法吗？
谢谢！