USER-DEFINED-FUNCTIONS-TABLE

an advanced table used to replace certain system functions 
Major Section:  SWITCHES-PARAMETERS-AND-MODES


Examples:
(table user-defined-functions-table 'untranslate-preprocess 'my-preprocess)
(table user-defined-functions-table 'untranslate 'my-untranslate)

This feature should perhaps 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 way ACL2 prints terms.

The first example associates the user-defined function symbol my-preprocess with untranslate-preprocess. As a result, when ACL2 prints a term, say during a proof, using its so-called ``untranslate'' process the first thing it does is to call my-preprocess 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.

The second example associates the user-defined function symbol my-untranslate with the built-in function symbol untranslate. As a result, the code for my-untranslate will be run whenever the untranslate process is run. The formals of the two functions must agree and must not contain any stobj names. Note that these overrides fail to occur upon guard violations and some other evaluation errors.

The untranslate-preprocess approach may suffice for most cases in which a user wants to modify the way output is produced by the theorem prover. We present an example immediately below, but see community book books/misc/untranslate-patterns.lisp for a more elaborate example. If the untranslate-preprocess approach does not seem sufficient for your purposes, you are invited to look at community book books/misc/rtl-untranslate.lisp for an example of user-defined untranslate (i.e., following the second example displayed above).

Suppose you have a large constant that you would prefer not to see in proofs. For example, you may have submitted the following definition (but imagine a much larger constant, say, a list of length 1,000,000). 

(defconst *a* '(a b c d))
If you submit the following (silly) theorem 
(thm (equal (cons x *a*) (car (cons yyy zzz))))
then you will see the following output: 
(EQUAL (CONS X '(A B C D)) YYY).
If *a* had represented a much larger structure, we would wish we could see the following instead. 
(EQUAL (CONS X *A*) YYY)
That can be accomplished as follows. First we make the following definition. 
(defun my-preprocess (term wrld)
  (declare (ignore wrld))
  (if (equal term (list 'quote *a*))
      '*a*
    nil))
Now we submit the following table event. 
(table user-defined-functions-table
       'untranslate-preprocess
       'my-preprocess)
This will install my-preprocess as a preprocessor before the normal untranslation routine is applied to printing a term. When the untranslation routine encounters the constant (QUOTE (A B C D)), it will replace it with *a*, and the usual untranlation routine will print this as *A*.