BREAK-LEMMA

a quick introduction to breaking rewrite rules in ACL2 

Parent topic:  BREAK-REWRITE
Home


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 t
at 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 lemma12.

The command 

ACL2 !>:monitor (:rewrite lemma12 . 2) t
will 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 t is replaced by an expression that evaluates to non-nil when 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 monitor on each rule. You may also change the break condition on a rule with monitor. Use 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 nil
The 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: 



  (cw-gstack *deep-gstack* state)
The loop in the rewriter will probably be evident!

BRR

to enable or disable the breaking of rewrite rules 

Parent topic:  BREAK-REWRITE
Home


Example:
:brr t       ; enable
:brr nil     ; disable


General Form:
(brr flg)
where flg evaluates to t or nil. This function modifies state so 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.''

When 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. See break-rewrite.

The rules monitored are selected by using the monitor and unmonitor 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 occur unless brr mode is enabled. Thus, the first time in a session that you wish to monitor a rewrite rule, use :brr t to enable brr mode. Thereafter you may select runes to be monitored with monitor and 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 disabling brr mode with :brr nil.

Why isn't 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.

BRR-COMMANDS

Break-Rewrite Commands 

Parent topic:  BREAK-REWRITE
Home


#.              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
: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
: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 loop, ld, on a ``wormhole'' state. Thus, you may execute any command 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. See break-rewrite for more details and see ld for general information about the standard ACL2 read-eval-print loop.

BRR@

to access context sensitive information within break-rewrite 

Parent topic:  BREAK-REWRITE
Home


Example:
(brr@ :target)      ; the term being rewritten
(brr@ :unify-subst) ; the unifying substitution


General Form:
(brr@ :symbol)
where :symbol is 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)
-------             ---------------------


: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.
In general brr@-expressions are 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 a is 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 *'d data.

MONITOR

to monitor the attempted application of a rule name 

Parent topic:  BREAK-REWRITE
Home


Example:
(monitor '(:rewrite assoc-of-app) 't)
:monitor (:rewrite assoc-of-app) t
:monitor (:definition app) (equal (brr@ :target) '(app c d))


General Form:
(monitor rune term)
where rune is a rune and term is a term, called the ``break condition.'' Rune must be either a :rewrite rune (of subclass backchain) or a :definition rune. (Note: Some :rewrite rules 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 unmonitor. To see which runes are monitored and what their break conditions are, evaluate (monitored-runes).

Monitor, unmonitor and monitored-runes are macros that expand into expressions involving 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 nil, 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 expr is non-nil. If the result is a true list, that list is appended to the front of 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 brr@ macro 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 (brr@ :sym) where :sym is one of several keyword symbols, including :target (the 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@.

For example, 

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 it returns nil.

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-nil true list (: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 :go causes break-rewrite to (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 :monitor merely ``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, :unify-subst, causes break-rewrite to print out the unifying substitution. Then in response to :eval$ nil the 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-if with its following expression, is a conditional exit command. It means exit break-rewrite if 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-rewrite expects more input. Therefore, it begins prompting the user for input. The end result, then, of the above :monitor command is that the rune in question is elaborately traced and interactive breaks occur whenever it rewrites its target to (foo a).

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: trace-rune, break-if-target-is, and 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.

MONITORED-RUNES

print the monitored runes and their break conditions 

Parent topic:  BREAK-REWRITE
Home


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 condition.

OK-IF

conditional exit from break-rewrite 

Parent topic:  BREAK-REWRITE
Home


Example Form:
:ok-if (null (brr@ :wonp))


General Form:
:ok-if expr
where expr is a term involving no free variables other than state and returning one non-state result which is treated as Boolean. This form is intended to be executed from within break-rewrite (see break-rewrite).

Consider first the simple situation that the (ok-if term) is a command read by break-rewrite. Then, if the term is non-nil, break-rewrite exits and otherwise it does not.

More generally, 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 break-rewrite returns 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 ok-if expressions on all outputs and thus create a convenient new way to exit break-rewrite.

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 :eval 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 :ok-if before :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.

UNMONITOR

to stop monitoring a rule name 

Parent topic:  BREAK-REWRITE
Home


Examples:
(unmonitor '(:rewrite assoc-of-app))
:unmonitor (:rewrite assoc-of-app)
:unmonitor :all


General Forms:
(unmonitor rune)
(unmonitor :all)
Here, rune is 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 consp 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.