Pattern matching supporting recognizers, e.g., those automatically generated by defdata, and case-match, with support for specifying type recognizers similar to that provided by definec.

(definec fact (n :nat) :pos (match n (0 1) (& (* n (fact (1- n)))))) (definec acl2-count2 (x :all) :nat (match x ((a . b) (+ 1 (acl2-count2 a) (acl2-count2 b))) (:rational (:integer (integer-abs x)) (& (+ (integer-abs (numerator x)) (denominator x)))) ((:r complex/complex-rationalp) (+ 1 (acl2-count2 (realpart x)) (acl2-count2 (imagpart x)))) (:string (length x)) (& 0))) ;; Compare with the definition of acl2-count (defun acl2-count (x) (declare (xargs :guard t :mode :program)) (if (consp x) (+ 1 (acl2-count (car x)) (acl2-count (cdr x))) (if (rationalp x) (if (integerp x) (integer-abs x) (+ (integer-abs (numerator x)) (denominator x))) (if (complex/complex-rationalp x) (+ 1 (acl2-count (realpart x)) (acl2-count (imagpart x))) (if (stringp x) (length x) 0))))) ;; Note that the two definitions are equivalent, ;; as the following is a theorem. (thm (equal (acl2-count2 x) (acl2-count x)))

The macro match provides pattern matching. It includes the functionality provided by case-match and also supports recognizers in a style similar to how definec allows you to specify defdata types.

There are two ways to specify recognizers. One is to use a keyword, such as :rational, in the above examples. Such keywords are turned into recognizers by creating a regular symbol with a "p" at the end, e.g, :rational gets turned into rationalp (but :atom gets turned into atom). The generated symbols are in the ACL2s package. The more general mechanism is to specify a recognizer using the (:r recognizer) form; an example is (:r complex/complex-rationalp) in the acl2-count2 definition above. In this way, you can also specify the package of the recognizer.

If you want to match a keyword, you can do that by quoting it.
So `':rational` matches the keyword, not the type.

If you are matching a recognizer, you can either have a single form after that, in which case, that form is an ACL2 expression that gets associated with the recognizer, or you can have a list of forms, in which case they are treated as nested matching forms. An example of such nesting is shown in the :rational case of the match in the definition of acl2-count2, above.

If you are not matching a recognizer, then match behaves like case-match.

One important difference with case-match is that match requires that the cases are complete. It does this by returning the following if there are no matches.

(illegal 'match "match is not exhaustive" ())