/usr/share/acl2-6.3/books/misc/radix.lisp is in acl2-books-source 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 | ; From Jun Sawada, July 2005.
;; Book for Radix conversion
;; Main functions that are defined in this books are:
;; (int2hex x len)
;; Converting a signed integer to a hexadecimal string of length len.
;; It includes uppercase letters from A to F in the resulting string.
;; (nat2hex x)
;; Converting a natural number to a hexadecimal string
;; It includes uppercase letters from A to F in the resulting string.
;; (int2oct x len)
;; Converting a signed integer to a octagonal string of length len.
;; (nat2oct x)
;; Converting a signed integer to a octagonal string.
;; (int2bin x len)
;; Converting a signed integer to a binary string of length len.
;; (nat2bin x)
;; Converting a natural number to a binary string.
;; (int2digits x len base)
;; Converting a signed integer to a string of digits of length len.
;; Base is used for the conversion.
;; (nat2digits x base)
;; Converting a natural number to a string of digits, using base
;; for the conversion.
(in-package "RADIX")
;; These books are included to prove some guards.
(local (include-book "arithmetic-2/meta/top" :dir :system))
(local (include-book "arithmetic-2/floor-mod/floor-mod" :dir :system))
;; Returns the maximum integer that is not larger than the log of x with base,
;; In TeX format, $\lfloor\log_{base}(x)\rfloor$.
;; Thus (ilog 10 3) = 2
(defun ilog (x base)
(declare (xargs :guard (and (natp x) (natp base) (<= 2 base))))
(if (or (zp x) (zp base) (< base 2)) 0
(if (< x base) 0
(1+ (ilog (floor x base) base)))))
(defun hex-digit (n cap)
(declare (xargs :guard (and (natp n) (<= 0 n) (< n 16) (booleanp cap))))
(if (< n 10)
(digit-to-char n)
(if cap
(code-char (+ n -10 (char-code #\A)))
(code-char (+ n -10 (char-code #\a))))))
(defun int2hex-lst (x len cap ans)
(declare (xargs :guard (and (integerp x) (natp len) (booleanp cap)
(listp ans))))
(if (zp len)
ans
(int2hex-lst (floor x 16) (1- len) cap
(cons (hex-digit (mod x 16) cap) ans))))
(defthm character-listp-int2hex-lst
(implies (character-listp ans)
(character-listp (int2hex-lst x len cap ans))))
; (int2hex x len cap) converts an integer x to a hexadecimal
; string of length len. If cap is non-nil, it uses ABCDEF as opposed to
; abcdef.
(defun int2hex (x len cap)
(declare (xargs :guard (and (integerp x) (natp len) (booleanp cap))))
(coerce (int2hex-lst x len cap nil) 'string))
; Returns how many characters of hex-digits are needed to print natural
; number x.
(defun hex-print-size (x)
(declare (xargs :guard (natp x)))
(1+ (ilog x 16)))
; (nat2hex x cap) converts natural number x to a hexadecimal string.
; If cap is non-nil, ABCDEF are used in the hexadecimal representation.
(defun nat2hex (x cap)
(declare (xargs :guard (and (booleanp cap) (natp x))))
(int2hex x (hex-print-size x) cap))
(defun convert-radix-lst (x len base ans)
(declare (xargs :guard (and (integerp x) (natp len)
(natp base) (<= 2 base) (<= base 10))))
(if (zp len)
ans
(convert-radix-lst (floor x base) (1- len) base
(cons (digit-to-char (mod x base)) ans))))
(defthm character-listp-convert-radix-lst
(implies (character-listp ans)
(character-listp (convert-radix-lst x len base ans))))
; (convert-radix x n r) converts an integer x to a digit-string of length n,
; using radix r. For example (convert-radix x 32 2) converts x to
; binary string of length 32.
(defun convert-int-radix (x n r)
(declare (xargs :guard (and (integerp x) (natp n)
(natp r) (<= 2 r) (<= r 10))))
(coerce (convert-radix-lst x n r nil) 'string))
; Returns how many digits are needed to represent natural number x
; using radix 'base'.
(defun radix-print-size (x base)
(declare (xargs :guard (and (natp x) (natp base) (<= 2 base))))
(1+ (ilog x base)))
; (nat2hex x cap) converts positive integer x to a hexadecimal string.
; If cap is non-nil, ABCDEF are used in the hexadecimal representation.
; Should convert-base be a better name?
(defun convert-nat-radix (x r)
(declare (xargs :guard (and (natp x) (natp r) (<= 2 r) (<= r 10))))
(convert-int-radix x (radix-print-size x r) r))
(defun nat2bin (x)
(convert-nat-radix x 2))
(defun nat2oct (x)
(convert-nat-radix x 8))
(defun int2bin (x len)
(convert-int-radix x len 2))
(defun int2oct (x len)
(convert-int-radix x len 8))
;; Following are examples to format the converted numbers.
;;
;;(fmx "hex of x is ~x0~%" (radix::int2hex 100 (radix::hex-print-size 100) t))
;;
;; Macro to print a non-negative integer in hex.
;(defmacro hexprint+ (x)
; `(fmx "~@0~%" (radix::nat2hex ,x T)))
;; Print an integer in hex assuming that it is 32-bit word.
;(defmacro hexprintw (x)
; `(fmx "~@0~%" (radix::int2hex ,x 8 T)))
;;; Print an integer in hex assuming that is is 64 bit word (quad-word).
;(defmacro hexprintq (x)
; `(fmx "~@0~%" (radix::int2hex ,x 16 T)))
|