		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-escape

Print an escape sequence.

Signature
(print-escape esc pstate) → new-pstate
Arguments: esc — Guard (escapep esc).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

We ensure that there is at least one digit in a hexadecimal escape sequence.

Definitions and Theorems

Function: print-escape

(defun print-escape (esc pstate)
 (declare (xargs :guard (and (escapep esc) (pristatep pstate))))
 (let ((__function__ 'print-escape))
  (declare (ignorable __function__))
  (escape-case
   esc :simple
   (print-simple-escape esc.escape pstate)
   :oct
   (print-oct-escape esc.escape pstate)
   :hex
   (b*
    ((pstate (print-astring "\\x" pstate))
     ((unless esc.escape)
      (raise
       "Misusage error: ~
                      hexadecimal escape sequence has no digits.")
      pstate)
     (pstate (print-hex-digit-achars esc.escape pstate)))
    pstate)
   :univ (print-univ-char-name esc.escape pstate))))

Theorem: pristatep-of-print-escape

(defthm pristatep-of-print-escape
  (b* ((new-pstate (print-escape esc pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: pristate->gcc-of-print-escape

(defthm pristate->gcc-of-print-escape
  (b* ((?new-pstate (print-escape esc pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: print-escape-of-escape-fix-esc

(defthm print-escape-of-escape-fix-esc
  (equal (print-escape (escape-fix esc) pstate)
         (print-escape esc pstate)))

Theorem: print-escape-escape-equiv-congruence-on-esc

(defthm print-escape-escape-equiv-congruence-on-esc
  (implies (escape-equiv esc esc-equiv)
           (equal (print-escape esc pstate)
                  (print-escape esc-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-escape-of-pristate-fix-pstate

(defthm print-escape-of-pristate-fix-pstate
  (equal (print-escape esc (pristate-fix pstate))
         (print-escape esc pstate)))

Theorem: print-escape-pristate-equiv-congruence-on-pstate

(defthm print-escape-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-escape esc pstate)
                  (print-escape esc pstate-equiv)))
  :rule-classes :congruence)