FINALIZE-EVENT-USER

Major Section:  SWITCHES-PARAMETERS-AND-MODES

This utility is intended for system hackers, not standard ACL2 users.

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 processing to take place just after the summary, by defining a function of state that returns one value, namely state. Your function should normally be a guard-verified :logic mode function with no guard other than that provided by the input requirement on state, that is, (state-p state); but later below we discuss how to avoid this requirement. You then attach (see defattach) your function to the function finalize-event-user. The following example illustrates how this all works.

(defun finalize-event-user-test (state)
  (declare (xargs :stobjs state))
  (cond ((and (boundp-global 'abbrev-evisc-tuple state)
              (open-output-channel-p *standard-co*
                                     :character
                                     state))
         (pprogn
          (if (eq (f-get-global 'abbrev-evisc-tuple state) :DEFAULT)
              (princ$ "Abbrev-evisc-tuple has its default value.~%"
                      *standard-co*
                      state)
            (princ$ "Abbrev-evisc-tuple has been modified.~%"
                    *standard-co*
                    state))))
        (t state)))

(defattach finalize-event-user finalize-event-user-test)

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

Note: Abbrev-evisc-tuple has its default value.

If the attachment function (above, finalize-event-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 finalize-event-user-test2 (state)
  (declare (xargs :stobjs state
                  :mode :program))
  (observation
   'my-test
   "~|Value of term-evisc-tuple: ~x0~|"
   (f-get-global 'term-evisc-tuple state)))

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

(defattach (finalize-event-user finalize-event-user-test2)
           :skip-checks t)

ACL2 !>(set-term-evisc-tuple (evisc-tuple 2 7 nil nil) state)
 (:TERM)
ACL2 !>(defconst *foo6* '(a b c))

Summary
Form:  ( DEFCONST *FOO6* ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

ACL2 Observation in MY-TEST:  
Value of term-evisc-tuple: (NIL 2 7 NIL)
 *FOO6*
ACL2 !>

Note that (as of this writing) the macro observation expands to a call of a :program-mode function. Thus, the trick shown above involving :skip-checks allows the use of :program-mode functions; for example, you can print with fmt.

See community book books/misc/defattach-bang.lisp for a variant of defattach that uses ec-call to avoid issues of guard verification.

Also see initialize-event-user, which discusses the handling of state globals by that utility as well as by finalize-event-user.