Monitor
To monitor attempted applications of certain rules by the rewriter
This function stores information about which runes should be
monitored during rewriting and what criteria are used to invoke an
interactive break when those runes are tried by the rewriter during a
subsequent proof attempt.
Outline
- Protocol for Using Monitors
- Example and General Forms
- Background on Rewriting
- Criteria for Breaks
- Example Break Conditions
- What If No Break Occurs?
Protocol for Using Monitors
When a proof fails and you expected it to succeed by applying rules you've
proved, it can be helpful to see what happens when (if) the rewriter attempts
to use your rules. The break-rewrite utility allows you to monitor
each attempt by the rewriter to use specific rules (runes). The basic
protocol is that you turn on the break-rewrite utility with brr and
then you use this facility, monitor, to specify the rules you want to
monitor and the criteria for entering an interactive break.
(The variant monitor! is like monitor but also makes sure the
break rewrite utility is turned on.) Then you attempt the failed proof
again. When a monitored rule is tried and the criteria for that rule are
satisfied, the rewriter triggers an interactive break allowing you to query
the environment and watch what happens. The break is a read-eval-print
loop (in fact it is managed by ld, the same function that provides
ACL2's top-level interactive loop). However, it is inside a wormhole, allowing you to see what happening in rewrite. But any changes
you make while in this break disappear when the break exits and the wormhole
evaporates. See brr-commands for a list of the commands that
specifically give you access to parts of the rewriter's state. Such breaks
do not allow you to change the course of the rewriter or otherwise guide the
proof attempt! Breaks do allow you to abort a proof attempt, which
you typically do when you've understood why your rule failed to apply. If
you're seeking an interactive proof checker see proof-builder. To
learn about the interactive breaks triggered when monitored runes are tried,
see break-rewrite.
The current topic deals with how to install a monitor on a rule.
Example and General Forms
Examples:
(monitor '(:rewrite assoc-of-app) 't)
(monitor '(:r assoc-of-app) t)
(monitor 'assoc-of-app t)
(monitor '(rewrite assoc-of-app) '(:condition t :depth 2))
(monitor '(rewrite assoc-of-app) '(:condition t :rf t :depth 2))
Keyword Command Examples:
:monitor assoc-of-app t
:monitor lemma42 (:condition (equal (brr@ :target) '(F A (G A (H B))))
:rf t
:depth 2
:abstraction (F x (G x y))
:lambda t))
General Forms:
(monitor x criteria)
(monitor x criteria t) ; a quiet version
(monitor! x criteria) ; like quiet monitor but turns on brr first
where (the value of) x is a rune or more generally a runic
designator (see theories) designating one or more runes of classes
:rewrite, :definition, :rewrite-quoted-constant, or :linear and (the value of)
criteria is a “keyword value list” — a list of
alternating keywords and values. If no :condition key is supplied,
:condition t is used. If criteria is some term, y, it is
treated as the keyword value list (:condition y). The following keywords
and values are supported but the details are discussed below.
- :rf — value must be T or NIL, defaults to
NIL
- :depth — value must be a natural number
- :abstraction — value must be a term and it is most often an
abstraction of the pattern that triggers x obtained by replacing some
subterms of that pattern by new variables
- :lambda — value must be t or nil
- :condition — value must be a term, called the “break
condition” which contains at most one free variable and that variable
must be state. An interactive break is initiated only if the
:condition term evaluates to non-nil. If not provided, the
:condition value defaults to 'T.
The keys :depth, :abstraction, and :lambda are only relevant
when the rule named by x rewrites with an equivalence relation that is a
refinement of the equivalence relation the rewriter is obligated to maintain
on the current target (see geneqv) and the rule's “pattern”
does not match the target. They specify criteria under which a failed
match is to be considered a “near miss.” Details are given
below.
The key :rf with value T indicates that breaks are to also
occur (if the :condition evaluates to non-nil and) the rune's
equivalence relation has failed to be a refinement of the equivalence relation
the rewriter is obligated to maintain on the current target. See refinement-failure. If :rf is nil or not provided, refinement
failures do not trigger breaks but the other kinds of breaks may occur.
Keywords other than :condition, :rf, :depth,
:abstraction, and :lambda are allowed with no constraints on their
values. The purpose of this allowance is so that the user who wants to attach
his or her own function to ACL2's brr-near-missp predicate can pass
information to that function.
When successful, monitor arranges for the rewriter to trigger an
interactive break when any rule named by x and of the above classes is
tried, provided the break-rewrite utility has been turned on —
using :brr t, :monitor!, or with-brr-data — and the circumstances of the attempt to apply the rule
satisfy the criteria as checked by the function brr-near-missp.
Monitor prints to the comment window a list of all the
currently-monitored runes and their criteria and returns the error-triple
(value :invisible). The so-called “quiet” versions above do
no printing.
Some :rewrite rules are considered ``simple abbreviations''; see simple. These can be be monitored, but are only tried at certain times
during the proof. Monitoring is carried out by code inside the rewriter but
abbreviation rules may be applied by a special purpose simplifier inside the
so-called preprocess phase of a proof. If you desire to monitor an
abbreviation rule, a warning will be printed suggesting that you may want to
supply the hint :DO-NOT '(PREPROCESS); see hints. Without such a
hint, an abbreviation rule can be applied during the preprocess phase of a
proof, and no such application will cause an interactive break.
To remove a rune from the list of monitored runes, use unmonitor. To see which runes are monitored and what their break
criteria are, evaluate (monitored-runes).
Monitor, unmonitor and monitored-runes are macros that
expand into expressions involving state. While these macros appear to
return the list of monitored runes this is an illusion. They
all print monitored rune information to the comment window and
then return error-triples instructing ld to print nothing. It is
impossible to return the list of monitored runes because it
exists only in the wormhole state with which you interact when a
break occurs. This allows you to change the monitored runes and
their conditions during the course of a proof attempt without changing the
state in which the proof is being constructed.
Note: This list of monitored runes is maintained as a locally bound
variable by break-rewrite. For example, suppose that at the top-level of ACL2
the list of monitored runes and their criteria is x. Suppose you then
start a proof attempt, a break-rewrite break occurs and in that break you use
monitor or unmonitor to change the list of monitored runes to
y. Now suppose that you release or abort from the break and ACL2 returns
to the top-level. You might think the list of monitored runes is y but
in fact it is x. The list is locally bound to value in the caller's
environment each time break-rewrite is entered and thus restored to the value
in the caller's environment when break-rewrite returns.
Background on Rewriting
Before we explain the criteria for triggering breaks we establish some
basic terminology about the rewriter. We start with how it applies
:rewrite rules. The rewriter walks through a term (typically
left-to-right, innermost first) maintaining a list of known assumptions
represented as a type-alist. It rewrites each subterm under those
assumptions. The subterm the rewriter is currently considering is called the
“target”. Each :rewrite rule is derived from some theorem
essentially of the form (implies (and hyp1 ... hypn) (equiv lhs rhs)),
where the hypi, lhs, and rhs are terms and equiv is known
equivalence relation. The lhs is always a function application
and the rule derived from the theorem is stored in the ACL2 logical world under the topmost function symbol of the lhs.
Each time the rewriter steps to a new target it retrieves all the rules
stored under the topmost function symbol of the target and tries each rule in
turn (provided the rule is enabled and its equiv is a congruence
relation in the current context). To try a :rewrite rule the rewriter
first attempts to match the lhs to the target. By “match” we
mean the rewriter tries to find a substitution for the variables of
lhs (consistent with the restrict hints governing the target)
such that applying the substitution to the lhs produces the target. If
the lhs matches the target, the rewriter then attempts to establish the
hypi by rewriting each of them in turn, instantiating each hypi with
the substitution. If the instance of each hypi rewrites to true, we know
— by the theorem justifying this rule — that that the instance of
lhs is equivalent to the corresponding instance of rhs, but the
instance of lhs is the target. So the rewriter is logically justified in
replacing the occurrence of the target by the instance of rhs and
recursively rewrites that. Heuristic considerations may prevent such a
replacement, e.g., the instantiated rhs is considered ``too
complicated,'' a loop might be detected, etc.
We can generalize and summarize this description just by saying that each
rule has a pattern, some hypotheses, and a result. We say the rule is
“about” the topmost function symbol in the pattern. If the
pattern matches the target, the hypotheses are true, and heuristic
considerations allow, we use the result. :Definition and
:rewrite-quoted-constant rules fit easily within this scheme. But
:linear rules are a little different. The conclusion of a :linear
rule an arithmetic inequality relating subterms, the pattern is one of those
subterms, and the result is the entire inequality conclusion. If the
hypotheses are all rewritten to true, the result is instantiated and added to
the context, telling the rewriter possibly useful information about the
target.
Criteria for Breaks
If matching fails it is sometimes useful to see why. How did the pattern
and the target differ? But since a rule about a given function symbol is
tried every time the target has that same topmost function symbol, most rules
fail to match much more often than they match. Triggering a break on every
failed match is counterproductive. Instead, we introduce the notion of a
“near miss” and allow you to set criteria that trigger breaks when
a failed match is a near miss. There are three built-in near miss criteria,
:depth, :abstraction, and :lambda. We expect any given
monitored command will probably specify only one of these three criteria,
depending on the pattern in the rule and your judgment of what might be going
wrong, but there is nothing preventing you from specifying multiple criteria.
If any one of them is satisfied by a failed match a break will occur.
- :depth n causes a break if the pattern of the rune fails to match the
target but the pattern does match down to depth n. For example, the
pattern (F X (G X (H Y (I Z)))) fails to match the target (F A (G B
C)), but it does match to depth 2. To check this criterion the break
utility abstracts the pattern by copying it and replacing every subterm at
n by a new variable symbol. The depth n abstractions of
(F X (G (H Y (I Z)))) for n=1, 2, and 3 are shown below.
- n = 1: (F GENSYM0 GENSYM1)
- n = 2: (F X (G GENSYM0 GENSYM1))
- n = 3: (F X (G X (H GENSYM0 GENSYM1)))
- :abstraction apat causes a break if the pattern of the rune fails to
match the target but the translation of apat does match the target. This
is useful when you want more control over the abstraction of the pattern than
:depth gives you. For example, the depth 2 abstraction of (F X (G
X (H Y (I Z)))) is (F X (G GENSYM0 GENSYM1)) but you may be interested
only in breaks when (F X (G X GENSYM1)) matches the target, i.e., where
the first arguments of F and G are the same. If so you could
specify the criterion :abstraction (F X (G X Y)) or, equivalently,
:abstraction (F X (G X GENSYM1)).
- :lambda t causes a break if the pattern of the rune fails to
match the target but does match everywhere except on quoted lambda
constants. This is checked by replacing each quoted lambda object in the
pattern by a new variable. This is particularly useful when your rule
contains a lambda$ expression, which translates to a quoted lambda
constant, but the occurrence of that constant in the target has been
rewritten (see rewrite-lambda-object). See also the discussion of
“Normal Forms in Loop$ Bodies” in stating-and-proving-lemmas-about-loop$s.
When a near miss break is caused it prints 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 (F X1 X2 X3)), specified when this rule
was monitored.
The message then displays all of the near miss break criteria that were
satisfied and then prompts you for input. This allows you to inspect the
pattern (via the brr-commands :lhs or :max-term depending on
whether the monitored lemma is a :rewrite rule or a :linear rule.
You can inspect the target term with the command :target. The ``+''
versions of those commands, e.g., :lhs+, will print the terms without
evisceration. If you want more information about why the pattern of the rule
failed to match the target, use the command :explain-near-miss or its
``+'' version. You may exit the break with any of the usual commands, e.g.,
:ok to continue the proof attempt (because perhaps you determined that
the lemma was never supposed to match this particular target) or :a! to
abort back to the top-level to fix the problem (because you figured out why
the lemma, as written, will not match the intended target).
On the other hand, suppose the pattern of the rune matches the target.
Then the break condition term, i.e., the :condition criterion, is
evaluated. The only variable allowed in the break condition term is
state, which in the context of the break-rewrite utility is a wormhole state. Suppose the break condition term evaluates to ans. If
ans is nil, no break occurs. If ans is t, an interactive
break occurs and the user is prompted for commands. Otherwise, ans is
expected to be a true list of commands to be fed to the break, i.e., to be
appended to standard-oi. Those commands are then executed just as though
the user typed them. If they exit the break, the user is not prompted for
further commands. If they don't exit the break, the user is prompted for more
commands.
Example Break Conditions
In order to develop effective break conditions it must be possible to
access context sensitive information, i.e., information about the context in
which the monitored rune is being tried. The brr@ macro
may be used in break conditions to access such information as the term being
rewritten and the current governing assumptions. This information is not
stored in the proof state but is transferred into the wormhole
state when breaks occur. The macro form is (brr@ :sym) where
:sym is one of several keyword symbols, including :target (the term
being rewritten), :unify-subst (the substitution that instantiates the
left-hand side of the conclusion of the rule so that it is the target term),
and :type-alist (the governing assumptions). See brr@.
For example,
ACL2 !>:monitor (:rewrite assoc-of-app)
(equal (brr@ :target) '(app (app a b) c))
will monitor (:rewrite assoc-of-app) but will cause an interactive
break only when the target term is literally (APP (APP A B) C).
Because break conditions are evaluated in the interaction environment, the
user developing a break condition for a given rune can test candidate
break conditions before installing them. For example, suppose an
unconditional break has been installed on a rune, that an interactive
break has occurred and that the user has determined both that this particular
application is uninteresting and that many more such applications will likely
occur. An appropriate response would be to develop an expression that
recognizes such applications and returns nil. Of course, the hard task
is figuring out what makes the current application uninteresting. But once a
candidate expression is developed, the user can evaluate it in the current
context simply to confirm that it returns nil.
Recall that when a break condition returns a non-nil true list that
list is appended to the front of standard-oi. For example,
ACL2 !>:monitor (:rewrite assoc-of-app) '(:go)
will cause (:rewrite assoc-of-app) to be monitored and will make the
break condition be '(:go). This break condition always evaluates to the
non-nil true list (:go). Thus, an interactive break will occur
every time (:rewrite assoc-of-app) is tried. The break is fed the
command :go. Now the command :go causes break-rewrite to
(a) evaluate the attempt to apply the lemma, (b) print the result of that
attempt, and (c) exit from the interactive break and let the proof attempt
continue. Thus, in effect, the above :monitor merely
“traces” the attempted applications of the rune but never causes
an interactive break requiring input from the user.
It is possible to use this feature to cause a conditional break where the
effective break condition is tested after the lemma has been tried.
For example:
ACL2 !>:monitor (:rewrite lemma12)
'(:unify-subst
:eval!
:ok-if (or (not (brr@ :wonp))
(not (equal (brr@ :rewritten-rhs) '(foo a))))
:rewritten-rhs)
causes the following behavior when (:rewrite lemma12) is tried. A
break always occurs, but it is fed the commands above. The first,
:unify-subst, causes break-rewrite to print out the unifying
substitution. Then in response to :eval! the lemma is tried but
with all runes temporarily unmonitored. Thus no breaks will
occur during the rewriting of the hypotheses of the lemma. When the attempt
has been made, control returns to break-rewrite (which will print the
results of the attempt, i.e., whether the lemma was applied, if so what the
result is, if not why it failed). The next command, the :ok-if with its
following expression, is a conditional exit command. It means exit
break-rewrite if either the attempt was unsuccessful, (not (brr@
:wonp)), or if the result of the rewrite is any term other than (foo
a). If this condition is met, the break is exited and the remaining break
commands are irrelevant. If this condition is not met then the next command,
:rewritten-rhs, prints the result of the application (which in this
contrived example is known to be (foo a)). Finally, the list of supplied
commands is exhausted but break-rewrite expects more input. Therefore,
it begins prompting the user for input. The end result of the above
:monitor command is that the rune in question is elaborately
traced and interactive breaks occur whenever it rewrites its target to (foo
a).
We recognize that the above break condition is fairly arcane. We suspect
that with experience we will develop some useful idioms. For example, it is
straightforward now to define macros that monitor runes in the ways
suggested by the following names: trace-rune, break-if-target-is,
and break-if-result-is. For example, the last could be defined as
(defmacro break-if-result-is (rune term)
`(monitor ',rune
'(quote (:eval :ok-if
(not (equal (brr@ :rewritten-rhs) ',term))))))
(Note however that the submitted term must be in translated form.)
Since we don't have any experience with this kind of control on lemmas we
thought it best to provide a general (if arcane) mechanism and hope that the
ACL2 community will develop the special cases that we find most
convenient.
Note: The combination of a non-trivial :condition and some near-miss
criteria can result in confusing behavior. To get a near-miss break a target
has to fail to match the rule's pattern but succeed in matching the near-miss
criteria. So the near-miss criteria is irrelevant if the target matches the
rule. But to get a break the target must match the rule in such a way that the
:condition is satisfied. Failure to get any breaks when you have a
non-trivial :condition and a very general near-miss criteria may mean
targets matching the near-miss criteria also matched the rule's pattern but
failed to satisfy your :condition. Our personal preference when
monitoring for near-misses is to use the default :condition of t, at
least until we see what kind of matches are arising.
What If No Break Occurs?
Suppose rune is a rune that names a rule about some function symbol
fn. What does it mean if you've installed a monitor on rune with
(:condition t :depth 1) and no break ever occurs? Then one of the
following is probably true.
- the break-rewrite utility is not turned on — you should evaluate
(brr t),
- rune is disabled in the theory used for subgoals mentioning fn
— you should enable it either with a global in-theory command or
a subgoal-specific :in-theory hint (see hints),
- rune names an abbreviation rule as discussed above — you should
add the hint :DO-NOT '(PREPROCESS) (see hints),
- the :hints supplied includes a :hands-off list that
includes fn — perhaps you should disable other rules about
fn (since that is presumably why you put fn on the :hands-off
list in the first place) and remove fn from the :hands-off
list,
- the only terms that the rewriter ever encountered with the topmost
function fn were within a HIDE,
- no target with the topmost function symbol fn was ever seen by
rewrite — perhaps fn was involved in the conjecture or introduced
into the proof attempt but was eliminated by another rewrite.
The rewriter is complicated. There may be other ways this could
happen!
