Assert-event
Assert that a given form returns a non-nil value
Assert-event provides a flexible way to check that evaluation
of an expression returns a non-nil value, causing an error otherwise.
Calls of assert-event are event forms; thus, they may occur in
books as well as encapsulate and progn events. See
also assert! and assert!-stobj for simple interfaces to
assert-event. See assert$ and assert* for
assertion-checking utilities to use in programs.
Basic calls of assert-event will take just one argument, called an
``assertion'', which is a form that evaluates to a single value that is not a
stobj. The following log shows a successful invocation — one
where the assertion evaluates to a non-nil value.
ACL2 !>(assert-event (equal (+ 3 4) 7))
:PASSED
ACL2 !>
Such a use of assert-event will probably suffice for most users, that
is, where the form evaluates to a single non-stobj value and there are no
keyword arguments. The keyword arguments, which are optional and discussed
below, extend that functionality, for example: multiple values are permitted
by keyword :stobjs-out, and keyword :on-skip-proofs can override the
default behavior of ignoring assertions when proofs are being skipped.
General Form:
(assert-event assertion
:event event ; default nil
;; evaluated keyword arguments:
:ctx ; default 'assert-event
:msg msg ; default t
:on-skip-proofs sp ; default nil
:safe-mode safe-mode ; default :same
:stobjs-out stobjs-out ; default nil
)
where assertion and event are not evaluated but all the other
arguments are evaluated, with the defaults shown above corresponding to values
after evaluation.
The following example illustrates all of the keyword arguments, which are
documented below.
(assert-event (mv (equal (+ 3 4) 7) state)
:event (defun f (x) (cons x x))
:ctx '(assert-event . <some-mv>)
:msg (msg "Oops, I forgot what ~x0+~x1 is!" 3 4)
:on-skip-proofs t
:safe-mode nil
:stobjs-out '(nil state))
Assert-event is a macro whose expansion directly produces a call of
the primitive event, value-triple, where: if a call of assert-event
speifies :msg msg, then the corresponding call of value-triple
specifies :check (or msg t). But unlike value-triple,
assert-event can specify an event to evaluate when the assertion has
non-nil value, using the :event keyword. (You can get a sense of
the value-triple call generated from an assert-event call by using
:trans1 on the assert-event form.) The remaining keyword
arguments of assert-event are also arguments of value-triple. Here
is a brief summary of the keyword arguments, but NOTE: see value-triple for more detailed explanations of keywords other than
:EVENT.
:EVENT event (default nil): When event is not nil, it
should be an event, that is, a form that may be in a book or a call of
encapsulate or progn. If the assertion evaluates to a
non-nil value (or to multiple values where the first value is not a stobj
and is non-nil; see :STOBJS-OUT below), then event is
evaluated; otherwise the evaluation results in an error.
:CTX ctx (default: 'assert-event): context for error messages.
:MSG msg (default: t): message to print when there is an
error (equivalent to keyword argument :CHECK of value-triple).
:ON-SKIP-PROOFS sp (default: nil): supply t to evaluate the
assertion even when skipping proofs (i.e., during include-book or the
second pass of an encapsulate event, or after invoking set-ld-skip-proofsp to skip proofs).
:SAFE-MODE safe-mode (default: :same): provides backward
compatibility, but is probably best ignored.
:STOBJS-OUT stobjs-out (default: nil): specify :auto to
allow any return, even with multiple values provided the first return value is
not a stobj; or specify a list starting with nil, corresponding to
the multiple values returned, with stobjs in stobj positions and nil
elsewhere. A stobjs-out of nil is treated as (nil). The first
return value is the one checked to be non-nil with one exception: when an
error-triple (mv erp val state) is returned, erp must be
nil and it is val that is checked to be non-nil.
Subtopics
- Assert!-stobj
- Variant of assert! and assert-event allowing stobjs
- Assert!
- Event variant of assert$ that abbreviates assert-event
