• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
      • Pl
      • Command
      • Puff
      • Pc
      • Ld-history
      • Oops
      • Extend-pe-table
      • Ubt
      • Puff*
      • Ubi
      • Undo
      • Pe
      • Make-termination-theorem
      • Command-descriptor
      • Reset-prehistory
      • Gthm
      • Formula
      • Pr
      • Pcb
      • Ubu
      • Disable-ubt
      • Pl2
      • Pbt
      • Enter-boot-strap-mode
      • Reset-kill-ring
      • Ubt!
      • U
      • Tthm
      • Pf
      • Ubu!
      • Pr!
      • Pcs
      • Pcb!
      • Get-command-sequence
      • Exit-boot-strap-mode
      • Ubu?
      • Ubt?
      • Ep-
      • Ubt-prehistory
      • Tau-database
      • Ep
      • Pe!
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• History

Extend-pe-table

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 event-name is the name of an existing event and form is to be displayed by history commands in place of the actual event that introduced event-name.

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 (all-p natp), you see the following.

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 all-natp, we will not see any use of the macro all-p.

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 all-natp as (all-p natp), rather than as the generated 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 all-natp with the form that introduced this name, as follows.

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

After evaluating this form, we see the desired call of all-natp. In essence, :pe and other history commands consider the defining event for all-natp to be (all-p natp) rather than the actual defun form that introduced all-natp.

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 extend-pe-table. For example:

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 extend-pe-table actually associates the indicated form with the most recent event introducing the given event name. Consider the following example (output elided as shown).

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 extend-pe-table.

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 extend-pe-table explicitly. It might have been better, however, to ``bake in'' such calls by way of the macro itself, as follows.

(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 all-p as shown immediately above, we can obtain the following (edited) log.

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 extend-pe-table is invoked. Second — in case an advanced user wishes to extend directly the underlying table, pe-table — we mention that this table associates each key, an event name, with an association list that maps so-called absolute event numbers with events to display. So for example, we can remove all custom printing of events for the name all-natp as follows.

(table pe-table 'all-natp nil)