diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index 182dbdd85d..30a4a6423d 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -2548,8 +2548,12 @@ nt-line)) (compiled-lang-nt-map lang))) -(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?)]) +(define (apply-reduction-relation* reductions exp + #:cache-all? [cache-all? (current-cache-all?)] + #:stop-when [stop-when (λ (x) #f)]) + (let-values ([(results cycle?) (traverse-reduction-graph reductions exp + #:cache-all? cache-all? + #:stop-when stop-when)]) results)) (struct search-success ()) @@ -2559,7 +2563,8 @@ ;; 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] - #:cache-all? [cache-all? (current-cache-all?)]) + #:cache-all? [cache-all? (current-cache-all?)] + #:stop-when [stop-when (λ (x) #f)]) (define visited (and cache-all? (make-hash))) (let/ec return (let ([answers (make-hash)] @@ -2581,20 +2586,25 @@ (set! cycle? #t)] [else (visit term) - (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 ([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)))))]))]))) + (cond + [(stop-when term) + (unless goal? + (hash-set! answers term #t))] + [else + (define 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 ([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)) diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index bd9fb37aef..0b0faa51f1 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -908,7 +908,8 @@ names of the reductions that were used. @defproc[(apply-reduction-relation* [r reduction-relation?] [t any/c] - [#:cache-all? cache-all? boolean? (current-cache-all?)]) + [#:cache-all? cache-all? boolean? (current-cache-all?)] + [#:stop-when stop-when (-> any/c any) (λ (x) #f)]) (listof any/c)]{ Accepts a reduction relation and a @@ -923,6 +924,13 @@ keeps a cache of all visited terms when traversing the graph and does not revisi 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. + +The @racket[stop-when] argument controls the stopping criterion. Specifically, it is +called with each term that @racket[apply-reduction-relation*] encounters. If it +ever returns a true value (anything except @racket[#f]), then @racket[apply-reduction-relation*] +considers the term to be irreducible (and so returns it and does not try to +reduce it further). + } @defparam[current-cache-all? cache-all? boolean?]{ diff --git a/collects/redex/reduction-semantics.rkt b/collects/redex/reduction-semantics.rkt index a95d0b7b74..ab13796c2d 100644 --- a/collects/redex/reduction-semantics.rkt +++ b/collects/redex/reduction-semantics.rkt @@ -70,7 +70,7 @@ [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) (#:cache-all? boolean?) (listof any/c))] + [apply-reduction-relation* (->* (reduction-relation? any/c) (#:cache-all? boolean? #:stop-when (-> any/c any)) (listof any/c))] [current-cache-all? (parameter/c boolean?)] [union-reduction-relations (->* (reduction-relation? reduction-relation?) () diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt index c58a04472f..c7475b7802 100644 --- a/collects/redex/tests/tl-test.rkt +++ b/collects/redex/tests/tl-test.rkt @@ -2508,6 +2508,36 @@ (test (sort (covered-cases c) <) '(("plain" . 1) ("shortcut" . 1) ("side-condition" . 2))))) + (let () + (define-language L + (e (e e) + (delay e) + +inf.0 + I) + (v (delay e) + +inf.0 + I)) + + (define red + (compatible-closure + (reduction-relation + L + (--> (+inf.0 +inf.0) (+inf.0 +inf.0)) + (--> (I e) e)) + L + e)) + + (test (apply-reduction-relation* + red + (term (I (delay (+inf.0 +inf.0)))) + #:stop-when (redex-match L v)) + (list (term (delay (+inf.0 +inf.0))))) + + (test (apply-reduction-relation* + red + (term (I (delay (+inf.0 +inf.0))))) + '())) + (let* ([S (reduction-relation empty-language (--> 1 1 uno))]