Print a decimal, octal, or hexadecimal constant.
(print-dec/oct/hex-const dohconst pstate) → new-pstate
For a decimal constant, the abstract syntax gives us the value (a positive integer), which we convert to ACL2 decimal digit characters, which we print.
For an octal constant,
first we print the leading zeros.
We convert the value, which is a non-negative integer,
into octal digits, using an auxiliary function from the library
that turns 0 into
For a hexadecimal constant, first we print the prefix. We ensure that there is at least one digit (otherwise it is not a syntactically valid hexadecimal constant), and we print them.
Function:
(defun print-dec/oct/hex-const (dohconst pstate) (declare (xargs :guard (and (dec/oct/hex-constp dohconst) (pristatep pstate)))) (let ((__function__ 'print-dec/oct/hex-const)) (declare (ignorable __function__)) (dec/oct/hex-const-case dohconst :dec (print-dec-digit-achars (str::nat-to-dec-chars dohconst.value) pstate) :oct (b* ((pstate (print-oct-digit-achars (repeat dohconst.leading-zeros #\0) pstate)) (pstate (print-oct-digit-achars (str::nat-to-oct-chars-aux dohconst.value nil) pstate))) pstate) :hex (b* (((unless dohconst.digits) (raise "Misusage error: ~ the hexadecimal constant has no digits.") (pristate-fix pstate)) (pstate (print-hprefix dohconst.prefix pstate)) (pstate (print-hex-digit-achars dohconst.digits pstate))) pstate))))
Theorem:
(defthm pristatep-of-print-dec/oct/hex-const (b* ((new-pstate (print-dec/oct/hex-const dohconst pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-dec/oct/hex-const-of-dec/oct/hex-const-fix-dohconst (equal (print-dec/oct/hex-const (dec/oct/hex-const-fix dohconst) pstate) (print-dec/oct/hex-const dohconst pstate)))
Theorem:
(defthm print-dec/oct/hex-const-dec/oct/hex-const-equiv-congruence-on-dohconst (implies (dec/oct/hex-const-equiv dohconst dohconst-equiv) (equal (print-dec/oct/hex-const dohconst pstate) (print-dec/oct/hex-const dohconst-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-dec/oct/hex-const-of-pristate-fix-pstate (equal (print-dec/oct/hex-const dohconst (pristate-fix pstate)) (print-dec/oct/hex-const dohconst pstate)))
Theorem:
(defthm print-dec/oct/hex-const-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-dec/oct/hex-const dohconst pstate) (print-dec/oct/hex-const dohconst pstate-equiv))) :rule-classes :congruence)