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

Adds the `test-->>∃' form.

Browse Source
This commit is contained in:
Casey Klein 2010-10-28 20:21:36 -05:00
parent 18a81f8552
commit 4542d071d5
4 changed files with 159 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1,4 +1,4 @@
#lang scheme/base
#lang racket/base
(require "matcher.ss"
"struct.ss"
@ -7,9 +7,11 @@
"loc-wrapper.ss"
"error.ss"
mzlib/trace
racket/contract
(lib "list.ss")
(lib "etc.ss")
(for-syntax syntax/parse))
(for-syntax syntax/parse
syntax/parse/experimental/contract))
(require (for-syntax (lib "name.ss" "syntax")
"loc-wrapper-ct.ss"
@ -2044,28 +2046,42 @@
(compiled-lang-nt-map lang)))
(define (apply-reduction-relation* reductions exp)
(let-values ([(results cycle?) (apply-reduction-relation*/cycle? reductions exp)])
(let-values ([(results cycle?) (traverse-reduction-graph reductions exp)])
results))
(define (apply-reduction-relation*/cycle? reductions exp)
(let ([answers (make-hash)]
[cycle? #f])
(let loop ([exp exp]
[path (make-immutable-hash '())])
(cond
[(hash-ref path exp #f)
(set! cycle? #t)]
[else
(let ([nexts (apply-reduction-relation reductions exp)])
(cond
[(null? nexts) (hash-set! answers exp #t)]
[else (for-each
(λ (next) (loop next (hash-set path exp #t)))
nexts)]))]))
(values (sort (hash-map answers (λ (x y) x))
string<=?
#:key (λ (x) (format "~s" x)))
cycle?)))
(struct search-success ())
(struct search-failure (cutoff?))
(define (traverse-reduction-graph reductions start #:goal [goal? #f] #:steps [steps +inf.0])
(let/ec return
(let ([answers (make-hash)]
[cycle? #f]
[cutoff? #f])
(let loop ([term start]
[path (make-immutable-hash '())]
[more-steps steps])
(if (and goal? (goal? term))
(return (search-success))
(cond
[(hash-ref path term #f)
(set! cycle? #t)]
[else
(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-each
(λ (next) (loop next (hash-set path term #t) (sub1 more-steps)))
nexts))]))])))
(if goal?
(search-failure cutoff?)
(values (sort (hash-map answers (λ (x y) x))
string<=?
#:key (λ (x) (format "~s" x)))
cycle?)))))
;; map/mt : (a -> b) (listof a) (listof b) -> (listof b)
;; map/mt is like map, except
@ -2133,36 +2149,37 @@
'#,(syntax-column stx)
'#,(syntax-position stx)))
(define (check-equiv-pred form p)
(unless (and (procedure? p) (procedure-arity-includes? p 2))
(raise-type-error form "procedure (arity 2)" p)))
(define-for-syntax test-equiv-ctc
#'(-> any/c any/c any/c))
(define-for-syntax test-equiv-name
"#:equiv argument")
(define-for-syntax test-equiv-default
#'equal?)
(define-syntax (test-->> stx)
(syntax-parse stx
[(form red:expr
(~or (~optional (~seq (~and #:cycles-ok (~bind [cycles-ok? #t])))
#:defaults ([cycles-ok? #f])
#:name "#:cycles-ok keyword")
(~optional (~seq #:equiv equiv?:expr)
#:defaults ([equiv? #'equal?])
#:name "#:equiv keyword"))
#:name "#:cycles-ok argument")
(~optional (~seq #:equiv equiv?)
#:defaults ([equiv?.c test-equiv-default])
#:name test-equiv-name))
...
e1:expr
e2:expr ...)
#`(let ([=? equiv?])
(check-equiv-pred 'form =?)
(test-->>/procs red e1 (list e2 ...) apply-reduction-relation*/cycle? #,(attribute cycles-ok?) =? #,(get-srcloc stx)))]))
#:declare equiv? (expr/c test-equiv-ctc #:name test-equiv-name)
#`(test-->>/procs red e1 (list e2 ...) traverse-reduction-graph #,(attribute cycles-ok?) equiv?.c #,(get-srcloc stx))]))
(define-syntax (test--> stx)
(syntax-parse stx
[(form red:expr
(~optional (~seq #:equiv equiv?:expr)
#:defaults ([equiv? #'equal?]))
(~optional (~seq #:equiv equiv?)
#:defaults ([equiv?.c test-equiv-default]))
e1:expr
e2:expr ...)
#`(let ([=? equiv?])
(check-equiv-pred 'form =?)
(test-->>/procs red e1 (list e2 ...) apply-reduction-relation/dummy-second-value #t =? #,(get-srcloc stx)))]))
#:declare equiv? (expr/c test-equiv-ctc #:name test-equiv-name)
#`(test-->>/procs red e1 (list e2 ...) apply-reduction-relation/dummy-second-value #t equiv?.c #,(get-srcloc stx))]))
(define (apply-reduction-relation/dummy-second-value red arg)
(values (apply-reduction-relation red arg) #f))
@ -2194,6 +2211,38 @@
(λ (v1) (fprintf (current-error-port) " actual: ~v\n" v1))
got))))])))
(define-syntax (test-->>∃ stx)
(syntax-parse stx
[(form (~optional (~seq #:steps steps) #:defaults ([steps.c #'1000]))
relation
start:expr
goal)
#:declare relation (expr/c #'reduction-relation?
#:name "reduction relation expression")
#:declare goal (expr/c #'(or/c (-> any/c any/c) (not/c procedure?))
#:name "goal expression")
#:declare steps (expr/c #'(or/c natural-number/c +inf.0)
#:name "steps expression")
#`(test-->>∃/proc relation.c start goal.c steps.c #,(get-srcloc stx))]))
(define (test-->>∃/proc relation start goal steps srcinfo)
(let ([result (traverse-reduction-graph
relation
start
#:goal (if (procedure? goal) goal (λ (x) (equal? goal x)))
#:steps steps)])
(inc-tests)
(when (search-failure? result)
(print-failed srcinfo)
(inc-failures)
(begin
(fprintf (current-error-port) "no reachable term ~a ~a"
(if (procedure? goal) "satisfying" "equal to")
goal)
(when (search-failure-cutoff? result)
(fprintf (current-error-port) " (but some terms were not unexplored)"))
(newline (current-error-port))))))
(define-syntax (test-predicate stx)
(syntax-case stx ()
[(_ p arg)
@ -2287,6 +2336,7 @@
test-equal
test-->>
test-->
test-->>∃ (rename-out [test-->>∃ test-->>E])
test-predicate
test-results)

31
collects/redex/redex.scrbl
View File

@ -1143,6 +1143,37 @@ step, using @racket[pred-expr] to determine equivalence.
(test-results)]
@defform/subs[(test-->>∃ option ... rel-expr start-expr spec-expr)
([option (code:line #:steps steps-expr)])
#:contracts ([rel-expr reduction-relation?]
[start-expr any/c]
[spec-expr (or/c (-> any/c any/c)
(not/c procedure?))]
[steps-expr (or/c natural-number/c +inf.0)])]{
Tests to see if the term @racket[start-expr] reduces according to the reduction
relation @racket[rel-expr] to a term specified by @racket[goal-expr] in
@racket[steps-expr] or fewer steps (default 1,000). The specification
@racket[goal-expr] may be either a predicate on terms or a term itself.
}
@defidform[test-->>E]{An alias for @racket[test-->>∃].}
@examples[
#:eval redex-eval
(define-language L
(n natural))
(define succ-mod8
(reduction-relation
L
(--> n ,(modulo (add1 (term n)) 8))))
(test-->>∃ succ-mod8 6 2)
(test-->>∃ succ-mod8 6 even?)
(test-->>∃ succ-mod8 6 8)
(test-->>∃ #:steps 6 succ-mod8 6 5)
(test-results)]
@defform[(test-predicate p? e)]{
Tests to see if the value of @racket[e] matches the predicate @racket[p?].
}

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

@ -42,6 +42,7 @@
test-equal
test-->>
test-->
test-->>∃ (rename-out [test-->>∃ test-->>E])
test-predicate
test-results)

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

@ -2155,7 +2155,7 @@
(test (capture-output (test--> R #:equiv mod2=? 7 1 0) (test-results))
"One test passed.\n")
(test (capture-output (test--> R #:equiv mod2=? 7 1) (test-results))
#rx"FAILED tl-test.(?:.+):[0-9.]+\nexpected: 1\n actual: 8\n actual: 7\n1 test failed \\(out of 1 total\\).\n"))
#rx"FAILED tl-test\\.(?:.+):[0-9.]+\nexpected: 1\n actual: 8\n actual: 7\n1 test failed \\(out of 1 total\\).\n"))
(let-syntax ([test-bad-equiv-arg
(λ (stx)
@ -2165,9 +2165,47 @@
(test-form (reduction-relation empty-language (--> any any))
#:equiv 1 2)
"no error raised")
#rx"expected argument of type")]))])
#rx"tl-test\\.(?:.+).*broke the contract")]))])
(test-bad-equiv-arg test-->)
(test-bad-equiv-arg test-->>))
(let ()
(capture-output (test-results))
(define-language L)
(define 1+
(reduction-relation
L
(--> number ,(add1 (term number)))))
(define (equal-to-7 x) (= x 7))
(test (capture-output (test-->>∃ #:steps 5 1+ 0 equal-to-7))
#rx"^FAILED .*\nno reachable term satisfying #<procedure:equal-to-7> \\(but some terms were not unexplored\\)\n$")
(test (capture-output (test-->>∃ 1+ 0 7)) "")
(test (capture-output (test-->>E 1+ 0 7)) "")
(test (capture-output (test-->>∃ #:steps +inf.0 1+ 0 7)) "")
(test (capture-output (test-->>∃ 1+ 0 equal-to-7)) "")
(define identity
(reduction-relation
L
(--> any any)))
(test (capture-output (test-->>∃ identity 0 1))
#rx"^FAILED .*\nno reachable term equal to 1\n$")
(test (capture-output (test-results)) "2 tests failed (out of 6 total).\n")
(test (with-handlers ([exn:fail:contract? exn-message])
(test-->>∃ 1+ 0 (λ (x y) x)))
#rx"tl-test\\.(?:.+).*broke the contract.*goal expression")
(test (with-handlers ([exn:fail:contract? exn-message])
(test-->>∃ 1 0 1))
#rx"tl-test\\.(?:.+).*broke the contract.*reduction relation expression")
(test (with-handlers ([exn:fail:contract? exn-message])
(test-->>∃ #:steps 1.1 1+ 0 1))
#rx"tl-test\\.(?:.+).*broke the contract.*steps expression"))
(print-tests-passed 'tl-test.ss)