# Case-match

Pattern matching or destructuring

General Form:
(case-match x
(pat1 dcl1 ... body1)
...
(patk dclk ... bodyk))

where x is a symbol, the pati are structural patterns as
described below, each “dcli ...” indicates 0 or more `declare` forms, and the bodyi are terms. The legal declare forms
are the same as for `let`: ignore, ignorable, and type.
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*, :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. This is the same as (QUOTE obj).
(QUOTE~ sym) where sym is a symbol, is like (QUOTE sym) except it
matches any symbol with the same symbol-name as sym.
Note that QUOTE~ is in the "ACL2" package.

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.

Technical point: The symbol sym referenced by the symbol !sym is
in the same package as !sym but with the leading exclamation point
character, \#!, removed from the `symbol-name` of !sym.

### Subtopics

- Pattern-match
- User-definable pattern-matching.