OOPS

undo a :u or :ubt


Parent topic:  HISTORY
Home

The keyword command :oops will undo the most recent :ubt (or :u, which we here consider just another :ubt). A second :oops will undo the next most recent :ubt, a third will undo the :ubt before that one, and a fourth :oops will return the logical world to its configuration before the first :oops.

Consider the logical world (see world) that represents the current extension of the logic and ACL2's rules for dealing with it. The :ubt and :u commands ``roll back'' to some previous world (see ubt). Sometimes these commands are used to inadvertently undo useful work and user's wish they could ``undo the last undo.'' That is the function provided by :oops.

:Oops is best described in terms of an implementation. Imagine a ring of four worlds and a marker (*) indicating the current ACL2 world:

This is called the ``kill ring'' and it is maintained as follows. When you execute an event the current world is extended and the kill ring is not otherwise affected. When you execute :ubt or :u, the current world marker is moved one step counterclockwise and that world in the ring is replaced by the result, say w0', of the :ubt or :u.

           w0 
         /    \
      *w0'     w1
         \    /
           w2

If you were to execute events at this point, w0' would be extended and no other changes would occur in the kill ring.

When you execute :oops, the marker is moved one step clockwise. Thus the kill ring becomes * w0 / \ w0' w1 \ / w2 and the current ACL2 world is w0 once again. That is, :oops ``undoes'' the :ubt that produced w0' from w0. Similarly, a second :oops will move the marker to w1, undoing the undo that produced w0 from w1. A third :oops makes w2 the current world. Note however that a fourth :oops restores us to the configuration above.

In general, the kill ring contains the current world and the three most recent worlds in which a :ubt or :u were done.

While :ubt may appear to discard the information in the events undone, we can see that the world in which the :ubt occurred is still available. No information has been lost about that world. But :ubt does discard information! :Ubt discards the information necessary to recover from the third most recent ubt! An :oops, on the other hand, discards no information, it just selects the next available world on the kill ring and doing enough :oopses will return you to your starting point.

We can put this another way. You can freely type :oops and inspect the world that you thus obtain with :pe, :pc, and other history commands. You can repeat this as often as you wish without risking the permanent loss of any information. But you must be more careful typing :ubt or :u. While :oops makes :ubt seem ``safe'' because the most recent :ubt can always be undone, information is lost when you execute :ubt.

PBT

print the commands back through a command descriptor


Parent topic:  HISTORY
Home

Examples:
:pbt :max      ; print back through the most recent command
:pbt :x        ; print back through the most recent command
:pbt fn        ; print back through the introduction of fn
:pbt 5         ; print back through the fifth command executed
:pbt (:x -4)   ; print back through the most recent five commands

See command-descriptor.

Pbt takes one argument, a command descriptor, and prints the commands from :max (aka :x) through the one described. See command-descriptor for a description of what a command descriptor is. See pc for a description of the format used to display commands. Pbt will print the commands that ubt will undo.

PC

print the command described by a command descriptor


Parent topic:  HISTORY
Home

Examples:
:pc 3    ; print the third command executed
:pc :max ; print the most recent command
:pc :x   ; print the most recent command
:pc fn   ; print the command that introduced fn

See command-descriptor.

Pc takes one argument, a command descriptor, and prints the command identified by that descriptor. See command-descriptor. For example

ACL2 !>:pc foo
 LVd     52 (DEFUN FOO (X) X)

Pc always prints a space first, followed by three (possibly blank) characters (``LVd'' above) explained below. Then pc prints the command number, a number uniquely identifying the command's position in the sequence of commands since the beginning of the user's session. Finally, the command itself is printed.

While pc always prints a space first, some history commands, for example :pcs and :pe, use the first column of output to delimit a region of commands or to point to a particular event within a command.

For example, :pcs 52 54 will print something like

/LVd     52 (DEFUN FOO (X) X)
 LV      53 (DEFUN BAR (X) (CONS X X))
\        54 (DEFTHM FOO-BAR (EQUAL (CAR (BAR X)) (FOO X)))
          : ...
        127 (DEFUN LATEST (X) X)

Here, the two slash characters in the first column are intended to suggest a bracket delimiting commands 52 through 54. The last command printed by pcs is always the most recent command, i.e., the command at :here, and is separated from the rest of the display by an elipsis if some commands are omitted.

Similarly, the :pe command will print a particular event within a command block and will indicate that event by printing a ``>'' in the first column. The symbol is intended to be an arrow pointing at the event in question.

For example, :pe true-listp-app might print:

         1 (INCLUDE-BOOK "list-book")
            \
>           (DEFTHM TRUE-LISTP-APP
                    (EQUAL (TRUE-LISTP (APP A B)) (TRUE-LISTP B)))

using the arrow to indicate the event itself. The slash printed to connect the command, include-book, with the event, defthm, is intended to suggest a tree branch indicating that the event is inferior to (and part of) the command.

The mysterious three characters sometimes preceding a command have the following interpretations. The first two have to do with the function symbols introduced by the command and are blank if no symbols were introduced.

At any time we can classify our function symbols into three disjoint sets, which we will here name with characters. The ``P'' functions are those in :program mode. The ``L'' functions are those in :logic mode whose guards have not been verified. The ``V'' functions are those in :logic mode whose guards have been verified. Note that verify-termination and verify-guards cause function symbols to be reclassified. If a command introduces function symbols then the first mysterious character indicates the class of the symbols at the time of introduction and the second character indicates the current class of the symbols (if the current class is different from the introductory class).

Thus, the display

 PLd     52 (DEFUN FOO (X) X)

tells us that command 52 introduced a :program function but that some command after 52 changed its mode to :logic and that the guards of foo have not been verified. That is, foo's termination has been verified even though it was not verified as part of the command that introduced foo. Had a subsequent command verified the guards of foo, the display would contain a V where the L is.

The display

 P d     52 (DEFUN FOO (X) X)

indicates that foo was introduced in :program mode and still is in that mode.

The third character indicates the enabled/disabled status of the runes introduced by the command. If the status character is blank then all the runes (if any) introduced are enabled. If the status character is ``D'' then some runes were introduced and they are all disabled. If the status character is ``d'' then at least one, but not all, of the runes introduced is disabled. Thus, in the display

 L d     52 (DEFUN FOO (X) X)

we see that some rune introduced by command 52 is disabled. As noted in the documentation for rune, a defun command introduces many runes, e.g., the axiomatic definition rule, (:definition fn), the executable counterpart rule, (:executable-counterpart fn), and type-prescriptions, (:type-prescription fn). The display above does not say which of the runes based on foo is disabled, but it does tell us one of them is.

PCB

print the command block described by a command descriptor


Parent topic:  HISTORY
Home

Examples:
:pcb :max ; print the most recent command block
:pcb :x   ; print the most recent command block
:pcb fn   ; print the command block that introduced fn
:pcb 5    ; print the fifth command block

See command-descriptor.

Pcb takes one argument, a command descriptor, and prints the command block of the command described. See command-descriptor for details of command descriptors. See pc for description of the format in which commands are displayed. The command block of a command consists of the command itself and all of the events it created. If the command created a single event and that event is in fact the command (i.e., if the command typed was just an event such as a defun or defthm rather than a macro that expanded to some event forms), then pcb just prints the command. Pcb sketches command and all of the events it created, rather than printing them fully. If you wish to see just the command, in its entirety, use pc. If you wish to see one of the events within the block, in its entirety, use pe. If you wish to see the command sketched and all of the events it created, in their entirety, use pcb!.

PCB!

print in full the command block described by a command descriptor


Parent topic:  HISTORY
Home

Examples:
:pcb! :max ; print the most recent command block
:pcb! :x   ; print the most recent command block
:pcb! fn   ; print the command block that introduced fn
:pcb! 5    ; print the fifth command block

See command-descriptor.

Pcb! takes one argument, a command descriptor, and prints the command block of the command described. Unlike pcb, pcb! prints the event forms in full; see pcb for details.

PCS

print the sequence of commands between two command descriptors


Parent topic:  HISTORY
Home

Examples:
:pcs 1 5              ; print commands 1 through 5
:pcs 5 1              ; same as above
:pcs :x (:x -3)       ; print the 3 most recently executed commands
:pcs fn assoc-of-fn   ; print the commands between the one that introduced
                      ; fn and the one that introduced assoc-of-fn

Pcs takes two arguments, both of which are command descriptors, and prints the commands between them with pc. The order of the two descriptors is irrelevant. See command-descriptor for a description of command descriptors. See pc for a description of the format in which commands are displayed.

PE

print the event named by a logical name


Parent topic:  HISTORY
Home

Example:
:pe fn   ; sketches the command that introduced fn and
         ; prints in full the event within it that created fn.

See logical-name.

Pe takes one argument, a logical name, and prints in full the most recent event corresponding to the name. Pe also sketches the command responsible for that event if the command is different from the event itself. See pc for a description of the format used to display a command. To remind you that the event is inferior to the command, i.e., you can only undo the entire command, not just the event, the event is indented slightly from the command and a slash (meant to suggest a tree branch) connects them.

Use pe! if you want all events corresponding to a given name; see pe!.

PE!

print all the events named by a logical name


Parent topic:  HISTORY
Home

Examples:
:pe! name ; prints each event that corresponds to name.

Pe! takes one argument, a logical name other than :here, and prints in full all the events for that name. Pe! also sketches the command responsible for that event in each case that the command is different from the event itself. See pc for a description of the format used to display a command. To remind you that the event is inferior to the command, i.e., you can only undo the entire command, not just the event, the event is indented slightly from the command and a slash (meant to suggest a tree branch) connects them.

Use pe if you want only the latest event corresponding to a given name, or if you want to use the logical name :here; see pe.

PF

print the formula corresponding to the given name


Parent topic:  HISTORY
Home

Examples:
:pf (:definition fn) ; prints the definition of fn as an equality
:pf fn               ; same as above

:pf (:rewrite foo)   ; prints the statement of the rewrite rule foo
:pf foo              ; same as above

pf takes one argument, an event name or a rune, and prints the formula associated with name.

PL

print the rules whose top function symbol is the given name


Parent topic:  HISTORY
Home

Examples:
:pl foo ; prints the rewrite rules that rewrite some call of foo

Pl takes one argument, a function symbol, and displays the lemmas that rewrite some term whose top function symbol is the given one. Note that names of macros are not relevant here; for example, for the rules about + you should give the command :pl binary-+.

In fact the kinds of rules printed by :pl are rewrite rules, definition rules, and meta rules.

PR

print the rules stored by the event with the given name


Parent topic:  HISTORY
Home

Examples:

:pr fn ; prints the rules from the definition of fn (including any
       ; :type-prescription rule and :definition rule)


:pr assoc-append ; if assoc-append is a rewrite rule, prints that rule

Also see pr!, which is similar but works at the command level instead of at the event level.

Pr takes one argument, a logical name, and prints the rules associated with it. In each case it prints the rune, the current enabled/disabled status, and other appropriate fields from the rule. It may be helpful to read the documentation for various kinds of rules in order to understand the information printed by this command. For example, the information printed for a linear rule might be:

  Rune:     (:LINEAR ABC)
  Status:   Enabled
  Hyps:     ((CONSP X))
  Concl:    (< (ACL2-COUNT (CAR X)) (ACL2-COUNT X))
  Max-term: (ACL2-COUNT (CAR X))
  Fixer:    NIL

The hyps and concl fields for this rule are fairly self-explanatory, but it is useful to see linear to learn about maximal terms (which, as one might guess, are stored under ``Max-term''). In order to learn about the ``Fixer'' one has to know to see linear-alias, which is quite unreasonable. The state of this documentation will surely improve.

Currently, this function does not print congruence rules or equivalence rules.

The expert user might also wish to use find-rules-of-rune. See find-rules-of-rune.

PR!

print rules stored by the command with a given command descriptor


Parent topic:  HISTORY
Home

Examples:

:pr! fn ; prints the rules from the definition of fn (including any
        ; :type-prescription rule and :definition rule), as well as all other
        ; rules created by the command that created by fn (which could be
        ; many rules if, for example, fn was defined by an include-book
        ; command).


:pr! :max ; prints all the rules stored by the most recent command

Also see pr, which is similar but works at the event level instead of at the command level.

Pr takes one argument, a command descriptor, and prints the rules created by the corresponding event. In each case it prints the rune, the current enabled/disabled status, and other appropriate fields from the rule. See pr for further details.

PUFF

replace a compound command by its immediate subevents


Parent topic:  HISTORY
Home

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.

A command is ``puffable'' if it is an encapsulate command, an include-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 several defun events is puffable. The only primitive event commands that are puffable are encapsulate and include-book commands. 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 innards of the book as though they had all be 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.

Finally, it is impossible to puff in the presence of include-book commands involving certified files that have been altered since they were included. 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 check sum 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 check sum of 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.

PUFF*

replace a compound command by its subevents


Parent topic:  HISTORY
Home

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

U

undo last command, without a query


Parent topic:  HISTORY
Home

Example:
:u

The keyword command :u is the same as :ubt :max, but with related queries suppressed appropriately. :Oops will undo the last :u. See ubt and see ubt!.

UBT

undo the commands back through a command descriptor


Parent topic:  HISTORY
Home

Examples:
:ubt :max      ; undo back through the most recent command
               ; (which just means undo the most recent command)
:ubt :x        ; same as :ubt :max
:u             ; same as :ubt :max with no questions asked
:ubt fn        ; undo back through the introduction of fn
               ; (including all the other events in fn's block)
:ubt 5         ; undo back through the fifth command executed
:ubt (:max -4) ; undo back through the most recent five commands
:ubt (:x -4)   ; undo back through the most recent five commands

See command-descriptor.

ubt takes one argument, a command descriptor, and undoes the commands from :max (aka :x) through the one described. See command-descriptor. Pbt will print the commands that ubt will undo. :Oops will undo the undo. See oops.

It is important to remember that a command may create several events. That is, the command that introduces fn1 may also introduce fn2. Undoing the command that created either of these will undo them both. The events created by a command constitute the command's ``block'' and we can only undo entire blocks. Use pcb to print the command block of a command if you wish to see what will be lost by undoing the command.

Ubt will not undo into ``prehistory''. :Ubt 1 will undo all of your commands. But :ubt -5 will cause an error, warning you that :ubt cannot undo system initialization.

UBT!

undo commands, without a query or an error


Parent topic:  HISTORY
Home

Example:
:ubt! :x-4

The keyword command :ubt! is the same as :ubt, but with related queries suppressed appropriately, and with a guarantee that it is ``error-free.'' More precisely, the error triple returned by :ubt! will always have a first component of nil. :Oops will undo the last :ubt!. See ubt and see u.