Explain-near-miss
show why a rule's pattern and the :target do not match
When a near miss break occurs (see monitor) the user
sees a message like this:
(1 Breaking (:REWRITE LEMMA) on (F (G A B) A '(A B C D ...)):
The pattern in this rule failed to match the target. However, this
is considered a NEAR MISS under the break criteria,
(:CONDITION 'T :ABSTRACTION ...), specified when this rule was
monitored. The following criterion is satisfied.
* The :ABSTRACTION pattern provided in your monitor, ...,
matches :TARGET.
It can be difficult to determine why the pattern of the rule, e.g., the
:lhs of a :rewrite rule, fails to match the :target term,
especially when large terms, large quoted constants, and lambda
expressions are involved.
Included among the :brr-commands is the :explain-near-miss
command which is intended to help explain. This command can only operate in
a near miss break. If called in another context an error may occur.
But in a near miss break, the situation is as follows. The prover has
tried to apply a rule that has been monitored with a break criterion meaning
``cause an interactive break when the target term (the term to currently
being rewritten) satisfies this criterion but the triggering pattern of the
rule fails to match the target term.'' When inside the resulting break, the
target term is given by the brr command :target. The
``triggering pattern'' of the rule in question depends on how the rule was
stored (see rule-classes). The triggering pattern of a :rewrite rule — the most common class of rule — is the left-hand
side of the concluding equality and can be obtained from within the break by
typing the brr command :lhs. The triggering pattern for a
:rewrite-quoted-constant rule is its right-hand side, but as
explained in rewrite-quoted-constant, the brr command :lhs
will display it. The triggering pattern for a :linear rule is
displayed by the :max-term brr command. The question the user
will typically ask in this situation is ``why doesn't the triggering pattern
match the target?''
To understand the answer you have to understand how the ACL2 matching
algorithm works. The matching algorithm is given two terms, t1 and
t2, and attempts to find a substitution s on the variables in
t1 such that when t1 is instantiated with s the result is
t2, i.e., t1/s = t2. Note that only the variables in the
pattern, t1, can be instantiated by s'. In the case of a near miss
break, no such substitution was found.
The :explain-near-miss command reruns the matching algorithm on the
triggering pattern and the target, expecting failure and collecting
information about where the failure occurred. The output is intended to be
self-explanatory.
The message displays the pattern in question and the target term, but it
also displays a version of the pattern in which the first unmatchable subterm
is replaced by the expression <pat>. That <pat> is displayed
in lowercase whereas the rest of the pattern and target are in uppercase.
It marks where the matching broke down.
The message goes on to show the mismatched subterms from the pattern and
the target, the substitution that was computed to match everything up to
<pat> and what the <pat> subterm of the pattern is when
instantiated with that substitution.
So, for example, suppose the rule's :lhs and the current :target
are as shown below. Then here is what :explain-near-miss would
print.
The ACL2 match algorithm attempted to match :LHS with :TARGET by finding
a substitution, s, such that :LHS/s = :TARGET. That attempt failed
when trying to match the subterm of :LHS marked <pat> in :LHS' below.
:LHS: (F X (G X Y) (H X))
:LHS': (F X (G <pat> Y) (H X))
:TARGET: (F A (G B A) (H A))
Below we show the substitution, s, computed prior to the failure; the
subterm of :LHS we're calling <pat>; the instantiated subterm, <pat>/s;
and the corresponding subterm, <tar>, of :TARGET.
s: ((X A))
<pat>: X
<pat>/s: A
<tar>: B
For the rewriter to get past this failure the match algorithm must
be able to extend substitution s to s' so that <pat>/s' is equal to
<tar> and our match algorithm could not find such an extension.
Note that the substitution s binds X to A to match the
first argument of the F-expression in the :LHS to the corresponding
argument in the :TARGET. Then it tries to match (G X Y) with (G
B A). It fails on the first argument of that subterm, where <pat> is
shown in :LHS', because X has been bound to A and A and
B are different. (Remember: only the variables of the pattern can be
bound by the substitution.)
When <pat> and its corresponding subterm <tar> are ``large'' but
unequal quoted constants or lambda expressions, :explain-near-miss
will call compare-objects on those objects. It can be hard to spot
how two large constants differ and compare-objects points out the
differences between two cons trees. :Explain-near-miss considers
an object ``large'' if the number of conses in it is 30 or greater.
The command :explain-near-miss+ is like :explain-near-miss
except it never eviscerates any term and runs compare-objects whenever
the failure is on two distinct quoted objects or lambda expressions
regardless of their sizes.
But note that compare-objects is not run by either version of
explain-near-miss when the failure is of the most common kinds:
- (a) a variable in the pattern has already been bound in the
substitution (i.e., bound earlier in the matching process) to a term that is
not identical to the corresponding term in the target, or
- (b) a term in the pattern has a different function symbol than the
corresponding term the target.
So do not expect the compare-objects output to appear often!
