4.6 Testing
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
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
> (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
> (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)
It defaults to (lambda (lhs rhs) (alpha-equivalent? (default-language) lhs rhs)).
syntax
(make-coverage subject)
subject = metafunction | relation-expr
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))
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)
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.
> (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)
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.
> (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.
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.
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.
> (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
syntax
(redex-generator language-id satisfying size-expr)
satisfying = (judgment-form-id pattern ...) | (metafunction-id pattern ...) = pattern
size-expr : natural-number/c
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.
> (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
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)
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.
(redex-check L any (property (term any)) #:attempts (* n attempts) #:source relation)
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))
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.
> (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)
procedure
n : natural-number/c
parameter
(default-check-attempts attempts) → void? attempts : natural-number/c
parameter
(redex-pseudo-random-generator generator) → void? generator : pseudo-random-generator?
procedure
v : any/c
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.