Major Section: MISCELLANEOUS
None of the examples show the use of the variable WORLD, 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 world).
A very useful fact to know is that (table-alist name world)
returns an alist representation of the current value of the table
named name.
The ACL2 source code is littered with :program mode
functions for manipulating world. In our source code, the
world is usually bound a variable named wrld; so searching
our code for that name might be helpful.
Using these utilities to look at the WORLD 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 WORLD in computed hints. But experts
might and it might lead to the formulation of a more convenient
language for computed hints.
None of our examples illustrated the 7 argument form of a computed
hint,
(fn ID CLAUSE WORLD STABLE-UNDER-SIMPLIFICATIONP HIST PSPV CTX).
When used, the variables HIST, PSPV, and CTX, 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.
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.
