Monitor
To monitor the attempted application of a rule name
Examples:
(monitor '(:rewrite assoc-of-app) 't)
:monitor (:rewrite assoc-of-app) t
(monitor '(:r assoc-of-app) t)
:monitor (:r assoc-of-app) t
:monitor assoc-of-app t
:monitor (:definition app) (equal (brr@ :target) '(app c d))
:monitor (:linear rule3) t
In the examples above, the first four forms are equivalent; see keyword-commands and see rune. Those are equivalent to the fifth form
if the event assoc-of-app corresponds to a rewrite rule, or more
precisely, to a single rune, (:rewrite assoc-of-app).
General Forms:
(monitor x condition)
:monitor y z ; same as (monitor 'y 'z)
(monitor x condition t) ; same as above, but avoiding output
where we focus below on the first form, in which the arguments are
evaluated. The second form quotes its arguments; see keyword-commands.
The third form is a quiet version of the first that avoids the need to invoke
brr explicitly, as discussed below.
Above, x (or more precisely, the result of evaluating x) is a
runic designator (see theories) other than a theory name (see theories) and (the value of) condition is a term, called the ``break
condition.'' If x is not a symbol then it must designate a rune
corresponding to a rule of class :rewrite, :definition, or :linear. If x is a symbol then it
represents all such runes that it designates, and there must be at least one
such. (Thus, x cannot name an event that generates only rules of classes
other than those three.)
Monitor does not affect proof attempts until the break-rewrite
utility is turned on with brr, for example, using :brr t. For a
shortcut that does this automatically while avoiding output, see monitor!.
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. Whether an
interactive break occurs depends on the value of the break condition
expression associated with the monitored rune. See break-rewrite for a description of the interactive loop entered, and in
particular, for discussion of what happens if you monitor or unmonitor a rune
while inside a break (in short: the effect disappears when existing the break,
unless it is a top-level break). Also see set-brr-evisc-tuple for how
to see output in full.
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 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.
Unconditional break points are obtained by using the break condition
t. We now discuss conditional break points. The break condition,
condition, 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, the break condition (that is, condition) is evaluated in
the wormhole interaction state. A break occurs only if the
result of evaluating condition 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.
