From 23d583fe0d48dc8d1d3b6cc9b1529e3d578c9e87 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Sun, 26 Jan 2014 19:57:51 -0600 Subject: [PATCH] add default-equiv and some examples in docs --- .../redex-doc/redex/scribblings/ref.scrbl | 54 ++++++++++++++++--- pkgs/redex-pkgs/redex-lib/redex/HISTORY.txt | 7 +++ .../redex/private/reduction-semantics.rkt | 9 ++-- .../redex-lib/redex/reduction-semantics.rkt | 3 +- 4 files changed, 62 insertions(+), 11 deletions(-) diff --git a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl index 2f8e6023f3..60ef66f8f1 100644 --- a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl +++ b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl @@ -1544,12 +1544,42 @@ Defaults to @racket['()]. @declare-exporting[redex/reduction-semantics redex] -@defform/subs[(test-equal e1 e2) - ([option (code:line #:equiv ~)]) - #:contracts ([~ (-> any/c any/c boolean)])]{ +@defform/subs[(test-equal e1 e2 option) + ([option (code:line #:equiv pred-expr) + (code:line)]) + #:contracts ([pred-expr (-> any/c any/c any/c)])]{ -Tests to see if @racket[e1] is equal to @racket[e2], modulo @racket[~]. -} +Tests to see if @racket[e1] is equal to @racket[e2], using @racket[pred-expr] as +the comparison. It defaults to @racket[(default-equiv)]. + +@examples[#:eval redex-eval + + (define-language L + (bt ::= + empty + (node any bt bt)) + (lt ::= + empty + (node any lt empty))) + + (define-metafunction L + linearize/a : bt lt -> lt + [(linearize/a empty lt) lt] + [(linearize/a (node any_val bt_left bt_right) lt) + (node any_val (linearize/a bt_left (linearize/a bt_right lt)) empty)]) + + (define-metafunction L + linearize : bt -> lt + [(linearize bt) (linearize/a bt empty)]) + + (test-equal (term (linearize empty)) + (term empty)) + (test-equal (term (linearize (node 1 + (node 2 empty empty) + (node 3 empty empty)))) + (term (node 1 (node 2 (node 3 empty empty) empty) empty))) + (test-results) +]} @defform/subs[(test-->> rel-expr option ... e1-expr e2-expr ...) ([option (code:line #:cycles-ok) @@ -1577,7 +1607,8 @@ 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. +then it is used to compare the expected and actual results. If it +isn't supplied, then @racket[(default-equiv)] is used. } @defform/subs[(test--> rel-expr option ... e1-expr e2-expr ...) @@ -1589,7 +1620,8 @@ then it is used to compare the expected and actual results. Tests to see if the term @racket[e1-expr], reduces to the terms @racket[e2-expr] in a single @racket[rel-expr] -step, using @racket[pred-expr] to determine equivalence. +step, using @racket[pred-expr] to determine equivalence (or +@racket[(default-equiv)] if @racket[pred-expr] isn't specified). } @examples[ @@ -1653,6 +1685,14 @@ counters so that next time this function is called, it prints the test results for the next round of tests. } +@defparam[default-equiv equiv (-> any/c any/c any/c)]{ + The value of this parameter is used as the default value + of the equivalence predicates + for @racket[test-equal], @racket[test-->], and @racket[test-->>]. + + It defaults to @racket[equal?]. +} + @defform/subs[(make-coverage subject) ([subject (code:line metafunction) (code:line relation-expr)])]{ diff --git a/pkgs/redex-pkgs/redex-lib/redex/HISTORY.txt b/pkgs/redex-pkgs/redex-lib/redex/HISTORY.txt index a3d29517aa..7df8cc34cb 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/HISTORY.txt +++ b/pkgs/redex-pkgs/redex-lib/redex/HISTORY.txt @@ -1,3 +1,10 @@ +v6.1 + + * added #:equiv option to test-equal + + * added default-equiv + + v6.0 * Added an enumerator for patterns. For example, here's how to get diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt index f7d6830cad..4b2a6dc75c 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt @@ -2267,7 +2267,7 @@ (define-for-syntax test-equiv-name "#:equiv argument") (define-for-syntax test-equiv-default - #'equal?) + #'(default-equiv)) (define-syntax (test-->> stx) (syntax-parse stx @@ -2391,10 +2391,12 @@ (eprintf " ~v does not hold for\n ~v\n" pred arg))) +(define default-equiv (make-parameter equal?)) + (define-syntax (test-equal stx) (syntax-case stx () [(_ e1 e2) - #`(test-equal/proc e1 e2 #,(get-srcloc stx) equal?)] + #`(test-equal/proc e1 e2 #,(get-srcloc stx) #,test-equiv-default)] [(_ e1 e2 #:equiv ~equal?) #`(test-equal/proc e1 e2 #,(get-srcloc stx) ~equal?)])) @@ -2472,7 +2474,8 @@ test--> test-->>∃ (rename-out [test-->>∃ test-->>E]) test-predicate - test-results) + test-results + default-equiv) (provide language-nts diff --git a/pkgs/redex-pkgs/redex-lib/redex/reduction-semantics.rkt b/pkgs/redex-pkgs/redex-lib/redex/reduction-semantics.rkt index c292e58cc1..b29fa0b7c0 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/reduction-semantics.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/reduction-semantics.rkt @@ -90,4 +90,5 @@ [covered-cases (-> coverage? (listof (cons/c string? natural-number/c)))] [redex-pseudo-random-generator (parameter/c pseudo-random-generator?)] [default-attempt-size attempt-size/c] - [default-check-attempts (parameter/c natural-number/c)]) + [default-check-attempts (parameter/c natural-number/c)] + [default-equiv (parameter/c (-> any/c any/c any/c))])