fixed PR 10684 and fixed up some old, broken tests and fiddled with the test suite infrastructure

svn: r17536

collects/redex/private/bitmap-test-util.ss

@@ -1,18 +1,12 @@
-(module bitmap-test-util mzscheme
+#lang scheme/gui
-  (require (lib "mred.ss" "mred")
+(require framework
-           (lib "mrpict.ss" "texpict")
+         slideshow
-           (lib "framework.ss" "framework")
-           (lib "class.ss")
          "../pict.ss"
-           "../reduction-semantics.ss")
+         "../reduction-semantics.ss"
+         "config.ss")
 
 (provide test done)
 
-  (define-struct failed-test (panel))
-  
-  (define show-diffs?-env "PLT_REDEX_TEST_NOSHOW_DIFFS")
-  (define show-diffs? (not (getenv show-diffs?-env)))
-  
 (define tests 0)
 (define failed '())
 (define (done)
@@ -32,7 +26,7 @@
 (define (test/proc line-number pict raw-bitmap-filename)
   (set! tests (+ tests 1))
   (let* ([bitmap-filename 
-            (build-path "bmps" 
+          (build-path (format "bmps-~a" (system-type))
                       (case (system-type)
                         [(unix) (string-append "unix-" raw-bitmap-filename)]
                         [else raw-bitmap-filename]))]
@@ -53,10 +47,8 @@
     (send bdc set-bitmap #f)
     (let ([diff-bitmap (compute-diffs old-bitmap new-bitmap)])
       (when diff-bitmap
-          (if show-diffs?
         (let ([failed-panel (make-failed-panel line-number bitmap-filename old-bitmap new-bitmap diff-bitmap)])
-                (set! failed (append failed (list (make-failed-test failed-panel)))))
+          (set! failed (append failed (list failed-panel))))))))
-              (set! failed (append failed (list #f))))))))
 
 (define (compute-diffs old-bitmap new-bitmap)
   (let* ([w (max (send old-bitmap get-width)
@@ -129,9 +121,9 @@
                             (set! current-index (modulo (+ current-index 1) (length failed)))
                             (update-gui))]))
        (define (update-gui) 
-           (send sp active-child (failed-test-panel (list-ref failed current-index))))
+         (send sp active-child (list-ref failed current-index)))
        (set! test-result-single-panel sp)
-         (send f show #t)
+       (when (get-show-bitmaps?) (send f show #t))
        sp)]))
 
 (define (make-failed-panel line-number filename old-bitmap new-bitmap diff-bitmap)
@@ -147,10 +139,8 @@
                     (λ (_1 _2)
                       (cond
                         [(send chk get-value)
-                           (send chk set-label "Hide diff")
                          (send right-hand set-label diff-bitmap)]
                         [else
-                           (send chk set-label "Show diff")
                          (send right-hand set-label new-bitmap)]))]))
   (define btn (new button%
                    [parent f]
@@ -168,4 +158,4 @@
                           [label diff-bitmap]))
   (send left-hand set-label old-bitmap)
   (send right-hand set-label new-bitmap)
-    f))
+  f)

collects/redex/private/config.ss

@@ -0,0 +1,5 @@
+#lang scheme
+(provide set-show-bitmaps? get-show-bitmaps?)
+(define show-bitmaps? #t)
+(define (set-show-bitmaps? sb?) (set! show-bitmaps? sb?))
+(define (get-show-bitmaps?) show-bitmaps?)

collects/redex/private/reduction-semantics.ss

@@ -220,11 +220,12 @@
 
 ;; the withs, freshs, and side-conditions come in backwards order
 (define-for-syntax (bind-withs orig-name main lang lang-nts stx where-mode body)
+  (let* ([bindings '()]
+         [body
           (let loop ([stx stx]
-             [body body]
+                     [to-not-be-in main])
-             [bindings '()])
             (syntax-case stx (side-condition where fresh)
-      [() (values body bindings)]
+              [() body]
               [((where x e) y ...)
                (let-values ([(names names/ellipses) (extract-names lang-nts 'reduction-relation #t #'x)])
                  (with-syntax ([(cpat) (generate-temporaries '(compiled-pattern))]
@@ -235,7 +236,9 @@
                                                            #'x)]
                                [(names ...) names]
                                [(names/ellipses ...) names/ellipses])
-           (loop #'(y ...) 
+                   (with-syntax ([(x ...) (generate-temporaries #'(names ...))])
+                     (set! bindings (cons #`[cpat (compile-pattern #,lang `side-conditions-rewritten #t)] bindings))
+                     (let ([rest-body (loop #'(y ...) #`(list x ... #,to-not-be-in))])
                        #`(let ([mtchs (match-pattern cpat (term e))])
                            (if mtchs
                                #,
@@ -245,51 +248,45 @@
                                      append
                                      (map (λ (mtch)
                                             (let ([bindings (mtch-bindings mtch)])
-                                        (term-let ([names/ellipses (lookup-binding bindings 'names)] ...) 
+                                              (let ([x (lookup-binding bindings 'names)] ...)
-                                                  #,body)))
+                                                (term-let ([names/ellipses x] ...) 
+                                                          #,rest-body))))
                                           mtchs))]
                                  [(predicate) 
                                   #`(andmap (λ (mtch)
                                               (let ([bindings (mtch-bindings mtch)])
-                                          (term-let ([names/ellipses (lookup-binding bindings 'names)] ...) 
+                                                (let ([x (lookup-binding bindings 'names)] ...)
-                                                    #,body)))
+                                                  (term-let ([names/ellipses x] ...) 
+                                                            #,rest-body))))
                                             mtchs)]
                                  [else (error 'unknown-where-mode "~s" where-mode)])
-                         #f))
+                               #f))))))]
-                 (cons #`[cpat (compile-pattern #,lang `side-conditions-rewritten #t)]
-                       bindings))))]
               [((side-condition s ...) y ...)
-       (loop #'(y ...) #`(and s ... #,body) bindings)]
+               #`(and s ... #,(loop #'(y ...) to-not-be-in))]
               [((fresh x) y ...)
                (identifier? #'x)
-       (loop #'(y ...) 
+               #`(term-let ([x (variable-not-in #,to-not-be-in 'x)]) 
-             #`(term-let ([x (variable-not-in #,main 'x)]) #,body)
+                           #,(loop #'(y ...) #`(list (term x) #,to-not-be-in)))]
-             bindings)]
               [((fresh x name) y ...)
                (identifier? #'x)
-       (loop #'(y ...)
                #`(term-let ([x (let ([the-name (term name)])
                                  (verify-name-ok '#,orig-name the-name)
-                               (variable-not-in #,main the-name))])
+                                 (variable-not-in #,to-not-be-in the-name))])
-                         #,body)
+                           #,(loop #'(y ...) #`(list (term x) #,to-not-be-in)))]
-             bindings)]
               [((fresh (y) (x ...)) z ...)
-       (loop #'(z ...)
                #`(term-let ([(y #,'...)
-                           (variables-not-in #,main 
+                             (variables-not-in #,to-not-be-in 
                                                (map (λ (_ignore_) 'y)
                                                     (term (x ...))))])
-                         #,body)
+                           #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in)))]
-             bindings)]
               [((fresh (y) (x ...) names) z ...)
-       (loop #'(z ...)
                #`(term-let ([(y #,'...)
                              (let ([the-names (term names)]
                                    [len-counter (term (x ...))])
                                (verify-names-ok '#,orig-name the-names len-counter)
-                             (variables-not-in #,main the-names))])
+                               (variables-not-in #,to-not-be-in the-names))])
-                         #,body)
+                           #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in)))]))])
-             bindings)])))
+    (values body bindings)))
 
 (define-syntax-set (do-reduction-relation)
   (define (do-reduction-relation/proc stx)
@@ -746,12 +743,12 @@
                case-id)))))))
   
   (define (process-extras stx orig-name name-table extras)
-    (let ([the-name #f]
+    (let* ([the-name #f]
            [the-name-stx #f]
-          [sides/withs/freshs '()])
+           [sides/withs/freshs 
             (let loop ([extras extras])
               (cond
-          [(null? extras) (values the-name sides/withs/freshs)]
+                [(null? extras) '()]
                 [else
                  (syntax-case (car extras) (side-condition fresh where)
                    [name 
@@ -784,11 +781,7 @@
                         (set! the-name-stx (car extras))
                         (loop (cdr extras))))]
                    [(fresh var ...)
-              (begin
+                    (append (map (λ (x)
-                (set! sides/withs/freshs
-                      (append 
-                       (reverse 
-                        (map (λ (x)
                                    (syntax-case x ()
                                      [x
                                       (identifier? #'x)
@@ -809,21 +802,17 @@
                                                           "malformed fresh variable clause"
                                                           stx
                                                           #'x)]))
-                             (syntax->list #'(var ...))))
+                                 (syntax->list #'(var ...)))
-                       sides/withs/freshs))
                             (loop (cdr extras)))]
                    [(side-condition exp ...)
-              (begin 
+                    (cons (car extras) (loop (cdr extras)))]
-                (set! sides/withs/freshs (cons (car extras) sides/withs/freshs))
-                (loop (cdr extras)))]
                    [(where x e)
-              (begin
+                    (cons (car extras) (loop (cdr extras)))]
-                (set! sides/withs/freshs (cons (car extras) sides/withs/freshs))
-                (loop (cdr extras)))]
                    [(where . x)
                     (raise-syntax-error orig-name "malformed where clause" stx (car extras))]
                    [_
-              (raise-syntax-error orig-name "unknown extra" stx (car extras))])]))))
+                    (raise-syntax-error orig-name "unknown extra" stx (car extras))])]))])
+      (values the-name sides/withs/freshs)))
   
 
   
@@ -1125,11 +1114,7 @@
                                              (list name
                                                    (car names)))))
                                          (loop name (cdr names))]))])
-                  
+                  (parse-extras #'((stuff ...) ...))
-                  (with-syntax ([(((tl-side-conds ...) ...) 
-                                  (tl-bindings ...)
-                                  (tl-side-cond/binds ...))
-                                 (parse-extras #'((stuff ...) ...))])
                     (with-syntax ([(((cp-let-bindings ...) rhs/wheres) ...)
                                    (map (λ (sc/b rhs)
                                           (let-values ([(body-code cp-let-bindings) 
@@ -1139,7 +1124,7 @@
                                                          sc/b 'flatten
                                                          #`(list (term #,rhs)))])
                                             (list cp-let-bindings body-code)))
-                                          (syntax->list #'(tl-side-cond/binds ...))
+                                        (syntax->list #'((stuff ...) ...))
                                         (syntax->list #'(rhs ...)))]
                                   [(((rg-cp-let-bindings ...) rg-rhs/wheres) ...)
                                    (map (λ (sc/b rhs) 
@@ -1150,7 +1135,7 @@
                                                          sc/b 'predicate
                                                          #`#t)])
                                             (list cp-let-bindings body-code)))
-                                          (syntax->list #'(tl-side-cond/binds ...))
+                                        (syntax->list #'((stuff ...) ...))
                                         (syntax->list #'(rhs ...)))])
                       (with-syntax ([(side-conditions-rewritten ...) 
                                      (map (λ (x) (rewrite-side-conditions/check-errs
@@ -1205,7 +1190,7 @@
                                     ;; See "!!" below for information on the `seq-' bindings:
                                     [seq-of-rhs #'(rhs ...)]
                                     [seq-of-lhs #'(lhs ...)]
-                                      [seq-of-tl-side-cond/binds #'(tl-side-cond/binds ...)]
+                                    [seq-of-tl-side-cond/binds #'((stuff ...) ...)]
                                     [seq-of-lhs-for-lw #'(lhs-for-lw ...)])
                         (with-syntax ([defs #`(begin
                                                 (define-values (name2 name-predicate)
@@ -1300,7 +1285,7 @@
                                   defs))
                                (syntax defs))
                            'disappeared-use
-                             (map syntax-local-introduce (syntax->list #'(original-names ...))))))))))))))))]
+                           (map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))))]
       [(_ prev-metafunction name lang clauses ...)
        (begin
          (unless (identifier? #'name)
@@ -1383,41 +1368,25 @@
          (raise-syntax-error syn-error-name "error checking failed.2" stx))]))
   
   (define (parse-extras extras)
-    (let loop ([stuffs (syntax->list extras)]
+    (for-each
-               [side-conditionss '()]
+     (λ (stuffs)
-               [bindingss '()]
+       (for-each
-               [bothss '()])
+        (λ (stuff)
-      (cond
+          (syntax-case stuff (where side-condition)
-        [(null? stuffs) (list (reverse side-conditionss)
-                              (reverse bindingss)
-                              (reverse bothss))]
-        [else 
-         (let s-loop ([stuff (syntax->list (car stuffs))]
-                      [side-conditions '()]
-                      [bindings '()]
-                      [boths '()])
-           (cond
-             [(null? stuff) (loop (cdr stuffs)
-                                  (cons (reverse side-conditions) side-conditionss)
-                                  (cons (reverse bindings) bindingss)
-                                  ; Want these in reverse order.
-                                  (cons boths bothss))]
-             [else 
-              (syntax-case (car stuff) (where side-condition)
             [(side-condition tl-side-conds ...) 
-                 (s-loop (cdr stuff)
+             (void)]
-                         (append (syntax->list #'(tl-side-conds ...)) side-conditions)
-                         bindings
-                         (cons (car stuff) boths))]
             [(where x e)
-                 (s-loop (cdr stuff)
+             (void)]
-                         side-conditions
+            [(where . args)
-                         (cons #'(x e) bindings)
+             (raise-syntax-error 'define-metafunction 
-                         (cons (car stuff) boths))]
+                                 "malformed where clause"
+                                 stuff)]
             [_
              (raise-syntax-error 'define-metafunction 
                                  "expected a side-condition or where clause"
-                                     (car stuff))])]))]))))
+                                 stuff)]))
+        (syntax->list stuffs)))
+     (syntax->list extras))))
 
 (define (build-metafunction lang cases parent-cases wrap dom-contract-pat codom-contract-pat name relation?)
   (let ([dom-compiled-pattern (and dom-contract-pat (compile-pattern lang dom-contract-pat #f))]

collects/redex/private/run-tests.ss

@@ -1,7 +1,11 @@
 ;; require this file to run all of the test suites for redex.
 
 #lang scheme/base
-(require scheme/runtime-path)
+(require scheme/runtime-path
+         "config.ss"
+         "test-util.ss")
+
+(set-show-bitmaps? #t)
 
 (define test-files
   '("lw-test.ss" 
@@ -17,8 +21,6 @@
 
 (define-runtime-path here ".")
 
-(putenv "PLT_REDEX_TEST_NOSHOW_DIFFS" "yes")
-
 (define (flush)
   ;; these flushes are here for running under cygwin, 
   ;; which somehow makes mzscheme think it isn't using

collects/redex/private/test-util.ss

@@ -35,7 +35,9 @@
 
 (define tests 0)
 (define failures 0)
-(define (reset-count) (set! tests 0))
+(define (reset-count) 
+  (set! tests 0)
+  (set! failures 0))
 
 (define (print-tests-passed filename)
   (cond

collects/redex/private/tl-test.ss

@@ -1212,6 +1212,35 @@
          '(x y z))
         (list '(x1 y1 z1 x y z)))
 
+  (test (apply-reduction-relation 
+         (reduction-relation 
+          empty-language
+          (--> any (any_y x)
+               (where any_y x)
+               (fresh x)))
+         (term junk))
+        (list '(x x1)))
+  
+  (test (apply-reduction-relation 
+         (reduction-relation 
+          empty-language
+          (--> any (any_y x)
+               (fresh x)
+               (where any_y x)
+               (fresh x)))
+         (term junk))
+        (list '(x x1)))
+  
+  (test (apply-reduction-relation 
+         (reduction-relation 
+          empty-language
+          (--> (variable ...) (variable_0 ... variable_1 ...)
+               (fresh ((variable_0 ...) (variable ...)))
+               (fresh ((variable_1 ...) (variable ...)))))
+         (term (x y)))
+        (list '(variable_0 variable_1 variable_2 variable_3)))
+
+  
   ;; test that redex match can be used in a side-condition 
   ;; with the same language that is used to define the 
   ;; reduction relation.