On this page:

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—including caching the results of side-conditions—so after a pattern has matched a given term, Redex assumes that the pattern will always match the term.

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

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


(redex-match lang pattern term-expr)

(redex-match lang pattern)
If redex-match is given a term-expr, it matches the pattern (in the language) against the result of term-expr. The result is #f or a list of match structures describing the matches (see match? and match-bindings).

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


> (redex-match nums
               (+ AE_1 AE_1)
               (term (+ (+ 1 2) 3)))



(redex-match? lang pattern any)

(redex-match? lang pattern)
Like redex-match, but returns only a boolean indicating whether the match was successful.

> (define-language nums
    (AE number
        (+ AE AE)))
> (redex-match? nums
                (+ AE_1 AE_2)
                (term (+ (+ 1 2) 3)))


> (redex-match? nums
                (+ AE_1 AE_1)
                (term (+ (+ 1 2) 3)))



(match? val)  boolean?

  val : any/c
Determines whether a value is a match structure.


(match-bindings m)  (listof bind?)

  m : match?
Returns a list of bind structs that binds the pattern variables in this match.


(struct bind (name exp)
    #:extra-constructor-name make-bind)
  name : symbol?
  exp : any/c
Instances of this struct are returned by redex-match. Each bind associates a name with an s-expression from the language, or a list of such s-expressions if the corresponding name clause is followed by an ellipsis. Nested ellipses produce nested lists.


(caching-enabled?)  boolean?

(caching-enabled? on?)  void?
  on? : boolean?
When this parameter is #t (the default), Redex caches the results of pattern matching, metafunction, and judgment-form evaluation. There is a separate cache for each pattern, metafunction, and judgment-form; when one fills (see set-cache-size!), Redex evicts all of the entries in that cache.

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.


(set-cache-size! size)  void?

  size : positive-integer?
Changes the size of the per-pattern, per-metafunction and per-judgment-form caches.

The default size is 63.


(check-redundancy)  boolean?

(check-redundancy check?)  void?
  check? : boolean?
Ambiguous patterns can slow down Redex’s pattern matching implementation significantly. To help debug such performance issues, set the check-redundancy parameter to #t. A true value causes Redex to, at runtime, report any redundant matches that it encounters.

Changed in version 1.9 of package redex-lib: Corrected spelling error, from check-redudancy to check-redundancy