Pattern matching or destructuring
General Form: (case-match x (pat1 dcl1 ... body1) ... (patk dclk ... bodyk))
With the few special exceptions described below, matching requires that the cons structure of
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
(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))
Technical point: The symbol