Major Section: ACL2 Documentation
ACL2 allows the user to monitor the application of rewrite rules.
When monitored rules are about to be tried by the rewriter, an
interactive break occurs and the user is allowed to watch and, in a
limited sense, control the attempt to apply the rule. This
interactive loop, which is technically just a call of the standard
top-level ACL2 read-eval-print loop,
ld, on a ``wormhole state''
(see wormhole), is called ``break-rewrite.'' While in
break-rewrite, certain keyword commands are available for accessing
information about the context in which the lemma is being tried.
These keywords are called break-rewrite ``commands.''
Also see dmr (Dynamically Monitor Rewrites) for a related utility, which allows you to watch progress of the rewriter in real time.
To abort from inside break-rewrite at any time, execute
For further information, see the related
doc topics listed below.
As explained in the documentation for
monitor, it is possible to
cause the ACL2 rewriter to monitor the attempted application of
selected rules. When such a rule is about to be tried, the rewriter
evaluates its break condition and if the result is non-
break-rewrite is entered.
Break-rewrite permits the user to inspect the current state by
evaluating break-rewrite commands. Type
help in break-rewrite to
see what the break-rewrite commands are. However, break-rewrite is actually
just a call of the general ACL2 read-eval-print loop,
ld, on a certain
state and the break-rewrite commands are simply aliases provided by
ld-keyword-aliases table (see ld-keyword-aliases). See ld for
details about this read-eval-print loop. Thus, with a few exceptions,
anything you can do at the ACL2 top-level can be done within break-rewrite.
For example, you can evaluate arbitrary expressions, use the keyword command
hack, access documentation, print events, and even define functions
and prove theorems. However, the ``certain state'' upon which
was called is a ``wormhole state'' (see wormhole) because
break-rewrite is not allowed to have any effect upon the behavior of rewrite.
What this means, very roughly but understandably, is that break-rewrite
operates on a copy of the state being used by rewrite and when
break-rewrite exits the wormhole closes and the state ``produced''
by break-rewrite disappears. Thus, break-rewrite lets you query the state of
the rewriter and even do experiments involving proofs, etc., but these
experiments have no effect on the ongoing proof attempt. In particular:
Note that the output from break-rewrite is sometimes abbreviated by default,
such as for the term causing the break. This can be controlled by setting
:term evisc-tuple; see set-evisc-tuple. (Another option: use
iprinting. See set-iprint.) But as noted above, if you use
set-evisc-tuple from inside the break-rewrite wormhole, its effect
will disappear when you exit the break. So you might want to issue a
set-evisc-tuple command from the top level, outside break-rewrite.
When you first enter break-rewrite a simple herald is printed such as:
(3 Breaking (:rewrite lemma12) on (delta a (+ 1 j)):The integer after the open parenthesis indicates the depth of nested break-rewrite calls. In this discussion we use
3consistently for this integer. Unless you abort or somehow enter unbalanced parentheses into the script, the entire session at a given depth will be enclosed in balanced parentheses, making it easy to skip over them in Emacs.
You then will see the break-rewrite prompt:
3 ACL2 !>The leading integer is, again, the depth. Because breaks often occur recursively it is convenient always to know the level with which you are interacting.
You may type arbitrary commands as in the top-level ACL2 loop. For example, you might type:
3 ACL2 !>:helpor
3 ACL2 !>:pe lemma12More likely, upon entering break-rewrite you will determine the context of the attempted application. Here are some useful commands:
3 ACL2 >:target ; the term being rewritten 3 ACL2 >:unify-subst ; the unifying substitution 3 ACL2 >:path ; the stack of goals pursued by the rewriter ; starting at the top-level clause being simplified ; and ending with the current applicationAt this point in the interaction the system has not yet tried to apply the monitored rule. That is, it has not tried to establish the hypotheses, considered the heuristic cost of backchaining, rewritten the right-hand side of the conclusion, etc. When you are ready for it to try the rule you can type one of several different ``proceed'' commands. The basic proceed commands are
:okexits break-rewrite without further interaction. When break-rewrite exits it prints ``
3)'', closing the parenthesis that opened the level
:goexits break-rewrite without further interaction, but prints out the result of the application attempt, i.e., whether the application succeeded, if so, what the
:targetterm was rewritten to, and if not why the rule was not applicable.
:evalcauses break-rewrite to attempt to apply the rule but interaction at this level of break-rewrite resumes when the attempt is complete. When control returns to this level of break-rewrite a message indicating the result of the application attempt (just as in
:go) is printed, followed by the prompt for additional user input.
:go are used when the break in question
is routine or uninteresting and
:eval is used when the break is one
that the user anticipates is causing trouble. For example, if you
are trying to determine why a lemma isn't being applied to a given
term and the
:target of the current break-rewrite is the term in
question, you would usually
:eval the rule and if break-rewrite
reports that the rule failed then you are in a position to determine
why, for example by carefully inspecting the
governing assumptions or why some hypothesis of the rule could not
It is often the case that when you are in break-rewrite you wish to
change the set of monitored runes. This can be done by using
unmonitor as noted above. For example, you might want
to monitor a certain rule, say
hyp-reliever, just when it is being
used while attempting to apply another rule, say
Typically then you would monitor
main-lemma at the ACL2 top-level,
start the proof-attempt, and then in the break-rewrite in which
main-lemma is about to be tried, you would install a monitor on
hyp-reliever. If during the ensuing
hyp-reliever is broken
you will know it is being used under the attempt to apply
hyp-reliever is being monitored it will be monitored
main-lemma has been tried. That is, if you let the proof
attempt proceed then you may see many other breaks on
breaks that are not ``under'' the attempt to apply
way to prevent this is to
:eval the application of
hyp-reliever before exiting. But this case arises
so often that ACL2 supports several additional ``flavors'' of
:eval! are just like their counterparts
:eval, respectively), except that while
processing the rule that is currently broken no runes are
monitored. When consideration of the current rule is complete,
the set of monitored runes is restored to its original
:eval$ are similar but take an additional argument
which must be a list of runes. An example usage of
3 ACL2 !>:eval$ ((:rewrite hyp-reliever))These three commands temporarily install unconditional breaks on the runes listed, proceed with the consideration of the currently broken rule, and then restore the set of monitored rules to its original setting.
Thus, there are nine ways to proceed from the initial entry into
break-rewrite although we often speak as though there are two,
:eval, and leave the others implicit. We group
because in all their flavors they exit break-rewrite without further
interaction (at the current level). All the flavors of
require further interaction after the rule has been tried.
To abort a proof attempt and return to the top-level of ACL2 you may at any
(a!) followed by a carriage return. If you are not in a raw
Lisp break, you may type
:a! instead. The utility
p! is completely
a! except that it pops up only one
ld level. If you
have just entered the break-rewrite loop, this will pop you out of that loop,
back to the proof. See a! and see p!.
We now address ourselves to the post-
:eval interaction with
break-rewrite. As noted, that interaction begins with
break-rewrite's report on the results of applying the rule: whether
it worked and either what it produced or why it failed. This
information is also printed by certain keyword commands available
addition, by using
brr@ (see brr@) you can obtain this
information in the form of ACL2 data objects. This allows the
development of more sophisticated ``break conditions'';
see monitor for examples. In this connection we point out the
(ok-if term). See ok-if. This command exits
term evaluates to non-
nil and otherwise does not
exit. Thus it is possible to define macros that provide other kinds
of exits from break-rewrite. The only way to exit break-rewrite
:ok (or, equivalently, the use of
ACL2 users who wish to know more about break-rewrite so that they can develop more convenient ways to monitor rules are encouraged to speak to J Moore.
The rest of this documentation discusses a few implementation details of break-rewrite and may not be interesting to the typical user.
There is no ACL2 function named break-rewrite. It is an illusion
created by appropriate calls to two functions named
brkpt2. As previously noted, break-rewrite is
ld operating on a
wormhole state. One might therefore wonder how break-rewrite can
apply a rule and then communicate the results back to the rewriter
running in the external state. The answer is that it cannot.
Nothing can be communicated through a wormhole. In fact,
brkpt2 are each calls of
ld running on wormhole states.
implements the pre-
:eval break-rewrite and
brkpt2 implements the
:eval break-rewrite. The rewriter actually calls
attempting to apply a rule and calls
brkpt2 afterwards. In both
cases, the rewriter passes into the wormhole the relevant
information about the current context. Logically
are no-ops and
rewrite ignores the
nil they return. But while
control is in them the execution of
rewrite is suspended and cannot
proceed until the break-rewrite interactions complete.
This design causes a certain anomoly that might be troubling.
Suppose that inside break-rewrite before
:evaling a rule (i.e., in
brkpt1 wormhole state) you define some function,
:eval the rule and eventually control returns to
break-rewrite (i.e., to
brkpt2 on a wormhole state with the results
of the application in it). You will discover that
foo is no longer
defined! That is because the wormhole state created during your
pre-:eval interaction is lost when we exit the wormhole to resume
the proof attempt. The post-
:eval wormhole state is in fact
identical to the initial pre-
:eval state (except for the results of
the application) because
rewrite did not change the external state
and both wormhole states are copies of it. A similar issue occurs
with the use of trace utilities: all effects of calling
untrace$ are erased when you proceed from a break in the break-rewrite
There is a lot more to know about break-rewrite, most of which is fairly easy to learn from looking at the code, since it is all expressed in ACL2. Feel free to ask questions of J Moore.