CASE-MATCH

pattern matching or destructuring 
Major Section:  ACL2-BUILT-INS


General Form:
(case-match x
  (pat1 dcl1 body1)
  ...
  (patk dclk bodyk))
where x is a variable symbol, the pati are structural patterns as described below, the dcli are optional declare forms and the bodyi are terms. Return the value(s) of the bodyi corresponding to the first pati matching x, or nil if none matches.

Pattern Language:
With the few special exceptions described below, matching requires that the cons structure of x be isomorphic to that of the pattern, down to the atoms in the pattern. Non-symbol atoms in the pattern match only themselves. Symbols in the pattern denote variables which match anything and which are bound by a successful match to the corresponding substructure of x. Variables that occur more than once must match the same (EQUAL) structure in every occurrence. 

Exceptions:
&               Matches anything and is not bound.  Repeated
                  occurrences of & in a pattern may match different
                  structures.
nil, t, *sym*   These symbols cannot be bound and match only their
                  global values.
!sym            where sym is a symbol that is already bound in the
                  context of the case-match, matches only the
                  current binding of sym.
'obj            Matches only itself.
Some examples are shown below.

Below we show some sample patterns and examples of things they match and do not match. 

pattern       matches         non-matches
(x y y)       (ABC 3 3)       (ABC 3 4)    ; 3 is not 4
(fn x . rst)  (P (A I) B C)   (ABC)        ; NIL is not (x . rst)
              (J (A I))                    ; rst matches nil
('fn (g x) 3) (FN (H 4) 3)    (GN (G X) 3) ; 'fn matches only itself
(& t & !x)    ((A) T (B) (C))              ; provided x is '(C)
Consider the two binary trees that contain three leaves. They might be described as (x . (y . z)) and ((x . y) . z), where x, y, and z are atomic. Suppose we wished to recognize those trees. The following case-match would do: 
(case-match tree
  ((x . (y . z))
   (and (atom x) (atom y) (atom z)))
  (((x . y) . z)
   (and (atom x) (atom y) (atom z))))
Suppose we wished to recognize such trees where all three tips are identical. Suppose further we wish to return the tip if the tree is one of those recognized ones and to return the number 7 otherwise. 
(case-match tree
  ((x . (x . x))
   (if (atom x) x 7))
  (((x . x) . x)
   (if (atom x) x 7))
  (& 7))
Note that case-match returns nil if no pati matches. Thus if we must return 7 in that case, we have to add as the final pattern the &, which always matches anything.