Успех печати с проверкой redex

Question

Я использую redex-check для проверки модели против другой и хотел бы видеть промежуточные (успешные) результаты для целей отладки. Самый очевидный способ сделать это - иметь свойство-expr напечатать данный термин как побочный эффект, но это неэлегантно. Есть ли еще один способ взглянуть на промежуточные попытки проверки редекса?

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)