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
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
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.
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
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 user-defined-functions-table 'untranslate-preprocess 'my-preprocess)This will install
my-preprocessas 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