测试使用PLT-归约

Question

我是新来的球拍，我在使用REDEX特别感兴趣的语义时只生成以及类型的条款。我已经为皮尔斯的类型和编程语言书中的类型化算术表达式做了一个小模型。该代码是在以下要点：https://gist.github.com/rodrigogribeiro/e0fd3e1e3ff017b614dcfeee9f9154e0

当我试图测试属性，如进展和保存，我想检查测试覆盖了多少代码，所以我运行以下，如在教程中：

(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

一些尝试和重做这个小练习一对夫妇的类型我得到一个合理的解决方案后（完整的代码是在以下gist）。要点只产生良好类型的术语使用#: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认为应予以考虑。