defmac

(in-package "ACL2")

(defxdoc defmac
  :parents (defmacro)
  :short "Define a macro that expands efficiently."
  :long "<p>Example forms</p>

@({
  (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))))))~/
})

<p>General Form:</p>

@({
  (defmac name macro-args
          :macro-fn name-macro-fn ; optional
          doc-string              ; optional
          dcl ... dcl             ; optional
          body)
})

<p>where @('name') is a new symbolic name (see @(see name)), @(see macro-args)
specifies the formals of the macro (see @(see macro-args) for a description),
and @('body') is a term.  @('Doc-string') is an optional @(see documentation)
string, which (as for @(tsee defmacro)) is essentially ignored by ACL2.  Each
@('dcl') is an optional declaration as for @(see defun) (see @(see
declare)).</p>

<p>See @(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 @(':')@(see program) mode functions in its body.</p>

<p>A @('defmac') form generates the following form, which introduces a @(see
defun) and a @(see 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 @(see defmacro), and each @('dcl') is as
specified for @(see 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
@(see 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').</p>

@({
  (progn
    (defun name-macro-fn (v1 ... vk)
      dcl ... dcl
      body)
    (defmacro name macro-args
      doc-string
      (name-macro-fn v1 ... vk))
    )
})

<p>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.</p>")