Major Section: HISTORY
Example Forms: ACL2 !>:puff* :max ACL2 !>:puff* :x ACL2 !>:puff* 15 ACL2 !>:puff* "book"whereGeneral Form: :puff* cd
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. 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).
