I'm new to racket and I'm specially interested in using redex. I've done a small model for typed arithmetic expressions as found in Pierce's types and programming languages book. The code is at the following gist: https://gist.github.com/rodrigogribeiro/e0fd3e1e3ff017b614dcfeee9f9154e0
When I tried to test properties like progress and preservation, I would like to check how much of the code is covered by tests so I ran the following, as in amb tutorial:
(let ([c (make-coverage red)])
(parameterize ([relation-coverage (list c)])
(check-reduction-relation
red
(λ (E) (progress-holds? E)))
(covered-cases c)))
But, it returns
'(("E-if-false" . 0) ("E-if-true" . 0) ("E-iszero-suc" . 0)
("E-iszero-zero" . 0) ("E-pred-suc" . 0) ("E-pred-zero" . 0))
which means that no rule of the semantics is ever executed, right? I'm thinking that the problem is racket is generating random terms that aren't necessarily well-typed.
My question: Is there a way to specify how to generate only well-typed terms?
After some tries and redoing this little exercise a couple of types I got a plausible solution (the complete code is at the following gist). The main point to generate only well-typed terms is to constrain redex generator using a #:satisfying clause, like the progress property test below:
(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))))
The line #:satisfying (types e t) says that only expressions e that judgment types e t holds should be considered.