		Search-engine friendly clone of the ACL2 documentation.

Macros

Macro-args

The formals list of a macro definition

Examples:
(x y z)
(x y z &optional max (base '10 basep))
(x y &rest rst)
(x y &key max base)
(&whole sexpr x y)

The ``lambda-list'' of a macro definition may include simple formal parameter names as well as appropriate uses of the following lambda-list keywords from Common Lisp, respecting the order shown:

&whole x
X does not represent an actual parameter; rather, it is bound to the entire macro call.
&optional x1 x2 ...
The actual for any xi may be omitted, in which case the actual for every xj with j > i must also be omitted.
&rest x
X does not represent an actual parameter; rather, it is bound to the list of all actuals provided from that position onward.
&body x
This is identical to &rest x.
&key x
The call may have a keyword argument for x by including :x val after all required actual parameters, in which case the formal x is bound to the actual val.
&allow-other-keys
Keyword arguments not specified by &key are allowed but ignored.

ACL2 does not support the Common Lisp lambda-list keywords &aux and &environment. In addition, there are the following restrictions:

(1) initialization forms in &optional and &key specifiers must be quoted values;

(2) &allow-other-keys may only be used once, as the last specifier; and

(3) destructuring is not allowed.

The use of default values is allowed, so that an optional or keyword argument may be given in any of the following forms.

arg or, equivalently, (arg)
(arg 'init)
(arg 'init supplied-p)

For the second and third forms above, init is the value when the argument is not supplied; for the first form, that default value is nil. Note that it must be quoted. The supplied-p argument is nil when the argument is not supplied, else is t, as illustrated by the demo below.

You are encouraged to experiment with the macro facility. One way to do so is to define a macro that does nothing but return the quotation of its arguments, e.g.,

(defmacro demo (x y &optional (opt '5) &key (key1 '6 key1p) key2)
  (list 'quote (list x y opt key1 key1p key2)))

You may then execute the macro on some sample forms, e.g.,

  term                         value
(demo 1 2)                (1 2 5 6 NIL NIL)
(demo 1 2 3)              (1 2 3 6 NIL NIL)
(demo 1 2 3 :key1 6)      (1 2 3 6 T NIL)
(demo 1 2 3 :key1 7)      (1 2 3 7 T NIL)
(demo 1 2 3 :key2 8)      (1 2 3 6 NIL 8)
(demo 1 2 :key1 3)        error:  non-even key/value arglist
                          (because :key1 is used as opt)

In particular, Common Lisp specifies (hence so does ACL2) that if you use both &rest and &key, then both will be bound using the same list of arguments. The following example should serve to illustrate how this works.

ACL2 !>(defmacro foo (&rest args &key k1 k2 k3)
         (list 'quote (list args k1 k2 k3)))

Summary
Form:  ( DEFMACRO FOO ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FOO
ACL2 !>(foo :k1 3 :k2 4 :k3 5)
((:K1 3 :K2 4 :K3 5) 3 4 5)
ACL2 !>(foo :k1 3 :k2 4)
((:K1 3 :K2 4) 3 4 NIL)
ACL2 !>(foo :k1 3 :bad-key 7)

ACL2 Error in macro expansion:  Illegal key/value args (:BAD-KEY 7)
in macro expansion of (FOO :K1 3 :BAD-KEY 7).  The argument list for
FOO is
(&REST ARGS &KEY K1 K2 K3).

ACL2 !>

If we don't want to get the error above, we can use &allow-other-keys, as follows.

ACL2 !>(defmacro bar (&rest args &key k1 k2 k3
                            &allow-other-keys)
         (list 'quote (list args k1 k2 k3)))

Summary
Form:  ( DEFMACRO BAR ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 BAR
ACL2 !>(bar :k1 3 :bad-key 7)
((:K1 3 :BAD-KEY 7) 3 NIL NIL)
ACL2 !>

Also see trans.

Subtopics

Set-duplicate-keys-action: Control action for macro calls with duplicate keyword arguments