Break-rewrite
A version of the ACL2 rewriter with interactive breaks
ACL2 allows the user to monitor the application of rewrite, definition, and linear rules. When the rewriter is
about to try to apply an enabled monitored rule, it can trigger
an interactive break managed by a version of the rewriter called
“break-rewrite”. These breaks can be caused by
- failure of a rewrite rule's equivalence relation
to be a known refinement of the permitted relations,
- failure of
a rule's triggering pattern to match the target term while “almost”
matching,
- failure to relieve the hypotheses of the rule, or
- failure of any of several heuristic checks to prevent looping in the rewriter.
From within this read-eval-print loop you can inspect the context, attempt
to apply the rule, and see what happens. This interactive loop is technically
just a call of the standard ACL2 read-eval-print loop, ld, on a
``wormhole state'' (see wormhole). 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.
Interactive breaks occur only if the break-rewrite utility is turned
on (see brr), a monitored rune is being considered by the rewriter,
and the break conditions specified in the monitor are satisfied (see monitor).
The following utilities can also be helpful for proof debugging.
- Dmr (Dynamically Monitor Rewrites) allows you to watch progress of
the rewriter in real time.
- The proof-builder allows you to interactively construct a
proof.
- with-brr-data helps you to find the source of a term in prover
output.
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.
When the break-rewrite facility is turned on (see brr), the
rewriter performs more sluggishly than when break-rewrite is turned off.
Therefore if you have done (brr t) to debug a rewriting problem, we
recommend that you do (brr nil) after the situation is remedied and you
resume normal proof development.
For further information, see the related :doc topics listed
below.
Advice to Developers and Maintainers of ACL2: If you intend to
modify break-rewrite, we strongly urge you to read the Essay on Break-Rewrite
in the source code file rewrite.lisp. There we explain the abstraction
provided by break-rewrite, how it is implemented as a state machine operating
in a wormhole, and some low-level tools for inspecting the state of
break-rewrite. Attempts to add new features without understanding virtually
everything about the implementation is most likely to create a mess.
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, an
interactive read-eval-print loop 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 such a break are
undone when proceeding from that break (including when proceeding via the
:eval brr-command). 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 pertains to iprinting (see set-iprint). When iprinting
is enabled in a break, it nevertheless is again disabled upon exiting the
break. However, the association of values with iprint indices persists even
after exiting the break; that is, you can still obtain their values, and if
you re-enable iprinting then indices will be generated from where they left
off rather than returning to index 1. The other exception pertains to setting
the brr-evisc-tuple while inside break-rewrite: the effects persist.
See set-brr-evisc-tuple.
When you 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
The output of the :path command shows a stack of simplification and
rewriting ``frames'' starting with the current top-level goal (in clausal form
as a list of literals) and ending with the current target. Frames should be
self-explanatory. Frames describing the attempt to apply a rewrite rule will
display the name of the equivalence relation the rule uses (unless the
relation is equal). All rewrite frames (including the attempt to apply a
given rewrite rule) will display the current geneqv (the sense of
equivalence the rewriter is obligated to maintain) unless the geneqv denotes
just the equality relation.
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 at the current depth. When
break-rewrite exits it prints ``3)'' (actually, of course, the current
depth!), closing the parenthesis that opened the current depth, 3,
interaction. However, between your typing the :ok command and the exit
from depth 3 you may well see deeper break-rewrite breaks —
triggered by any of your monitored runes — as the rewriter tries to
apply the lemma that prompted the current depth 3 break.
:go
exits break-rewrite without further interaction at the current depth, but
as it exits it 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
depth 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 for the current depth 3.
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 you then :eval and get
a break on hyp-reliever you will know it is being used under the attempt
to apply main-lemma.
However, when the rewriter leaves this attempt to apply main-lemma,
hyp-reliever will no longer be monitored. That is, the list of monitored
runes is maintained as a local variable of break-rewrite. See monitored-runes.
:Ok!, :go!, and :eval! are just like their counterparts
(:ok, :go, and :eval, respectively), except that before
proceeding they unmonitor all runes. Of course, this is only done in the
scope of the interactive break in which these commands were used. When
control returns to the top-level of the ACL2 loop the monitored runes will
have reverted to its original value there. These commands allow you to
proceed from the current depth without getting any deeper breaks.
:Ok$, :go$, and :eval$ are similar but take an additional
argument which must be a list of runic designators (or a single designator).
See rune. Two examples the use of :eval$ are
3 ACL2 !>:eval$ hyp-reliever
and
3 ACL2 !>:eval$ (hyp-reliever (:definition foo))
The second command above is exactly equivalent to
3 ACL2 !>:monitor hyp-reliever t
3 ACL2 !>:monitor (:definition foo) t
3 ACL2 !>:eval
Analogous remarks apply to :go$ and :ok$. If you want to specify
more sophisticated break criteria (rather than just :condition t) you
must use the :monitor command explicitly before proceeding.
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 depth). All the flavors of :eval require
further interaction after the rule has been tried.
You are not permitted to “re-:eval” a rule. That is,
after issuing the :eval command in a given break, you cannot issue it
again in that break. The rule has been evaluated, the results are available
to you, and that's that! All you can do, aside from inspecting the context,
is allow rewrite to continue, by issuing an :ok or :go, or
abort.
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 or, equivalently (if you are
not in a raw Lisp break) use the keyword command :a!. See a!.
We now address ourselves to the post-:eval interaction with
break-rewrite. As noted, post-:eval 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'' that test the context
of the pending break and that return a list of commands to execute if a break
occurs; 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 :go or 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.
We have not discussed “near-miss” breaks. These are caused
when a monitored rune specifies one of the near-miss break criteria and the
rune's pattern fails to match the target but “almost” matches
according to the criteria. See monitor for a discussion of near-miss
break criteria. But for example, if main-lemma rewrites the term
(f (g (h x) y) x) and you've installed a monitor on it like this:
:monitor main-lemma (:abstraction (f (g u v) w))
then if the rewriter encountered the target term (F (G (MUMBLE A) B)
C) it would cause a near-miss break because the pattern of main-lemma
does not match the target but the specified abstraction of the pattern does
match the target.
You interact with a near-miss break just like the breaks described above,
except some commands (e.g., :eval) are unavailable because the rule did
not match and thus there is no way to proceed except to exit the break and try
the next lemma.
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 — which is why we don't
write it in typewriter font in this documentation. Break-rewrite is an
illusion created by appropriate calls to three ``break point handlers'' named
near-miss-brkpt1, 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, the break point handlers are each calls of ld
running on wormhole states. They maintain a state machine
inside the wormhole. For example, brkpt1 is called by rewrite after a
successful match, if the monitored :condition is true, an interactive
break occurs. Upon an :ok or :eval, the wormhole's status
information is updated, the wormhole is exited (losing any state changes made
inside the wormhole), rewrite continues to do whatever rewrite does for that
lemma, and then brkpt2 is called. Brkpt2 then uses the state
information in the wormhole to decide whether to interact or not.
This helps explain why the rewriter behaves more sluggishly when (brr
t) has been done: it is entering and exiting wormholes to figure out whether
to trigger an interactive break. When you are through with break-rewrite, we
recommend (brr nil).
This design causes certain anomalies that might be troubling.
Suppose you are inside a depth 3 break before :evaling a
rule (i.e., you're in the brkpt1 wormhole state) you define
some function, foo. Suppose then you :eval the rule and eventually
control returns to the depth 3 break (i.e., now you're in the brkpt2
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 attempted applications of certain rules by the rewriter
- Brr
- To enable or disable the breaking of rewrite rules
- Brr-commands
- Break-Rewrite Commands
- Dmr
- Dynamically monitor rewrites and other prover activity
- With-brr-data
- Finding the source of a term in prover output
- Geneqv
- the rewriter's generated equivalence relation
- Refinement-failure
- what to do when a rewrite rule fails the refinement check
- 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
- Cw-gstack
- Debug a rewriting loop or stack overflow
- Ok-if
- Conditional exit from break-rewrite
- Windows-installation
- Installing ACL2 on Windows
- Brr-near-missp
- attachable function for determining “near misses”
- Monitored-runes
- Print the monitored runes and their break conditions
- Unmonitor
- To stop monitoring a rule name
- Monitor!
- A quiet combination of monitor and brr
