		Search-engine friendly clone of the ACL2 documentation.

Hexify-width

Convert numbers into readable hex strings, fixing the number of digits printed

(hexify-width x width) produces output just like hexify, but when printing an integer it always prints the given number of digits. When the number to be printed is longer, it truncates the more significant digits, and when it is shorter, it pads with 0s.

ACL2 !> (cw "foo is ~s0~%" (str::hexify-width (1- (expt 2 32)) 12))
foo is #ux0000_FFFF_FFFF
NIL
ACL2 !>

The #ux is for compatibility with the ACL2::sharp-u-reader.

Definitions and Theorems

Function: hexify-width

(defun hexify-width (x width)
 (declare (xargs :guard (posp width)))
 (b* ((width (mbe :logic (if (posp width) width 1)
                  :exec width)))
  (cond
   ((integerp x)
    (b*
     ((xsign (< x 0))
      (xabs (abs x))
      (chars (explode-atom xabs 16))
      (fixed-chars (cond ((<= width (len chars))
                          (nthcdr (- (len chars) width) chars))
                         (t (append (make-list (- width (len chars))
                                               :initial-element #\0)
                                    chars))))
      (nice-chars
       (list*
         #\# #\u #\x
         (append
              (and xsign '(#\-))
              (cons (first fixed-chars)
                    (insert-underscores (nthcdr 1 fixed-chars)))))))
     (implode nice-chars)))
   ((symbolp x) (symbol-name x))
   ((stringp x) x)
   (t (prog2$ (er hard? 'hexify-width
                  "Unexpected argument ~x0.~%" x)
              "")))))