Defmacro
Define a macro
Example Defmacros:
(defmacro xor (x y)
(list 'if x (list 'not y) y))
(defmacro git (sym key)
(list 'getprop sym key nil
'(quote current-acl2-world)
'(w state)))
(defmacro one-of (x &rest rst)
(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))))))
Example Expansions:
term macroexpansion
(xor a b) (if a (not b) b)
(xor a (foo b)) (if a (not (foo b)) (foo b))
(git 'car 'lemmas) (getprop 'car 'lemmas nil
'current-acl2-world
(w state))
(one-of x a b c) (or (eq x 'a)
(or (eq x 'b)
(or (eq x 'c) nil)))
(one-of x 1 2 3) ill-formed (guard violation)
General Form:
(defmacro name macro-args doc-string dcl ... dcl body)
where name is a new symbolic name (see name), macro-args
specifies the formal parameters of the macro, and body is a term whose
only free variables are the macro-args. The formal parameters can be
specified in a much more general way than is allowed by ACL2 defun
events; see macro-args for a description of keyword (&key)
and optional (&optional) parameters as well as other so-called
``lambda-list keywords'', &rest and &whole. Doc-string, if
non-nil, is an optional string that can provide documentation but is
essentially ignored by ACL2. Each dcl is an optional declaration (see
declare) except that the only xargs keyword permitted by
defmacro is :guard.
There are two restrictions on body aside from it simply being a term
in macro-args. Both restrictions relate to ancestral uses of apply$ in body, i.e., uses of apply$ by body or any function
that might be called during the evaluation of body. First, only badged
primitive functions may be applied. See badge for a way to obtain the
complete list of badged primitives. Second, loop$ and lambda$ may
not be used anywhere in the ancestry of body. See
ignored-attachment and prohibition-of-loop$-and-lambda$ for more
discussion. Note: It is permitted for the value of body to mention
apply$, loop$, and lambda$.
For compute-intensive applications, see defmac, which can speed up
macroexpansion by introducing an auxiliary defun. For a variant of
defmacro that automatically quotes arguments by default, but provides a
way for calls to evaluate specified arguments, see defmacroq.
Macroexpansion occurs when a form is read in, i.e., before the evaluation
or proof of that form is undertaken. To experiment with macroexpansion, see
trans. When a form whose car is name arises as the form
is read in, the arguments are bound as described in CLTL pp. 60 and 145, the
guard is checked, and then the body is evaluated. The result is
used in place of the original form.
In ACL2, macros do not have access to the ACL2 state, state. (If
state or any user-defined stobj (see stobj) is a macro
argument, it is treated as an ordinary variable, bound at macro-expansion time
to a piece of syntax.) This is in part a reflection of CLTL, p. 143, ``More
generally, an implementation of Common Lisp has great latitude in deciding
exactly when to expand macro calls with a program. ... Macros should be
written in such a way as to depend as little as possible on the execution
environment to produce a correct expansion.'' In ACL2, the product of
macroexpansion is independent of the current environment and is determined
entirely by the macro body and the functions and constants it references. It
is possible, however, to define macros that produce expansions that refer to
state or other single-threaded objects (see stobj) or variables
not among the macro's arguments. See the git example above. For a
related utility that does have access to the ACL2 state, see make-event.
Subtopics
- Prohibition-of-loop$-and-lambda$
- Certain events do not allow loop$s or lambda$s
- Ignored-attachment
- Why attachments are sometimes not used
- Defmac
- Define a macro that expands efficiently.
- Defmacro-untouchable
- Define an ``untouchable'' macro
- Defmacro+
- An enhancement of defmacro
with XDOC integration.
- Defmacroq
- Define a macro that quotes arguments not wrapped in :eval
