		Search-engine friendly clone of the ACL2 documentation.

Case-match

Pattern-match

User-definable pattern-matching.

Examples:

(pattern-match
 x
 ((cons a b) ... body1 ... )
 ((three-elt-constructor a & c) ... body2 ...)
 (& default-value))

pm is a convenient abbreviation for pattern-match.

Pattern-match is similar to case-match, but the two macros interpret patterns differently. If the pattern is (a b c), case-match interprets this as a three-element list and, if the input is also a three-element list, binds the first to a, second to b, and third to c. Pattern-match, on the other hand, interprets (a b c) as the application of a constructor a to arguments b and c. Aside from this difference, pattern-match contains much the same features as case-match. See case-match for the significance of special characters such as & and !. Also see pattern-match-list, pattern-matches, and pattern-matches-list.

Usage

(pattern-match
   input
   (pattern1 declare-form condition11 condition12 ... declare-form body1)
   (pattern2 condition21 condition22 ... body2)
    ...)

In the previous invocation, pattern-match first matches the input to pattern1. If it matches, condition11, condition12, ... are evaluated using any variable bindings that pattern1 created, and using the declare form preceding them if there is one. (The declare form is primarily useful for declaring ignored variables.) If they all evaluate to non-nil, body1 is evaluated and returned with the same variable bindings and with the declare form preceding it, if any. If pattern1 does not match or any of the conditions evaluate to nil, body1 is not evaluated and pattern2 is tried, and so on. The list of patterns should be comprehensive or else end with a listing of the form (& finalbody), so that finalbody serves as a default value.

In each pattern clause the declare forms and conditions are optional. Conditions may be included without declare forms and vice versa. To distinguish declare forms from conditions we simply check whether the first item following the pattern and/or the last item before the body are declare forms; everything between the pattern and body that is not a declare form is assumed to be a condition.

Each pattern may be a variable, to be bound to the value of the input; an existing variable name prefixed by ! or a constant, the value of which is to be compared with the input value; the special symbol & which matches anything, or an application of a constructor to a number of arguments. Each constructor must have an associated macro which allows pattern-match to process it. The macro defines what is acceptable syntax, i.e. the number and type of arguments the constructor can take, the conditions under which the input matches the constructor, and the significance of the arguments. For example, cons-pattern-matcher is defined so that in a pattern match statement, the constructor cons is required to take exactly two arguments; it matches any input satisfying (consp input), and its arguments are treated as subpatterns to be matched to the car and cdr of the input, respectively.

Extensions

The pattern-match book includes built-in support for the constructors cons, list, and list*. Support may be added for user-defined constructors. Some ``special constructors'' are also supported, with less obvious behavior. raw takes one argument, which is matched to the input using case-match syntax; that is, no constructors are recognized. bind takes two arguments, one a variable symbol and one a pattern; if the pattern matches the input, then the input is bound to the variable. any compares the input to each of its arguments using equal; if any of the arguments are equal to the input then it is considered a match. force assumes that the pattern matches and makes the specified bindings without checking.

For example, the following pattern-match statement returns (1 ((1 2 . 3))):

(pattern-match (list 1 (cons 1 (cons 2 3)))
  ((cons a (bind k (raw ((a b . c))))) (list a k)))

For documentation on enabling pattern-match to recognize new constructors, see def-pattern-match-constructor and for more see constructor-pattern-match-macros.

Note 1: Currently pattern-match does not bind the input expression to an internal variable, but simply copies it everywhere it is used. Therefore it is wise, if the input is from some expensive calculation, to bind it to a variable before applying pattern-match.

Note 2: The default value of a pattern-match expression in case no patterns match is nil. Because of this, if the pattern-match expression is supposed to evaluate to a special shape (an mv, or state, for instance), a default value of the correct shape must be defined by including a final clause of the form (& default-value-of-correct-shape).

Subtopics

Constructor-pattern-match-macros: How to write pattern-match macros for custom constructors.
Def-pattern-match-constructor: Allow pattern-match to recognize a constructor.
Pattern-match-list: Pattern matching to a list of terms.
Pattern-matches-list: Check that a list of terms matches a list of patterns.
Pattern-matches: Check whether a term matches a pattern.
Pml: pml is an abbreviation for pattern-match-list.
Pm: pm is an abbreviation for pattern-match.