PUFF*

replace a compound command by its subevents 
Major Section:  HISTORY


Example Forms:
ACL2 !>:puff* :max
ACL2 !>:puff* :x
ACL2 !>:puff* 15
ACL2 !>:puff* "book"

General Form:
:puff* cd
where cd is a command descriptor (see command-descriptor) for a ``puffable'' command. See puff for the definition of ``puffable'' and for a description of the basic act of ``puffing'' a command. In particular, see puff for a discussion of a sense in which puff, and hence puff*, should be viewed as a hack. Puff* is just the recursive application of puff. Puff* prints the region puffed, using pcs.

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.

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