Break-rewrite
The read-eval-print loop entered to monitor rules
ACL2 allows the user to monitor the application of rewrite, definition, and linear 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''; see brr-commands.
For a related proof debugging utility, see with-brr-data. Also see
dmr (Dynamically Monitor Rewrites), which allows you to watch progress
of the rewriter in real time.
To abort from inside break-rewrite at any time, execute :a!.
Output from break-rewrite is abbreviated by default, but that can be
changed. See set-brr-evisc-tuple.
For further information, see the related :doc topics listed
below.
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
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 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, at a high level, 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. For example, all invocations of
trace$ and untrace$ that are made during a break at a monitored rune are undone when proceeding from that break. 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.
There are however exceptions to this loss of state when exiting a break.
One exception is that the effect of turning on iprinting in a break (see set-iprint) will persist even after exiting the break. The other exceptions
pertain to setting the brr-evisc-tuple or invoking monitor or
unmonitor: if these are done inside the break-rewrite loop at level 1
of interaction (i.e., at the top level) then their effects will persist even
after exiting the break.
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
Exceptions are that :ubt and related commands such as
:ubu, as well as puff and puff*, are only allowed
to touch commands issued after entering the interactive break.
(Technical detail: that is because disable-ubt is invoked when
entering the break.)
More likely than typing a history command, 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 and perhaps the linear-arithmetic :pot-list 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 (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
analogous to 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 after :eval, namely :wonp,
:rewritten-rhs or (for linear rules) :poly-list, and
:failure-reason. In addition, by using 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).
Note that when inside break-rewrite, all history commands, such as
:pe, show the enabled status of rules with respect to the
current point in the proof attempt. For example, if you break while the
prover is working on Subgoal 3, and the hints supplied for the proof
specify ("Subgoal 3" :in-theory (disable foo)) for some rule foo,
then :pe will indicate that foo is disabled: even
though foo may be enabled globally, it is shown as disabled because it is
disabled during Subgoal 3. See subtopics of history for a list of all
such history commands. In addition to those commands, the function disabledp is also evaluated inside break-rewrite with respect to the current
enabled state of the prover.
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 anomaly 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.
A similar issue occurs with the use of trace utilities: all effects of
calling trace$ and untrace$ are erased when you proceed from a
break in the break-rewrite loop.
See the subtopics listed below to learn more about
break-rewrite.
Subtopics
- Monitor
- To monitor the attempted application of a rule name
- Brr
- To enable or disable the breaking of rewrite rules
- Dmr
- Dynamically monitor rewrites and other prover activity
- With-brr-data
- Finding the source of a term in prover output
- Break-lemma
- A quick introduction to breaking rewrite rules in ACL2
- Why-brr
- An explanation of why ACL2 has an explicit brr mode
- Brr@
- To access context sensitive information within break-rewrite
- Brr-commands
- Break-Rewrite Commands
- Cw-gstack
- Debug a rewriting loop or stack overflow
- Ok-if
- Conditional exit from break-rewrite
- Windows-installation
- Installing ACL2 on Windows
- Unmonitor
- To stop monitoring a rule name
- Monitor!
- A quiet combination of monitor and brr
- Monitored-runes
- Print the monitored runes and their break conditions
