1

我是球拍新手，我对使用 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))

这意味着永远不会执行任何语义规则，对吗？我认为问题在于球拍正在生成不一定正确输入的随机术语。

我的问题：有没有办法指定如何只生成类型良好的术语？

4

1 回答 1

2

经过一些尝试并重做这个小练习几种类型后，我得到了一个合理的解决方案（完整的代码在以下要点中）。仅生成类型良好的术语的要点是使用#:satisfying子句约束 redex 生成器，如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

于 2017-09-01T23:18:59.323 回答