Major Section: ACL2-BUILT-INS
General Form: (case-match x (pat1 dcl1 body1) ... (patk dclk bodyk))where
xis a variable symbol, the
patiare structural patterns as described below, the
declareforms and the
bodyiare terms. Return the value(s) of the
bodyicorresponding to the first
nilif none matches.
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
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
zare atomic. Suppose we wished to recognize those trees. The following
(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
(case-match tree ((x . (x . x)) (if (atom x) x 7)) (((x . x) . x) (if (atom x) x 7)) (& 7))Note that
patimatches. Thus if we must return
7in that case, we have to add as the final pattern the
&, which always matches anything.