		Search-engine friendly clone of the ACL2 documentation.

Match

Pattern matching supporting predicates, including recognizers automatically generated by defdata, disjunctive patterns and patterns containing arbitrary code. Can be thought of as ACL2s version of case-match.

Examples

;; Predicate/recognizer patterns are defined using keywords.
;; The keyword pos corresponds to the recognizer posp. For all
;; keywords except atom, we generate the corresponding
;; predicate/recognizer by adding a p to the end of the symbol.

;; This function, given an integer as input, returns 1 if it is
;; positive, else 2 if it is even, else 3. Match forms are checked
;; to make sure that they are exhaustive. If not, that is an error,
;; e.g., if you remove one of the cases to match, you will get an
;; error. Note that :even gets turned into the predicate evenp,
;; which is not a recognizer (as its domain is not all).

(definec int-class (x :int) :pos
  (match x
    (:pos 1)
    (:even 2)
    (:neg 3)))

;; Here is a more complex example, showing that predicate/recognizer
;; patterns can be nested. The match form matches any positive x,
;; and then checks if it even or odd. The nested match forms must
;; also be exhaustive, given that x is positive. If x is not
;; positive, then we check if it is negative and then we perform
;; another nested check. 

;; Finally, we check if x is 0. Constants such as 0 can be used as
;; patterns, as shown below.

(definec int-class2 (x :int) :pos
  (match x
    (:pos 
     (:even 1)
     (:odd 2))
    (:neg
     (:even 3)
     (:odd 4))
    (0 5)))
  
;; The next definition is equivalent to the previous definition, but
;; makes maximal use of &.

;; & matches anything and is not bound. Repeated occurrences of &
;; may match different structures. 

(definec int-class3 (x :int) :pos
  (match x
    (:pos 
     (:even 1)
     (& 2))
    (:neg
     (:even 3)
     (& 4))
    (& 5)))

(definec fact (n :nat) :pos
  (match n
    (0 1)
    (& (* n (fact (1- n))))))

;; The following three definitions of fib are equivalent.

;; Disjunctive patterns are defined with the use of :or, as shown in
;; the first definition of fib. This match form can be thought of as
;; expanding into the match form of the second version of fib. A
;; disjunctive pattern can have any positive number of patterns.

(definec fib (n :nat) :pos
  :skip-tests t
  (match n
    ((:or 0 1) 1)
    (& (+ (fib (1- n)) (fib (- n 2))))))

(definec fib (n :nat) :pos
  :skip-tests t
  (match n
    (0 1)
    (1 1)
    (& (+ (fib (1- n)) (fib (- n 2))))))

;; Patterns with arbitrary code are defined with the use of :t, as
;; shown below, where the pattern checks if n is less than 2.

(definec fib (n :nat) :pos
  :skip-tests t
  (match n
    ((:t (< n 2)) 1)
    (& (+ (fib (1- n)) (fib (- n 2))))))

;; The following definitions of pascal are equivalent.

;; !sym, where sym is a symbol that is already bound in the context
;; of the match form, matches only the current binding of
;; sym. Hence, in the first definition of pascal, the last pattern
;; in the :or form matches a list whose first element is anything,
;; but whose second element is i (the first argument to
;; pascal). Notice that the first argument is also i, which explains
;; the equivalence between the two versions of pascal.

(definec pascal (i :nat j :nat) :pos
  :skip-tests t
  (match (list i j)
    ((:or (0 &) (& 0) (& !i)) 1)
    (& (+ (pascal (1- i) (1- j))
          (pascal (1- i) j)))))

(definec pascal (i :nat j :nat) :pos
  :skip-tests t
  (match (list i j)
    ((0 &) 1)
    ((& 0) 1)
    ((!i !i) 1)
    (& (+ (pascal (1- i) (1- j))
          (pascal (1- i) j)))))

;; The following examples show how to use match with conses.  In mem,
;; we first check if x is nil. The symbols nil, t, *sym* and cannot
;; be bound and only match their global values, as was the case for
;; constants, as we have seen above. The pattern (f . r) matches any
;; cons, with f being the car and r being the cdr. Since mem is
;; checking whether e is a member of x, notice the use of !e to
;; match e with the first element of x.

(definec mem (e :all x :tl) :bool
  (match x
    (nil nil)
    ((!e . &) t)
    ((& . r) (mem e r))))

(definec subset (x :tl y :tl) :bool
  (match x
    (nil t)
    ((f . r) (and (mem f y) (subset r y)))))

;; If you want to match an object, say obj, you can use the pattern
;; 'obj.  This allows you to match keywords that may otherwise be
;; interpreted as types.

;; Here is the definition of the built-in function 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)))))

;; Here is an equivalent definition using match. 

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


;; Note that the two definitions are equivalent, 
;; as the following is a theorem. 

(thm (equal (acl2-count2 x) (acl2-count x)))

;; More complex patterns than (f . r) can be used to match with
;; conses and lists. For example, (x x y), ('x (':x x) . t), and
;; ('x (:x x)) are allowed patterns. The first pattern matches
;; (1 1 2), ((1 2) (1 2) (3)), etc. The second pattern only matches
;; lists whose first element is the symbol x, whose second element
;; is a list of length two whose first element is the keyword x, and
;; whose cddr is t. The third pattern only matches lists of length
;; two, whose first element is the symbol x and whose second element
;; is a list of length two whose first element is of type x (i.e.,
;; recognized by xp).

;; There are restrictions on the patterns that are used to match
;; conses and lists. At the top level, all of the patterns above are
;; allowed, but inside of such patterns, disjunctive patterns, and
;; code patterns (using :t) are not supported. Type patterns (such
;; as :int, :bool, (:r intp), etc) are supported.

Purpose

The macro match provides pattern matching. It includes the functionality similar to that provided by case-match and more. It supports predicate/recognizer patterns in a style similar to how definec allows you to specify defdata types. These patterns can be nested. The match macro also provides disjunctive patterns and patters containing arbitrary code. Patterns are required to be exhaustive.

There are two ways to specify predicates/recognizers. One is to use a keyword, such as :rational; see the examples above. Such keywords are turned into predicates/recognizers by creating a regular symbol with a "p" at the end, e.g., :rational gets turned into rationalp (the only special case is that :atom gets turned into atom). The generated symbols are in the ACL2s package. The more general mechanism is to specify a predicate/recognizer using the (:r predicate/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 predicate/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 predicate/recognizer, you can either have a single form after that, in which case, that form is an ACL2 expression that gets associated with the predicate/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.

Disjunctive patterns and patterns containing arbitrary code are also supported. See the examples above.

If you are not matching any of the above patterns (predicate/recognizer, disjunctive, code), then match behaves like case-match.

One important difference with case-match is that match requires that the cases are exhaustive (or complete). It does this by, essentially, adding the following as a final case.

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

During contract checking (or guard verification), if the above case is reachable, that will lead to an error. The reason for this is to not have any hidden control flow, which can make debugging hard. Finally, we note that nested patterns are also required to be exhaustive.