Elide portions of a term, for use with pretty.
(eviscerate x config) → eviscerated-x
Sometimes terms are too big to practically print. Much like ACL2's built-in pretty-printer, our pretty-printing functions have special support for printing ``eviscerated'' terms where, e.g., some particular subterms are elided in certain ways.
The pretty-printer itself does not do any elision. Instead,
ACL2 has its own, built-in evisceration functions that support fancy features such as ACL2::iprinting. However, much like ACL2's pretty printer itself, these functions are in program mode and take state, which is sometimes inconvenient. So, here, we (re)implement a simple evisceration function that provides fewer features but avoids state.
Suppose we want to pretty-print the following constant:
ACL2 !> (defconst *demo* '(foo (bar aaa bbb ccc (baz 1 2 3)) 1 2 3 4 5 6 (baz 3 2 1)))
ACL2 !> (str::pretty *demo*) "(FOO (BAR AAA BBB CCC (BAZ 1 2 3)) 1 2 3 4 5 6 (BAZ 3 2 1))"
To print with evisceration, we (1) eviscerate the term and then (2) tell pretty to print it with evisceration enabled. For example:
ACL2 !> (let* ((econfig (str::make-eviscconfig :print-level 100 :print-length 2))) (str::pretty (str::eviscerate *demo* econfig) :eviscp t)) "(FOO (BAR AAA ...) ...)"
Above the use of
ACL2 !> (let* ((econfig (str::make-eviscconfig :print-level 100 :print-length 4))) (str::pretty (str::eviscerate *demo* econfig) :eviscp t)) "(FOO (BAR AAA BBB CCC ...) 1 2 ...)"
There are also other options for hiding all subterms with a certain car, and for making particular replacements of particular subterms; see eviscconfig for details.
(defun eviscerate (x config) (declare (xargs :guard (eviscconfig-p config))) (let ((acl2::__function__ 'eviscerate)) (declare (ignorable acl2::__function__)) (b* (((eviscconfig config)) ((when (or config.print-level config.print-length (eviscerate1p x config))) (eviscerate1 x 0 config))) x)))