FINALIZE-EVENT-USER

user-supplied code to complete events, e.g., with extra summary output

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)

So for example:

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.