fix a very very old bug in Redex uncovered by the new enumerator

The new test case in this commit shows the bad behavior;
the fix was to replace the regexp #rx".*[^0-9]([0-9]+)$"
with #rx"([0-9]+)$", ie make the regexp work properly in
the empty case (since regexps promise to find longest matches
anyway).

Also, Rackety

pkgs/redex-pkgs/redex-lib/redex/private/fresh.rkt

@@ -1,44 +1,46 @@
 #lang racket/base
-(require racket/contract)
+(require racket/contract
+         racket/set)
 
-(define re:gen-d #rx".*[^0-9]([0-9]+)$")
 (define (variable-not-in sexp var)
-  (let* ([var-str (symbol->string var)]
+  (define var-str (symbol->string var))
-         [var-prefix (let ([m (regexp-match #rx"^(.*[^0-9])[0-9]+$" var-str)])
+  (define var-prefix
-                       (if m
+    (let ([m (regexp-match #rx"^(.*[^0-9])[0-9]+$" var-str)])
-                           (cadr m)
+      (if m
-                           var-str))]
+          (cadr m)
-         [found-exact-var? #f]
+          var-str)))
-         [nums (let loop ([sexp sexp]
+  (define found-exact-var? #f)
-                          [nums null])
+  (define nums
-                 (cond
+    (let loop ([sexp sexp]
-                   [(pair? sexp) (loop (cdr sexp) (loop (car sexp) nums))]
+               [nums (set)])
-                   [(symbol? sexp) 
+      (cond
-                    (when (eq? sexp var)
+        [(pair? sexp) (loop (cdr sexp) (loop (car sexp) nums))]
-                      (set! found-exact-var? #t))
+        [(symbol? sexp) 
-                    (let* ([str (symbol->string sexp)]
+         (when (equal? sexp var)
-                           [match (regexp-match re:gen-d str)])
+           (set! found-exact-var? #t))
-                      (if (and match
+         (define str (symbol->string sexp))
-                               (is-prefix? var-prefix str))
+         (define match (regexp-match #rx"([0-9]+)$" str))
-                          (cons (string->number (cadr match)) nums)
+         (if (and match
-                          nums))]
+                  (is-prefix? var-prefix str))
-                   [else nums]))])
+             (set-add nums (string->number (list-ref match 1)))
-    (cond
+             nums)]
-      [(not found-exact-var?) var]
+        [else nums])))
-      [(null? nums) (string->symbol (format "~a1" var))]
+  (cond
-      [else (string->symbol (format "~a~a" var-prefix (find-best-number nums)))])))
+    [(not found-exact-var?) var]
+    [(set-empty? nums) (string->symbol (format "~a1" var))]
+    [else (string->symbol (format "~a~a" var-prefix (find-best-number nums)))]))
 
 (define (find-best-number nums)
-  (let loop ([sorted (sort nums <)]
+  (let loop ([sorted (sort (set->list nums) <)]
              [i 1])
     (cond
       [(null? sorted) i]
       [else 
-       (let ([fst (car sorted)])
+       (define fst (car sorted))
-         (cond
+       (cond
-           [(< i fst) i]
+         [(< i fst) i]
-           [(> i fst) (loop (cdr sorted) i)]
+         [(> i fst) (loop (cdr sorted) i)]
-           [(= i fst) (loop (cdr sorted) (+ i 1))]))])))
+         [(= i fst) (loop (cdr sorted) (+ i 1))])])))
 
 (define (variables-not-in sexp vars)
   (let loop ([vars vars]
@@ -46,14 +48,16 @@
     (cond
       [(null? vars) null]
       [else 
-       (let ([new-var (variable-not-in sexp (car vars))])
+       (define new-var (variable-not-in sexp (car vars)))
-         (cons new-var
+       (cons new-var
-               (loop (cdr vars)
+             (loop (cdr vars)
-                     (cons new-var sexp))))])))
+                   (cons new-var sexp)))])))
 
 (define (is-prefix? str1 str2)
   (and (<= (string-length str1) (string-length str2))
-       (equal? str1 (substring str2 0 (string-length str1)))))
+       (for/and ([c1 (in-string str1)]
+                 [c2 (in-string str2)])
+         (equal? c1 c2))))
 
 (provide/contract
  [variable-not-in (any/c symbol? . -> . symbol?)]

pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt

@@ -2820,6 +2820,7 @@
         (term x4))
   (test (variable-not-in (term (x x1 x1 x2 x2)) 'x)
         (term x3))
+  (test (variable-not-in (term (|| |1|)) '||) '|2|)
   
   (test (variables-not-in (term (x y z)) '(x))
         '(x1))