		Search-engine friendly clone of the ACL2 documentation.

Macro-libraries

Match-tree

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 (:! x) binding pattern is the same as (:? x) in match-tree itself, but is treated differently by macros treematch, when-match, and unless-match; see below.

Macro support

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 (:! x) binders, treematch invokes match-tree with an alist consisting of the previous bindings of those variables; then, the pattern will only match if the corresponding location in the object is equal to the existing binding of the variable, like in case-match when a symbol is prefixed with !. For example, in the following form:

(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 (foo bar).

Two b* binders unless-match and when-match also use match-tree. One can think of them as expending to a call of treematch with one pattern and a default:

(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))

Reasoning

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 match-tree to match-tree-alist. This is a simpler function with fewer conditionals that equals that value whenever the pattern matches; presumably the alist isn't relevant otherwise. The theory match-tree-alist-opener-theory opens calls of match-tree-alist. You may additionally want a rule such as assoc-equal-of-cons to simplify lookups in the alist.

We generally rewrite the first return value (matchedp) to match-tree-matchedp (which is equivalent) when the match was successful. However, we can use different rules to do this and these rules have different side effects to help with reasoning:

match-tree-equals-match-tree-matchedp-when-successful simply rewrites the matchedp return value to match-tree-matchedp, without side effects.
match-tree-obj-equals-subst-when-successful rewrites the matchedp value to the conjunction of match-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 the matchedp value to the conjunction of match-tree-matchedp and match-tree-matchedp-open, and equivalent function that has rules to open calls on known patterns enabled by default (collected in the theory match-tree-opener-theory.
match-tree-obj-equals-subst-and-open-when-successful rewrites the matchedp 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 matchedp return value as a negative literal (hypothesis/negated conclusion) of a clause, not when backchaining or a positive literal (negated hypothesis/conclusion). To prove that a pattern does in fact match, or a consequence when it doesn't match, the rule match-tree-open unconditionally rewrites the matchedp value to match-tree-matchedp-open, which by default opens into a conjunction of conditions.

Subtopics

Treematch: Utility similar to case-match that uses match-tree.
When-match: B* binder for match-tree
Unless-match: B* binder for match-tree.