Macrolet
Local binding of macro symbols
See flet for an analogous utility for defining functions
locally.
Example Form:
(defun f1 (x)
(macrolet ((mac (a) (list 'quote a)))
(cons x (mac x))))
The Example Form above is equivalent to the following, in which the call of
local macro mac has been expanded.
(defun f1-alt (x)
(cons x (quote x)))
The General Forms are similar to those of flet.
General Forms:
(macrolet (def1 ... defk) body)
(macrolet (def1 ... defk) declare-form1 .. declare-formk body)
where body is a term, and each defi is a definition as in defmacro but with the leading defmacro symbol omitted. See defmacro, but see declare for the declarations permitted directly
under the defi. On the other hand, regarding the declare-formi (if
any are supplied): each must be of the form (declare decl1 ... decln),
where each decli is of the form (inline g1 ... gm) or (notinline
g1 ... gm), and each gi is defined by some defi. Unlike the
related utility flet, those inline and notinline
declarations are unlikely to have any effect.
The innermost flet or macrolet binding of a symbol, f,
above a call of f, is the one that provides the definition of f for
that call. Note that neither flet nor macrolet provide recursion:
that is, the definition of f in an flet or macrolet binding of
f is ignored in the body of that binding.
The following requirements are imposed by Common Lisp and enforced by
ACL2.
- Every variable occurring in the body of a defi must be a formal
parameter name of that defi.
- No function or macro symbol called in the body of a defi may be
defined by a superior flet or macrolet binding. (Not every Common
Lisp implementation includes this restriction for superior macrolet
bindings, but at least one (GCL) does so we include it in ACL2.)
Although macrolet behaves in ACL2 essentially as it does in Common
Lisp, ACL2 imposes the following restrictions and qualifications.
- Every declare form for a local definition (def1
through defk, above) must be an ignore, ignorable, or type
expression.
- Each defi must bind a different symbol.
- Each defi must bind a symbol that is a legal name for an ACL2 macro.
In particular, the symbol may not be in the keyword package or the main Lisp
package. Moreover, the symbol may not be a built-in ACL2 function or
macro.
- When an expression (macrolet (... defi ...) ...) occurs in the body
of a DO loop$ expression, nevertheless constructs such as
PROGN and SETQ that ACL2 permits in DO loop$ bodies are
not permitted in defi (unless they occur within the scope of a DO
loop$ expression in that body).
Macrolet bindings are evaluated in parallel. Consider the following
example.
(defun f1 (x) (cons x 'x))
(macrolet ((f1 (x) x)
(f2 () (list 'quote
; The following reference is to the global f1,
; not to the identity macro just above.
(f1 3))))
(f2))
The macrolet form above evaluates to (3 . x), not to 3, as
explained in the comment above. Here is a somewhat analogous form that one
might expect to evaluate to 3, but that is not the case; see below.
(macrolet ((f1 (x) x))
(macrolet ((f2 () (list 'quote (f1 3))))
(f2)))
The body of f2 calls a symbol, f1, that is bound by a superior
macrolet binding. As noted above, this is illegal (also for superior
flet bindings).
Under the hood, ACL2 expands away macrolet bindings. The following
example illustrates this point.
ACL2 !>:trans (macrolet ((mac (a) (list 'cons a a)))
(car (mac b)))
(CAR (CONS B B))
=> *
ACL2 !>
Macrolet is part of Common Lisp. See any Common Lisp documentation
for more information. We conclude by pointing out an important aspect of
macrolet shared by ACL2 and Common Lisp: The binding is lexical, not
dynamic. That is, the macrolet binding of a symbol only applies to calls
of that symbol in the body of the macrolet, not other calls made in the
course of evaluation. See flet for discussion of this point.
