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

changed apply-reduction-relation* so that it notices cycles and ignores them

Browse Source 
svn: r13519
This commit is contained in:
Robby Findler 2009-02-11 20:25:32 +00:00
parent 7b11c290f5
commit 3ee1a899ee
2 changed files with 19 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
collects/redex/private/reduction-semantics.ss
View File

@ -1661,13 +1661,18 @@
(compiled-lang-nt-map lang)))
(define (apply-reduction-relation* reductions exp)
(let ([answers (make-hash)])
(let ([answers (make-hash)]
[cycles (make-hash)])
(let loop ([exp exp])
(let ([nexts (apply-reduction-relation reductions exp)])
(cond
[(null? nexts) (hash-set! answers exp #t)]
[else (for-each loop nexts)])))
(hash-map answers (λ (x y) x))))
(unless (hash-ref cycles exp #f)
(hash-set! cycles exp #t)
(let ([nexts (apply-reduction-relation reductions exp)])
(cond
[(null? nexts) (hash-set! answers exp #t)]
[else (for-each loop nexts)]))))
(sort (hash-map answers (λ (x y) x))
string<=?
#:key (λ (x) (format "~s" x)))))
;; map/mt : (a -> b) (listof a) (listof b) -> (listof b)

14
collects/redex/redex.scrbl
View File

@ -819,11 +819,12 @@ names of the reductions that were used.
[t any?])
(listof (listof any?))]{
apply-reduction-relation* accepts a list of reductions and a
term. It returns the results of following every reduction
path from the term. If there are infinite reduction
sequences starting at the term, this function will not
terminate.
The function @scheme[apply-reduction-relation*] accepts a reduction relation and a
term. Starting from @scheme[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).
}
@defidform[-->]{ Recognized specially within
@ -974,7 +975,8 @@ Tests to see if @scheme[e1] is equal to @scheme[e2].
@defform[(test--> reduction-relation e1 e2 ...)]{
Tests to see if the value of @scheme[e1] (which should be a term),
reduces to the @scheme[e2]s under @scheme[reduction-relation].
reduces to the @scheme[e2]s under @scheme[reduction-relation]
(using @scheme[apply-reduction-relation*], so it may not terminate).
}
@defform[(test-predicate p? e)]{