[plt-scheme] redex: leveraging generated checks and coverage

On Thu, Sep 17, 2009 at 4:09 PM, Eric Tanter <etanter at dcc.uchile.cl> wrote:
>> My guess is that you have a side-condition somewhere that Redex is
>> having trouble satisfying randomly.
>> [..]
>
> right, that may definitely be the case
>
>> (define-language M
>>  (q (side-condition number_1 (= (term number_1) 12345431))))
>>
>>> (redex-check M q #t)
>>
>> redex-check: unable to generate pattern number_1 in 100 attempts
>>
>> This error message should really include the side-condition part of
>> the pattern since it's that part, not number_1, that's actually
>> causing the difficulty. I'll fix that.
>
> That'd be better indeed.

This is fixed in SVN (but not in time for the 4.2.2 release).

> (define-language L
    (n number))
> (redex-check L (side-condition n #f) #t)
redex-check: unable to generate pattern (side-condition n
#<syntax:5:35>) in 100 attempts

If the pattern that can't be satisifed is the left-hand side of a
relation clause, the message points to that clause.

> (check-reduction-relation
   (reduction-relation
    L
    (--> n n
         (side-condition #f)
         foo))
   (λ (_) #t))
check-reduction-relation: unable to generate LHS of foo in 100 attempts
> (check-reduction-relation
   (reduction-relation
    L
    (--> n n
         (side-condition #f)))
   (λ (_) #t))
check-reduction-relation: unable to generate LHS of clause at
unsaved-editor4524:18:9 in 100 attempts

>>> * Finally, I really enjoy the coverage report for a reduction relation.
>>> There does not seem to be a similar functionality for metafunctions,
>>> though.
>>> It would be nice if I could get confidence that my test cases, in
>>> addition
>>> to testing all reduction rules, actually cover each possible path in the
>>> metafunctions (ie. telling me, for each metafunction, how many times each
>>> clause has matched).
>>
>> I'll add a metafunction-coverage parameter that works like
>> relation-coverage.
>
> Cool! I look forward to that!
>

This is in SVN too (again, not for 4.2.2).

(define-language L
  (n number))

(define-metafunction L
  [(plus n_1 n_2)
   ,(+ (term n_1) (term n_2))])

(define sum
  (reduction-relation
   L
   (--> (+) 0 "zero")
   (--> (+ n) n "one")
   (--> (+ n_1 n_2 n_3 ...)
        (+ (plus n_1 n_2) n_3 ...)
        "many")))

> (let ([plus-cov (make-coverage plus)]
          [sum-cov (make-coverage sum)])
     (parameterize ([relation-coverage (list plus-cov sum-cov)])
        (apply-reduction-relation* sum '(+ 0 1 2 3 4 5)))
      (values (covered-cases plus-cov)
                   (covered-cases sum-cov)))
(("unsaved-editor4545:9:2" . 5))
(("many" . 5) ("one" . 1) ("zero" . 0))