		Search-engine friendly clone of the ACL2 documentation.

Macros

Macro-aliases-table

A table used to associate function names with macro names

Example Form:
(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)).

General Form:

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

or more generally

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

where macro-name-form and function-name-form evaluate to values MAC and FN, subject to the following requirements.

MAC is a symbol that is a macro name.
FN is a symbol.
FN is either a function symbol or else a symbol that does not have a definition (a new name). In particular, FN is not a macro name.

After admitting the table event displayed above, we may say that MAC is a macro-alias for FN.

Further Explanation

See table for a general discussion of tables and the table event, which is used to manipulate tables. The table, macro-aliases-table, is an alist that can associate macro symbols with function symbols, so that macro names may be used as runic designators (see theories and discussion below). For a convenient way to add entries to this table, see add-macro-alias, which allows the second argument to be, itself, a macro-alias. To remove entries conveniently from the table, see remove-macro-alias.

As hinted above, this table is used by theory functions; see theories. For example, in order that (disable append) be interpreted as (disable binary-append), it suffices that (table macro-aliases-table 'append 'binary-append), has been executed. In fact, this table does indeed establish many of the macros provided by the ACL2 system as macro-aliases, such as establishing append as a macro-alias for binary-append. This only takes place 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.

Note that the value FN of function-name-form (above) is allowed to be a symbol to be defined later as a function symbol. The following examples illustrate some approaches that work and some that do not.

;;;;;;;;;;
;;; Example 1: No errors, with function defined before setting the table.
;;;;;;;;;;

(defun fn (x) x)
(defmacro mac (x) (list 'fn x))
(table macro-aliases-table 'mac 'fn) ; or (add-macro-alias mac fn)
(in-theory (disable mac))

;;;;;;;;;;
;;; Example 2: No errors, with function defined after setting the table.
;;;;;;;;;;

(defmacro mac (x) (list 'fn x))

; Legal, even though fn is not yet defined:
(table macro-aliases-table 'mac 'fn) ; or (add-macro-alias mac fn)

(defun fn (x) x)
(in-theory (disable mac))

;;;;;;;;;;
;;; Example 3: ERROR.
;;;;;;;;;;

(defun fn (x) x)
(defmacro mac1 (x) (fn x))
(defmacro mac2 (x) (list 'mac1 x))

; BAD, since the table event above anticipates fn to be defined as
; a function, not a macro (but, no error yet) -- but not (yet) an error:
(table macro-aliases-table 'mac2 'mac1) ; or (add-macro-alias mac2 mac1)

; ERROR, since mac2 does not designate rules, because it aliases a macro:
(in-theory (disable mac2))

; OK, but too late to help with that in-theory event; see below:
(table macro-aliases-table 'mac1 'fn) ; or (add-macro-alias mac1 fn)

; ERROR, since mac2 is still associated with mac1, not with fn:
(in-theory (disable mac2))

;;;;;;;;;;
;;; Example 4: Fixed version of Example 3.
;;;;;;;;;;

(defun fn (x) x)
(defmacro mac1 (x) (fn x))
(defmacro mac2 (x) (list 'mac1 x))
(add-macro-alias mac1 fn); or (table macro-aliases-table 'mac1 'fn)

; The following is equivalent to (add-macro-alias mac2 fn), since
; mac1 is a macro-alias for fn by virtue of the preceding event.
(add-macro-alias mac2 mac1)

; Success:
(in-theory (disable mac2))