From 4542d071d521c0201b5bb06682a0a09946de72ca Mon Sep 17 00:00:00 2001
From: Casey Klein <clklein@racket-lang.org>
Date: Thu, 28 Oct 2010 20:21:36 -0500
Subject: [PATCH] =?UTF-8?q?Adds=20the=20`test-->>=E2=88=83'=20form.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../redex/private/reduction-semantics.rkt     | 124 ++++++++++++------
 collects/redex/redex.scrbl                    |  31 +++++
 collects/redex/reduction-semantics.rkt        |   1 +
 collects/redex/tests/tl-test.rkt              |  42 +++++-
 4 files changed, 159 insertions(+), 39 deletions(-)

diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt
index e806198c40..8c615bd46f 100644
--- a/collects/redex/private/reduction-semantics.rkt
+++ b/collects/redex/private/reduction-semantics.rkt
@@ -1,4 +1,4 @@
-#lang scheme/base
+#lang racket/base
 
 (require "matcher.ss"
          "struct.ss"
@@ -7,9 +7,11 @@
          "loc-wrapper.ss"
 	 "error.ss"
          mzlib/trace
+         racket/contract
          (lib "list.ss")
          (lib "etc.ss")
-         (for-syntax syntax/parse))
+         (for-syntax syntax/parse
+                     syntax/parse/experimental/contract))
 
 (require (for-syntax (lib "name.ss" "syntax")
                      "loc-wrapper-ct.ss"
@@ -2044,28 +2046,42 @@
          (compiled-lang-nt-map lang)))
 
 (define (apply-reduction-relation* reductions exp)
-  (let-values ([(results cycle?) (apply-reduction-relation*/cycle? reductions exp)])
+  (let-values ([(results cycle?) (traverse-reduction-graph reductions exp)])
     results))
 
-(define (apply-reduction-relation*/cycle? reductions exp)
-  (let ([answers (make-hash)]
-        [cycle? #f])
-    (let loop ([exp exp]
-               [path (make-immutable-hash '())])
-      (cond
-        [(hash-ref path exp #f)
-         (set! cycle? #t)]
-        [else
-         (let ([nexts (apply-reduction-relation reductions exp)])
-           (cond
-             [(null? nexts) (hash-set! answers exp #t)]
-             [else (for-each 
-                    (λ (next) (loop next (hash-set path exp #t)))
-                    nexts)]))]))
-    (values (sort (hash-map answers (λ (x y) x))
-                  string<=?
-                  #:key (λ (x) (format "~s" x)))
-            cycle?)))
+(struct search-success ())
+(struct search-failure (cutoff?))
+
+(define (traverse-reduction-graph reductions start #:goal [goal? #f] #:steps [steps +inf.0])
+  (let/ec return
+    (let ([answers (make-hash)]
+          [cycle? #f]
+          [cutoff? #f])
+      (let loop ([term start]
+                 [path (make-immutable-hash '())]
+                 [more-steps steps])
+        (if (and goal? (goal? term))
+            (return (search-success))
+            (cond
+              [(hash-ref path term #f)
+               (set! cycle? #t)]
+              [else
+               (let ([nexts (apply-reduction-relation reductions term)])
+                 (cond
+                   [(null? nexts) 
+                    (unless goal? 
+                      (hash-set! answers term #t))]
+                   [else (if (zero? more-steps)
+                             (set! cutoff? #t)
+                             (for-each 
+                              (λ (next) (loop next (hash-set path term #t) (sub1 more-steps)))
+                              nexts))]))])))
+      (if goal?
+          (search-failure cutoff?)
+          (values (sort (hash-map answers (λ (x y) x))
+                        string<=?
+                        #:key (λ (x) (format "~s" x)))
+                  cycle?)))))
 
 ;; map/mt : (a -> b) (listof a) (listof b) -> (listof b)
 ;; map/mt is like map, except
@@ -2133,36 +2149,37 @@
      '#,(syntax-column stx)
      '#,(syntax-position stx)))
 
-(define (check-equiv-pred form p)
-  (unless (and (procedure? p) (procedure-arity-includes? p 2))
-    (raise-type-error form "procedure (arity 2)" p)))
+(define-for-syntax test-equiv-ctc
+  #'(-> any/c any/c any/c))
+(define-for-syntax test-equiv-name
+  "#:equiv argument")
+(define-for-syntax test-equiv-default
+  #'equal?)
 
 (define-syntax (test-->> stx)
   (syntax-parse stx
     [(form red:expr
            (~or (~optional (~seq (~and #:cycles-ok (~bind [cycles-ok? #t])))
                            #:defaults ([cycles-ok? #f])
-                           #:name "#:cycles-ok keyword")
-                (~optional (~seq #:equiv equiv?:expr)
-                           #:defaults ([equiv? #'equal?])
-                           #:name "#:equiv keyword"))
+                           #:name "#:cycles-ok argument")
+                (~optional (~seq #:equiv equiv?)
+                           #:defaults ([equiv?.c test-equiv-default])
+                           #:name test-equiv-name))
            ...
            e1:expr
            e2:expr ...)
-     #`(let ([=? equiv?])
-         (check-equiv-pred 'form =?)
-         (test-->>/procs red e1 (list e2 ...) apply-reduction-relation*/cycle? #,(attribute cycles-ok?) =? #,(get-srcloc stx)))]))
+     #:declare equiv? (expr/c test-equiv-ctc #:name test-equiv-name)
+     #`(test-->>/procs red e1 (list e2 ...) traverse-reduction-graph #,(attribute cycles-ok?) equiv?.c #,(get-srcloc stx))]))
 
 (define-syntax (test--> stx)
   (syntax-parse stx
     [(form red:expr
-           (~optional (~seq #:equiv equiv?:expr)
-                      #:defaults ([equiv? #'equal?]))
+           (~optional (~seq #:equiv equiv?)
+                      #:defaults ([equiv?.c test-equiv-default]))
            e1:expr
            e2:expr ...)
-     #`(let ([=? equiv?])
-         (check-equiv-pred 'form =?)
-         (test-->>/procs red e1 (list e2 ...) apply-reduction-relation/dummy-second-value #t =? #,(get-srcloc stx)))]))
+     #:declare equiv? (expr/c test-equiv-ctc #:name test-equiv-name)
+     #`(test-->>/procs red e1 (list e2 ...) apply-reduction-relation/dummy-second-value #t equiv?.c #,(get-srcloc stx))]))
 
 (define (apply-reduction-relation/dummy-second-value red arg)
   (values (apply-reduction-relation red arg) #f))
@@ -2194,6 +2211,38 @@
                 (λ (v1) (fprintf (current-error-port) "  actual: ~v\n" v1))
                 got))))])))
 
+(define-syntax (test-->>∃ stx)
+  (syntax-parse stx
+    [(form (~optional (~seq #:steps steps) #:defaults ([steps.c #'1000]))
+           relation
+           start:expr
+           goal)
+     #:declare relation (expr/c #'reduction-relation? 
+                                #:name "reduction relation expression")
+     #:declare goal (expr/c #'(or/c (-> any/c any/c) (not/c procedure?)) 
+                            #:name "goal expression")
+     #:declare steps (expr/c #'(or/c natural-number/c +inf.0) 
+                             #:name "steps expression")
+     #`(test-->>∃/proc relation.c start goal.c steps.c #,(get-srcloc stx))]))
+
+(define (test-->>∃/proc relation start goal steps srcinfo)
+  (let ([result (traverse-reduction-graph 
+                 relation
+                 start 
+                 #:goal (if (procedure? goal) goal (λ (x) (equal? goal x)))
+                 #:steps steps)])
+    (inc-tests)
+    (when (search-failure? result)
+      (print-failed srcinfo)
+      (inc-failures)
+      (begin
+        (fprintf (current-error-port) "no reachable term ~a ~a" 
+                 (if (procedure? goal) "satisfying" "equal to")
+                 goal)
+        (when (search-failure-cutoff? result)
+          (fprintf (current-error-port) " (but some terms were not unexplored)"))
+        (newline (current-error-port))))))
+
 (define-syntax (test-predicate stx)
   (syntax-case stx ()
     [(_ p arg)
@@ -2287,6 +2336,7 @@
          test-equal
          test-->>
          test-->
+         test-->>∃ (rename-out [test-->>∃ test-->>E])
          test-predicate
          test-results)
 
diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl
index 5dfa6daf51..6de06fea73 100644
--- a/collects/redex/redex.scrbl
+++ b/collects/redex/redex.scrbl
@@ -1143,6 +1143,37 @@ step, using @racket[pred-expr] to determine equivalence.
        
        (test-results)]
 
+@defform/subs[(test-->>∃ option ... rel-expr start-expr spec-expr)
+              ([option (code:line #:steps steps-expr)])
+              #:contracts ([rel-expr reduction-relation?]
+                           [start-expr any/c]
+                           [spec-expr (or/c (-> any/c any/c)
+                                            (not/c procedure?))]
+                           [steps-expr (or/c natural-number/c +inf.0)])]{
+Tests to see if the term @racket[start-expr] reduces according to the reduction 
+relation @racket[rel-expr] to a term specified by @racket[goal-expr] in 
+@racket[steps-expr] or fewer steps (default 1,000). The specification 
+@racket[goal-expr] may be either a predicate on terms or a term itself.
+}
+@defidform[test-->>E]{An alias for @racket[test-->>∃].}
+
+@examples[
+#:eval redex-eval
+       (define-language L
+         (n natural))
+
+       (define succ-mod8
+         (reduction-relation
+          L
+          (--> n ,(modulo (add1 (term n)) 8))))
+
+       (test-->>∃ succ-mod8 6 2)
+       (test-->>∃ succ-mod8 6 even?)
+       (test-->>∃ succ-mod8 6 8)
+       (test-->>∃ #:steps 6 succ-mod8 6 5)
+       
+       (test-results)]
+
 @defform[(test-predicate p? e)]{
 Tests to see if the value of @racket[e] matches the predicate @racket[p?].
 }
diff --git a/collects/redex/reduction-semantics.rkt b/collects/redex/reduction-semantics.rkt
index 78f97c49c7..4f8e83b577 100644
--- a/collects/redex/reduction-semantics.rkt
+++ b/collects/redex/reduction-semantics.rkt
@@ -42,6 +42,7 @@
          test-equal
          test-->>
          test-->
+         test-->>∃ (rename-out [test-->>∃ test-->>E])
          test-predicate
          test-results)
 
diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt
index 76ce4b7b6c..dd01d5eda4 100644
--- a/collects/redex/tests/tl-test.rkt
+++ b/collects/redex/tests/tl-test.rkt
@@ -2155,7 +2155,7 @@
     (test (capture-output (test--> R #:equiv mod2=? 7 1 0) (test-results))
           "One test passed.\n")
     (test (capture-output (test--> R #:equiv mod2=? 7 1) (test-results))
-          #rx"FAILED tl-test.(?:.+):[0-9.]+\nexpected: 1\n  actual: 8\n  actual: 7\n1 test failed \\(out of 1 total\\).\n"))
+          #rx"FAILED tl-test\\.(?:.+):[0-9.]+\nexpected: 1\n  actual: 8\n  actual: 7\n1 test failed \\(out of 1 total\\).\n"))
   
   (let-syntax ([test-bad-equiv-arg
                 (λ (stx)
@@ -2165,9 +2165,47 @@
                                (test-form (reduction-relation empty-language (--> any any))
                                           #:equiv 1 2)
                                "no error raised")
-                             #rx"expected argument of type")]))])
+                             #rx"tl-test\\.(?:.+).*broke the contract")]))])
     (test-bad-equiv-arg test-->)
     (test-bad-equiv-arg test-->>))
 
+  (let ()
+    (capture-output (test-results))
+    (define-language L)
+    
+    (define 1+
+      (reduction-relation 
+       L
+       (--> number ,(add1 (term number)))))
+    
+    (define (equal-to-7 x) (= x 7))
+    (test (capture-output (test-->>∃ #:steps 5 1+ 0 equal-to-7))
+          #rx"^FAILED .*\nno reachable term satisfying #<procedure:equal-to-7> \\(but some terms were not unexplored\\)\n$")
+    
+    (test (capture-output (test-->>∃ 1+ 0 7)) "")
+    (test (capture-output (test-->>E 1+ 0 7)) "")
+    (test (capture-output (test-->>∃ #:steps +inf.0 1+ 0 7)) "")
+    (test (capture-output (test-->>∃ 1+ 0 equal-to-7)) "")
+    
+    (define identity
+      (reduction-relation
+       L
+       (--> any any)))
+    
+    (test (capture-output (test-->>∃ identity 0 1))
+          #rx"^FAILED .*\nno reachable term equal to 1\n$")
+    
+    (test (capture-output (test-results)) "2 tests failed (out of 6 total).\n")
+    
+    (test (with-handlers ([exn:fail:contract? exn-message])
+            (test-->>∃ 1+ 0 (λ (x y) x)))
+          #rx"tl-test\\.(?:.+).*broke the contract.*goal expression")
+    (test (with-handlers ([exn:fail:contract? exn-message])
+            (test-->>∃ 1 0 1))
+          #rx"tl-test\\.(?:.+).*broke the contract.*reduction relation expression")
+    (test (with-handlers ([exn:fail:contract? exn-message])
+            (test-->>∃ #:steps 1.1 1+ 0 1))
+          #rx"tl-test\\.(?:.+).*broke the contract.*steps expression"))
+  
   (print-tests-passed 'tl-test.ss)
   
\ No newline at end of file