Pc
Print the command described by a command descriptor
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, doing so in full unless the
ld-evisc-tuple is non-nil, in which case it abbreviates using that
evisc-tuple; see evisc-tuple. See command-descriptor. For
example:
ACL2 !>:pc foo
LVd 52 (DEFUN FOO (X) X)
Pc always prints a space first, followed by four (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 (perhaps as modified using extend-pe-table) 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 ellipsis if some commands are omitted.
Similarly, the :pe command will print a particular
event (perhaps as modified using extend-pe-table) 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 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 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. You may also see the use of (lower-case) ``v'' to
indicate functions introduced by encapsulate. 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; see disabledp for how to obtain the disabled runes for a given
function symbol.
Remark for users of the break-rewrite utility. Inside the
:brr loop, the status character shows whether rules are disabled
at the current point of the proof that is currently underway, rather than
whether rules are disabled globally. For example, if you break while the
prover is working on Subgoal 3, and the hints supplied for the proof
specify ("Subgoal 3" :in-theory (disable foo)), then regardless of
whether or not rules associated with foo are enabled globally, the status
character indicates whether they are enabled while processing Subgoal 3.
Finally, a fourth character is printed, indicating whether functions are
memoized. A symbol may be memoized if it is a function symbol that is
not constrained (i.e., introduced by defchoose or in the signature of an encapsulate event). If the command introduces no
symbol that may be memoized, then a space is printed. Otherwise, if every
memoizable symbol is memoized, an ``M'' is printed. Otherwise, an
``m'' is printed.
