• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
      • Pretty-printing
        • Pretty-printing-implementation
        • Eviscerate
        • Pretty
        • Revappend-pretty
        • Pretty-list
      • Printtree
      • Base64
      • Charset-p
      • Strtok!
      • Cases
      • Concatenation
      • Html-encoding
      • Character-kinds
      • Substrings
      • Strtok
      • Equivalences
      • Url-encoding
      • Lines
      • Explode-implode-equalities
      • Ordering
      • Numbers
      • Pad-trim
      • Coercion
      • Std/strings/digit-to-char
      • Substitution
      • Symbols
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Pretty-printing

Pretty

Pretty-print any ACL2 object into a string.

Signature

(pretty x &key (config '*default-printconfig*) 
        (col '0) 
        (eviscp 'nil)) 
 
  → 
pretty-x

Arguments

x — The ACL2 object to pretty-print.

config — Optional pretty-printer configuration options.
    Guard (printconfig-p config).

col — Optional starting column number.
    Guard (natp col).

eviscp — Optional flag for use with eviscerated objects.
    Guard (booleanp eviscp).

Returns

pretty-x — Type (stringp pretty-x).

This is our simplest pretty-printing function.

Examples:

ACL2 !>(str::pretty '(1 2 3))
"(1 2 3)"

ACL2 !>(str::pretty (make-list 30 :initial-element 'str::hello))
"(STR::HELLO STR::HELLO STR::HELLO
             STR::HELLO STR::HELLO STR::HELLO
             STR::HELLO STR::HELLO STR::HELLO
             STR::HELLO STR::HELLO STR::HELLO
             STR::HELLO STR::HELLO STR::HELLO
             STR::HELLO STR::HELLO STR::HELLO
             STR::HELLO STR::HELLO STR::HELLO
             STR::HELLO STR::HELLO STR::HELLO
             STR::HELLO STR::HELLO STR::HELLO
             STR::HELLO STR::HELLO STR::HELLO)"

ACL2 !>(str::pretty (make-list 30 :initial-element 'str::hello)
                    :config (make-printconfig
                              :home-package (pkg-witness "STR")
                              :print-lowercase t))
"(hello hello hello hello hello hello
        hello hello hello hello hello hello
        hello hello hello hello hello hello
        hello hello hello hello hello hello
        hello hello hello hello hello hello)"

Definitions and Theorems

Function: pretty-fn

(defun pretty-fn (x config col eviscp)
  (declare (xargs :guard (and (printconfig-p config)
                              (natp col)
                              (booleanp eviscp))))
  (let ((acl2::__function__ 'pretty))
    (declare (ignorable acl2::__function__))
    (rchars-to-string (ppr x col config eviscp nil))))

Theorem: stringp-of-pretty

(defthm stringp-of-pretty
  (b* ((pretty-x (pretty-fn x config col eviscp)))
    (stringp pretty-x))
  :rule-classes :type-prescription)