|
|
|---|
|
|
|
|---|
Control suppression of details when printing
ACL2 output is generally printed in full. However, ACL2 can be
directed to abbreviate, or ``eviscerate'', objects before printing them. To
``eviscerate'' an object we replace certain substructures within it by strings
that are printed in their stead. Such replacement is made relative to a
so-called ``evisc-tuple'', which has four components:
The following example illustrates the use of an evisc-tuple that limits the
print-level to 3 — only three descents into list structures are
permitted before replacing a subexpression by `
ACL2 !>(fms "~x0~%" (list (cons #\0 '((a b ((c d)) e f g) u v w x y))) *standard-co* state (evisc-tuple 3 4 nil nil)) ((A B (#) E ...) U V W ...) <state> ACL2 !>
Notice that it is impossible to read the printed value back into ACL2,
since there is no way for the ACL2 reader to interpret `
In the above example we pass an evisc-tuple explicitly to a printing function, in this case, fms (see fmt). But ACL2 also does its own printing, for example during a proof attempt. There are global evisc-tuples that control ACL2's printing; see set-evisc-tuple and see without-evisc.