Puff*
Replace a compound command by its subevents
Example Forms:
ACL2 !>:puff* :max
ACL2 !>:puff* :x
ACL2 !>:puff* 15
ACL2 !>(puff* 15) ; same as just above
ACL2 !>(puff* 15 t) ; same as just above, but keep partial results
ACL2 !>:puff* "book"
General Forms:
:puff* cd
(puff* 'cd) ; argument can be any expression evaluating to cd
(puff* 'cd b) ; where b is t or nil
where cd is a command descriptor (see command-descriptor). See puff for the definition of ``puffable'' and
for a description of the basic act of ``puffing'' a command.
Puff* is just the recursive application of puff: it puffs not only
the indicated command, but all of the commands thus generated, and recursively
until none of the resulting commands can be puffed. As noted in the
documentation for puff, :puff should be viewed as a sort of hack;
hence so should puff*. Puff* prints the region puffed, using
pcs.
Thus, to puff a command is to replace it by its immediate
subevents, each of which is executed as a command. To puff* a
command is to replace the command by each of its immediate
subevents and then to puff* each of the puffable commands among
the newly introduced ones. NOTE: because one call of :puff* may give rise
to many calls of :puff, it can take considerable time for a call of
:puff* to complete when many books are involved.
For example, suppose "ab" is a book containing the following
(in-package "ACL2")
(include-book "a")
(include-book "b")
Suppose that book "a" only contained defuns for the
functions a1 and a2 and that "b" only contained defuns for b1 and b2.
Now consider an ACL2 state in which only two commands have
been executed, the first being (include-book "ab") and the second being
(include-book "c"). Thus, the relevant part of the display produced by
:pbt 1 would be:
1 (INCLUDE-BOOK "ab")
2 (INCLUDE-BOOK "c")
Call this state the ``starting state'' in this example,
because we will refer to it several times.
Suppose :puff 1 is executed in the starting state. Then the
first command is replaced by its immediate subevents and :pbt 1
would show:
1 (INCLUDE-BOOK "a")
2 (INCLUDE-BOOK "b")
3 (INCLUDE-BOOK "c")
Contrast this with the execution of :puff* 1 in the starting state. Puff* would first puff (include-book "ab") to get
the state shown above. But then it would recursively puff* the
puffable commands introduced by the first puff. This continues
recursively as long as any puff introduced a puffable command.
The end result of :puff* 1 in the starting state is
1 (DEFUN A1 ...)
2 (DEFUN A2 ...)
3 (DEFUN B1 ...)
4 (DEFUN B2 ...)
5 (INCLUDE-BOOK "c")
Observe that when puff* is done, the originally indicated command, (include-book "ab"), has been replaced by the corresponding
sequence of primitive events. Observe also that puffable commands elsewhere in the history, for example, command 2 in
the starting state, are not affected (except that their command
numbers grow as a result of the splicing in of earlier commands).
:Puff* may cause an error, for example because of a name conflict
caused by two different local lemmas with the same name, or because a local event in a book has been elided (see puff). By default, the
logical world is reverted to its value before that execution of
puff*. However, if the optional Boolean second argument is t, then
the world is preserved from the successful :puff commands executed before
the failed one. That behavior can help with debugging, since both the warning
message and the return value tell you which command could not be puffed
successfully.
