Major Section: EVENTS
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
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 file 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*
term))
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*.
