added current-cache-all?, a parameter that controls the caching strategy

that apply-reduction-relation* (and thus test-->>) uses
also make apply-reduction-relation* call remove-duplicates
  on the result of apply-reduction-relation
This commit is contained in:
Robby Findler 2011-05-07 18:49:19 -05:00
parent 70b0eb8ac9
commit 33c848fcda
4 changed files with 44 additions and 13 deletions

View File

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

View File

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

View File

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

View File

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