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

Thanks Casey, that is great. I look forward to the 4.2.3 release then.

One more request actually, wrt traces: the code in the traces view  
does not enjoy the same syntax highlight (matching parenthesis, color  
levels) than the definition window. Would it be possible to make it  
so? that would be useful to visually parse huge terms. I have found  
myself several times copy/pasting the content of a traces window into  
the definition window just to get that support.
Or maybe there is already a way to activate that?

Cheers,

-- Éric


On Oct 1, 2009, at 7:03 AM, Casey Klein wrote:

> 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))