USER-DEFINED-FUNCTIONS-TABLE

an advanced table used to replace certain system functions
Major Section:  EVENTS

Example:
(table user-defined-functions-table 'untranslate 'my-untranslate)
This example associates the user-defined function symbol my-untranslate with the build-in function symbol untranslate. As a result, the code for my-untranslate will be run whenever the function untranslate is called. The formals of the two functions must agree and must not contain any stobj names.

This feature should only be used by advanced users who have a thorough understanding of the system functions being replaced. There are currently two ways a user can affect the behavior of untranslate.

First, one can associate untranslate and untranslate-lst with names of functions in this table, to be used in place of untranslate and untranslate-lst (respectively). Note that these overrides fail to occur upon guard violations and some other evaluation errors.

Next, suppose that neither untranslate nor untranslate-lst is associated with a function in the table, but that untranslate-preprocess is associated with a function symbol, fn. Then when ACL2 applies untranslate to a term, the first thing it does is to call fn on two arguments: that term and the current ACL2 logical world. If the call produces a non-nil result, then that result is passed to the untranslate process.

See file books/misc/rtl-untranslate.lisp for an example of user-defined untranslate.