		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing

Eviscerate

Elide portions of a term, for use with pretty.

Signature
(eviscerate x config) → eviscerated-x
Arguments: x — The term to eviscerate.; config — Guard (eviscconfig-p config).
Returns: eviscerated-x — A new version of x, perhaps with some subterms replaced.

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, eviscerate is a separate function that can be used, ahead of time, to elide certain sub-terms. Typically the result of eviscerate is then given to, e.g., pretty, along with a special :eviscp flag) to indicate that elisions have been made.

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.

Our function is very much styled after ACL2's and should be familiar if you know about ACL2's evisc-tuples, except that instead of evisc-tuples we use eviscconfig structures.

Examples

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)))

To print without evisceration we can just use pretty directly (with its default printconfig:

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 print-length truncates the printing after two items in each list. Extending the print-length lets us see more of the term:

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.

Definitions and Theorems

Function: eviscerate

(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)))

Subtopics

Eviscconfig: Controls how to eviscerate a term—our alternative to ACL2's evisc-tuples.
Eviscerate1: Main function for eviscerating a term.
Eviscerate1p: Helper function for avoiding consing when evisceration will not change a term.