		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Radix-print-int

Print an integer in a particular print base, with radix.

Signature
(radix-print-int x base acc) → new-acc
Arguments: x — Guard (integerp x).; base — Guard (print-base-p base).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: radix-print-int

(defun radix-print-int (x base acc)
  (declare (type integer x)
           (type (unsigned-byte 5) base))
  (declare (xargs :guard (and (integerp x) (print-base-p base))))
  (declare (xargs :split-types t))
  (let ((acl2::__function__ 'radix-print-int))
    (declare (ignorable acl2::__function__))
    (case base
      (10 (cons #\.
                (if (< x 0)
                    (revappend-nat-to-dec-chars (- x)
                                                (cons #\- acc))
                  (revappend-nat-to-dec-chars x acc))))
      (16 (let ((acc (list* #\x #\# acc)))
            (if (< x 0)
                (revappend-nat-to-hex-chars (- x)
                                            (cons #\- acc))
              (revappend-nat-to-hex-chars x acc))))
      (8 (let ((acc (list* #\o #\# acc)))
           (if (< x 0)
               (revappend-nat-to-oct-chars (- x)
                                           (cons #\- acc))
             (revappend-nat-to-oct-chars x acc))))
      (otherwise (let ((acc (list* #\b #\# acc)))
                   (if (< x 0)
                       (revappend-nat-to-bin-chars (- x)
                                                   (cons #\- acc))
                     (revappend-nat-to-bin-chars x acc)))))))

Theorem: character-listp-of-radix-print-int

(defthm character-listp-of-radix-print-int
  (implies (character-listp acc)
           (b* ((new-acc (radix-print-int x base acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)