		Search-engine friendly clone of the ACL2 documentation.

Macros

Macro-aliases-table

A table used to associate function names with macro names

Example:
(table macro-aliases-table 'append 'binary-append)

This example associates the function symbol binary-append with the macro name append. As a result, the name append may be used as a runic designator (see theories) by the various theory functions. Thus, for example, it will be legal to write

(in-theory (disable append))

as an abbreviation for

(in-theory (disable binary-append))

which in turn really abbreviates

(in-theory (set-difference-theories (current-theory :here)
                                    '(binary-append)))

General Form:

(table macro-aliases-table 'macro-name 'function-name)

or very generally

(table macro-aliases-table macro-name-form function-name-form)

where macro-name-form and function-name-form evaluate, respectively, to a macro name and a symbol in the current ACL2 world. See table for a general discussion of tables and the table event used to manipulate tables.

Note that function-name-form (above) does not need to evaluate to a function symbol, but only to a symbol. As a result, one can introduce the alias before defining a recursive function, as follows.

(table macro-aliases-table 'mac 'fn)
(defun fn (x)
  (if (consp x)
      (mac (cdr x))
    x))

Although this is obviously a contrived example, this flexibility can be useful to macro writers; see for example the definition of ACL2 system macro defun-inline.

The table macro-aliases-table is an alist that associates macro symbols with function symbols, so that macro names may be used as runic designators (see theories). For a convenient way to add entries to this table, see add-macro-alias. To remove entries from the table with ease, see remove-macro-alias.

This table is used by the theory functions; see theories. For example, in order that (disable append) be interpreted as (disable binary-append), it is necessary that the example form above has been executed. In fact, this table does indeed associate many of the macros provided by the ACL2 system, including append, with function symbols. Loosely speaking, it only does so when the macro is ``essentially the same thing as'' a corresponding function; for example, (append x y) and (binary-append x y) represent the same term, for any expressions x and y.