User-defined-functions-table
An advanced table used to replace certain system functions
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 untranslate-patterns
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 or the source code for
define 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 untranslation routine will print this as
*A*.
Subtopics
- Untranslate-patterns
- A database used to extend untranslate, ACL2's function for
displaying terms during proofs, with pattern-based rules.
- Add-const-to-untranslate-preprocess
- Extend untranslate-preprocess
to keep a constant unexpanded in output.
