1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
<html>
<head><title>MACRO-ALIASES-TABLE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>MACRO-ALIASES-TABLE</h2>a <a href="TABLE.html">table</a> used to associate function names with macro names
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
Example:
(table macro-aliases-table 'append 'binary-append)
</pre>
This example associates the function symbol <code><a href="BINARY-APPEND.html">binary-append</a></code> with the
macro name <code><a href="APPEND.html">append</a></code>. As a result, the name <code><a href="APPEND.html">append</a></code> may be used as a
runic designator (see <a href="THEORIES.html">theories</a>) by the various theory
functions. Thus, for example, it will be legal to write
<pre>
(in-theory (disable append))
</pre>
as an abbreviation for
<pre>
(in-theory (disable binary-append))
</pre>
which in turn really abbreviates
<pre>
(in-theory (set-difference-theories (current-theory :here)
'(binary-append)))
<p>
General Form:
(table macro-aliases-table 'macro-name 'function-name)
</pre>
or very generally
<pre>
(table macro-aliases-table macro-name-form function-name-form)
</pre>
where <code>macro-name-form</code> and <code>function-name-form</code> evaluate,
respectively, to a macro name and a function name in the current
ACL2 <a href="WORLD.html">world</a>. See <a href="TABLE.html">table</a> for a general discussion of tables and
the <code>table</code> event used to manipulate tables.<p>
The <code><a href="TABLE.html">table</a></code> <code><a href="MACRO-ALIASES-TABLE.html">macro-aliases-table</a></code> is an alist that associates
macro symbols with function symbols, so that macro names may be used
as runic designators (see <a href="THEORIES.html">theories</a>). For a convenient way to
add entries to this <a href="TABLE.html">table</a>, see <a href="ADD-MACRO-ALIAS.html">add-macro-alias</a>. To remove
entries from the <a href="TABLE.html">table</a> with ease, see <a href="REMOVE-MACRO-ALIAS.html">remove-macro-alias</a>.<p>
This <a href="TABLE.html">table</a> is used by the theory functions. For example, in order
that <code>(disable append)</code> be interpreted as <code>(disable binary-append)</code>,
it is necessary that the example form above has been executed. In
fact, this <a href="TABLE.html">table</a> does indeed associate many of the macros provided
by the ACL2 system, including <code><a href="APPEND.html">append</a></code>, with function symbols.
Loosely speaking, it only does so when the macro is ``essentially
the same thing as'' a corresponding function; for example,
<code>(append x y)</code> and <code>(binary-append x y)</code> represent the same term,
for any expressions <code>x</code> and <code>y</code>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
