		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Atom-size

How many characters are required to print an atom? (BOZO: roughly)

Signature
(atom-size x config) → size
Arguments: x — Guard (atom x).; config — Guard (printconfig-p config).
Returns: size — Type (posp size).

BOZO this doesn't seem quite right in certain cases.

Symbols: I don't think we're properly accounting for the empty symbol's bars, or for any escape characters that we need for a symbol.

Complex rationals: I don't think we're accounting for the #c() parts.

Definitions and Theorems

Function: atom-size

(defun atom-size (x config)
 (declare (xargs :guard (and (atom x) (printconfig-p config))))
 (let ((acl2::__function__ 'atom-size))
  (declare (ignorable acl2::__function__))
  (cond
   ((symbolp x)
    (b*
     ((name (symbol-name x))
      (name-size (if (my-needs-slashes name config)
                     (+ 2 (length name))
                   (length name)))
      ((when (keywordp x)) (+ 1 name-size))
      (pkg-name (symbol-package-name x))
      (home-package (printconfig->home-package config))
      ((when
          (or (equal (symbol-package-name home-package)
                     pkg-name)
              (eq x
                  (intern-in-package-of-symbol name home-package))))
       name-size)
      (pkg-size (if (my-needs-slashes pkg-name config)
                    (+ 4 (length pkg-name))
                  (+ 2 (length pkg-name)))))
     (+ name-size pkg-size)))
   ((integerp x)
    (b* ((base (printconfig->print-base config))
         (radixp (printconfig->print-radix config))
         (size (int-size x base))
         ((unless radixp) size)
         ((when (eql base 10)) (+ 1 size)))
      (+ 2 size)))
   ((characterp x)
    (case x
      (#\Newline 9)
      (#\Rubout 8)
      (#\Return 8)
      (#\Space 7)
      (#\Page 6)
      (#\Tab 5)
      (otherwise 3)))
   ((stringp x) (+ 2 (length x)))
   ((rationalp x)
    (b* ((base (printconfig->print-base config))
         (radixp (printconfig->print-radix config))
         (size (int-size (numerator x) base))
         (size (+ size (int-size (denominator x) base)))
         ((unless radixp) (+ 1 size))
         ((when (eql base 10)) (+ 5 size)))
      (+ 3 size)))
   ((complex-rationalp x)
    (+ (atom-size (realpart x) config)
       (atom-size (imagpart x) config)))
   (t (progn$ (raise "Bad atom.") 1)))))

Theorem: posp-of-atom-size

(defthm posp-of-atom-size
  (b* ((size (atom-size x config)))
    (posp size))
  :rule-classes :type-prescription)