4 The Redex Reference
(require redex) | package: redex-gui-lib |
The redex library provides all of the names documented here.
Alternatively, use the redex/reduction-semantics and redex/pict libraries, which provide only non-GUI functionality (i.e., everything except redex/gui), making them suitable for programs that should not depend on racket/gui/base.
4.1 Patterns
(require redex/reduction-semantics) | package: redex-lib |
This section covers Redex’s pattern language, which is used in many of Redex’s forms. Patterns are matched against terms, which are represented as S-expressions.
Pattern matching uses a cache—
In the following grammar, literal identifiers (such as any) are matched symbolically, as opposed to using the identifier’s lexical binding:
pattern | = | any | ||
| | _ | |||
| | number | |||
| | natural | |||
| | integer | |||
| | real | |||
| | string | |||
| | boolean | |||
| | variable | |||
| | (variable-except id ...) | |||
| | (variable-prefix id) | |||
| | variable-not-otherwise-mentioned | |||
| | hole | |||
| | symbol | |||
| | (name id pattern) | |||
| | (in-hole pattern pattern) | |||
| | (hide-hole pattern) | |||
| | (side-condition pattern guard-expr) | |||
| | (compatible-closure-context id) | |||
| | (compatible-closure-context id #:wrt id) | |||
| | (cross id) | |||
| | (pattern-sequence ...) | |||
| | other-literal | |||
pattern-sequence | = | pattern | ||
| | ... ; literal ellipsis | |||
| | ..._id |
The any pattern matches any term. This pattern may also be suffixed with an underscore and another identifier, in which case a match binds the full name (as if it were an implicit name pattern) and match the portion before the underscore.
The _ pattern matches any term, but does not bind _ as a name, nor can it be suffixed to bind a name.
The number pattern matches any number.
The number identifier can be suffixed with an underscore and additional characters, in which case the pattern binds the full name (as if it were an implicit name pattern) when matching the portion before the underscore. For example, the pattern
number_1
matches the same as number, but it also binds the identifier number_1 to the matching portion of a term.
When the same underscore suffix is used for multiple instances if number within a larger pattern, then the overall pattern matches only when all of the instances match the same number.
The natural pattern matches any exact non-negative integer. Like number, this pattern can be suffixed with an underscore and additional characters to create a binding.
The integer pattern matches any exact integer. Like number, this pattern can be suffixed with an underscore and additional characters to create a binding.
The real pattern matches any real number. Like number, this pattern can be suffixed with an underscore and additional characters to create a binding.
The string pattern matches any string. Like number, this pattern can be suffixed with an underscore and additional characters to create a binding.
The boolean pattern matches #true and #false (which are the same as #t and #f, respectively). Like number, this pattern can be suffixed with an underscore and additional characters to create a binding.
The variable pattern matches any symbol. Like number, this pattern can be suffixed with an underscore and additional characters to create a binding.
The variable-except pattern matches any symbol except those listed in its argument. This pattern is useful for ensuring that reserved words in the language are not accidentally captured by variables.
The variable-prefix pattern matches any symbol that begins with the given prefix.
The variable-not-otherwise-mentioned pattern matches any symbol except those that are used as literals elsewhere in the language.
The hole pattern matches anything when inside the first argument to an in-hole pattern. Otherwise, it matches only a hole.
The symbol pattern stands for a literal symbol that must match exactly, unless it is the name of a non-terminal in a relevant language or contains an underscore.
If symbol is a non-terminal, it matches any of the right-hand sides of the non-terminal. If the non-terminal appears twice in a single pattern, then the match is constrained to expressions that are the same, unless the pattern is part of a define-language definition or a contract (e.g., in define-metafunction, define-judgment-form, or define-relation) in which case there is no constraint. Also, the non-terminal will be bound in the expression in any surrounding side-condition patterns unless there the pattern is in a define-language definition.
If symbol is a non-terminal followed by an underscore, for example e_1, it is implicitly the same as a name pattern that matches only the non-terminal, (name e_1 e) for the example. Accordingly, repeated uses of the same name are constrained to match the same expression.
If the symbol is a non-terminal followed by _!_, for example e_!_1, it is also treated as a pattern, but repeated uses of the same pattern are constrained to be different. For example, this pattern:
(e_!_1 e_!_1 e_!_1)
matches lists of three es, but where all three of them are distinct.
If the _!_ is used under the ellipsis then the ellipsis is effectively ignored while checking to see if the es are different. For example, the pattern (e_!_1 ...) matches any sequence of es, as long as they are all distinct. Also, unlike e_1 patterns, the nesting depth of _!_ patterns do not have to be the same. For example, this pattern:
(e_!_1 ... e_!_1)
matches all sequences of es that have at least one element, as long as they are all distinct.
Unlike a _ pattern, the _!_ patterns do not bind names.
If _ names and _!_ are mixed, they are treated as separate. That is, this pattern (e_1 e_!_1) matches just the same things as (e e), but the second doesn’t bind any variables.
If the symbol otherwise has an underscore, it is an error.
The pattern (name id pattern) matches pattern and binds using it to the name id.
The (in-hole pattern pattern) pattern matches the first pattern, looking for a way to decompose the term such that the second pattern matches at some sub-expression where the hole appears while matching the first pattern.
The first pattern must be a pattern that matches with exactly one hole.
The (hide-hole pattern) pattern matches what the embedded pattern matches but if the pattern matcher is looking for a decomposition, it ignores any holes found in that pattern.
The (side-condition pattern guard-expr) pattern matches what the embedded pattern matches, and then guard-expr is evaluated. If guard-expr produces #f, the pattern fails to match, otherwise the pattern matches. Any occurrences of name in the pattern (including those implicitly present via _ patterns) are bound using term-let in guard-expr.
The (compatible-closure-context nt) pattern matches context that correspond to where the compatible closure of a relation would match. More precisely, it is a context whose shape follows the definition of nt, but allowing for a hole at each place where the definition of nt refers to itself.
For example, with this language definition:(define-language L (e ::= (λ (x) e) (e e) x) (C ::= (λ (x) C) (C e) (e C) hole) (x ::= variable-not-otherwise-mentioned)) The (compatible-closure-context nt1 #:wrt nt2) pattern similarly is a context, but it decomposes terms matching the non-terminal nt1, placing a hole at each place where an nt2 non-terminal appears.
For example, with this language definition:(define-language L (e ::= v (e e) x) (v ::= (λ (x) e)) (C ::= V (C e) (e C) hole) (V ::= (λ (x) C)) (x ::= variable-not-otherwise-mentioned)) the pattern (compatible-closure-context v #:wrt e) is equivalent to the pattern V and the pattern the pattern (compatible-closure-context e #:wrt e) is equivalent to the pattern C. More generally, leaving off the #:wrt argument is the same as using the same non-terminal twice.The (cross nt) pattern is an unfortunately-named version of compatible-closure-context that exists for backward compatibility and does not support #:wrt.
The (pattern-sequence ...) pattern matches a term list, where each pattern-sequence element matches an element of the list. In addition, if a list pattern contains an ellipsis, the ellipsis is not treated as a literal, instead it matches any number of duplicates of the pattern that came before the ellipses (including 0). Furthermore, each (name symbol pattern) in the duplicated pattern binds a list of matches to symbol, instead of a single match. (A nested duplicated pattern creates a list of list matches, etc.) Ellipses may be placed anywhere inside the row of patterns, except in the first position or immediately after another ellipses.
Multiple ellipses are allowed. For example, this pattern:
matches this term:
(term (a a))
three different ways. One where the first a in the pattern matches nothing, and the second matches both of the occurrences of a, one where each named pattern matches a single a and one where the first matches both and the second matches nothing.
If the ellipses is named (i.e., has an underscore and a name following it, like a variable may), the pattern matcher records the length of the list and ensures that any other occurrences of the same named ellipses must have the same length.
As an example, this pattern:
((name x a) ..._1 (name y a) ..._1)
only matches this term:
(term (a a))
one way, with each named pattern matching a single a. Unlike the above, the two patterns with mismatched lengths is ruled out, due to the underscores following the ellipses.
Also, like underscore patterns above, if an underscore pattern begins with ..._!_, then the lengths must be different.
Thus, with the pattern:
((name x a) ..._!_1 (name y a) ..._!_1)
and the expression
(term (a a))
two matches occur, one where x is bound to '() and y is bound to '(a a) and one where x is bound to '(a a) and y is bound to '().
The other-literal pattern stands for a literal value—
such as a number, boolean, or string— that must match exactly.
Changed in version 1.8 of package redex-lib: Non-terminals are syntactically classified
as either always producing exactly one hole or may
produce some other number of holes,
and the first argument to in-hole is allowed
to accept only patterns that produce exactly one hole.
Changed in version 1.15: Added compatible-closure-context
syntax
(redex-match lang pattern term-expr)
(redex-match lang pattern)
If redex-match has only a lang and pattern, the result is a procedure for efficiently testing whether terms match the pattern with respect to the language lang. The procedure accepts a single term and returns #f or a list of match structures describing the matches.
> (define-language nums (AE number (+ AE AE)))
> (redex-match nums (+ AE_1 AE_2) (term (+ (+ 1 2) 3))) (list (match (list (bind 'AE_1 '(+ 1 2)) (bind 'AE_2 3))))
> (redex-match nums (+ AE_1 (+ AE_2 AE_3)) (term (+ (+ 1 2) 3))) #f
> (redex-match nums (+ AE_1 AE_1) (term (+ (+ 1 2) 3))) #f
syntax
(redex-match? lang pattern any)
(redex-match? lang pattern)
> (define-language nums (AE number (+ AE AE)))
> (redex-match? nums (+ AE_1 AE_2) (term (+ (+ 1 2) 3))) #t
> (redex-match? nums (+ AE_1 AE_1) (term (+ (+ 1 2) 3))) #f
procedure
(match-bindings m) → (listof bind?)
m : match?
parameter
(caching-enabled? on?) → void? on? : boolean?
Caching should be disabled when matching a pattern that depends on values other than the in-scope pattern variables or evaluating a metafunction or judgment-form that reads or writes mutable external state.
Changed in version 1.6 of package redex-lib: Extended caching to cover judgment forms.
procedure
(set-cache-size! size) → void?
size : positive-integer?
The default size is 63.
parameter
(check-redundancy check?) → void? check? : boolean?
Changed in version 1.9 of package redex-lib: Corrected spelling error, from check-redudancy to check-redundancy
4.2 Terms
Object language expressions in Redex are written using term. It is similar to Racket’s quote (in many cases it is identical) in that it constructs lists as the visible representation of terms.
The grammar of terms is (note that an ellipsis stands for repetition unless otherwise indicated):
term | = | identifier | ||
| | (term-sequence ...) | |||
| | ,expr | |||
| | (in-hole term term) | |||
| | hole | |||
| | (mf-apply identifier term ...) | |||
| | datum | |||
term-sequence | = | term | ||
| | ,@expr | |||
| | ... ; literal ellipsis |
A term written identifier is equivalent to the corresponding symbol, unless the identifier is bound by term-let, define-term, or a pattern variable or the identifier is hole (as below).
A term written (term-sequence ...) constructs a list of the terms constructed by the sequence elements.
A term written ,expr evaluates expr and substitutes its value into the term at that point.
A term written ,@expr evaluates the expr, which must produce a list. It then splices the contents of the list into the expression at that point in the sequence.
A term written (in-hole term term) is the dual to the pattern in-hole – it accepts a context and an expression and uses plug to combine them.
A term written hole produces a hole.
A term written (mf-apply f arg ...) asserts that f is a metafunction and produces the term (f arg ...).
A term written as any other datum not listed above produces that datum. For example, (term (1 x #t)) is the same as '(1 x #t).
Term substitution and metafunction application do not occur within compound datums. For example,
is the same as '#hash((x . a)), not '#hash((x . 1)).
The term form behaves similarly to quasiquote, except for a few special forms that are recognized (listed below) and that names bound by term-let are implicitly substituted with the values that those names were bound to, expanding ellipses as in-place sublists (in the same manner as syntax-case patterns).
The optional #:lang keyword must supply an identifier bound by define-language, and adds a check that any symbol containing an underscore in term could have been bound by a pattern in the language referenced by lang-id. In practice, this means that the underscore must be preceded by a non-terminal in that language or a built-in pattern such as number. This form of term is used internally by default, so this check is applied to terms that are constructed by Redex forms such as reduction-relation and define-metafunction.
For example,
(term-let ([body '(+ x 1)] [(expr ...) '(+ - (values * /))] [((id ...) ...) '((a) (b) (c d))]) (term (let-values ([(id ...) expr] ...) body)))
evaluates to
'(let-values ([(a) +] [(b) -] [(c d) (values * /)]) (+ x 1))
It is an error for a term variable to appear in an expression with an ellipsis-depth different from the depth with which it was bound by term-let. It is also an error for two term-let-bound identifiers bound to lists of different lengths to appear together inside an ellipsis.
Symbols in a term whose names end in guillemets (French quotes) around a number (for example asdf«5000») will be modified to contain a smiley face character (for example asdf«5000☺»). This is to prevent collisions with names generated by the freshening process that binding forms use.
syntax
syntax
syntax
syntax
(term-let ([tl-pat expr] ...) body)
tl-pat = identifier | (tl-pat-ele ...) tl-pat-ele = tl-pat | tl-pat ... ; a literal ellipsis
Note that each ellipsis should be the literal symbol consisting of three dots (and the ... elsewhere indicates repetition as usual). If tl-pat is an identifier, it matches any value and binds it to the identifier, for use inside term. If it is a list, it matches only if the value being matched is a list value and only if every subpattern recursively matches the corresponding list element. There may be a single ellipsis in any list pattern; if one is present, the pattern before the ellipses may match multiple adjacent elements in the list value (possibly none).
This form is a lower-level form in Redex, and not really designed to be used directly. For let-like forms that use Redex’s full pattern matching facilities, see redex-let, redex-let*, term-match, term-match/single.
This form raises an exception recognized by exn:fail:redex? if any right-hand side does not match its left-hand side in exactly one way.
In some contexts, it may be more efficient to use term-match/single (lifted out of the context).
syntax
(redex-let* language ([pattern expression] ...) body ...+)
syntax
(define-term identifier term)
syntax
(term-match language [pattern expression] ...)
When evaluating a term-match expression, the patterns are compiled in an effort to speed up matching. Using the procedural result multiple times to avoid compiling the patterns multiple times.
syntax
(term-match/single language [pattern expression] ...)
The term-match/single form raises an exception recognized by exn:fail:redex? if no clauses match or if one of the clauses matches multiple ways.
When evaluating a term-match/single expression, the patterns are compiled in an effort to speed up matching. Using the procedural result multiple times to avoid compiling the patterns multiple times.
procedure
(variable-not-in t prefix) → symbol?
t : any/c prefix : symbol?
The variables-not-in function does not expect the symbols in vars to be distinct, but it does produce a list of distinct symbols.
procedure
(exn:fail:redex? v) → boolean?
v : any/c
4.3 Languages
syntax
(define-language lang-name non-terminal-def ... maybe-binding-spec)
non-terminal-def = (non-terminal-name ...+ ::= pattern ...+) | (non-terminal-name pattern ...+) | ((non-terminal-name ...+) pattern ...+) maybe-binding-spec =
| #:binding-forms binding-pattern ... binding-pattern = pattern | binding-pattern #:exports beta | binding-pattern #:refers-to beta | binding-pattern #:...bind (id beta beta) beta = nothing | symbol | (shadow beta-sequence ...) beta-sequence = beta | ... ; literal ellipsis
A non-terminal-def comprises one or more non-terminal names (considered aliases) followed by one or more productions.
(define-language lc-lang (e ::= (e e ...) x (λ (x ...) e)) (v ::= (λ (x ...) e)) (E ::= (v ... E e ...) hole) (x y ::= variable-not-otherwise-mentioned))
It has non-terminals: e for the expression language, x and y for variables, v for values, and E for the evaluation contexts.
Non-terminals used in define-language are not bound in side-condition patterns. Duplicate non-terminals that appear outside of the binding-forms section are not constrained to be the same unless they have underscores in them.
4.3.1 Binding Forms
Typical languages provide a mechanism for the programmer to introduce new names and give them meaning. The language forms used for this (such as Racket’s let and λ) are called binding forms.
Binding forms require special treatment from the language implementer. In Redex, this treatment consists of declaring the binding forms at the time of language definition. Explicitly declaring binding forms makes safely manipulating terms containing binding simpler and easier, eliminating the need to write operations that (explicitly) respect the binding structure of the language.
When maybe-binding-spec is provided, it declares binding specifications for certain forms in the language. The binding-pattern specification is an extension of Redex’s pattern language, allowing the keywords #:refers-to, #:exports, and #:...binds to appear nested inside a binding pattern.
The language, lc-lang, above does not declare any binding specifications, despite the clear intention of λ as a binding form. To understand the consequences of not specifying any binding forms, consider the behavior of substitution on terms of lc-lang.
Passing the #:lang argument to term allows the substitute metafunction to determine the language of its arguments.
> (term (substitute (x (λ (x) (λ (y) x))) x (y y)) #:lang lc-lang) '((y y) (λ ((y y)) (λ (y) (y y))))
This call is intended to replace all free occurrences of x with (y y) in the first argument to substitute. But, because lc-lang is missing a binding forms declaration, substitute replaces all instances of x with (y y) in the term (x (λ (x) (λ (y) x))). Note that even the x that appears in what is normally a binding position has been replaced, resulting in an ill-formed lambda expression.
In order to have substitute behave correctly when substituting over terms that contain bound variables, the language lc-lang must declare its binding specification. Consider the following simplification of the lc-lang definition, this time with a binding form declaration for λ.
(define-language lc-bind (e ::= (e e) x (λ (x) e)) (v ::= (λ (x) e)) (x y ::= variable-not-otherwise-mentioned) #:binding-forms (λ (x) e #:refers-to x))
Just like Racket’s λ, in lc-bind all instances of the argument variable in the body of the lambda refer to the argument. In a binding declaration, this is specified using the #:refers-to keyword. Now the previous example has the right behavior.
> (term (substitute (x (λ (x) (λ (y) x))) x (y y)) #:lang lc-bind) '((y y) (λ (x«0») (λ (y«1») x«0»)))
Note that sometimes substitute changes the names of the bound identifiers, in this case replacing the x and y with identifiers that have « and » in their names.
The #:refers-to declaration says that, in a λ term, the e subterm has the name from the x subterm in scope.
4.3.2 Multiple Variables in a Single Scope
To generalize to the version of λ in lc-lang, we need to cope with multiple variables at once. And in order to do that, we must handle the situation where some of the names are the same. Redex’s binding support offers only one option for this, namely taking the variables in order, using the keyword shadow. It also allows us to specify the binding structure for let:
(define-language lc-bind+let (e ::= x number (λ (x ...) e) (e e) (let ([x e] ...) e)) (x ::= variable-not-otherwise-mentioned) #:binding-forms (λ (x ...) e #:refers-to (shadow x ...)) (let ([x e_x] ...) e_body #:refers-to (shadow x ...)))
This #:binding-forms declaration says that the subterm e of the λ expression refers to all of the binders in λ. Similarly, the e_body refers to all of the binders in the let expression.
> (term (substitute (let ([x 5] [y x]) (y x)) x z) #:lang lc-bind+let) '(let ((x«2» 5) (y«3» z)) (y«3» x«2»))
The intuition behind the name of the shadow form can be seen in the following example:
> (term (substitute (let ([x 1] [y x] [x 3]) x) x z) #:lang lc-bind+let) '(let ((x«4» 1) (y«5» z) (x«6» 3)) x«4»)
Because the lc-bind+let language does not require that all binders in its let form be distinct from one another, the binding forms specification must declare what happens when there is a conflict. The shadow form specifies that duplicate binders will be shadowed by earlier binders in its list of arguments. (Of course, if we were interested in modelling Racket’s let form, we’d want that term to be malformed syntax.)
It is possible to have multiple uses of #:refers-to in a single binding specification. For example, consider a language with a letrec form.
(define-language lc-bind+letrec (e ::= x number (λ (x ...) e) (e e) (let ([x e] ...) e) (letrec ([x e] ...) e)) (x ::= variable-not-otherwise-mentioned) #:binding-forms (λ (x ...) e #:refers-to (shadow x ...)) (let ([x e_x] ...) e_body #:refers-to (shadow x ...)) (letrec ([x e_x] ...) #:refers-to (shadow x ...) e_body #:refers-to (shadow x ...)))
In this binding specification the subterms corresponding to both ([x e_x] ...) and e_body refer to the bound variables (shadow x ...).
> (term (substitute (letrec ([x x]) x) x y) #:lang lc-bind+letrec) '(letrec ((x«7» x«7»)) x«7»)
> (term (substitute (letrec ([x (λ (a) (y a))] [y (λ (b) (z b))] [z a]) (x 7)) a (λ (x) 5)) #:lang lc-bind+letrec)
'(letrec ((x«8» (λ (a«11») (y«9» a«11»)))
(y«9» (λ (b«12») (z«10» b«12»)))
(z«10» (λ (x) 5)))
(x«8» 7))
4.3.3 Ellipses in Binding Forms
Some care must be taken when writing binding specifications that match patterns with ellipses. If a pattern symbol is matched underneath ellipses, it may only be mentioned under the same number of ellipses. Consider, for example, a language with Racket’s let-values binding form.
(define-language lc-bind+values (e ::= x number (λ (x ...) e) (e e) (values e ...) (let-values ([(x ...) e] ...) e)) (x ::= variable-not-otherwise-mentioned) #:binding-forms (λ (x ...) e #:refers-to (shadow x ...)) (let-values ([(x ...) e_x0] ...) e_body #:refers-to (shadow (shadow x ...) ...)))
In the binding specification for the let-values form, the bound variable, x, occurs only under a single ellipsis, thus when it is mentioned in a #:refers-to clause it is restricted to be mentioned only underneath a single ellipsis. Therefore the body of the let-values form must refer to (shadow (shadow x ...) ...) rather than (shadow x ... ...).
4.3.4 Compound Forms with Binders
So far, the nonterminals mentioned in #:refers-to have always stood directly for variables that appear in the terms. But sometimes the variables are down inside some piece of the term, or only some of the variables are relevant. The #:exports clause can be used to handle such situations.
When a binding form with an #:exports clause is mentioned, the names brought into scope are determined by recursively examining everything mentioned by that #:exports clause. Consider the following version of the lc-bind language with lists that allows for pattern matching in binding positions.
(define-language lc-bind+patterns (e ::= x number (λ (p) e) (e e) (list e ...)) (x ::= variable-not-otherwise-mentioned) (p ::= (listp p ...) x) #:binding-forms (λ (p) e #:refers-to p) (listp p ...) #:exports (shadow p ...))
In this language functions accept patterns as arguments, therefore all variables mentioned in a pattern in binding position should be bound in the body of the function. A call to the substitute metafunction shows this behavior.
> (term (substitute (x (λ ((listp w (listp x y) z)) (list z y x w))) x u) #:lang lc-bind+patterns)
'(u
(λ ((listp w«13» (listp x«14» y«15») z«16»)) (list z«16» y«15» x«14» w«13»)))
The use of the #:exports clause in the binding specification for lc-bind+patterns allows the use of nested binding patterns seen in the example. More precisely, each p may itself be a pattern that mentions any number of bound variables.
4.3.5 Binding Repetitions
In some situations, the #:exports and #:refers-to keywords are not sufficiently expressive to be able to describe the binding structure of different parts of a repeated sequence relate to each other. For example, consider the let* form. Its shape is the same as let, namely (let* ([x e] ...) e), but the binding structure is different.
In a let* form, each variable is accessible to each of the es that follow it, with all of the variables available in the body (the final e). With #:exports, we can build an expression form that has a structure like that, but we must write syntax that nests differently than let*.
(define-language lc-bind+awkward-let* (e ::= (let*-awk c e) natural x (+ e ...)) (x ::= variable-not-otherwise-mentioned) (c ::= (clause x e c) ()) #:binding-forms (let*-awk c e #:refers-to c) (clause x e c #:refers-to x) #:exports (shadow x c))
The let*-awk form binds like Racket’s let*, with each clause’s variable being active for the subsequent ones, but the syntax is different with extra nesting inside the clauses:
> (term (substitute (let*-awk (clause x y (clause y x ())) (+ x y z)) x 1) #:lang lc-bind+awkward-let*) '(let*-awk (clause x«17» y (clause y«18» x«17» ())) (+ x«17» y«18» z))
> (term (substitute (let*-awk (clause x y (clause y x ())) (+ x y z)) y 2) #:lang lc-bind+awkward-let*) '(let*-awk (clause x«19» 2 (clause y«20» x«19» ())) (+ x«19» y«20» z))
In order to get the same syntax as Racket’s let*, we need to use the #:...bind binding pattern annotation. A #:...bind can appear wherever a ... might appear, and it has the same function, namely indicating a repetition of the preceding pattern. In addition, however it comes with three extra pieces that follow the #:...bind form that describe how the binding structure inside the repetition is handled. The first part is a name that can be used by a #:refers-to outside of the repetition to indicate all of the exported variables of the sequence. The middle piece indicates the variables from a specific repetition of the ellipsis are exported to all subsequent repetitions of the ellipsis. The last piece is a beta that moves backwards through the sequence, indicating what is exported from the last repetition of the sequence to the one before, from the one before to the one before that, and then finally from the first one to the export of the entire sequence (as named by the identifier in the first position).
So, in this example, we use #:...bind to express the scope of let*.
(define-language lc-bind+let* (e ::= (let* ([x e] ...) e) natural x (+ e ...)) (x ::= variable-not-otherwise-mentioned) #:binding-forms (let* ([x e] #:...bind (clauses x (shadow clauses x))) e_body #:refers-to clauses))
It says that the name of the exported variables from the entire sequence is clauses, which means that all of the variable exported from the sequence in the second position of the let* bind variables in the body (thanks to the last #:refers-to in the example). The x in the second position following the #:...bind says that x is in scope for each of the subsequent [x e] elements of the sequence. The final (shadow clauses x) says that the variables in a subsequent clauses are exported by the current one, as well as x, which then is exported by the entire sequence.
> (term (substitute (let* ([x y] [y x]) (+ x y z)) x 1) #:lang lc-bind+let*) '(let* ((x«22» y) (y«21» x«22»)) (+ x«22» y«21» z))
> (term (substitute (let* ([x y] [y x]) (+ x y z)) y 2) #:lang lc-bind+let*) '(let* ((x«24» 2) (y«23» x«24»)) (+ x«24» y«23» z))
syntax
syntax
syntax
syntax
(define-extended-language extended-lang base-lang non-terminal-def ... maybe-binding-spec)
non-terminal-def = (non-terminal-name ...+ ::= pattern ...+) | (non-terminal-name pattern ...+) | ((non-terminal-name ...+) pattern ...+) maybe-binding-spec =
| #:binding-forms binding-declaration ...
(define-extended-language lc-num-lang lc-lang (e ::= .... ; extend the previous `e' non-terminal number +) (v ::= .... ; extend the previous `v' non-terminal number +))
extends lc-lang with two new alternatives (+ and number) for the v non-terminal, carries forward the e, E, x, and y non-terminals. Note that the meaning of variable-not-otherwise-mentioned adapts to the language where it is used, so in this case it is equivalent to (variable-except λ +) because λ and + are used as literals in this language.
The four-period ellipses indicates that the new language’s non-terminal has all of the alternatives from the original language’s non-terminal, as well as any new ones. If a non-terminal occurs in both the base language and the extension, the extension’s non-terminal replaces the originals. If a non-terminal only occurs in the base language, then it is carried forward into the extension. And, of course, define-extended-language lets you add new non-terminals to the language.
If a language has a group of multiple non-terminals defined together, extending any one of those non-terminals extends all of them.
syntax
(define-union-language L base/prefix-lang ...)
base/prefix-lang = lang-id | (prefix lang-id)
(define-language L1 (e ::= (+ e e) number)) (define-language L2 (e ::= (if e e e) true false)) (define-union-language L1-plus-L2 L1 L2)
If a language has a prefix, then all of the non-terminals from that language have the corresponding prefix in the union language. The prefix helps avoid unintended collisions between the constituent language’s non-terminals.
(define-language UT (e (e e) (λ (x) e) x)) (define-language WT (e (e e) (λ (x t) e) x) (t (→ t t) num))
(define-union-language B (ut. UT) (wt. WT))
procedure
(make-immutable-binding-hash lang [assocs]) → dict?
lang : compiled-lang? assocs : (listof pair?) = '()
Added in version 1.14 of package redex-lib.
procedure
(make-binding-hash lang [assocs]) → dict?
lang : compiled-lang? assocs : (listof pair?) = '()
Added in version 1.14 of package redex-lib.
procedure
(language-nts lang) → (listof symbol?)
lang : compiled-lang?
procedure
(compiled-lang? l) → boolean?
l : any/c
parameter
(default-language lang) → void? lang : (or/c false/c compiled-lang?)
The default-language parameter is set to the appropriate language inside judgment forms and metafunctions, and by apply-reduction-relation.
procedure
(alpha-equivalent? lang lhs rhs) → boolean?
lang : compiled-lang? lhs : any/c rhs : any/c (alpha-equivalent? lhs rhs) → boolean? lhs : any/c rhs : any/c
If the lang argument is not supplied, it defaults to the value of (default-language), which must not #f.
metafunction
(substitute val old-var new-val)
(substitute val (old-var new-val) ...)
> (define-language lc-bind (e ::= (e e) x (λ (x ...) e)) (x ::= variable-not-otherwise-mentioned) #:binding-forms (λ (x ...) e #:refers-to (shadow x ...)))
> (define-metafunction lc-bind β-reduce : (λ (x ..._1) e) e ..._1 -> e [(β-reduce (λ (x ...) e) e_x ...) (substitute e [x e_x] ...)]) > (term (β-reduce (λ (x y) (x y)) y z)) '(y z)
Note that substitute is merely a convenience metafunction. Any manually-written substitution in the correct language will also be capture-avoiding, provided that the language’s binding forms are correctly defined. However, substitute may be significantly faster.
Changed in version 1.19 of package redex-lib: Added support for simultaneous substitutions
4.4 Reduction Relations
syntax
(reduction-relation language domain codomain base-arrow reduction-case ... shortcuts)
domain =
| #:domain pattern codomain =
| #:codomain pattern base-arrow =
| #:arrow base-arrow-name reduction-case = (arrow-name pattern term red-extras ...) red-extras = rule-name | (fresh fresh-clause ...) | (side-condition racket-expression) | (where pattern term) | (where/hidden pattern term) | (where/error pattern term) | (bind pattern term) | (bind/hidden pattern term) | (judgment-holds (judgment-form-id pat/term ...)) | (judgment-holds (relation-id term ...)) | (side-condition/hidden racket-expression) shortcuts =
| with shortcut ... shortcut =
[(old-arrow-name pattern term) (new-arrow-name identifier identifier)] rule-name = identifier | string | (computed-name racket-expression) fresh-clause = var | ((var1 ...) (var2 ...)) pat/term = pattern | term
The optional domain and codomain clauses provide contracts for the relation. If the codomain is not present, but the domain is, then the codomain is expected to be the same as the domain.
The arrow-name in each reduction-case clause is either base-arrow-name (default -->) or an arrow name defined by shortcuts (described below). In either case, the pattern refers to language and binds variables in the corresponding term. Following the pattern and term can be the name of the reduction rule and declarations of fresh variables and side-conditions.
For example, the expression
(reduction-relation lc-lang (--> (in-hole c_1 ((λ (variable_i ...) e_body) v_i ...)) (in-hole c_1 ,(foldl lc-subst (term e_body) (term (v_i ...)) (term (variable_i ...)))) beta-v))
defines a reduction relation for the lc-lang grammar.
A rule’s name (used in typesetting, the stepper, traces, and apply-reduction-relation/tag-with-names) can be given as a literal (an identifier or a string) or as an expression that computes a name using the values of the bound pattern variables (much like the rule’s right-hand side). Some operations require literal names, so a rule definition may provide both a literal name and a computed name. In particular, only rules that include a literal name may be replaced using extend-reduction-relation, used as breakpoints in the stepper, and selected using render-reduction-relation-rules. The output of apply-reduction-relation/tag-with-names, traces, and the stepper prefers the computed name, if it exists. Typesetting a rule with a computed name shows the expression that computes the name only when the rule has no literal name or when it would not typeset in pink due to with-unquote-rewriters in the context; otherwise, the literal name (or nothing) is shown.
Fresh variable clauses generate variables that do not occur in the term being reduced. If the fresh-clause is a variable, that variable is used both as a binding in the term and as the prefix for the freshly generated variable. (The variable does not have to be a non-terminal in the language of the reduction relation.)
The second form of fresh-clauses generates a sequence of variables. In that case, the ellipses are literal ellipses; that is, you must actually write ellipses in your rule. The variable var1 is like the variable in first case of a fresh-clause; namely it is used to determine the prefix of the generated variables and it is bound in the right-hand side of the reduction rule, but unlike the single-variable fresh clause, it is bound to a sequence of variables. The variable var2 is used to determine the number of variables generated and var2 must be bound by the left-hand side of the rule.
The expressions within side-condition clauses and side-condition/hidden clauses are collected with and and used as guards on the case being matched. The argument to each side-condition should be a Racket expression, and the pattern variables in the pattern are bound in that expression. A side-condition/hidden clause is the same as a side-condition clause, except that the condition is not rendered when typesetting via redex/pict.
Each where clause acts as a side condition requiring a successful pattern match, and it can bind pattern variables in the side-conditions (and where clauses) that follow and in the metafunction result.
A where/hidden clause is the same as a where clause, but the clause is not rendered when typesetting via redex/pict.
The where/error clause clause is like where, except that a failure to match is an error and, if multiple matches are possible, the right-hand side must produce the same result for each of the different matches (in the sense of alpha-equivalent? using the language that this reduction relation is defined with).
Each judgment-holds clause acts like a where clause, where the left-hand side pattern incorporates each of the patterns used in the judgment form’s output positions.
Each shortcut clause defines arrow names in terms of base-arrow-name and earlier shortcut definitions. The left- and right-hand sides of a shortcut definition are identifiers, not patterns and terms. These identifiers need not correspond to non-terminals in language and if they do, that correspondence is ignored (more precisely, the shortcut is not restricted only to terms matching the non-terminal).
For example, this expression
(reduction-relation lc-num-lang (==> ((λ (variable_i ...) e_body) v_i ...) ,(foldl lc-subst (term e_body) (term (v_i ...)) (term (variable_i ...)))) (==> (+ number_1 ...) ,(apply + (term (number_1 ...)))) with [(--> (in-hole c_1 a) (in-hole c_1 b)) (==> a b)])
defines reductions for the λ-calculus with numbers, where the ==> shortcut is defined by reducing in the context c.
A fresh clause in reduction-case defined by shortcut refers to the entire term, not just the portion matched by the left-hand side of shortcut’s use.
Changed in version 1.14 of package redex-lib: Added the #:codomain clause.
syntax
(extend-reduction-relation reduction-relation language more ...)
If the original reduction-relation has a rule with the same name as one of the rules specified in the extension, the old rule is removed.
procedure
(union-reduction-relations r ...) → reduction-relation?
r : reduction-relation?
procedure
r : reduction-relation?
syntax
(compatible-closure reduction-relation lang non-terminal)
In the below example, r is intended to calculate a boolean or. Since r does not recursively break apart its input, it will not reduce subexpressions within a larger non-matching expression t.
(define-language unary-arith [e ::= Z (S e) (+ e e)])
(define addition-without-context (reduction-relation unary-arith #:domain e (--> (+ (S e_1) e_2) (+ e_1 (S e_2))) (--> (+ Z e) e)))
(define nested-example (term (+ (+ (S Z) (S Z)) (+ (S Z) (S Z)))))
> (apply-reduction-relation addition-without-context nested-example) '()
The compatible-closure operator allows us to close addition-without-context over all nested e contexts and then we can use it to find the sum.
(define addition-compat-closure (compatible-closure addition-without-context unary-arith e))
> (apply-reduction-relation* addition-compat-closure nested-example) '((S (S (S (S Z)))))
syntax
(context-closure reduction-relation lang pattern)
Continuing the example in the documentation for compatible-closure, one might find that there are too many reductions that can take place. The original example, in fact, reduces to two different terms in a single step.
> (apply-reduction-relation addition-compat-closure nested-example) '((+ (+ (S Z) (S Z)) (+ Z (S (S Z)))) (+ (+ Z (S (S Z))) (+ (S Z) (S Z))))
If we wanted to force an order of evaluation, requiring that we evaluate the left side of the addition before moving on to the right, we can do that by limiting the context where the addition is performed. Here is one definition of a context that does that limitation.
> (apply-reduction-relation (context-closure addition-without-context unary-arith-E E) nested-example) '((+ (+ Z (S (S Z))) (+ (S Z) (S Z))))
procedure
(reduction-relation? v) → boolean?
v : any/c
procedure
(apply-reduction-relation r t) → (listof any/c)
r : (or/c reduction-relation? IO-judgment-form?) t : any/c
procedure
(apply-reduction-relation/tag-with-names r t) → (listof (list/c (or/c #f string?) any/c)) r : (or/c reduction-relation? IO-judgment-form?) t : any/c
procedure
(apply-reduction-relation* r t [ #:all? all #:cache-all? cache-all? #:stop-when stop-when] #:error-on-multiple? error-on-multiple?) → (listof any/c) r : (or/c reduction-relation? IO-judgment-form?) t : any/c all : boolean? = #f cache-all? : boolean? = (or all? (current-cache-all?)) stop-when : (-> any/c any) = (λ (x) #f) error-on-multiple? : boolean?
If the cache-all? argument is #t, then apply-reduction-relation* keeps a cache of all visited terms when traversing the graph and does not revisit any of them. This cache can, in some cases, use a lot of memory, so it is off by default and the cycle checking happens by keeping track only of the current path it is traversing through the reduction graph.
The stop-when argument controls the stopping criterion. Specifically, it is called with each term that apply-reduction-relation* encounters. If it ever returns a true value (anything except #f), then apply-reduction-relation* considers the term to be irreducible (and so returns it and does not try to reduce it further).
If error-on-multiple? is #t, then an error is signalled if any of the terms reduce to more than one other term.
Changed in version 1.18 of package redex-lib: Added error-on-multiple?.
parameter
(current-cache-all? cache-all?) → void? cache-all? : boolean?
> (define-language empty-lang)
> (define R (reduction-relation empty-lang (--> 0 1) (--> 0 2) (--> 2 3) (--> 3 3))) > (apply-reduction-relation R 0) '(2 1)
> (apply-reduction-relation* R 0) '(1)
syntax
syntax
syntax
4.5 Other Relations
syntax
(define-metafunction language metafunction-contract [(name pattern ...) term metafunction-extras ...] ...)
metafunction-contract =
|
id : pattern-sequence ... -> range maybe-pre-condition maybe-post-condition maybe-pre-condition = #:pre term |
maybe-post-condition = #:post term |
range = pattern | pattern or range | pattern ∨ range | pattern ∪ range metafunction-extras = (side-condition racket-expression) | (side-condition/hidden racket-expression) | (where pat term) | (where/hidden pat term) | (where/error pat term) |
(judgment-holds (judgment-form-id pat/term ...)) |
(judgment-holds (relation-id term ...)) | (clause-name name) | or term
The contract, if present, is matched against every input to the metafunction and, if the match fails, an exception is raised. If a metavariable is repeated in a contract, it does not require the terms to be equal, unless there is an underscore subscript (i.e., the binding works like it does in define-language, not how it works in the patterns in the left-hand sides of the metafunction clauses).
If present, the term inside the maybe-pre-condition is evaluated after a successful match to the input pattern in the contract (with any variables from the input contract bound). If it returns #f, then the input contract is considered to not have matched and an error is also raised. When a metafunction returns, the expression in the maybe-post-condition is evaluated (if present), with any variables from the input or output contract bound.
The side-condition, hidden-side-condition, where, where/hidden, and where/error clauses behave as in the reduction-relation form.
The resulting metafunction raises an exception recognized by exn:fail:redex? if no clauses match or if one of the clauses matches multiple ways (and that leads to different results for the different matches).
The side-condition extra is evaluated after a successful match to the corresponding argument pattern. If it returns #f, the clause is considered not to have matched, and the next one is tried. The side-condition/hidden extra behaves the same, but is not typeset.
The where and where/hidden extra are like side-condition and side-condition/hidden, except the match guards the clause. The where/error extra is like where, except that the pattern must match.
The judgment-holds clause is like side-condition and where, except the given judgment or relation must hold for the clause to be taken.
The clause-name is used only when typesetting. See metafunction-cases.
The or clause is used to define piecewise conditional metafunctions. In particular, if any of the where or side-condition clauses fail, then evaluation continues after an or clause, treating the term that follows as the result (subject to any subsequent where clauses or side-conditions. This construction is equivalent to simply duplicating the left-hand side of the clause, once for each or expression, but signals to the typesetting library to use a large left curly brace to group the conditions in the or.
For example, here are two equivalent definitions of a biggest metafunction that typeset differently:
> (define-metafunction lc-lang biggest : natural natural -> natural [(biggest natural_1 natural_2) natural_2 (side-condition (< (term natural_1) (term natural_2)))] [(biggest natural_1 natural_2) natural_1]) > (render-metafunction biggest)
> (define-metafunction lc-lang biggest : natural natural -> natural [(biggest natural_1 natural_2) natural_2 (side-condition (< (term natural_1) (term natural_2))) or natural_1]) > (render-metafunction biggest)
Note that metafunctions are assumed to always return the same results for the same inputs, and their results are cached, unless caching-enabled? is set to #f. Accordingly, if a metafunction is called with the same inputs twice, then its body is only evaluated a single time.
As an example, these metafunctions finds the free variables in an expression in the lc-lang above:
(define-metafunction lc-lang free-vars : e -> (x ...) [(free-vars (e_1 e_2 ...)) (∪ (free-vars e_1) (free-vars e_2) ...)] [(free-vars x) (x)] [(free-vars (λ (x ...) e)) (- (free-vars e) (x ...))])
The first argument to define-metafunction is the grammar (defined above). Following that are three cases, one for each variation of expressions (e in lc-lang). The free variables of an application are the free variables of each of the subterms; the free variables of a variable is just the variable itself, and the free variables of a λ expression are the free variables of the body, minus the bound parameters.
Here are the helper metafunctions used above.
(define-metafunction lc-lang ∪ : (x ...) ... -> (x ...) [(∪ (x_1 ...) (x_2 ...) (x_3 ...) ...) (∪ (x_1 ... x_2 ...) (x_3 ...) ...)] [(∪ (x_1 ...)) (x_1 ...)] [(∪) ()]) (define-metafunction lc-lang - : (x ...) (x ...) -> (x ...) [(- (x ...) ()) (x ...)] [(- (x_1 ... x_2 x_3 ...) (x_2 x_4 ...)) (- (x_1 ... x_3 ...) (x_2 x_4 ...)) (side-condition (not (memq (term x_2) (term (x_3 ...)))))] [(- (x_1 ...) (x_2 x_3 ...)) (- (x_1 ...) (x_3 ...))])
Note the side-condition in the second case of -. It ensures that there is a unique match for that case. Without it, (term (- (x x) x)) would lead to an ambiguous match.
Changed in version 1.4 of package redex-lib: Added #:post conditions.
Changed in version 1.5: Added or clauses.
syntax
(define-metafunction/extension f language metafunction-contract [(g pattern ...) term metafunction-extras ...] ...)
For example, define-metafunction/extension may be used to extend the free-vars function above to the forms introduced by the language lc-num-lang.
(define-metafunction/extension free-vars lc-num-lang free-vars-num : e -> (x ...) [(free-vars-num number) ()] [(free-vars-num (+ e_1 e_2)) (∪ (free-vars-num e_1) (free-vars-num e_2))])
syntax
(in-domain? (metafunction-name term ...))
syntax
(define-judgment-form language mode-spec contract-spec invariant-spec rule rule ...)
mode-spec =
| #:mode (form-id pos-use ...) contract-spec =
| #:contract (form-id pattern-sequence ...) invariant-spec =
| #:inv term pos-use = I | O rule =
[premise ... dashes rule-name conclusion] |
[conclusion premise ... rule-name] conclusion = (form-id pat/term ...) premise = (judgment-form-id pat/term ...) maybe-ellipsis | (relation-id pat/term ...) maybe-ellipsis | (where pattern term) | (where/hidden pattern term) | (where/error pattern term) | (side-condition term) | (side-condition/hidden term) rule-name =
| string | non-ellipsis-non-dashes-var pat/term = pattern | term maybe-ellipsis =
| ... dashes = --- | ---- | ----- | etc.
If a mode-spec appears, each rule must be such that its premises can be evaluated left-to-right without “guessing” values for any of their pattern variables. Redex checks this property using mode-spec declaration, which partitions positions into inputs I and outputs O. Output positions in conclusions and input positions in premises must be terms; input positions in conclusions and output positions in premises must be patterns. The rule-names are used by build-derivations and by render-judgment-form.
If a mode-spec is not present, Redex cannot compute a derivation for the judgment form, instead it can check that a given derivation is valid according to the rules.
When the optional contract-spec declaration is present, Redex dynamically checks that the terms flowing through these positions match the provided patterns, raising an exception recognized by exn:fail:redex? if not. The term in the optional invariant-spec is evaluated after the output positions have been computed and the contract has matched successfully, with variables (that have underscores) from the contract bound; a result of #f is considered to be a contract violation and an exception is raised.
> (define-language nats (n ::= z (s n)))
> (define-judgment-form nats #:mode (sum I I O) #:contract (sum n n n) [----------- "zero" (sum z n n)] [(sum n_1 n_2 n_3) ------------------------- "add1" (sum (s n_1) n_2 (s n_3))])
> (judgment-holds (sum (s (s z)) (s z) (s (s (s z))))) #t
> (judgment-holds (sum (s (s z)) (s z) (s (s (s n))))) #t
> (judgment-holds (sum (s (s z)) (s z) (s (s (s (s n)))))) #f
> (judgment-holds (sum (s (s z)) (s z) (s (s (s n)))) n) '(z)
> (judgment-holds (sum (s (s z)) (s z) (s (s (s (s n))))) n) '()
> (judgment-holds (sum (s (s z)) (s z) (s (s (s n)))) (s n)) '((s z))
> (define-judgment-form nats #:mode (sumr O O I) #:contract (sumr n n n) [------------ "z" (sumr z n n)] [(sumr n_1 n_2 n_3) -------------------------- "s" (sumr (s n_1) n_2 (s n_3))]) > (judgment-holds (sumr n_1 n_2 (s (s z))) (n_1 n_2)) '(((s (s z)) z) ((s z) (s z)) (z (s (s z))))
> (define-extended-language nat-exprs nats (e ::= (+ e e) n))
> (define-judgment-form nat-exprs #:contract (same-exp e e) [(sum n_1 n_2 n_3) -------------------------- "add" (same-exp (+ n_1 n_2) n_3)] [-------------- "refl" (same-exp e e)] [(same-exp e_1 e_2) (same-exp e_2 e_3) ------------------ "trans" (same-exp e_1 e_3)] [(same-exp e_2 e_1) ------------------ "sym" (same-exp e_1 e_2)] [(same-exp e_1 e_2) ---------------------------------- "compat-l" (same-exp (+ e_1 e_3) (+ e_2 e_3))] [(same-exp e_1 e_2) ---------------------------------- "compat-r" (same-exp (+ e_3 e_1) (+ e_3 e_2))])
> (define same-exp-derivation (let* ([one `(s z)] [two `(s ,one)] [three `(s ,two)] [four `(s ,three)] [five `(s ,four)] [six `(s ,five)]) (derivation `(same-exp (+ ,four ,two) (+ ,one (+ ,two ,three))) "trans" (list (derivation `(same-exp (+ ,four ,two) ,six) "add" (list (car (build-derivations (sum ,four ,two n))))) (derivation `(same-exp ,six (+ ,one (+ ,two ,three))) "sym" (list (derivation `(same-exp (+ ,one (+ ,two ,three)) ,six) "trans" (list (derivation `(same-exp (+ ,one (+ ,two ,three)) (+ ,one ,five)) "compat-r" (list (derivation `(same-exp (+ ,two ,three) ,five) "add" (list (car (build-derivations (sum ,two ,three n))))))) (derivation `(same-exp (+ ,one ,five) ,six) "add" (list (car (build-derivations (sum ,one ,five n)))))))))))))
> (parameterize ([pretty-print-columns 20]) (derivation->pict nat-exprs same-exp-derivation))
> (judgment-holds same-exp same-exp-derivation) #t
The premises must be in the same order in the derivation struct’s subs field as they appear in the definition of the judgment form.
> (define-judgment-form nats #:mode (le I I) #:contract (le n n) [-------- (le z n)] [(le n_1 n_2) -------------------- (le (s n_1) (s n_2))])
> (define-metafunction nats pred : n -> n or #f [(pred z) #f] [(pred (s n)) n])
> (define-judgment-form nats #:mode (gt I I) #:contract (gt n n) [(where n_3 (pred n_1)) (le n_2 n_3) ---------------------- (gt n_1 n_2)]) > (judgment-holds (gt (s (s z)) (s z))) #t
> (judgment-holds (gt (s z) (s z))) #f
A rule’s side-condition and side-condition/hidden premises are similar to those in reduction-relation and define-metafunction, except that they do not implicitly unquote their right-hand sides. In other words, a premise of the form (side-condition term) is close to the premise (where #t term), except it does not typeset with the “#t = ”, as that would and it holds whenever the expression evaluates to any non #f value (not just #t).
> (define-judgment-form nats #:mode (even I) #:contract (even n) [-------- "evenz" (even z)] [(even n) ---------------- "even2" (even (s (s n)))])
> (define-judgment-form nats #:mode (all-even I) #:contract (all-even (n ...)) [(even n) ... ------------------ (all-even (n ...))]) > (judgment-holds (all-even (z (s (s z)) z))) #t
> (judgment-holds (all-even (z (s (s z)) (s z)))) #f
> (define-language vertices (v a b c))
> (define-judgment-form vertices #:mode (edge I O) #:contract (edge v v) [(edge a b)] [(edge b c)])
> (define-judgment-form vertices #:mode (path I I) #:contract (path v v) [---------- (path v v)] [(path v_2 v_1) -------------- (path v_1 v_2)] [(edge v_1 v_2) (path v_2 v_3) -------------- (path v_1 v_3)])
> (judgment-holds (path a c))
"typing-rules.rkt" —
defines a type system in a way that supports mechanized typesetting. When a typing judgment form can be given a mode, it can also be encoded as a metafunction using where clauses as premises, but Redex cannot typeset that encoding as inference rules. "sos.rkt" —
defines an SOS-style semantics in a way that supports mechanized typesetting. "multi-val.rkt" —
defines a judgment form that serves as a multi-valued metafunction.
(collection-file-path «filename.rkt» "redex" "examples" "define-judgment-form")
Note that current-traced-metafunctions also traces judgment forms and is helpful when debugging.
syntax
(define-extended-judgment-form language judgment-form-id mode-spec contract-spec invariant-spec rule ...)
The mode specification in this judgment form and the original must be the same.
syntax
(define-overriding-judgment-form language judgment-form-id mode-spec contract-spec invariant-spec rule ...)
The mode-spec, contract-spec, invariant-spec, and rules are as in define-judgment-form.
The mode specification in this judgment form and the original must be the same.
syntax
(judgment-holds judgment-or-relation)
(judgment-holds judgment-or-relation term) (judgment-holds judgment-form-id derivation-expr)
judgment-or-relation = (judgment-form-id pat/term ...) | (relation-id pat/term ...)
In its second form, produces a list of terms by instantiating the supplied term template with each satisfying assignment of pattern variables. In the second case, if a relation is supplied, there are no pattern variables, so the result is either a list with one element or the empty list.
In both of the first two forms, any given judgment form must have a mode.
In its third form, the judgment-form-id must not have a mode, and the derivation-expr must produce a derviation struct. The result of judgment-holds is #t when the derivation is valid, according to the rules of the judgment form, and #f otherwise. Note that the premises of the derivation must appear in the same order as the premises in the definition of the judgment form.
> (judgment-holds (sum (s (s z)) (s z) n)) #t
> (judgment-holds (sum (s (s z)) (s z) n) n) '((s (s (s z))))
syntax
(build-derivations judgment-or-relation)
> (build-derivations (even (s (s z))))
(list
(derivation
'(even (s (s z)))
"even2"
(list (derivation '(even z) "evenz" '()))))
struct
(struct derivation (term name subs) #:extra-constructor-name make-derivation) term : any/c name : (or/c string? #f) subs : (listof derivation?)
The term field holds an s-expression based rendering of the conclusion of the derivation, the name field holds the name of the clause with term as the conclusion, and subs contains the sub-derivations.
See also build-derivations.
syntax
syntax
syntax
(define-relation language relation-contract [(name pattern ...) term ... metafunction-extras ...] ...)
relation-contract =
| form-id ⊂ pattern x ... x pattern | form-id ⊆ pattern × ... × pattern
The contract specification for a relation restricts the patterns that can be used as input to a relation. For each argument to the relation, there should be a single pattern, using x or × to separate the argument contracts.
> (define-language types ((τ σ) int num (τ → τ)))
> (define-relation types subtype ⊆ τ × τ [(subtype int num)] [(subtype (τ_1 → τ_2) (σ_1 → σ_2)) (subtype σ_1 τ_1) (subtype τ_2 σ_2)] [(subtype τ τ)]) > (judgment-holds (subtype int num)) #t
> (judgment-holds (subtype (int → int) (num → num))) #f
> (judgment-holds (subtype (num → int) (num → num))) #t
procedure
(judgment-form? v) → boolean?
v : any/c
procedure
(IO-judgment-form? v) → boolean?
v : any/c
parameter
(current-traced-metafunctions) → (or/c 'all (listof symbol?))
(current-traced-metafunctions traced-metafunctions) → void? traced-metafunctions : (or/c 'all (listof symbol?))
The tracing looks just like the tracing done by the racket/trace library, except that the first column printed by each traced call indicate if this call to the metafunction is cached. Specifically, a c is printed in the first column if the result is just returned from the cache and a space is printed if the metafunction or judgment call is actually performed.
Defaults to '().
> (define-judgment-form nats #:mode (odd I) #:contract (odd n) [-------- "oddsz" (odd (s z))] [(odd n) ---------------- "odd2" (odd (s (s n)))])
> (parameterize ([current-traced-metafunctions '(odd)]) (judgment-holds (odd (s (s (s z))))))
>(odd (s (s (s z))))
> (odd (s z))
< ((odd (s z)))
<((odd (s (s (s z)))))
#t
> (parameterize ([current-traced-metafunctions '(odd)]) (judgment-holds (odd (s (s (s (s (s z))))))))
>(odd (s (s (s (s (s z))))))
c> (odd (s (s (s z))))
< ((odd (s (s (s z)))))
<((odd (s (s (s (s (s z)))))))
#t
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