On this page:
test-equal
test-->>
test-->
test-->>∃
test-->>E
test-judgment-holds
test-predicate
test-match
test-no-match
test-results
default-equiv
make-coverage
coverage?
relation-coverage
covered-cases
generate-term
redex-enum
redex-index
redex-check
depth-dependent-order?
redex-generator
counterexample
exn:  fail:  redex:  test
check-reduction-relation
check-metafunction
default-attempt-size
default-check-attempts
redex-pseudo-random-generator
exn:  fail:  redex:  generation-failure?
8.12

4.6 Testing🔗ℹ

syntax

(test-equal e1 e2 option)

 
option = #:equiv pred-expr
  | 
 
  pred-expr : (-> any/c any/c any/c)
Tests to see if e1 is equal to e2, using pred-expr as the comparison. It defaults to (default-equiv).

Examples:
> (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
Tests to see if the term e1-expr, reduces to the terms e2-expr under rel-expr, using pred-expr to determine equivalence.

If #:pred is specified, it is applied to each reachable term until one of the terms fails to satisfy the predicate (i.e., the predicate returns #f). If that happens, then the test fails and a message is printed with the term that failed to satisfy the predicate.

The procedure supplied after #:equiv is always passed the result of reducing the expression as its first argument and (one of) the expected result(s) as its second argument.

This test uses apply-reduction-relation*, so it does not terminate when the resulting reduction graph is infinite, although it does terminate if there are cycles in the (finite) graph.

If #:cycles-ok is not supplied then any cycles detected are treated as a test failure. If a pred-expr is supplied, then it is used to compare the expected and actual results. If it isn’t supplied, then (default-equiv) is used.

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
Tests to see if the term e1-expr, reduces to the terms e2-expr in a single rel-expr step, using pred-expr to determine equivalence (or (default-equiv) if pred-expr isn’t specified).

Examples:
> (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)
Tests to see if the term start-expr reduces according to the reduction relation rel-expr to a term specified by goal-expr in steps-expr or fewer steps (default 1,000). The specification goal-expr may be either a predicate on terms or a term itself.

syntax

test-->>E

An alias for test-->>∃.

Examples:
> (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)
In the first form, tests to see if (judgment-form-or-relation pat/term ...) holds. In the second form, tests to see if the result of derivation-expr is a derivation and, if so, that it is derivable using modeless-judgment-form.

syntax

(test-predicate p? e)

Tests to see if the value of e matches the predicate p?.

syntax

(test-match lang-id pat e)

Tests to see if the value of e matches, via redex-match?, the pattern pat.

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

Tests to see if the value of e does not match, via redex-match?, the pattern pat.

Examples:
> (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?

Prints out how many tests passed and failed, and resets the counters so that next time this function is called, it prints the test results for the next round of tests.

parameter

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

(default-equiv equiv)  void?
  equiv : (-> any/c any/c any/c)
The value of this parameter is used as the default value of the equivalence predicates for test-equal, test-->, and test-->>.

It defaults to (lambda (lhs rhs) (alpha-equivalent? (default-language) lhs rhs)).

syntax

(make-coverage subject)

 
subject = metafunction
  | relation-expr
Constructs a structure (recognized by coverage?) to contain per-case test coverage of the supplied metafunction or reduction relation. Use with relation-coverage and covered-cases.

procedure

(coverage? v)  boolean?

  v : any/c
Returns #t for a value produced by make-coverage and #f for any other.

parameter

(relation-coverage)  (listof coverage?)

(relation-coverage tracked)  void?
  tracked : (listof coverage?)
Redex populates the coverage records in tracked (default null), counting the times that tests exercise each case of the associated metafunction and relations.

procedure

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

  c : coverage?
Extracts the coverage information recorded in c, producing an association list mapping names (or source locations, in the case of metafunctions or unnamed reduction-relation cases) to application counts.

Examples:
> (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
Generates terms in a number of different ways:
  • 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))

The argument size-expr bounds the height of the generated term (measured as the height of its parse tree).

The optional keyword argument attempt-num-expr (default 1) provides coarse grained control over the random decisions made during generation; increasing attempt-num-expr tends to increase the complexity of the result. For example, the absolute values of numbers chosen for integer patterns increase with attempt-num-expr.

The random generation process does not actively consider the constraints imposed by side-condition or _!_ patterns; instead, it uses a “guess and check” strategy in which it freely generates candidate terms then tests whether they happen to satisfy the constraints, repeating as necessary. The optional keyword argument retries-expr (default 100) bounds the number of times that generate-term retries the generation of any pattern. If generate-term is unable to produce a satisfying term after retries-expr attempts, it raises an exception recognized by exn:fail:redex:generation-failure?.

syntax

(redex-enum language pattern)

Constructs an enumeration that produces terms that match the given pattern, or #f if it cannot build an enumeration (which happens if the given pattern contains side-conditions).

It constructs a two-way enumeration only in some cases. The pattern must be unambiguous and there are other technical shortcomings of the implementation as well that cause the result to be a one-way enumeration in some situations.

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

Computes the index for an occurrence of the given term in the enumerator corresponding to the given pattern or returns #f if there is no enumerator.

This is useful when the pattern is ambiguous as you might still learn of an index that corresponds to the term even though the enumeration that redex-enum produces is a one-way enumeration.

Examples:
> (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)
Searches for a counterexample to property-expr, interpreted as a predicate universally quantified over the pattern variables bound by the pattern(s) in template. redex-check constructs and tests a candidate counterexample by choosing a random term t based on template and then evaluating property-expr using the match-bindings produced by matching t against pattern. The form of template controls how t is generated:
  • 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.

redex-check generates at most attempts-expr (default (default-check-attempts)) random terms in its search. The size and complexity of these terms tend to increase with each failed attempt. The #:attempt-size keyword determines the rate at which terms grow by supplying a function that bounds term size based on the number of failed attempts (see generate-term’s size-expr argument). By default, the bound grows according to the default-attempt-size function.

When print?-expr produces any non-#f value (the default), redex-check prints the test outcome on current-output-port. When print?-expr produces #f, redex-check prints nothing, instead
  • 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.

The optional #:prepare keyword supplies a function that transforms each generated example before redex-check checks property-expr. This keyword may be useful when property-expr takes the form of a conditional, and a term chosen freely from the grammar is unlikely to satisfy the conditional’s hypothesis. In some such cases, the prepare keyword can be used to increase the probability that an example satisfies the hypothesis.

The #:retries keyword behaves identically as in generate-term, controlling the number of times the generation of any pattern will be reattempted. It can’t be used together with #:satisfying.

If keep-going?-expr produces any non-#f value, redex-check will stop only when it hits the limit on the number of attempts showing all of the errors it finds. This argument is allowed only when print?-expr is not #f.

When passed a metafunction or reduction relation via the optional #:source argument, redex-check distributes its attempts across the left-hand sides of that metafunction/relation by using those patterns, rather than pattern, as the basis of its generation. If any left-hand side generates a term that does not match pattern, then the test input is discarded. #:source cannot be used with #:satisfying. See also check-reduction-relation and check-metafunction.

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

Changed in version 1.10 of package redex-lib: Instead of raising an error, redex-check now discards test cases that don’t match the given pattern when using #:source.

parameter

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

(depth-dependent-order? depth-dependent)  void?
  depth-dependent : (or/c boolean? 'random)
 = 'random
Toggles whether or not Redex will dynamically adjust the chance that more recursive clauses of judgment forms or metafunctions are chosen earlier when attempting to generate terms with forms that use #:satisfying. If it is #t, Redex favors more recursive clauses at lower depths and less recursive clauses at depths closer to the limit, in an attempt to generate larger terms. When it is #f, all clause orderings have equal probability above the bound. By default, it is 'random, which causes Redex to choose between the two above alternatives with equal probability.

syntax

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

 
satisfying = (judgment-form-id pattern ...)
  | (metafunction-id pattern ...) = pattern
 
  size-expr : natural-number/c
WARNING: redex-generator is a new, experimental form, and its API may change.

Returns a thunk that, each time it is called, either generates a random s-expression based on satisfying or fails to (and returns #f). The terms returned by a particular thunk are guaranteed to be distinct.

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))])
> (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
Produced by redex-check, check-reduction-relation, and check-metafunction when testing falsifies a property.

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
Raised by redex-check, check-reduction-relation, and check-metafunction when testing a property raises an exception. The exn:fail:redex:test-source component contains the exception raised by the property, and the exn:fail:redex:test-term component contains the term that induced the exception.

syntax

(check-reduction-relation relation property kw-args ...)

 
kw-arg = #:attempts attempts-expr
  | #:retries retries-expr
  | #:print? print?-expr
  | #:attempt-size attempt-size-expr
  | #:prepare prepare-expr
 
  property : (-> any/c any/c)
  attempts-expr : natural-number/c
  retries-expr : natural-number/c
  print?-expr : any/c
  attempt-size-expr : (-> natural-number/c natural-number/c)
  prepare-expr : (-> any/c any/c)
Tests relation as follows: for each case of relation, check-reduction-relation generates attempts random terms that match that case’s left-hand side and applies property to each random term.

Only the primary pattern of each case’s left-hand side is considered. If there are where clauses or side-conditions (or anything else from the red-extras portion of the grammar), they are ignored.

This form provides a more convenient notation for
(redex-check L any (property (term any))
             #:attempts (* n attempts)
             #:source relation)
when relation is a relation on L with n rules.

syntax

(check-metafunction metafunction property kw-args ...)

 
kw-arg = #:attempts attempts-expr
  | #:retries retries-expr
  | #:print? print?-expr
  | #:attempt-size attempt-size-expr
  | #:prepare prepare-expr
 
  property : (-> (listof any/c) any/c)
  attempts-expr : natural-number/c
  retries-expr : natural-number/c
  print?-expr : any/c
  attempt-size-expr : (-> natural-number/c natural-number/c)
  prepare-expr : (-> (listof any/c) (listof any/c))
Like check-reduction-relation but for metafunctions. check-metafunction calls property with lists containing arguments to the metafunction. Similarly, prepare-expr produces and consumes argument lists.

Only the primary pattern of each case’s left-hand side is considered. If there are where clauses or side-conditions (or anything else from the metafunction-extras portion of the grammar), they are ignored.

Examples:
> (define-language empty-lang)
> (define-metafunction empty-lang
    Σ : number ... -> number
    [(Σ) 0]
    [(Σ number) number]
    [(Σ number_1 number_2) ,(+ (term number_1) (term number_2))]
    [(Σ number_1 number_2 ...) (Σ number_1 (Σ number_2 ...))])
> (check-metafunction Σ (λ (args)
                          (printf "trying ~s\n" args)
                          (equal? (apply + args)
                                  (term (Σ ,@args))))
                      #:attempts 2)

trying ()

trying ()

trying (0)

trying (0)

trying (2 1)

trying (0 1)

trying (0)

trying (1)

check-metafunction: no counterexamples in 8 attempts (tried 2 attempts with each clause)

The default value of the #:attempt-size argument to redex-check and the other randomized testing forms, this procedure computes an upper bound on the size of the next test case from the number of previously attempted tests n. Currently, this procedure computes the base 5 logarithm, but that behavior may change in future versions.

parameter

(default-check-attempts)  natural-number/c

(default-check-attempts attempts)  void?
  attempts : natural-number/c
Determines the default value for redex-check’s optional #:attempts argument. By default, attempts is 1,000.

generate-term and the randomized testing forms (e.g., redex-check) use the parameter generator to construct random terms. The parameter’s initial value is (current-pseudo-random-generator).

Recognizes the exceptions raised by generate-term, redex-check, etc. when those forms are unable to produce a term matching some pattern.

Debugging PLT Redex Programs

It is easy to write grammars and reduction rules that are subtly wrong. Typically such mistakes result in examples that get stuck when viewed in a traces window.

The best way to debug such programs is to find an expression that looks like it should reduce, but doesn’t, then try to find out which pattern is failing to match. To do so, use the redex-match form.

In particular, first check if the term in question matches the your system’s main non-terminal (typically the expression or program non-terminal). If it does not match, simplify the term piece by piece to determine whether the problem is in the term or the grammar.

If the term does match your system’s main non-terminal, determine by inspection which reduction rules should apply. For each such rule, repeat the above term-pattern debugging procedure, this time using the rule’s left-hand side pattern instead of the system’s main non-terminal. In addition to simplifying the term, also consider simplifying the pattern.

If the term matches the left-hand side, but the rule does not apply, then one of the rule’s side-condition or where clauses is not satisfied. Using the bindings reported by redex-match, check each side-condition expression and each where pattern-match to discover which clause is preventing the rule’s application.