PLT-Redexを使用してセマンティクスをテストするときに型付きの言葉のみを生成する

Question

私はラケットには新しく、特にredexの使用に興味があります。私は、Pierceの型とプログラミング言語の本で見つかった型付き算術式の小さなモデルを作成しました。コードは次の要点にあります：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

いくつか試してやり直した後に、この小さなエクササイズで2つのタイプを試してみました。私は考えられる解決策を得ました（完全なコードは次の通りですgist）。だけうまく型付けされた用語を生成するための主なポイントは以下のprogress性試験と同様に、#:satisfying句を使用して可約式発電機を制約することです：

(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)のみtypes e tが考慮されるべき保持判断eを表現することを言います。