The redex-check form does not correctly respect _!_ about redex HOT 7 CLOSED

Where sufficiently large includes the lambda calculus

#lang racket
(require redex)
(define-language L
  [e x (e e ...) (lambda (x_!_ ...) e)]
  [x variable-not-otherwise-mentioned])
(redex-check L e_chk (redex-match? L e (term e_chk)))

from redex.

@ianj 's example was fixed in late July, but hasn't made it to a release yet.

from redex.

While Ian's example works in the nightly build of racket, the larger calculus I linked above still produces lambdas with multiple variables of the same name.

from redex.

I adjusted the code in the gist by deleting all of the uses of
redex-check and then putting this at the bottom of the file:

(random-seed 0)
(define is-P? (redex-match? ccon P))
(redex-check ccon P is-P? #:attempts 1500)

and I am not seeing any failures. Could you please make some adjustments to
what I've done to clarify the bad behavior you're seeing?

Thanks,
Robby

from redex.

The following will reproduce the error consistently:

(random-seed 0)
(define is-e? (redex-match? ccon e))
(redex-check ccon e is-e? #:source step #:attempts 3000)

The output is:

redex-check: (predc (if ((lambda (W E W Y) JwX) (thunk (case k D nqF X B)) (thunk (+ t O)) 5 (inr unit)) u L)) does not match e

Notice the two matching arguments in the lambda.

from redex.

That's because this clause in step:

(in-hole E ((lambda (x ..._1) e) tv ..._1))

generates things that are not es.

I can see how this is confusing, and that there is really not anything you can reasonably do to compensate, so I've pushed a change to Redex so that it just discards such test cases instead of signaling errors.

ba99493

from redex.

Ah! Thanks so much for all the help with this.

from redex.