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 with argument list (ctx body state) that returns one value, namely state. We describe ctx and body at the end below, but you may simply prefer to ignore these arguments.) 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 (ctx body state)
  (declare (xargs :stobjs state)
           (ignore ctx body))
  (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)
           (ignore ctx body))
  (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.

Finally, as promised above, we briefly describe the arguments ctx and body. These are the arguments passed to the call of macro with-ctx-summarized under which finalize-event-user (or initialize-event-user) was called. Thus, they are unevaluated expressions. For example, system function defthm-fn1 has a body of the following form.

(with-ctx-summarized
 (if (output-in-infixp state) event-form (cons 'defthm name))
 (let ((wrld (w state))
       (ens (ens state))
       .....

(if (output-in-infixp state) event-form (cons 'defthm name))

 (let ((wrld (w state))
       (ens (ens state))
       .....

You might find it helpful to use trace$ to get a sense of ctx and body, for example, (trace$ finalize-event-user).