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

Adds a term-equivalence predicate to the test--> and test-->> forms.

Browse Source 
svn: r18767
This commit is contained in:
Casey Klein 2010-04-09 00:08:39 +00:00
parent 26b3cb7eb2
commit 52c6b4ef15
3 changed files with 104 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -8,7 +8,8 @@
"error.ss"
mzlib/trace
(lib "list.ss")
(lib "etc.ss"))
(lib "etc.ss")
(for-syntax syntax/parse))
(require (for-syntax (lib "name.ss" "syntax")
"loc-wrapper-ct.ss"
@ -2064,22 +2065,41 @@
'#,(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-syntax (test-->> stx)
(syntax-case stx ()
[(_ red #:cycles-ok e1 e2 ...)
#`(test-->>/procs red e1 (list e2 ...) apply-reduction-relation*/cycle? #t #,(get-srcloc stx))]
[(_ red e1 e2 ...)
#`(test-->>/procs red e1 (list e2 ...) apply-reduction-relation*/cycle? #f #,(get-srcloc 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"))
...
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)))]))
(define-syntax (test--> stx)
(syntax-case stx ()
[(_ red e1 e2 ...)
#`(test-->>/procs red e1 (list e2 ...) apply-reduction-relation/dummy-second-value #t #,(get-srcloc stx))]))
(syntax-parse stx
[(form red:expr
(~optional (~seq #:equiv equiv?:expr)
#:defaults ([equiv? #'equal?]))
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)))]))
(define (apply-reduction-relation/dummy-second-value red arg)
(values (apply-reduction-relation red arg) #f))
(define (test-->>/procs red arg expected apply-red cycles-ok? srcinfo)
(define (test-->>/procs red arg expected apply-red cycles-ok? equiv? srcinfo)
(unless (reduction-relation? red)
(error 'test--> "expected a reduction relation as first argument, got ~e" red))
(let-values ([(got got-cycle?) (apply-red red arg)])
@ -2092,7 +2112,7 @@
(print-failed srcinfo)
(fprintf (current-error-port) "found a cycle in the reduction graph\n")]
[else
(unless (set-equal? expected got)
(unless (set-equal? expected got equiv?)
(inc-failures)
(print-failed srcinfo)
(for-each
@ -2102,8 +2122,8 @@
(λ (v1) (fprintf (current-error-port) " actual: ~v\n" v1))
got))])))
(define (set-equal? s1 s2)
(define (⊆ s1 s2) (andmap (λ (x1) (member x1 s2)) s1))
(define (set-equal? s1 s2 equiv?)
(define (⊆ s1 s2) (andmap (λ (x1) (memf (λ (x) (equiv? x1 x)) s2)) s1))
(and (⊆ s1 s2)
(⊆ s2 s1)))

50
collects/redex/redex.scrbl
View File

@ -1062,20 +1062,52 @@ all non-GUI portions of Redex) and also exported by
Tests to see if @scheme[e1] is equal to @scheme[e2].
}
@defform/subs[(test-->> reduction-relation maybe-cycles e1 e2 ...)
([cycles (code:line) #:cycles-ok])]{
@defform/subs[(test-->> rel-expr option ... e1-expr e2-expr ...)
([option (code:line #:cycles-ok)
(code:line #:equiv pred-expr)])
#:contracts ([rel-expr reduction-relation?]
[pred-expr (--> any/c any/c any/c)]
[e1-expr any/c]
[e2-expr any/c])]{
Tests to see if the value of @scheme[e1] (which should be a term),
reduces to the @scheme[e2]s under @scheme[reduction-relation]
(using @scheme[apply-reduction-relation*], so it may not terminate).
Tests to see if the term @scheme[e1-expr],
reduces to the terms @scheme[e2-expr] under @scheme[rel-expr],
using @scheme[pred-expr] to determine equivalence. This test uses
@scheme[apply-reduction-relation*], so it does not terminate
when the resulting reduction graph is infinite.
}
@defform[(test--> reduction-relation e1 e2 ...)]{
@defform/subs[(test--> rel-expr option ... e1-expr e2-expr ...)
([option (code:line #:equiv pred-expr)])
#:contracts ([rel-expr reduction-relation?]
[pred-expr (--> any/c any/c anyc)]
[e1-expr any/c]
[e2-expr any/c])]{
Tests to see if the value of @scheme[e1] (which should be a term),
reduces to the @scheme[e2]s in a single step, under @scheme[reduction-relation]
(using @scheme[apply-reduction-relation]).
Tests to see if the term @scheme[e1-expr],
reduces to the terms @scheme[e2-expr] in a single @scheme[rel-expr]
step, using @scheme[pred-expr] to determine equivalence.
}
@examples[
#:eval redex-eval
(define-language L
(i integer))
(define R
(reduction-relation
L
(--> i i)
(--> i ,(add1 (term i)))))
(define (mod2=? i j)
(= (modulo i 2) (modulo j 2)))
(test--> R #:equiv mod2=? 7 1)
(test--> R #:equiv mod2=? 7 1 0)
(test-results)]
@defform[(test-predicate p? e)]{
Tests to see if the value of @scheme[e] matches the predicate @scheme[p?].

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

@ -1896,5 +1896,35 @@
"One test passed.\n")
(test (capture-output (test--> red (term (x)) (term x) (term ((x)))) (test-results))
"One test passed.\n"))
(let ()
(define-language L
(i integer))
(define R
(reduction-relation
L
(--> i i)
(--> i ,(add1 (term i)))))
(define (mod2=? i j)
(= (modulo i 2) (modulo j 2)))
(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.ss:[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)
(syntax-case stx ()
[(_ test-form)
#'(test (with-handlers ([exn:fail:contract? exn-message])
(test-form (reduction-relation empty-language (--> any any))
#:equiv 1 2)
"no error raised")
#rx"expected argument of type")]))])
(test-bad-equiv-arg test-->)
(test-bad-equiv-arg test-->>))
(print-tests-passed 'tl-test.ss))