		Search-engine friendly clone of the ACL2 documentation.

Explode-atom

Convert any atom into a character-listp that contains its printed representation, rendering numbers in your choice of print base.

(explode-atom x print-base) prints the atom x as a list of characters, using some print-base-p to decide what base to print numbers in.

Examples:

(explode-atom 15 10) --> (#\1 #\5)              ; 15 in decimal
(explode-atom 15 16) --> (#\F)                  ; 15 in hex
(explode-atom "foo" 10) --> (#\f #\o #\o)
(explode-atom 'acl2::foo 10) --> (#\F #\O #\O)  ; note: no package

Function: explode-atom

(defun
 explode-atom (x print-base)
 (declare (xargs :guard (and (or (acl2-numberp x)
                                 (characterp x)
                                 (stringp x)
                                 (symbolp x))
                             (print-base-p print-base))))
 (cond
  ((rationalp x)
   (cond
    ((integerp x)
     (cond ((< x 0)
            (cons #\-
                  (explode-nonnegative-integer (- x)
                                               print-base nil)))
           (t (explode-nonnegative-integer x print-base nil))))
    (t
     (append (explode-atom (numerator x) print-base)
             (cons #\/
                   (explode-nonnegative-integer (denominator x)
                                                print-base nil))))))
  ((complex-rationalp x)
   (list*
        #\# #\C #\(
        (append (explode-atom (realpart x) print-base)
                (cons #\Space
                      (append (explode-atom (imagpart x) print-base)
                              '(#\)))))))
  ((characterp x) (list x))
  ((stringp x) (coerce x 'list))
  (t (coerce (symbol-name x) 'list))))