Major Section: EVENTS
We assume familiarity with guard verification; see verify-guards.
Unlike verify-guards, the macro call (verify-guards+ mac ...) will
verify guards for a function, fn, such that the macro mac is
associated with the function symbol fn in macro-aliases-table
(also see add-macro-alias). For example, if you define a macro app and
list append function binary-app, and you associate macro app with
function symbol binary-app in macro-aliases-table, then evaluation
of the form (verify-guard+ app) will have the effect of evaluating
(verify-guards fn). Note that in this setting, evaluation of
(verify-guard app) would cause an error, because app is a macro and
verify-guards, unlike verify-guards+, cannot handle macros.
The rest of this documentation topic discusses why we do not simply
arrange that verify-guards be permitted to take a macro alias. The
following example shows a soundness issue in doing so.
(encapsulate
()
(defun f1 (x)
(declare (xargs :guard (consp x)
:verify-guards nil))
(car x))
(defun f2 (x)
(declare (xargs :guard t
:verify-guards nil))
(cdr x))
(defmacro mac (x)
x)
(add-macro-alias mac f2) ; silly macro alias ;
(local (add-macro-alias mac f1)) ; alternate silly macro alias ;
(verify-guards mac))
If we were to allow macro aliases in verify-guards, this event would be
admitted, because on the first pass we are verifying guards of f1. But
after the encapsulate form completes evaluation, it would appear that
f2 is guard-verified. That could of course cause a raw Lisp error.
The enhanced functionality provided by verify-guards+ does not have the
above problem, because it takes advantage of make-event to avoid taking
advantage of the contradictory results produced by the two calls of
add-macro-alias. See make-event. If the specific example above is
modified by replacing verify-guards with verify-guards+, then the
first pass through the encapsulate form will expand the form
(verify-guards+ mac) to (verify-guards f1). That same expansion will
be used for the verify-guards+ call during the second pass through the
encapsulate form, which is evaluated successfully and leaves us in a
world where f1 is guard-verified and f2 is not.
