		Search-engine friendly clone of the ACL2 documentation.

Match

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.

Examples

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

Purpose

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