fix an equal? into an alpha equivalence test

closes racket#99

Author: rfindler

redex-lib/redex/private/judgment-form.rkt

@@ -128,7 +128,7 @@
 (require 'mode-utils
          (for-syntax 'mode-utils))
 
-(define-for-syntax (generate-binding-constraints names names/ellipses bindings syn-err-name)
+(define-for-syntax (generate-binding-constraints lang names names/ellipses bindings syn-err-name)
   (define (id/depth stx)
     (syntax-case stx ()
       [(s (... ...))
@@ -146,7 +146,7 @@
                  (let ([b-id/depth (id/depth b)]
                        [n-id/depth (id/depth w/e)])
                    (if (= (id/depth-depth b-id/depth) (id/depth-depth n-id/depth))
-                       (cons #`(equal? #,x (term #,b)) cs)
+                       (cons #`(alpha-equivalent? #,lang #,x (term #,b)) cs)
                        (raise-ellipsis-depth-error
                         syn-err-name
                         (id/depth-id n-id/depth) (id/depth-depth n-id/depth)
@@ -197,7 +197,8 @@
                             #'pat-stx)]
                           [lang-stx rt-lang])
               (define-values (binding-constraints temporaries env+)
-                (generate-binding-constraints (syntax->list #'(names ...))
+                (generate-binding-constraints rt-lang
+                                              (syntax->list #'(names ...))
                                               (syntax->list #'(names/ellipses ...))
                                               env
                                               orig-name))
@@ -297,7 +298,7 @@
                         (syntax->list #'names)
                         (syntax->list #'names/ellipses))))
             (define-values (binding-constraints temporaries env+)
-              (generate-binding-constraints output-names output-names/ellipses env orig-name))
+              (generate-binding-constraints rt-lang output-names output-names/ellipses env orig-name))
             (define rest-body
               (loop rest-clauses #`(list (term #,output-pattern) #,to-not-be-in) env+))
             (define call

redex-test/redex/tests/tl-judgment-form.rkt

@@ -730,6 +730,33 @@
 
   (test (judgment-holds (J (1) any) any) (list 1)))
 
+(let ()
+  (define-language L
+    (x ::= variable-not-otherwise-mentioned)
+    (e ::= x (λ (x) e))
+    #:binding-forms
+    (λ (x) e #:refers-to x))
+
+  (define-judgment-form L
+    #:mode (equal1 I I)
+    #:contract (equal1 e e)
+
+    [(where (e e) (e_1 e_2))
+     -----------------
+     (equal1 e_1 e_2)])
+
+  (define-judgment-form L
+    #:mode (equal2 I I)
+    #:contract (equal2 e e)
+
+    [(where e e_1)
+     (where e e_2)
+     -----------------
+     (equal2 e_1 e_2)])
+
+  (test (judgment-holds (equal1 (λ (x1) x1) (λ (x2) x2))) #t)
+  (test (judgment-holds (equal2 (λ (x1) x1) (λ (x2) x2))) #t))
+
 (parameterize ([current-namespace (make-base-namespace)])
   (eval '(require errortrace))
   (eval '(require redex/reduction-semantics))