diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index 746a5f4604..88ed466f6a 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -2088,8 +2088,8 @@ nt-line)) (compiled-lang-nt-map lang))) -(define (apply-reduction-relation* reductions exp) - (let-values ([(results cycle?) (traverse-reduction-graph reductions exp)]) +(define (apply-reduction-relation* reductions exp #:cache-all? [cache-all? (current-cache-all?)]) + (let-values ([(results cycle?) (traverse-reduction-graph reductions exp #:cache-all? cache-all?)]) results)) (struct search-success ()) @@ -2098,7 +2098,9 @@ ;; traverse-reduction-graph : ;; reduction-relation term #:goal (-> any boolean?) #:steps number? #:visit (-> any/c void?) -> (or/c search-success? search-failure?) ;; reduction-relation term #:goal #f #:steps number? #:visit (-> any/c void?) -> (values (listof any/c) boolean?) -(define (traverse-reduction-graph reductions start #:goal [goal? #f] #:steps [steps +inf.0] #:visit [visit void]) +(define (traverse-reduction-graph reductions start #:goal [goal? #f] #:steps [steps +inf.0] #:visit [visit void] + #:cache-all? [cache-all? (current-cache-all?)]) + (define visited (and cache-all? (make-hash))) (let/ec return (let ([answers (make-hash)] [cycle? #f] @@ -2126,9 +2128,13 @@ (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))]))]))) + (for ([next (in-list (remove-duplicates nexts))]) + (when (or (not visited) + (not (hash-ref visited next #f))) + (when visited (hash-set! visited next #t)) + (loop next + (hash-set path term #t) + (sub1 more-steps)))))]))]))) (if goal? (search-failure cutoff?) (values (sort (hash-map answers (λ (x y) x)) @@ -2136,6 +2142,8 @@ #:key (λ (x) (format "~s" x))) cycle?))))) +(define current-cache-all? (make-parameter #f)) + ;; map/mt : (a -> b) (listof a) (listof b) -> (listof b) ;; map/mt is like map, except ;; a) it uses the last argument instead of the empty list @@ -2421,6 +2429,7 @@ apply-reduction-relation/tag-with-names apply-reduction-relation/tagged apply-reduction-relation* + current-cache-all? variable-not-in variables-not-in) diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index 5ad608c228..be05030e87 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -890,17 +890,30 @@ names of the reductions that were used. @defproc[(apply-reduction-relation* [r reduction-relation?] - [t any/c]) + [t any/c] + [#:cache-all? cache-all? boolean? (current-cache-all?)]) (listof any/c)]{ -The function @racket[apply-reduction-relation*] accepts a reduction relation and a +Accepts a reduction relation and a term. Starting from @racket[t], it follows every reduction path and returns all of the terms that do not reduce further. If there are infinite reduction sequences that do not repeat, this function will not terminate (it does terminate if the only infinite reduction paths are cyclic). + +If the @racket[cache-all?] argument is @racket[#t], then @racket[apply-reduction-relation*] +keeps a cache of all visited terms when traversing the graph and does not revisit +any of them. This cache can, in some cases, use a lot of memory, so it is off by +default and the cycle checking happens by keeping track only of the current path +it is traversing through the reduction graph. } +@defparam[current-cache-all? cache-all? boolean?]{ + Controls the behavior of @racket[apply-reduction-relation*] + and @racket[test-->>]'s cycle checking. See @racket[apply-reduction-relation*] + for more details. +} + @examples[ #:eval redex-eval (define-language empty-lang) @@ -913,7 +926,7 @@ terminate (it does terminate if the only infinite reduction paths are cyclic). (--> 3 3))) (apply-reduction-relation R 0) (apply-reduction-relation* R 0)] - + @defidform[-->]{ Recognized specially within @racket[reduction-relation]. A @racket[-->] form is an error elsewhere. } @@ -1131,10 +1144,12 @@ predicate. This test uses @racket[apply-reduction-relation*], so it does not terminate -when the resulting reduction graph is infinite. - - +when the resulting reduction graph is infinite, although it +does terminate if there are cycles in the (finite) graph. +If @racket[#:cycles-ok] is not supplied then any cycles detected +are treated as a test failure. If a @racket[pred-expr] is supplied, +then it is used to compare the expected and actual results. } @defform/subs[(test--> rel-expr option ... e1-expr e2-expr ...) diff --git a/collects/redex/reduction-semantics.rkt b/collects/redex/reduction-semantics.rkt index 0b00e439a5..e2989116be 100644 --- a/collects/redex/reduction-semantics.rkt +++ b/collects/redex/reduction-semantics.rkt @@ -66,7 +66,8 @@ [apply-reduction-relation (-> reduction-relation? any/c (listof any/c))] [apply-reduction-relation/tag-with-names (-> reduction-relation? any/c (listof (list/c (or/c false/c string?) any/c)))] - [apply-reduction-relation* (-> reduction-relation? any/c (listof any/c))] + [apply-reduction-relation* (->* (reduction-relation? any/c) (#:cache-all? boolean?) (listof any/c))] + [current-cache-all? (parameter/c boolean?)] [union-reduction-relations (->* (reduction-relation? reduction-relation?) () #:rest (listof reduction-relation?) diff --git a/doc/release-notes/redex/HISTORY.txt b/doc/release-notes/redex/HISTORY.txt index 3f023c7acb..bf36412979 100644 --- a/doc/release-notes/redex/HISTORY.txt +++ b/doc/release-notes/redex/HISTORY.txt @@ -1,5 +1,11 @@ * added support for typsetting define-relation relations + * made apply-reduction-relation* call remove-duplicates + on the result of apply-reduction-relation + + * added the #:cache-all? argument to apply-reduction-relation* + and the current-cache-all? parameter + v5.1.1 * changed pattern language to disallow unquote