Fixed check-reduction-relation's handling of cases with `where' and

`side-condition' clauses.

svn: r12995

collects/redex/private/reduction-semantics.ss

@@ -510,16 +510,13 @@
                  p)])))))
   
   (define (do-leaf stx orig-name lang name-table from to extras lang-id)
-    (let ([lang-nts (language-id-nts lang-id orig-name)])
+    (let* ([lang-nts (language-id-nts lang-id orig-name)]
+           [rw-sc (λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))])
       (let-values ([(name fresh-vars side-conditions/withs) (process-extras stx orig-name name-table extras)])
         (let-values ([(names names/ellipses) (extract-names lang-nts orig-name #t from)])
-          (with-syntax ([side-conditions-rewritten 
-                         (rewrite-side-conditions/check-errs 
-                          lang-nts
-                          orig-name
-                          #t
-                          from)]
-                        [to to #;#`,(begin (printf "~s\n" #,name) (term #,to))]
+          (with-syntax ([side-conditions-rewritten (rw-sc from)]
+                        [lhs-w/extras (rw-sc #`(side-condition #,from #,(bind-withs side-conditions/withs #'#t)))]
+                        [to to]
                         [name name]
                         [lang lang]
                         [(names ...) names]
@@ -550,14 +547,15 @@
             #`(do-leaf-match
                name
                `side-conditions-rewritten
+               `lhs-w/extras
                (λ (main bindings)
                  ;; nested term-let's so that the bindings for the variables 
                  ;; show up in the `fresh' side-conditions, the bindings for the variables
                  ;; show up in the withs, and the withs show up in the 'fresh' side-conditions
                  (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
-                   (term-let (fresh-var-clauses ...)
-                     #,(bind-withs side-conditions/withs
-                                    #'(make-successful (term to))))))))))))
+                           (term-let (fresh-var-clauses ...)
+                                     #,(bind-withs side-conditions/withs
+                                                   #'(make-successful (term to))))))))))))
   
   ;; the withs and side-conditions come in backwards order
   (define (bind-withs stx body)
@@ -756,7 +754,7 @@
    (rewrite-proc-name child-make-proc)
    (subst lhs-frm-id (rewrite-proc-lhs child-make-proc) rhs-from)))
 
-(define (do-leaf-match name pat proc)
+(define (do-leaf-match name pat w/extras proc)
   (make-rewrite-proc
    (λ (lang)
      (let ([cp (compile-pattern lang pat #t)])
@@ -771,7 +769,7 @@
                        other-matches)
                other-matches)))))
    name
-   pat))
+   w/extras))
 
 (define-syntax (test-match stx)
   (syntax-case stx ()

collects/redex/private/rg-test.ss

@@ -540,16 +540,17 @@
   (define-language L
     (e (+ e ...) number)
     (E (+ number ... E* e ...))
-    (E* hole E*))
-  (define R
-    (reduction-relation
-     L
-     (==> (+ number ...) whatever)
-     (--> (side-condition number (even? (term number))) whatever)
-     with
-     [(--> (in-hole E a) whatever)
-      (==> a b)]))
-  (let ([generated null])
+    (E* hole E*)
+    (n 4))
+  
+  (let ([generated null]
+        [R (reduction-relation
+            L
+            (==> (+ number ...) whatever)
+            (--> (side-condition number (even? (term number))) whatever)
+            with
+            [(--> (in-hole E a) whatever)
+             (==> a b)])])
     (test (begin
             (check-reduction-relation 
              R (λ (term) (set! generated (cons term generated)))
@@ -558,6 +559,7 @@
              #:attempts 1)
             generated)
           (reverse '((+ (+)) 0))))
+  
   (let ([S (reduction-relation L (--> 1 2 name) (--> 3 4))])
     (test (check-reduction-relation S (λ (x) #t) #:attempts 1) #t)
     (test (current-error-port-output 
@@ -565,7 +567,23 @@
           "checking name failed after 1 attempts:\n1\n")
     (test (current-error-port-output 
            (λ () (check-reduction-relation S (curry eq? 1))))
-          "checking unnamed failed after 1 attempts:\n3\n")))
+          "checking unnamed failed after 1 attempts:\n3\n"))
+  
+  (let ([T (reduction-relation
+            L
+            (==> number number
+                 (where num number)
+                 (side-condition (eq? (term num) 4))
+                 (where numb num)
+                 (side-condition (eq? (term numb) 4)))
+            with
+            [(--> (9 a) b)
+             (==> a b)])])
+    (test (check-reduction-relation 
+           T (curry equal? '(9 4)) 
+           #:attempts 1
+           #:decisions (decisions #:num (build-list 5 (λ (x) (λ _ x)))))
+          #t)))
 
 ; check-metafunction
 (let ()

collects/redex/private/tl-test.ss

@@ -1156,7 +1156,9 @@
         [else #f]))
     
     ; test shortcut in terms of shortcut
-    (test (rewrite-proc-lhs (third (reduction-relation-make-procs r)))
-          '((5 2) 1)))
+    (test (match (rewrite-proc-lhs (third (reduction-relation-make-procs r)))
+            [`(((side-condition 5 ,(? procedure?)) 2) 1) #t]
+            [else #f])
+          #t))
   
   (print-tests-passed 'tl-test.ss))