Major Section: HISTORY
Example Forms: ACL2 !>:puff* :max ACL2 !>:puff* :x ACL2 !>:puff* 15 ACL2 !>:puff* "book"where
General Form: :puff* cd
cdis 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.
Puff*is just the recursive application of puff.
Puff*prints the region puffed, using
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
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
defuns for the functions
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
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.
:puff 1 is executed in the starting state. Then the first
command is replaced by its immediate subevents and
:pbt 1 would
1 (INCLUDE-BOOK "a") 2 (INCLUDE-BOOK "b") 3 (INCLUDE-BOOK "c")Contrast this with the execution of
:puff* 1in 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* 1in 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).