suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

add the #:stop-when argument to apply-reduction-relation*

Browse Source
This commit is contained in:
Robby Findler 2011-10-23 12:10:21 -05:00
parent 23d38b14a4
commit 9d371153fd
4 changed files with 67 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
collects/redex/private/reduction-semantics.rkt
View File

@ -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))

10
collects/redex/redex.scrbl
View File

@ -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?]{

2
collects/redex/reduction-semantics.rkt
View File

@ -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?)
()

30
collects/redex/tests/tl-test.rkt
View File

@ -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))]