Match an object against a flexible pattern and return the unifying substitution

Match-tree is a function that takes a pattern, object, and alist, and returns two values: matchedp, which is true only if the pattern matched the object under the bindings already present in alist, and result-alist, an extension of the input alist containing the unifying substitution.

Invocation:

(match-tree pattern obj alist) --> (mv matchedp new-alist) )} <p>Pseudo-formally, if the input alist is empty, a pattern P matches an object X and produces bindings as follows:</p> @({ Match conditions Bindings produced P is an atom and P = X P is (:? <symb>) (<symb> . X) P is (:! <symb>) (<symb> . X) P is (:?S <symb>) and X is a symbol (<symb> . X) P is (:?V <symb>) and X is a nonnil symbol (<symb> . X) P is (:?F <symb>) and X is a non-quote symbol (<symb> . X) P is (:?L <symb>) and X is not quote (<symb> . X) P is none of the above, (car P) matches (car X), (cdr P) matches (cdr X), car bindings and the car and cdrs' bindings UNION agree on all symbols bound in both. cdr bindings.

If the input alist is not empty, then the bindings produced must also agree with any bindings of the same symbols that are present in the input alist, and the result alist is the bindings unioned with the input alist.

The

Match-tree supports the utility treematch, which is similar in spirit to case-match; e.g.,

(treematch x ((cons (:? a) (:? b)) (list a b)) ((foo (:v q)) (list q)) (& (list x)))

expands to approximately:

(b* ( ;; (cons (:? a) (:? b)) case: ((mv matchedp alist) (match-tree '(cons (:? a) (:? b)) x nil)) ((when matchedp) (let* ((a (cdr (assoc 'a alist))) (b (cdr (assoc 'b alist)))) (list a b))) ;; (foo (:v q)) case: ((mv matchedp alist) (match-tree '(foo (:v q) (:? y)) x nil)) ((when matchedp) (let* ((q (cdr (assoc 'q alist)))) (list q)))) ;; default case: (list x))

When a pattern contains

(let ((y 'bar)) (treematch x ((foo (:! y)) ...) ...))

the match-tree call generated is:

(match-tree '(foo (:! y)) x (list (cons 'y y)))

which means that this match will only succeed if x equals

Two b* binders

(b* (((when-match obj pattern) match-form)) default-form)

and

(b* (((unless-match obj pattern) default-form)) match-form)

are both basically equivalent to

(treematch obj (pattern match-form) (& default-form))

The main advantage of match-tree over case-match is reasoning efficiency. When using case-match, each pattern-matching form macroexpands to a conjunction of conditions followed by a series of bindings. These are relatively automatic to reason about, but they make it difficult to debug problems in proofs (because it takes a lot of reading and decoding car/cdr nests to figure out which patterns did and did not match), and they are expensive to reason about because when a pattern does NOT match, ACL2 typically splits into cases for the disjunction of the matching conditions.

Since match-tree is a function, the user can control how or whether to open it. We offer a couple of levels of reasoning about it, bundled in theories.

We generally rewrite the second (new-alist) return value of

We generally rewrite the first return value (matchedp) to

match-tree-equals-match-tree-matchedp-when-successful simply rewrites thematchedp return value tomatch-tree-matchedp , without side effects.match-tree-obj-equals-subst-when-successful rewrites thematchedp value to the conjunction ofmatch-tree-matchedp and a term equating the object with the substitution of the result alist into the pattern. Rules that expand the substitution are enabled by default, so this quickly produces a hypothesis that gives the shape of the object defined by the pattern.match-tree-open-when-successful rewrites thematchedp value to the conjunction ofmatch-tree-matchedp andmatch-tree-matchedp-open , and equivalent function that has rules to open calls on known patterns enabled by default (collected in the theorymatch-tree-opener-theory .match-tree-obj-equals-subst-and-open-when-successful rewrites thematchedp value to the conjunction of all three:match-tree-matchedp ,match-tree-matchedp-open , and the equivalence of the object with the substitution.

These rules only take effect when we see the

- Treematch
- Utility similar to
case-match that usesmatch-tree . - When-match
B* binder formatch-tree - Unless-match
B* binder formatch-tree .