使用redex-check打印成功

Question

我正在使用redex-check來針對另一個模型驗證模型，並希望查看用於調試目的的中間（成功）結果。最明顯的做法是讓屬性表達式將給定的術語打印爲副作用，但這不夠雅觀。是否有另一種方法來查看中間redex-check嘗試？

Answer 1

它看起來像你有正確的想法如何做到這一點。事實上，example for redex-check in the docs actually does this：

(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)