USING-COMPUTED-HINTS-8

Some Final Comments
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.