		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-dec/oct/hex-const

Print a decimal, octal, or hexadecimal constant.

Signature
(print-dec/oct/hex-const dohconst pstate) → new-pstate
Arguments: dohconst — Guard (dec/oct/hex-constp dohconst).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep 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 nil, which is what we want, because the octal constant 0 is represented as one leading zero and value zero.

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.

Definitions and Theorems

Function: print-dec/oct/hex-const

(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: pristatep-of-print-dec/oct/hex-const

(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: pristate->gcc-of-print-dec/oct/hex-const

(defthm pristate->gcc-of-print-dec/oct/hex-const
  (b* ((?new-pstate (print-dec/oct/hex-const dohconst pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: print-dec/oct/hex-const-of-dec/oct/hex-const-fix-dohconst

(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: print-dec/oct/hex-const-dec/oct/hex-const-equiv-congruence-on-dohconst

(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: print-dec/oct/hex-const-of-pristate-fix-pstate

(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: print-dec/oct/hex-const-pristate-equiv-congruence-on-pstate

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