Replace events displayed by history commands

Example Form: (extend-pe-table all-natp (all-p natp)) General Form: (extend-pe-table event-name form)

where

We motivate and illustrate this utility with the following example. Suppose you develop a macro to define the notion that each element of a list satisfies a given predicate, as follows.

(defmacro all-p (pred) (declare (xargs :guard (symbolp pred))) (let ((name (intern$ (concatenate 'string "ALL-" (symbol-name pred)) (symbol-package-name pred)))) `(defun ,name (lst) (if (atom lst) t (and (,pred lst) (,name (cdr lst)))))))

So for example, after evaluating

ACL2 !>:pe all-natp L 2:x(ALL-P NATP) >L (DEFUN ALL-NATP (LST) (IF (ATOM LST) T (AND (NATP LST) (ALL-NATP (CDR LST))))) ACL2 !>

So far so good. But suppose that instead, you introduce this event within
a call of `progn`, as follows.

(progn (defun f1 (x) x) (defun f2 (x) x) (all-p natp))

Then when we ask to see the event introducing

ACL2 !>:pe all-natp 2:x(PROGN (DEFUN F1 # ...) (DEFUN F2 # ...) ...) >L (DEFUN ALL-NATP (LST) (IF (ATOM LST) T (AND (NATP LST) (ALL-NATP (CDR LST))))) ACL2 !>

Perhaps we therefore prefer that history commands display the event
for `defun` event. Of course, in this simple example that might not be important;
but it is easy to imagine examples where a small macro invocation generates a
large, ugly primitive event that is best not viewed by any user!

A solution is to associate the name

(extend-pe-table all-natp (all-p natp))

After evaluating this form, we see the desired call of `pe` and other history commands consider the
defining event for

ACL2 !>:pe all-natp 2 (PROGN (DEFUN F1 # ...) (DEFUN F2 # ...) ...) >L (ALL-P NATP) ACL2 !>

As mentioned above, other history commands are sensitive to the
result of evaluating a call of

ACL2 !>:pcb all-natp 2 (PROGN (DEFUN F1 # ...) (DEFUN F2 # ...) ...) L (DEFUN F1 (X) ...) L (DEFUN F2 (X) ...) L (ALL-P NATP) ACL2 !>

Note that

ACL2 !>(encapsulate () (program) (all-p alistp)) [[.. elided ..]] T ACL2 !>:pe all-alistp 4:x(ENCAPSULATE NIL ...) >P (DEFUN ALL-ALISTP (LST) (IF (ATOM LST) T (AND (ALISTP LST) (ALL-ALISTP (CDR LST))))) ACL2 !>(extend-pe-table all-alistp (all-p alistp)) Summary Form: ( TABLE PE-TABLE ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) PE-TABLE ACL2 !>:pe all-alistp 4 (ENCAPSULATE NIL ...) >P (ALL-P ALISTP) ACL2 !>(verify-termination all-alistp) [[.. elided ..]] ALL-ALISTP ACL2 !>:pe all-alistp L 6:x(VERIFY-TERMINATION ALL-ALISTP) >L (DEFUN ALL-ALISTP (LST) (IF (ATOM LST) T (AND (ALISTP LST) (ALL-ALISTP (CDR LST))))) Additional events for the logical name ALL-ALISTP: 4 (ENCAPSULATE NIL ...) >PL (ALL-P ALISTP) ACL2 !>(extend-pe-table all-alistp (:termination-verified (all-p alistp))) Summary Form: ( TABLE PE-TABLE ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) PE-TABLE ACL2 !>:pe all-alistp L 6 (VERIFY-TERMINATION ALL-ALISTP) >L (:TERMINATION-VERIFIED (ALL-P ALISTP)) Additional events for the logical name ALL-ALISTP: 4 (ENCAPSULATE NIL ...) >PL (ALL-P ALISTP) ACL2 !>

Note that by using `pe!`, in place of `pe`, you can
avoid using the information that was provided by

ACL2 !>:pe! all-alistp L 6 (VERIFY-TERMINATION ALL-ALISTP) >L (DEFUN ALL-ALISTP (LST) (IF (ATOM LST) T (AND (ALISTP LST) (ALL-ALISTP (CDR LST))))) Additional events for the logical name ALL-ALISTP: 4 (ENCAPSULATE NIL ...) >PL (DEFUN ALL-ALISTP (LST) (IF (ATOM LST) T (AND (ALISTP LST) (ALL-ALISTP (CDR LST))))) ACL2 !>

In the examples above we invoked

(defmacro all-p (&whole form pred) (declare (xargs :guard (symbolp pred))) (let ((name (intern$ (concatenate 'string "ALL-" (symbol-name pred)) (symbol-package-name pred)))) `(progn (defun ,name (lst) (if (atom lst) t (and (,pred lst) (,name (cdr lst))))) (extend-pe-table ,name ,form))))

Then in a fresh session, after defining

ACL2 !>(all-p natp) [[.. elided ..]] ACL2 !>:pe all-natp 2:x(ALL-P NATP) ACL2 !>

We close with two remarks. First, note that the indicated event must have
already been defined at the time

(table pe-table 'all-natp nil)