On-failure
Run an event, printing a custom error message if it fails.
General Form:
(on-failure event
:ctx ctx ; default "event processing"
:erp erp ; default t
:val val ; default nil
:msg msg ; default nil
)
where event is an embedded-event-form, and the other arguments
are passed to fail-event as explained below. Thus, none of the
arguments is evaluated. The General Form above expands to the following.
(ORELSE EVENT
(FAIL-EVENT CTX ERP VAL MSG))
Thus, first event is evaluated — see orelse — and
either it succeeds or else the indicated error occurs — see fail-event.
Consider the following example.
(on-failure (defund f (x) x)
:ctx (defund . f) ; see :doc ctx
:erp t ; see :doc er-soft+
:val nil ; see :doc er-soft+
:msg ("Failed:~|~%~x0" (#\0 . (defun f (x) x))))
If f is not already defined, then this is essentially equivalent to
(defund f (x) x). But if f currently has a conflicting definition,
then the event will fail and the final error message, unless error output is
inhibited (see set-inhibit-output-lst), will be the following.
ACL2 Error in (DEFUND F ...): Failed:
(DEFUN F (X) X)
For another example of the use of on-failure, which uses the macro
msg to construct a msgp, see the definition of function
report-event-when-error-fn in community-book
books/kestrel/utilities/orelse.lisp.
