MACRO-ALIASES-TABLE

a table used to associate function names with macro names

Major Section: EVENTS

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 function name in the current ACL2 world. See table for a general discussion of tables and the table event used to manipulate tables.

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. 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.