Генерация только хорошо типизированных терминов при тестировании семантики с использованием PLT-Redex

Question

Я новичок в ракетке, и я особенно заинтересован в использовании redex. Я сделал небольшую модель для типизированных арифметических выражений, которую можно найти в книге Пирса о типах и языках программирования. Код приведен ниже: https://gist.github.com/rodrigogribeiro/e0fd3e1e3ff017b614dcfeee9f9154e0

Когда я попытался протестировать свойства, такие как прогресс и сохранение, я хотел бы проверить, какая часть кода покрыта тестами, поэтому я выполнил следующее, как в учебнике amb:

(let ([c (make-coverage red)])
     (parameterize ([relation-coverage (list c)])
     (check-reduction-relation
      red
      (λ (E) (progress-holds? E)))
      (covered-cases c)))

Но это возвращает

'(("E-if-false" . 0) ("E-if-true" . 0) ("E-iszero-suc" . 0) 
  ("E-iszero-zero" . 0) ("E-pred-suc" . 0) ("E-pred-zero" . 0))

что означает, что ни одно правило семантики никогда не выполняется, верно? Я думаю, что проблема в том, что рэкет генерирует случайные термины, которые не обязательно хорошо напечатаны.

Мой вопрос: есть ли способ указать, как генерировать только хорошо напечатанные термины?

Answer 1

После нескольких попыток и повторения этого небольшого упражнения парой типов я получил правдоподобное решение (полный код приведен ниже). Главное, чтобы генерировать только хорошо типизированные термины, - это ограничить генератор переопределений с помощью #:satisfying оговорка, как progress Тест свойства ниже:

(define (progress)
  (let ([c (make-coverage eval-tyexp)])
    (parameterize ([relation-coverage (list c)])
        (redex-check TyExp 
               #:satisfying (types e t) 
               (progress-holds? (term e)))
        (covered-cases c))))

Линия #:satisfying (types e t) говорит, что только выражения e это суждение types e t трюмы должны быть рассмотрены.