Assert!-stobj
Variant of assert! and assert-event allowing stobjs
The assert!-stobj macro is a variant of assert! that
expects its first argument to evaluate to multiple values, specifically, two
values where the first is not a stobj and the second is a specified
stobj. Assert!-stobj is an event macro: its calls may appear as
top-level events in books as well as encapsulate and
progn forms. As with assert!, calls of assert!-stobj
directly abbreviate corresponding calls of the built-in event macro,
assert-event. You may find it more convenient to use assert-event, which has more options. In particular, with assert-event
the assertion may evaluate to a single value or to any number of multiple
values, with no limit on the number of stobjs retured, and a keyword option
:STOBJS-OUT :auto that makes it unnessary to to specify the shape of the
return.
See assert$ and assert* for assertion-checking utilities to
use in programs.
Example Forms:
(assert!-stobj (mv-let (erp val state)
(set-inhibit-output-lst nil)
(declare (ignore val))
(mv (null erp) state))
state)
(defstobj st fld)
(assert!-stobj (let ((st (update-fld 3 st)))
(mv (eql (fld st) 3)
st))
st)
General Forms:
(assert!-stobj assertion st)
(assert!-stobj assertion st event)
where: assertion evaluates to multiple values (mv val st), where
val is an ordinary value and st — which is the second argument
above — is a stobj (either user-defined or state); and
event, if supplied and non-nil, is an event to be evaluated
if the first return value is not nil. It is an error if the first return
value is nil. As noted above, a call of assert!-stobj is an event: it can go into a book or an encapsulate or progn
event.
Calls of assert!-stobj skip evaluation of the given assertion when
proofs are being skipped: during include-book, during the second pass
of an encapsulate event, and after evaluating (set-ld-skip-proofsp
t state).
The two General Forms above may be expressed, respectively, in terms of the
more flexible built-in event macro, assert-event, as follows.
See assert-event for more detailed documentation.
(assert-event assertion
:stobjs-out '(nil st)
:ctx ''assert!-stobj)
(assert-event assertion
:stobjs-out '(nil st)
:event event
:ctx ''assert!-stobj)
