match-tree

(in-package "ACL2")

(verify-guards match-tree
  :hints (("Goal" :in-theory (enable match-tree-binder-p))))

(def-b*-binder unless-match
  :decls ((declare (xargs :guard (equal (len args) 2))))
  :body (treematch-fn (car args)
    (cadr args)
    `(progn$ . ,FORMS)
    rest-expr))

(def-b*-binder when-match
  :decls ((declare (xargs :guard (equal (len args) 2))))
  :body (treematch-fn (car args)
    (cadr args)
    rest-expr
    `(progn$ . ,FORMS)))

(deftheory match-tree-alist-opener-theory
  '(match-tree-alist-expand-atom match-tree-alist-expand-binder
    match-tree-alist-expand-cons))

(deftheory match-tree-opener-theory
  '(match-tree-check-binding match-tree-matchedp-open-when-binder
    match-tree-matchedp-open-when-consp
    match-tree-matchedp-open-of-atom))

(defxdoc match-tree
  :parents (macro-libraries)
  :short "Match an object against a flexible pattern and return the unifying substitution"
  :long " 
<p>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.</p>

<p>Invocation:</p>
@({
  (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.
 })

<p>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.</p>

<p>The @('(:! x)') binding pattern is the same as @('(:? x)') in match-tree
itself, but is treated differently by macros @(see treematch), @(see
when-match), and @(see unless-match); see below.</p>

<h2>Macro support</h2>

<p>Match-tree supports the utility @(see treematch), which is similar in spirit to @(see case-match); e.g., </p>

@({
 (treematch x
   ((cons (:? a) (:? b))    (list a b))
   ((foo (:v q))            (list q))
   (&                       (list x)))
 })
<p>expands to approximately:</p>
@({
 (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))
 })

<p>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 @(see
case-match) when a symbol is prefixed with @('!').  For example, in the
following form:</p>

@({
 (let ((y 'bar))
   (treematch x
      ((foo (:! y))  ...)
      ...))
 })
<p>the match-tree call generated is:</p>
@({
 (match-tree '(foo (:! y)) x (list (cons 'y y)))
 })
<p>which means that this match will only succeed if x equals @('(foo bar)').</p>

<p>Two @(see 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:</p>

@({
 (b* (((when-match obj pattern)
       match-form))
    default-form)
 })
<p>and</p>
@({
 (b* (((unless-match obj pattern)
       default-form))
    match-form)
 })
<p>are both basically equivalent to</p>
@({
 (treematch obj
   (pattern match-form)
   (& default-form))
 })
    
<h2>Reasoning</h2>

<p>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.</p>

<p>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.</p>

<p>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.</p>

<p>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:</p>

<ul>
<li>@('match-tree-equals-match-tree-matchedp-when-successful') simply
rewrites the @('matchedp') return value to @('match-tree-matchedp'), without side
effects.</li>

<li>@('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.</li>

<li>@('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').</li>

<li>@('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.</li>

</ul>

<p>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.</p>



")

(defxdoc treematch
  :parents (match-tree)
  :short "Utility similar to @('case-match') that uses @('match-tree')."
  :long "<p>See @(see match-tree) for details.</p>")

(defxdoc when-match
  :parents (match-tree)
  :short "@('B*') binder for @('match-tree')"
  :long "<p>See @(see match-tree) for details.</p>")

(defxdoc unless-match
  :parents (match-tree)
  :short "@('B*') binder for @('match-tree')."
  :long "<p>See @(see match-tree) for details.</p>")