syntax (test-equal e1 e2 option)

option   =   #:equiv pred-expr     |

pred-expr   :   (-> any/c any/c any/c)

> (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)

Both tests passed.

syntax (test-->> rel-expr option ... e1-expr e2-expr ...)

option   =   #:cycles-ok     |   #:equiv pred-expr     |   #:pred pred-expr

rel-expr   :   (or/c reduction-relation? IO-judgment-form?)    pred-expr   :   (-> any/c any)    e1-expr   :   any/c    e2-expr   :   any/c

syntax (test--> rel-expr option ... e1-expr e2-expr ...)

option   =   #:equiv pred-expr

rel-expr   :   (or/c reduction-relation? IO-judgment-form?)    pred-expr   :   (-> any/c any/c any/c)    e1-expr   :   any/c    e2-expr   :   any/c

> (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)

FAILED :10.0 expected: 1   actual: 8   actual: 7

> (test--> R #:equiv mod2=? 7 1 0)

> (test-results)

1 test failed (out of 2 total).

syntax (test-->>∃ option ... rel-expr start-expr goal-expr)

option   =   #:steps steps-expr

rel-expr   :   (or/c reduction-relation? IO-judgment-form?)    start-expr   :   any/c    goal-expr   :   (or/c (-> any/c any/c)       (not/c procedure?))    steps-expr   :   (or/c natural-number/c +inf.0)

syntax test-->>E

> (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)

FAILED :17.0 term 8 not reachable from 6

> (test-->>∃ #:steps 6 succ-mod8 6 5)

FAILED :18.0 term 5 not reachable from 6 (within 6 steps)

> (test-results)

2 tests failed (out of 4 total).

syntax (test-judgment-holds (judgment-form-or-relation pat/term ...))

(test-judgment-holds modeless-judgment-form derivation-expr)

syntax (test-predicate p? e)

syntax (test-match lang-id pat e)

> (define-language L     (n natural))

> (test-match L n (term 1))

> (test-match L n (term #t))

FAILED :22.0   did not match pattern "n": #t

> (test-results)

1 test failed (out of 2 total).

syntax (test-no-match lang-id pat e)

> (define-language L     (n natural))

> (test-no-match L n (term 1))

FAILED :25.0   did match pattern "n": 1

> (test-no-match L n (term #t))

> (test-results)

1 test failed (out of 2 total).

procedure (test-results) → void?

parameter (default-equiv) → (-> any/c any/c any/c)

(default-equiv equiv) → void?

equiv : (-> any/c any/c any/c)

syntax (make-coverage subject)

subject   =   metafunction     |   relation-expr

procedure (coverage? v) → boolean?

v : any/c

parameter (relation-coverage) → (listof coverage?)

(relation-coverage tracked) → void?

tracked : (listof coverage?)

procedure (covered-cases c) → (listof (cons/c string? natural-number/c))

c : coverage?

> (define-language empty-lang)

> (define-metafunction empty-lang     [(plus number_1 number_2)      ,(+ (term number_1) (term number_2))])

> (define equals     (reduction-relation      empty-lang      (--> (+) 0 "zero")      (--> (+ number) number)      (--> (+ number_1 number_2 number ...)           (+ (plus number_1 number_2)              number ...)           "add")))

> (let ([equals-coverage (make-coverage equals)]         [plus-coverage (make-coverage plus)])     (parameterize ([relation-coverage (list equals-coverage                                             plus-coverage)])       (apply-reduction-relation* equals (term (+ 1 2 3)))       (values (covered-cases equals-coverage)               (covered-cases plus-coverage))))

'(("#f:30:0" . 1) ("add" . 2) ("zero" . 0)) '(("#f:29:0" . 2))

syntax (generate-term from-pattern)

(generate-term from-judgment-form)

(generate-term from-metafunction)

(generate-term from-reduction-relation)

from-pattern   =   language pattern size-expr kw-args ...     |   language pattern     |   language pattern #:i-th index-expr     |   language pattern #:i-th           from-judgment-form   =   language #:satisfying (judgment-form-id pattern ...)     |   language #:satisfying (judgment-form-id pattern ...) size-expr           from-metafunction   =   language #:satisfying (metafunction-id pattern ...) = pattern     |   language #:satisfying (metafunction-id pattern ...) = pattern size-expr     |   #:source metafunction size-expr kw-args     |   #:source metafunction           from-reduction-relation   =   #:source reduction-relation-expr size-expr kw-args ...     |   #:source reduction-relation-expr           kw-args   =   #:attempt-num attempt-num-expr     |   #:retries retries-expr

size-expr   :   natural-number/c    attempt-num-expr   :   natural-number/c    retries-expr   :   natural-number/c

• from-pattern: In the first case, randomly makes an expression matching the given pattern whose size is bounded by size-expr; the second returns a function that accepts a size bound and returns a random term. Calling this function (even with the same size bound) may be more efficient than using the first case.

  Examples:

  > (define-language L     (e ::=        (e e)        (λ (x) e)        x)     (x ::= a b c))

  > (for/list ([i (in-range 10)])     (generate-term L e 3))

  '((a (λ (c) b))   ((a (λ (c) c)) a)   a   c   ((λ (c) (b b)) (λ (a) (b c)))   c   (λ (b) (λ (b) a))   c   (c a)   (c ((c a) a)))

  The #:i-th option uses an enumeration of the non-terminals in a language. If index-expr is supplied, generate-term returns the corresponding term and if it isn’t, generate-term returns a function from indices to terms.

  Example:

  > (for/list ([i (in-range 9)])     (generate-term L e #:i-th i))

  '(a (a a) (λ (a) a) b (a (a a)) (λ (b) a) c ((a a) a) (λ (c) a))

  Base type enumerations such as boolean, natural and integer are what you might expect:

  Examples:

  > (for/list ([i (in-range 10)])     (generate-term L boolean #:i-th i))

  '(#t #f #t #f #t #f #t #f #t #f)

  > (for/list ([i (in-range 10)])     (generate-term L natural #:i-th i))

  '(0 1 2 3 4 5 6 7 8 9)

  > (for/list ([i (in-range 10)])     (generate-term L integer #:i-th i))

  '(0 1 -1 2 -2 3 -3 4 -4 5)

  The real base type enumeration consists of all integers and flonums, and the number pattern consists of complex numbers with real and imaginary parts taken from the real enumeration.

  Examples:

  > (for/list ([i (in-range 20)])     (generate-term L real #:i-th i))

  '(0   +inf.0   1   -inf.0   -1   +nan.0   2   0.0   -2   5e-324   3   -5e-324   -3   1e-323   4   -1e-323   -4   1.5e-323   5   -1.5e-323)

  > (for/list ([i (in-range 20)])     (generate-term L number #:i-th i))

  '(+inf.0   0   +inf.0+inf.0i   1   0.0+inf.0i   -inf.0+inf.0i   -inf.0   0+1i   +nan.0+inf.0i   -1   0.0-inf.0i   0.0+inf.0i   +nan.0   0-1i   5e-324+inf.0i   2   0.0+nan.0i   -5e-324+inf.0i   0.0   0+2i)

  The string enumeration produces all single character strings before going on to strings with multiple characters. For each character it starts the lowercase Latin characters, then uppercase Latin, and then every remaining Unicode character. The variable enumeration is the same, except it produces symbols instead of strings.

  Examples:

  > (generate-term L string #:i-th 0)

  "a"

  > (generate-term L string #:i-th 1)

  "b"

  > (generate-term L string #:i-th 26)

  "A"

  > (generate-term L string #:i-th 27)

  "B"

  > (generate-term L string #:i-th 52)

  "\u0000"

  > (generate-term L string #:i-th 53)

  "\u0001"

  > (generate-term L string #:i-th 956)

  "μ"

  > (generate-term L variable #:i-th 1)

  'b

  > (generate-term L variable #:i-th 27)

  'B

  The variable-prefix, variable-except, and variable-not-otherwise-mentioned are defined similarly, as you expect.

  Examples:

  > (define-language L     (used ::= a b c)     (except ::= (variable-except a))     (unused ::= variable-not-otherwise-mentioned))

  > (for/list ([i (in-range 10)])     (generate-term L (variable-prefix a:) #:i-th i))

  '(a:a a:b a:c a:d a:e a:f a:g a:h a:i a:j)

  > (for/list ([i (in-range 10)])     (generate-term L except #:i-th i))

  '(b c d e f g h i j k)

  > (for/list ([i (in-range 10)])     (generate-term L unused #:i-th i))

  '(d e f g h i j k l m)

  Finally, the any pattern enumerates terms of the above base types.

  Example:

  > (for/list ([i (in-range 20)])     (generate-term L any #:i-th i))

  '(()   (())   +inf.0   (() ())   "a"   ((()))   #t   ((()) ())   a   (() . +inf.0)   0   ((()) . +inf.0)   "b"   (+inf.0)   #f   (+inf.0 ())   b   (+inf.0 . +inf.0)   +inf.0+inf.0i   (() () ()))

  In addition, all other pattern types are supported except for mismatch repeat ..._!_ patterns and side-condition patterns.

  The enumerators do not repeat terms unless the given pattern is ambiguous. Roughly speaking, the enumerator generates all possible ways that a pattern might be parsed and since ambiguous patterns have multiple ways they might be parsed, those multiple parsings turn into repeated elements in the enumeration.

  Example:

  > (for/list ([i (in-range 9)])     (generate-term L (boolean_1 ... boolean_2 ...) #:i-th i))

  '(() (#t) (#t) (#t #t) (#f) (#t #f) (#f) (#f #t) (#f #f))

  Other sources of ambiguity are in-hole and overlapping non-terminals.

  Examples:

  > (define-language L     (e ::= (e e) (λ (x) e) x)     (E ::= hole (e E) (E e))     (x ::= a b c))

  > (for/list ([i (in-range 9)])     (generate-term L (in-hole E e) #:i-th i))

  '(a   (a a)   (a a)   (a (a a))   (λ (a) a)   (a (λ (a) a))   (a a)   ((a a) a)   ((λ (a) a) a))

  > (define-language L     (overlap ::= natural integer))

  > (for/list ([i (in-range 10)])     (generate-term L overlap #:i-th i))

  '(0 0 1 1 2 -1 3 2 4 -2)

  For similar reasons, enumerations for mismatch patterns (using _!_) do not work properly when given ambiguous patterns; they may repeat elements of the enumeration.

  Examples:

  > (define-language Bad     (ambig ::= (x ... x ...)))

  > (generate-term Bad (ambig_!_1 ambig_!_1) #:i-th 4)

  '((x x) ())

  In this case, the elements of the resulting list are the same, even though they should not be, according to the pattern. Internally, the enumerator has discovered two different ways to generate ambig (one where the x comes from the first ellipses and one from the second) but those two different ways produce the same term and so the enumerator incorrectly produces (x x).

  See also redex-enum.

• from-judgment-form: Randomly picks a term that satisfies the given use of the judgment form.

  Examples:

  > (define-language L     (nat ::= Z (S nat)))

  > (define-judgment-form L     #:mode (sum I I O)     [---------------      (sum Z nat nat)]     [(sum nat_1 nat_2 nat_3)      -------------------------------      (sum (S nat_1) nat_2 (S nat_3))])

  > (for/list ([i (in-range 10)])     (generate-term L #:satisfying                    (sum nat_1 nat_2 nat_3)                    3))

  '((sum (S (S (S Z))) (S Z) (S (S (S (S Z)))))   (sum Z (S (S Z)) (S (S Z)))   (sum (S (S Z)) (S Z) (S (S (S Z))))   (sum (S (S Z)) Z (S (S Z)))   (sum (S (S Z)) (S (S Z)) (S (S (S (S Z)))))   (sum (S (S (S Z))) Z (S (S (S Z))))   (sum Z Z Z)   (sum (S (S Z)) (S Z) (S (S (S Z))))   (sum (S (S (S (S Z)))) Z (S (S (S (S Z)))))   (sum Z (S (S Z)) (S (S Z))))

• from-metafunction: The first form randomly picks a term that satisfies the given invocation of the metafunction, using techniques similar to how the from-judgment-form case works. The second form uses a more naive approach; it simply generates terms that match the patterns of the cases of the metafunction; it does not consider the results of the metafunctions, nor does it consider patterns from earlier cases when generating terms based on a particular case. The third case is like the second, except it returns a function that accepts the size and keywords arguments that may be more efficient if multiple random terms are generated.

  Examples:

  > (define-language L    (n number))

  > (define-metafunction L     [(F one-clause n) ()]     [(F another-clause n) ()])

  > (for/list ([i (in-range 10)])     (generate-term #:source F 5))

  '((one-clause 4)   (one-clause 1)   (another-clause 1)   (one-clause 1)   (another-clause 1)   (one-clause 1)   (another-clause 1)   (another-clause 0)   (one-clause 0)   (one-clause 1))

• from-reduction-relation: In the first case, generate-term randomly picks a rule from the reduction relation and tries to pick a term that satisfies its domain pattern, returning that. The second case returns a function that accepts the size and keyword arguments that may be more efficient if multiple random terms are generated.

  Examples:

  > (define-language L    (n number))

  > (for/list ([i (in-range 10)])     (generate-term      #:source      (reduction-relation       L       (--> (one-clause n) ())       (--> (another-clause n) ()))      5))

  '((another-clause 0)   (one-clause 0)   (another-clause 0)   (another-clause 1)   (one-clause 0)   (another-clause 2)   (one-clause 1)   (one-clause 2)   (one-clause 0)   (one-clause 1))

syntax (redex-enum language pattern)

> (define-language L     (e ::= (e e) x (λ (x) e))     (x ::= variable-not-otherwise-mentioned))

> (from-nat (redex-enum L e) 3886654839907963757723234276487685940)

'(λ (f) (f (f (f x))))

> (from-nat (redex-enum L e) 3886654839907963757723234276487685942)

'(c (f (f (f x))))

> (from-nat (redex-enum L e) 3886654839907963757723234276487685945)

'(((a a) a) (f (f (f x))))

> (to-nat (redex-enum L e)           (term (λ (f) ((λ (x) (f (x x)))                         (λ (x) (f (x x)))))))

68069248527054969607740967414758416542534392945933384867539062268798775005

syntax (redex-index language pattern term)

> (define-language L     (e ::= (e e) x (λ (x) e))     (x ::= variable-not-otherwise-mentioned))

> (redex-index L e                (term (λ (f) ((λ (x) (f (x x)))                              (λ (x) (f (x x)))))))

68069248527054969607740967414758416542534392945933384867539062268798775005

> (define-language L     ; e is an ambiguous non-terminal     ; because there are multiple ways to     ; parse (cons (λ (x) x) (λ (x) x))     (e ::= (e e) x (cons e e) v)     (v ::= (cons v v) (λ (x) e))     (x ::= variable-not-otherwise-mentioned))

> (redex-index L e                (term ((λ (x) (x x))                       (λ (x) (x x)))))

366600362279251777597

syntax (redex-check template property-expr kw-arg ...)

template   =   language pattern     |   language pattern #:ad-hoc     |   language pattern #:in-order     |   language pattern #:uniform-at-random p-value     |   language pattern #:enum bound     |   language #:satisfying (judgment-form-id pattern ...)     |   language #:satisfying (metafunction-id pattern ...) = pattern           kw-arg   =   #:attempts attempts-expr     |   #:source metafunction     |   #:source relation-expr     |   #:retries retries-expr     |   #:print? print?-expr     |   #:attempt-size attempt-size-expr     |   #:prepare prepare-expr     |   #:keep-going? keep-going?-expr

property-expr   :   any/c    attempts-expr   :   natural-number/c    relation-expr   :   reduction-relation?    retries-expr   :   natural-number/c    print?-expr   :   any/c    attempt-size-expr   :   (-> natural-number/c natural-number/c)    prepare-expr   :   (-> any/c any/c)

• language pattern: In this case, redex-check uses an ad hoc strategy for generating pattern. For the first 10 seconds, it uses in-order enumeration to pick terms. After that, it alternates back and forth between in-order enumeration and the ad hoc random generator. After the 10 minute mark, it switches over to using just the ad hoc random generator.

• language pattern #:ad-hoc: In this case, redex-check uses an ad hoc random generator to generate terms that match pattern.

• language pattern #:in-order: In this case, redex-check uses an enumeration of pattern, checking each t one at a time

• language pattern #:uniform-at-random p-value: that to index into an enumeration of pattern. If the enumeration is finite, redex-check picks a natural number uniformly at random; if it isn’t, redex-check uses a geometric distribution with p-value as its probability of zero to pick the number of bits in the index and then picks a number uniformly at random with that number of bits.

• language pattern #:enum bound: This is similar to #:uniform-at-random, except that Redex always picks a random natural number less than bound to index into the enumeration

• language #:satisfying (judgment-form-id pattern ...): Generates terms that match pattern and satisfy the judgment form.

• language #:satisfying (metafunction-id pattern ...) = pattern: Generates terms matching the two patterns, such that if the first is the argument to the metafunction, the second will be the result.

• returning a counterexample structure when the test reveals a counterexample,

• returning #t when all tests pass, or

• raising a exn:fail:redex:test when checking the property raises an exception.

> (define-language empty-lang)

> (random-seed 0)

> (redex-check    empty-lang    ((number_1 ...)     (number_2 ...))    (equal? (reverse (append (term (number_1 ...))                             (term (number_2 ...))))            (append (reverse (term (number_1 ...)))                    (reverse (term (number_2 ...))))))

redex-check: counterexample found after 11 attempts: ((+inf.0) (0))

> (redex-check    empty-lang    ((number_1 ...)     (number_2 ...))    (equal? (reverse (append (term (number_1 ...))                             (term (number_2 ...))))            (append (reverse (term (number_2 ...)))                    (reverse (term (number_1 ...)))))    #:attempts 200)

redex-check: no counterexamples in 200 attempts

> (let ([R (reduction-relation             empty-lang             (--> (Σ) 0)             (--> (Σ number) number)             (--> (Σ number_1 number_2 number_3 ...)                  (Σ ,(+ (term number_1) (term number_2))                     number_3 ...)))])     (redex-check      empty-lang      (Σ number ...)      (printf "~s\n" (term (number ...)))      #:attempts 3      #:source R))

() (0) (0 2) redex-check: no counterexamples in 3 attempts (tried 1 attempt with each clause)

> (redex-check    empty-lang    number    (begin      (printf "checking ~s\n" (term number))      (positive? (term number)))    #:prepare (λ (n)                (printf "preparing ~s; " n)                (add1 (abs (real-part n))))    #:attempts 3)

preparing +inf.0; checking +inf.0 preparing 0; checking 1 preparing +inf.0+inf.0i; checking +inf.0 redex-check: no counterexamples in 3 attempts

> (define-language L     (nat ::= Z (S nat)))

> (define-judgment-form L     #:mode (sum I I O)     [---------------      (sum Z nat nat)]     [(sum nat_1 nat_2 nat_3)      -------------------------------      (sum (S nat_1) nat_2 (S nat_3))])

> (redex-check L                #:satisfying                (sum nat_1 nat_2 nat_3)                (equal? (judgment-holds                         (sum nat_1 nat_2 nat_4) nat_4)                        (term (nat_3)))                #:attempts 100)

redex-check: no counterexamples in 100 attempts

> (redex-check L                #:satisfying                (sum nat_1 nat_2 nat_3)                (equal? (term nat_1) (term nat_2)))

redex-check: counterexample found after 1 attempt: (sum Z (S (S Z)) (S (S Z)))

parameter (depth-dependent-order?) → (or/c boolean? 'random)

(depth-dependent-order? depth-dependent) → void?

depth-dependent : (or/c boolean? 'random)

=  'random

syntax (redex-generator language-id satisfying size-expr)

satisfying   =   (judgment-form-id pattern ...)     |   (metafunction-id pattern ...) = pattern

size-expr   :   natural-number/c

> (define-language L     (nat ::= Z (S nat)))

> (define-judgment-form L     #:mode (sum I I O)     [---------------      (sum Z nat nat)]     [(sum nat_1 nat_2 nat_3)      -------------------------------      (sum (S nat_1) nat_2 (S nat_3))])

> (define gen-sum (redex-generator L (sum nat_1 nat_2 nat_3) 3))

> (for/list ([_ (in-range 5)])     (gen-sum))

'((sum (S (S Z)) (S Z) (S (S (S Z))))   (sum (S (S (S (S Z)))) Z (S (S (S (S Z)))))   (sum (S (S (S (S (S Z))))) Z (S (S (S (S (S Z))))))   (sum (S (S (S (S (S (S Z)))))) (S Z) (S (S (S (S (S (S (S Z))))))))   (sum    (S (S (S (S (S (S (S Z)))))))    (S (S Z))    (S (S (S (S (S (S (S (S (S Z)))))))))))

struct (struct   counterexample (term)

#:extra-constructor-name make-counterexample

#:transparent)

term : any/c

struct (struct   exn:fail:redex:test exn:fail:redex (source term)

#:extra-constructor-name make-exn:fail:redex:test)

source : exn:fail?

term : any/c