Puff
Replace a compound command by its immediate subevents
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 below). Puff
replaces the command at cd by the immediate subevents of the command, executed as commands. Puff then prints, using pcs, the puffed region.
We consider puff to be a sort of hack; it is generally robust and
sound, but that is not guaranteed. If any existing ACL2 event resulted from
puff, ACL2 considers proofs to have been skipped, and thus certify-book is disallowed until such events have been undone (see ubt).
Other than the few exceptions noted later below, a ``puffable'' command is an encapsulate, include-book, or certify-book command, or any command other than those consisting of a
single primitive event. For example, since defun is a primitive
event, a defun command is not puffable. But a macro form that expands
into one or more events is puffable. The only primitive events that
are puffable are calls of encapsulate or include-book. In
this sense, make-event is not considered primitive — that is, it
can be puffed — and moreover, an immediate subevent that is a call of
make-event is generally replaced by its expansion (see make-event). A puffable command contains (interesting) subevents,
namely, the events in the body of the encapsulate, in the file of the
book included, or in the command block.
The puff command ``lifts'' the immediate subevents of the indicated
command so that they become commands themselves. The command puff* recursively puffs the newly introduced commands.
See puff*, which also gives an example illustrating both puff and
puff*. Puff undoes the command at cd and replaces it
by its immediate subevents. Thus, in general the length of the history
grows when a puff command is executed. If puff causes an error
(see below), the logical world remains unchanged from its initial
configuration.
The intended use of puff is to allow the user access to the events ``hidden'' inside compound commands. For example, while trying
to prove some theorem, p, about a constrained function, fn, one
might find that the encapsulate, cd, that introduced fn
failed to include an important constraint, q. Without puff,
the only way to proceed is to undo back through cd, create a suitable
encapsulate that proves and exports q as well as the old constraints, re-execute the new encapsulate, re-execute the events since cd, and then try p again. Unfortunately, it may be
hard to prove q and additional events may have to be inserted into
the encapsulate to prove it. It may also be hard to formulate the
``right'' q, i.e., one that is provable in the encapsulate and
provides the appropriate facts for use in the proof of p.
Using puff, the user can erase the encapsulate at cd,
replacing it by the events in its body. Now the formerly constrained
function, fn, is defined as its witness. The user can experiment with
formulations and proofs of q suitable for p. Of course, to get into
the ultimately desired state — where fn is constrained
rather than defined and q is exported by an encapsulate at
cd — the user must ultimately undo back to cd and carry out
the more tedious program described above. But by using puff it is easier
to experiment.
Similar applications of puff allow the user of a book to expose the
top-level events in the book as though they had all been typed as commands. The user might then ``partially undo'' the book, keeping only some
of the events in it.
Puff operates as follows. First, it determines the list of immediate
subevents of the command indicated by cd. It causes an error if
there is only one subevent and that subevent is identical to the command — i.e., if the command at cd is a primitive. Next,
puff undoes back through the indicated command. This not only
erases the command at cd but all the commands executed
after it. Finally, puff re-executes the subevents of (the now erased)
cd followed by all the commands that were executed afterwards.
Observe that the commands executed after cd will generally have
higher command numbers than they did before the puff. For example,
suppose 100 commands have been executed and that :puff 80 is then
executed. Suppose command 80 contains 5 immediate subevents (i.e., is
an encapsulation of five events). Then, after puffing, command
80 is the first event of the puffed command, command 81 is the
second, and so on; 104 commands appear to have been executed.
When puffing an encapsulate or include-book, the local commands are executed. Note that this will replace constrained
functions by their witnesses.
Here are some details and a few exceptions.
- An encapsulate command that generates unknown-constraints,
such as one generated by the macro define-trusted-clause-processor, is
not puffable.
- When an encapsulate has a non-empty signature, it is not
puffable if the `puff' command issued is :puff*, rather than
:puff. That is because puffing may fail in this case, as discussed
immediately below, and it may be annoying to deal with the failure, for
example if :puff* takes a long time to run.
- An attempt to puff may fail for an encapsulate with a non-empty
signature that contains at least one use of make-event and also
comes from a certified book. The reason is that local definitions may be
elided. Here is an example of such a book.
(in-package "ACL2")
(encapsulate
((f (x) t))
(make-event '(local (defun f (x) (cons x x))))
(defthm f-prop (consp (f x))))
If we first certify this book, then we include it in a new ACL2 session, and
next we issue the command :puff 1, then we can see that the local
definition in our encapsulate event has been elided:
ACL2 !>:pcb! 1
1 (ENCAPSULATE
((F (X) T))
(RECORD-EXPANSION
(MAKE-EVENT '(LOCAL (DEFUN F (X) (CONS X X))))
(LOCAL (VALUE-TRIPLE :ELIDED)))
(DEFTHM F-PROP (CONSP (F X))))
(DEFTHM F-PROP (CONSP (F X)))
ACL2 !>
Now an attempt to execute the command, :puff 1, causes an error because
f lacks a definition.
ACL2 !>:puff 1
ACL2 Error in ( DEFTHM F-PROP ...): The symbol F (in package "ACL2")
has neither a function nor macro definition in ACL2. Please define
it. See :DOC near-misses. Note: this error occurred in the context
(F X).
ACL2 !>
- Similarly, a local event that involves make-event
expansion may be elided when the event is from a book whose include-book form has been puffed. This will result in an error if the
elided event is necessary to support later events in the puff of the
command. Here is an example, where the attempt to puff an include-book
for this book will fail, giving an error for ( DEFUN G ...) stating that
the symbol F has not been defined.
(in-package "ACL2")
(make-event '(local (defun f (x) x)))
(local (defun g (x) (f x)))
- An attempt to puff an include-book command may fail for a
book that has been modified, as described later in this documentation
topic.
- The puff of an include-book command for an uncertified
book will simply expose the contents of the book. However, if the book is
certified then the puff will replace each event by its make-event
expansion. Also, ACL2 considers that (certified) book to have been included;
future attempts to include that book will be considered to be redundant.
Finally, we note that it is an error to puff in the presence of include-book events for certified books that have been altered since
they were included. (Note that this restriction only applies to include-book, not to certify-book.) To be specific, suppose
"arith" is a certified book that has been included in a session.
Suppose that after "arith" was included, the source file is modified.
(This might happen if the user of "arith" is not its author and the
author happens to be working on a new version of "arith" during the
same time period.) Now suppose the user tries to puff the command
that included "arith". The attempt to obtain the subevents in
"arith" will discover that the book-hash of "arith" has
changed and an error will be caused. No change is made in the logical world. A similar error is caused if, in this same situation, the user tries
to puff any command that occurred before the inclusion of "arith"!
That is, puff may cause an error and leave the world unchanged
even if the command puffed is not one involving the modified book.
This happens because in order to reconstruct the world after the puffed
command, puff must obtain the events in the book and if the
book's source file has changed there is no assurance that the reconstructed
world is the one the user intends.
Warning: We do not detect changes to uncertified books that have
been included and are then puffed or re-included! The act of including an
uncertified book leaves no trace of the book-hash value for the book.
Furthermore, the act prints a warning message disclaiming soundness. In light
of this, :puff quietly ``re-''executes the current contents of the
book.
