racket - 使用 redex-check 打印成功

Question

我正在使用 redex-check 来验证一个模型与另一个模型，并希望查看中间（成功）结果以进行调试。最明显的方法是让 property-expr 打印给定的术语作为副作用，但这是不优雅的。还有其他方法可以查看中间的 redex-check 尝试吗？

Answer 1

看起来您对如何执行此操作有正确的想法。事实上，文档中的示例redex-check实际上是这样做的：

(let ([R (reduction-relation
            empty-lang
            (--> (Σ) 0)
            (--> (Σ number) number)
            (--> (Σ number_1 number_2 number_3 ...)
                 (Σ ,(+ (term number_1) (term number_2))
                    number_3 ...)))])
    (redex-check
     empty-lang
     (Σ number ...)
     (printf "~s\n" (term (number ...)))
      #:attempts 3
      #:source R))

将以下结果写入current-output-port：

()
(0)
(2 0)
redex-check: no counterexamples in 1 attempt (with each clause)