diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss index 67d8a79288..aa16494ca5 100644 --- a/collects/redex/private/reduction-semantics.ss +++ b/collects/redex/private/reduction-semantics.ss @@ -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))) diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index 5ccef04d8d..cc273a9f87 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -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?]. diff --git a/collects/redex/tests/tl-test.ss b/collects/redex/tests/tl-test.ss index f362953079..3fc208f7dd 100644 --- a/collects/redex/tests/tl-test.ss +++ b/collects/redex/tests/tl-test.ss @@ -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))