Major Section: BREAK-REWRITE
Example: :brr t ; if you haven't done that yet :monitor (:rewrite lemma12) t ; to install a break point on the ; rule named (:rewrite lemma12)
ACL2 does not support Nqthm's
break-lemma but supports a very
similar and more powerful break facility. Suppose some proof is
failing; apparently some particular rule is not being used and you
wish to learn why. Then you need the ACL2 break-rewrite facility.
See break-rewrite and all of its associated
doc topics for
details. The following basic steps are required.
(1) To enable the ``break rewrite'' feature, you must first execute
ACL2 !>:brr tat the top-level of ACL2. Equivalently, evaluate
(brr t). Break-rewrite stays enabled until you disable it with
(brr nil). When break-rewrite is enabled the ACL2 rewriter will run slower than normal but you will be able to monitor the attempts to apply specified rules.
(2) Decide what runes (see rune) you wish to monitor. For
example, you might want to know why
(:rewrite lemma12 . 2) is not
being used in the attempted proof. That, by the way, is the name of
the second rewrite rule generated from the event named
ACL2 !>:monitor (:rewrite lemma12 . 2) twill install an ``unconditional'' break point on that rule. The ``
t'' at the end of the command means it is unconditional, i.e., a break will occur every time the rule is tried. ACL2 supports conditional breaks also, in which case the
tis replaced by an expression that evaluates to non-
nilwhen you wish for a break to occur. See monitor. The above keyword command is, of course, equivalent to
ACL2 !>(monitor '(:rewrite lemma12 . 2) t)which you may also type. You may install breaks on as many rules as you wish. You must use
monitoron each rule. You may also change the break condition on a rule with
unmonitor(see unmonitor) to remove a rule from the list of monitored rules.
(3) Then try the proof again. When a monitored rule is tried by the
rewriter you will enter an interactive break, called break-rewrite.
See break-rewrite for a detailed description. Very simply,
break-rewrite lets you inspect the context of the attempted
application both before and after the attempt. When break-rewrite
is entered it will print out the ``target'' term being rewritten.
If you type
:go break-rewrite will try the rule and then exit,
telling you (a) whether the rule was applied, (b) if so, how the
target was rewritten, and (c) if not, why the rule failed. There
are many other commands. See brr-commands.
(4) When you have finished using the break-rewrite feature you should disable it to speed up the rewriter. You can disable it with
ACL2 !>:brr nilThe list of monitored rules and their break conditions persists but is ignored. If you enable break-rewrite later, the list of monitored rules will be displayed and will be used again by rewrite.
You should disable the break-rewrite feature whenever you are not intending to use it, even if the list of monitored rules is empty, because the rewriter is slowed down as long as break-rewrite is enabled.
Finally, a wonderful trick is the following. When there is a stack
overflow, abort the proof and then try it again after turning on
rewrite stack monitoring with
:brr t. Then, provoke the stack
overflow again. Quit the ACL2 top-level loop and execute the
following form in raw Lisp:
The loop in the rewriter will probably be evident!
(cw-gstack *deep-gstack* state)
Major Section: BREAK-REWRITE
Example: :brr t ; enable :brr nil ; disablewhere
General Form: (brr flg)
nil. This function modifies
stateso that the attempted application of certain rewrite rules are ``broken.'' ``
Brr'' stands for ``break-rewrite'' and can be thought of as a mode with two settings. The normal mode is ``disabled.''
brr mode is ``enabled'' the ACL2 rewriter monitors the attempts
to apply certain rules and advises the user of those attempts by
entering an interactive wormhole break. From within this break the
user can watch selected application attempts.
The rules monitored are selected by using the
commands. It is possible to break a rune ``conditionally'' in the
sense that an interactive break will occur only if a specified
predicate is true of the environment at the time of the attempted
application. See monitor and see unmonitor.
Even if a non-empty set of rules has been selected, no breaks will
brr mode is enabled. Thus, the first time in a session
that you wish to monitor a rewrite rule, use
t to enable
mode. Thereafter you may select runes to be monitored with
unmonitor with the effect that whenever monitored rules are
tried (and their break conditions are met) an interactive break will
occur. Be advised that when
brr mode is enabled the rewriter is
somewhat slower than normal. Furthermore, that sluggishness
persists even if no runes are monitored. You may regain normal
performance -- regardless of what runes are monitored -- by
brr mode with
brr mode disabled automatically when no runes are
monitored? More generally, why does ACL2 have
brr mode at all? Why
not just test whether there are monitored runes? If you care about
the answers, see why-brr.
Major Section: BREAK-REWRITE
#. abort to ACL2 top-level :target term being rewritten :unify-subst substitution making :lhs equal :target :hyps hypotheses of the rule :hyp i ith hypothesis of the rule :lhs left-hand side of rule's conclusion :rhs right-hand side of rule's conclusion :type-alist type assumptions governing :target :initial-ttree ttree before :eval (see ttree) :ancestors negations of backchaining hypotheses being pursued :wonp indicates if application succeed (after :eval) :rewritten-rhs rewritten :rhs (after :eval) :final-ttree ttree after :eval (see ttree) :failure-reason reason rule failed (after :eval) :path rewrite's path from top clause to :target :frame i ith frame in :path :top top-most frame in :path :ok exit break :go exit break, printing result :eval try rule and re-enter break afterwards :ok! :ok but no recursive breaks :go! :go but no recursive breaks :eval! :eval but no recursive breaks :ok$ runes :ok with runes monitored during recursion :go$ runes :go with runes monitored during recursion :eval$ runes :eval with runes monitored during recursion :help this message :standard-help :help message from ACL2 top-level
Break-rewrite is just a call of the standard ACL2 read-eval-print
ld, on a ``wormhole'' state. Thus, you may execute most
commands you might normally execute at the top-level of ACL2.
However, all state changes you cause from within break-rewrite are
lost when you exit or
:eval the rule. You cannot modify stobjs from
within the break. See break-rewrite for
more details and see ld for general information about the
standard ACL2 read-eval-print loop.
Major Section: BREAK-REWRITE
Example: (brr@ :target) ; the term being rewritten (brr@ :unify-subst) ; the unifying substitutionwhere
General Form: (brr@ :symbol)
:symbolis one of the following keywords. Those marked with
*probably require an implementor's knowledge of the system to use effectively. They are supported but not well documented. More is said on this topic following the table.
:symbol (brr@ :symbol) ------- ---------------------In general
:target the term to be rewritten. This term is an instantiation of the left-hand side of the conclusion of the rewrite-rule being broken. This term is in translated form! Thus, if you are expecting (equal x nil) -- and your expectation is almost right -- you will see (equal x 'nil); similarly, instead of (cadr a) you will see (car (cdr a)). In translated forms, all constants are quoted (even nil, t, strings and numbers) and all macros are expanded.
:unify-subst the substitution that, when applied to :target, produces the left-hand side of the rule being broken. This substitution is an alist pairing variable symbols to translated (!) terms.
:wonp t or nil indicating whether the rune was successfully applied. (brr@ :wonp) returns nil if evaluated before :EVALing the rule.
:rewritten-rhs the result of successfully applying the rule or else nil if (brr@ :wonp) is nil. The result of successfully applying the rule is always a translated (!) term and is never nil.
:failure-reason some non-nil lisp object indicating why the rule was not applied or else nil. Before the rule is :EVALed, (brr@ :failure-reason) is nil. After :EVALing the rule, (brr@ :failure-reason) is nil if (brr@ :wonp) is t. Rather than document the various non-nil objects returned as the failure reason, we encourage you simply to evaluate (brr@ :failure-reason) in the contexts of interest. Alternatively, study the ACL2 function tilde-@- failure-reason-phrase.
:lemma * the rewrite rule being broken. For example, (access rewrite-rule (brr@ :lemma) :lhs) will return the left-hand side of the conclusion of the rule.
:type-alist * a display of the type-alist governing :target. Elements on the displayed list are of the form (term type), where term is a term and type describes information about term assumed to hold in the current context. The type-alist may be used to determine the current assumptions, e.g., whether A is a CONSP.
:ancestors * a list of translated terms each of which may be assumed to be true because the rewriter is currently trying to prove each nil. When the rewriter recursively rewrites a hypothesis of a rule it adds the negation of the hypothesis to ancestors. Ancestors is primarily used to prevent infinite backchaining.
:gstack * the current goal stack. The gstack is maintained by rewrite and is the data structure printed as the current ``path.'' Thus, any information derivable from the :path brr command is derivable from gstack. For example, from gstack one might determine that the current term is the second hypothesis of a certain rewrite rule.
brr@-expressionsare used in break conditions, the expressions that determine whether interactive breaks occur when monitored runes are applied. See monitor. For example, you might want to break only those attempts in which one particular term is being rewritten or only those attempts in which the binding for the variable
ais known to be a
consp. Such conditions can be expressed using ACL2 system functions and the information provided by
brr@. Unfortunately, digging some of this information out of the internal data structures may be awkward or may, at least, require intimate knowledge of the system functions. But since conditional expressions may employ arbitrary functions and macros, we anticipate that a set of convenient primitives will gradually evolve within the ACL2 community. It is to encourage this evolution that
brr@provides access to the
Major Section: BREAK-REWRITE
Example: (monitor '(:rewrite assoc-of-app) 't) :monitor (:rewrite assoc-of-app) t :monitor (:definition app) (equal (brr@ :target) '(app c d))where
General Form: (monitor rune term)
runeis a rune and
termis a term, called the ``break condition.''
Runemust be either a
:rewriterune (of subclass
backchain) or a
:definitionrune. (Note: Some
:rewriterules are considered ``simple abbreviations'' -- see simple -- and cannot be monitored. Monitoring is carried out by code inside the rewriter but abbreviation rules are applied by a special purpose simplifier.) 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. See break-rewrite for a description of the interactive loop entered. Whether an interactive break occurs depends on the value of the break condition expression associated with the monitored rune.
To remove a rune from the list of monitored runes, use
To see which runes are monitored and what their break conditions
monitored-runes are macros that expand into
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 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,
expr, 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
t, or a true list of commands to be fed to the
resulting interactive break. Whenever the system attempts to use
the associated rule,
expr is evaluated in the wormhole interaction
state. A break occurs only if the result of evaluating
nil. If the result is a true list, that list is appended to the
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
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
:sym is one of several keyword symbols, including
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@.
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
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-
(: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
break-rewriteto (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
:monitormerely ``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,
break-rewriteto print out the unifying substitution. Then in response to
nilthe 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-ifwith its following expression, is a conditional exit command. It means exit
break-rewriteif 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-rewriteexpects more input. Therefore, it begins prompting the user for input. The end result, then, of the above
:monitorcommand is that the rune in question is elaborately traced and interactive breaks occur whenever it rewrites its target to
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:
break-if-result-is. For example, the last
could be defined as
(defmacro break-if-result-is (rune term) `(monitor ',rune ''(: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.
Major Section: BREAK-REWRITE
Example and General Form: :monitored-runes
This macro prints a list, each element of which is of the form
(rune expr), showing each monitored rune and its current break
Major Section: BREAK-REWRITE
Example Form: :ok-if (null (brr@ :wonp))where
General Form: :ok-if expr
expris a term involving no free variables other than
stateand returning one non-
stateresult which is treated as Boolean. This form is intended to be executed from within
Consider first the simple situation that the
(ok-if term) is a
command read by
break-rewrite. Then, if the term is non-
break-rewrite exits and otherwise it does not.
ok-if returns an ACL2 error triple
(mv erp val state). (See ld for more on error triples.) If
any form being evaluated as a command by
the triple returned by
(ok-if term) then the effect of that form
is to exit break-rewrite if term is non-
nil. Thus, one
might define a function or macro that returns the value of
expressions on all outputs and thus create a convenient new way to
The exit test,
term, generally uses
brr@ to access context sensitive
information about the attempted rule application. See brr@.
Ok-if is useful inside of command sequences produced by break
conditions. See monitor.
:ok-if is most useful after an
command has caused
break-rewrite to try to apply the rule because in
the resulting break environment
expr can access such things as
whether the rule succeeded, if so, what term it produced, and if
not, why. There is no need to use
:evaling the rule
since the same effects could be achieved with the break condition on
the rule itself. Perhaps we should replace this concept with
:eval-and-break-if? Time will tell.
Major Section: BREAK-REWRITE
Examples: (unmonitor '(:rewrite assoc-of-app)) :unmonitor (:rewrite assoc-of-app) :unmonitor :allHere,
General Forms: (unmonitor rune) (unmonitor :all)
runeis a rune that is currently among those with break points installed. This function removes the break.
Subtle point: Because you may want to unmonitor a ``rune'' that is
no longer a rune in the current ACL2 world, we don't actually check
this about rune. Instead, we simply check that rune is a
beginning with a
keywordp. That way, you'll know you've made a
mistake if you try to
:unmonitor binary-append instead of
:unmonitor (:definition binary-append), for example.