BREAK-REWRITE

the read-eval-print loop entered to monitor rewrite rules 
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.''

To abort from inside break-rewrite at any time, execute sharpsign-period (#.).

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-nil, 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 the ld-special 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 ld 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.

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 3 consistently 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 !>:help
or 
3 ACL2 !>:pe lemma12
More 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 application
At 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 :ok, :go, and :eval. 
:ok
exits break-rewrite without further interaction. When break-rewrite exits it prints ``3)'', closing the parenthesis that opened the level 3 interaction. 
:go
exits break-rewrite without further interaction, but prints out the result of the application attempt, i.e., whether the application succeeded, if so, what the :target term was rewritten to, and if not why the rule was not applicable. 
:eval
causes 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.

Generally speaking, :ok and :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 :type-alist of governing assumptions or why some hypothesis of the rule could not be established.

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 :monitor and :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 main-lemma. 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 :eval hyp-reliever is broken you will know it is being used under the attempt to apply main-lemma.

However, once hyp-reliever is being monitored it will be monitored even after main-lemma has been tried. That is, if you let the proof attempt proceed then you may see many other breaks on hyp-reliever, breaks that are not ``under'' the attempt to apply main-lemma. One way to prevent this is to :eval the application of main-lemma and then :unmonitor hyp-reliever before exiting. But this case arises so often that ACL2 supports several additional ``flavors'' of proceed commands.

:Ok!, :go!, and :eval! are just like their counterparts (:ok, :go, and :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 setting.

:Ok$, :go$, and :eval$ are similar but take an additional argument which must be a list of runes. An example usage of :eval$ is 

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, :ok and :eval, and leave the others implicit. We group :go with :ok because in all their flavors they exit break-rewrite without further interaction (at the current level). All the flavors of :eval 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 time type #. (that is, number-sign followed by a period) followed by a carriage return.

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 after :eval, namely :wonp, :rewritten-rhs, and :failure-reason. In 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 macro form (ok-if term). See ok-if. This command exits break-rewrite if 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 after :eval is :ok (or, equivalently, the use of ok-if).

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 brkpt1 and 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, brkpt1 and brkpt2 are each calls of ld running on wormhole states. Brkpt1 implements the pre-:eval break-rewrite and brkpt2 implements the post-:eval break-rewrite. The rewriter actually calls brkpt1 before 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 brkpt1 and brkpt2 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 the brkpt1 wormhole state) you define some function, foo. Suppose then you :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.

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.