Defmac
Define a macro that expands efficiently.
Example forms
(include-book "misc/defmac" :dir :system)
(defmac my-xor (x y)
(list 'if x (list 'not y) y))
(defmac my-mac (x &optional (y '3 y-p))
`(list ,x ,y ,y-p))
(defmac one-of (x &rest rst)
:macro-fn one-of-function
"stubbed-out :doc."
(declare (xargs :guard (symbol-listp rst)))
(cond ((null rst) nil)
(t (list 'or
(list 'eq x (list 'quote (car rst)))
(list* 'one-of x (cdr rst))))))~/
General Form:
(defmac name macro-args
:macro-fn name-macro-fn ; optional
doc-string ; optional
dcl ... dcl ; optional
body)
where name is a new symbolic name (see name), macro-args
specifies the formals of the macro (see macro-args for a description),
and body is a term. Doc-string is an optional documentation
string, which (as for defmacro) is essentially ignored by ACL2. Each
dcl is an optional declaration as for defun (see declare).
See defmacro for a discussion of defmacro, which is the
traditional way of introducing macros. Defmac is similar to defmacro
except that the resulting macro may execute significantly more efficiently, as
explained below. You can use defmac just as you would normally use
defmacro, though your defmac form should include the declaration
(declare (xargs :mode :program)) to be truly compatible with defmacro,
which allows calls of :program mode functions in its body.
A defmac form generates the following form, which introduces a defun and a defmacro. Here we refer to the ``General Form'' above;
hence the :macro-fn, doc-string, and each dcl are optional. The
doc-string is as specified for defmacro, and each dcl is as
specified for defun. :Macro-fn specifies name-macro-fn (used
below) as illustrated above, but if :macro-fn is not specified then
name-macro-fn is obtained by adding the suffix "-MACRO-FN" to the
symbol-name of name to get a symbol in the same package as
name. The list (v1 ... vk) enumerates all the names introduced in
macro-args.
(progn
(defun name-macro-fn (v1 ... vk)
dcl ... dcl
body)
(defmacro name macro-args
doc-string
(name-macro-fn v1 ... vk))
)
The reason for introducing a defun is efficiency. ACL2 expands a macro
call by running its own evaluator on the body of the macro, and this can be
relatively slow if that body is large. But with defmac, the evaluator
call reduces quickly to a single raw Lisp call of the (executable counterpart
of) the auxiliary function on the actuals of the macro.
