Using-computed-hints-8
Some Final Comments
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.
