Major Section: BREAK-REWRITE
Example: (monitor '(:rewrite assoc-of-app) 't) :monitor (:rewrite assoc-of-app) t :monitor (:definition app) (equal (brr@ :target) '(app c d)) General Form: (monitor rune term)where
rune is a rune and term is a term, called the ``break
condition.'' Rune must be either a :rewrite rune or a
:definition rune.When a rune is monitored any attempt to apply it may result in an interactive break in an ACL2 ``wormhole state.'' There you will get a chance to see how the application proceeds. See break-rewrite for a description of the interactive loop entered. Whether an interactive break occurs depends on the value of the break condition expression associated with the monitored rune.
NOTE: Some :rewrite rules are considered ``simple abbreviations'';
see simple. These can be be monitored, but only 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 conditions
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 (see 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 the proof is being constructed.
Unconditional break points are obtained by using the break condition
t. We now discuss conditional break points. The break condition,
expr, must be a term that contains no free variables other than
state and that returns a single non-state result. In fact, the
result should be nil, t, or a true list of commands to be fed to the
resulting interactive break. Whenever the system attempts to use
the associated rule, expr is evaluated in the wormhole interaction
state. A break occurs only if the result of evaluating expr is
non-nil. If the result is a true list, that list is appended to the
front of standard-oi and hence is taken as the initial user commands
issued to the interactive break.
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 a (app b c)))
will monitor (:rewrite assoc-of-app) but will cause an interactive
break only when the target term, the term being rewritten, is
(app a (app 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 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$ nil
: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$ nil 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, then, 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.
