radix - ACL2 Book

other

(in-package "RADIX")

other

(local (include-book "arithmetic-3/bind-free/top" :dir :system))

other

(local (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system))

ilogfunction

(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)))))

hex-digitfunction

(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))))))

int2hex-lstfunction

(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))))

other

(defthm character-listp-int2hex-lst
  (implies (character-listp ans)
    (character-listp (int2hex-lst x
        len
        cap
        ans))))

int2hexfunction

(defun int2hex
  (x len cap)
  (declare (xargs :guard (and (integerp x)
        (natp len)
        (booleanp cap))))
  (coerce (int2hex-lst x len cap nil)
    'string))

hex-print-sizefunction

(defun hex-print-size
  (x)
  (declare (xargs :guard (natp x)))
  (1+ (ilog x 16)))

nat2hexfunction

(defun nat2hex
  (x cap)
  (declare (xargs :guard (and (booleanp cap) (natp x))))
  (int2hex x
    (hex-print-size x)
    cap))

convert-radix-lstfunction

(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))))

other

(defthm character-listp-convert-radix-lst
  (implies (character-listp ans)
    (character-listp (convert-radix-lst x
        len
        base
        ans))))

convert-int-radixfunction

(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))

radix-print-sizefunction

(defun radix-print-size
  (x base)
  (declare (xargs :guard (and (natp x)
        (natp base)
        (<= 2 base))))
  (1+ (ilog x base)))

convert-nat-radixfunction

(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))

nat2binfunction

(defun nat2bin
  (x)
  (convert-nat-radix x 2))

nat2octfunction

(defun nat2oct
  (x)
  (convert-nat-radix x 8))

int2binfunction

(defun int2bin
  (x len)
  (convert-int-radix x len 2))

int2octfunction

(defun int2oct
  (x len)
  (convert-int-radix x len 8))