Defmacro-untouchable
Define an ``untouchable'' macro
Strictly speaking, macros cannot be untouchable the way functions
are untouchable; see push-untouchable. However, one can define a macro
that is, in effect, untouchable, by using defmacro-untouchable to
introduce a trivial untouchable function into the definition. Consider for
example the following definition.
(defmacro-untouchable mac (x)
(list 'consp x))
Let's look at the single-step macroexpansion of a call of the newly-defined
macro, mac.
ACL2 !>:trans1 (mac (f a))
(PROG2$ (UNTOUCHABLE-MARKER 'MAC)
(CONSP (F A)))
ACL2 !>
We see that this expansion is just as if we had used defmacro
instead of defmacro-untouchable, except that a prog2$ wrapper
lays down a call of untouchable-marker, which is a built-in untouchable
function. In effect, that call makes the macro, mac, untouchable.
Of course, you are welcome to write your own variant of
defmacro-untouchable, introducing your own untouchable function. The
result would presumably be roughly equivalent to using
defmacro-untouchable; but using defmacro-untouchable has two
advantages. One advantage is that calls of a macro introduced with
defmacro-untouchable should have no Lisp execution overhead caused by the
use of prog2$ or untouchable-marker, because of special handling
provided by ACL2 for such calls of prog2$ as well as inlining of
untouchable-marker. The other advantage is that an attempt to use the
resulting macro without an active trust tag will generally give a more helpful
error message, mentioning the prior use of defmacro-untouchable as the
source of the error.
