MONITOR

to monitor the attempted application of a rule name 
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))


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 or a :definition rune.

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.

NOTE: Some :rewrite rules are considered ``simple abbreviations''; see simple. These can be be monitored, but only at certain times during the proof. Monitoring is carried out by code inside the rewriter but abbreviation rules may be applied by a special purpose simplifier inside the so-called preprocess phase of a proof. If you desire to monitor an abbreviation rule, a warning will be printing suggesting that you may want to supply the hint :DO-NOT '(PREPROCESS); see hints. Without such a hint, an abbreviation rule can be applied during the preprocess phase of a proof, and no such application will cause an interactive break.

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
            '(quote (: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.