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
|
<html>
<head><title>USING-COMPUTED-HINTS-8.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>USING-COMPUTED-HINTS-8</h2>Some Final Comments
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
None of the examples show the use of the variable <code>WORLD</code>, which is
allowed in computed hints. There are some (undocumented) ACL2
utilities that might be useful in programming hints, but these
utilities need access to the ACL2 logical world (see <a href="WORLD.html">world</a>).<p>
A very useful fact to know is that <code>(table-alist name world)</code>
returns an alist representation of the current value of the <code><a href="TABLE.html">table</a></code>
named <code>name</code>.<p>
The ACL2 source code is littered with <code>:</code><code><a href="PROGRAM.html">program</a></code> mode
functions for manipulating world. In our source code, the
world is usually bound a variable named <code>wrld</code>; so searching
our code for that name might be helpful.
<p>
Using these utilities to look at the <code>WORLD</code> one can, for example,
determine whether a symbol is defined recursively or not, get the
body and formals of a defined function, or fetch the statement of a
given lemma. Because these utilities are not yet documented, we do
not expect users to employ <code>WORLD</code> in computed hints. But experts
might and it might lead to the formulation of a more convenient
language for computed hints.<p>
None of our examples illustrated the 7 argument form of a computed
hint,
<code>(fn ID CLAUSE WORLD STABLE-UNDER-SIMPLIFICATIONP HIST PSPV CTX)</code>.
When used, the variables <code>HIST</code>, <code>PSPV</code>, and <code>CTX</code>, are bound
to the clause history, the package of ``special variables'' governing
the clause, and the ``error message context.'' These variables are
commonly used throughout our source code but are, unfortunately,
undocumented. Again, we expect a few experts will find them useful
in developing computed hints.<p>
If you start using computed hints extensively, please contact the
developers of ACL2 and let us know what you are doing with them and
how we can help.
<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>
|
