		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Obj-size

How many characters are required to print an object. (bounded)

Signature
(obj-size x size max eviscp config) → size
Arguments: x — Object whose size we are counting.; size — Size we've counted up so far.
Guard (natp size).; max — Limit on how large of a size to compute.
Guard (natp max).; eviscp — Is evisceration enabled?.
Guard (booleanp eviscp).; config — For settings like print-base, etc.
Guard (printconfig-p config).
Returns: size — Type (posp size).

Definitions and Theorems

Function: obj-size

(defun obj-size (x size max eviscp config)
  (declare (xargs :guard (and (natp size)
                              (natp max)
                              (booleanp eviscp)
                              (printconfig-p config))))
  (let ((acl2::__function__ 'obj-size))
    (declare (ignorable acl2::__function__))
    (b* ((size (lnfix size))
         (max (lnfix max))
         ((when (> size max)) size)
         ((when (atom x))
          (+ size (atom-size x config)))
         ((when (and eviscp (evisceratedp x)))
          (+ size
             (max 1 (length (eviscerated->guts x)))))
         ((when (atom (cdr x)))
          (if (not (cdr x))
              (obj-size (car x)
                        (+ 2 size)
                        max eviscp config)
            (obj-size (cdr x)
                      (obj-size (car x)
                                (+ 5 size)
                                max eviscp config)
                      max eviscp config)))
         ((when (and (eq (car x) 'quote)
                     (consp (cdr x))
                     (null (cddr x))))
          (obj-size (cadr x)
                    (+ 1 size)
                    max eviscp config)))
      (obj-size (cdr x)
                (obj-size (car x)
                          (+ 1 size)
                          max eviscp config)
                max eviscp config))))

Theorem: posp-of-obj-size

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