User-supplied code to complete events, e.g., with extra summary output
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
(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)) (newline *standard-co* state))) (t state))) (defattach-system 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,
(defun finalize-event-user-test2 (ctx body 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-system (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
See community book
Also see initialize-event-user, which discusses the handling of
state globals by that utility as well as by
Finally, as promised above, we briefly describe the arguments
(with-ctx-summarized (cons 'defthm name) (let ((wrld (w state)) (ens (ens state)) .....
(cons 'defthm name)
(let ((wrld (w state)) (ens (ens state)) .....
You might find it helpful to use trace$ to get a sense of