PRINT-SUMMARY-USER

Major Section:  SWITCHES-PARAMETERS-AND-MODES

ACL2 prints summaries at the conclusions of processing events (unless summaries are inhibited; see set-inhibit-output-lst and also see set-inhibited-summary-types). You may arrange for information to be printed at the end of the summary, by defining a function of state that returns an ordinary value (typically nil, but the value is irrelevant). This function should normally be a guard-verified :logic mode function with no explicit guard (hence, its guard is actually (state-p state)), but later below we discuss how to avoid this requirement. It is then attached (see defattach) to the function print-summary-user. The following example illustrates how this all works.

(defun print-summary-user-test (state)
  (declare (xargs :stobjs state))
  (and (f-boundp-global 'abbrev-evisc-tuple state)
       (observation-cw
        'my-test
        "~|Value of abbrev-evisc-tuple: ~x0~|"
        (f-get-global 'abbrev-evisc-tuple state))))

(defattach print-summary-user print-summary-user-test)

After admission of the two events above, every event summary will conclude with extra printout, for example:

ACL2 Observation in MY-TEST:  
Value of abbrev-evisc-tuple: :DEFAULT

If the attachment function (above, print-summary-user-test) does not meet all the requirements stated above, then you can use the :skip-checks argument of defattach to get around the requirement, as illustrated by the following example.

(defun print-summary-user-test2 (state)
  (declare (xargs :stobjs state
                  :mode :program))
  (observation-cw
   'my-test
   "~|Value of term-evisc-tuple: ~x0~|"
   (f-get-global 'term-evisc-tuple state)))

(defttag t) ; needed for :skip-checks t

(defattach (print-summary-user print-summary-user-test2)
           :skip-checks t)