		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-char

Print a character.

Signature
(print-char char pstate) → new-pstate
Arguments: char — Guard (natp char).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

We UTF-8-encode the character code into one, two, three, or four bytes.

This is the most basic printing function in our printer. All other printing functions call this one, directly or indirectly.

Definitions and Theorems

Function: print-char

(defun print-char (char pstate)
 (declare (xargs :guard (and (natp char) (pristatep pstate))))
 (declare (xargs :guard (grammar-character-p char)))
 (let ((__function__ 'print-char))
  (declare (ignorable __function__))
  (b*
   ((bytes-rev (pristate->bytes-rev pstate))
    (encoding (cond ((< char 128) (list char))
                    ((< char 2048)
                     (list (logior (ash char -6) 192)
                           (logior (logand char 63) 128)))
                    ((< char 65536)
                     (list (logior (ash char -12) 224)
                           (logior (logand (ash char -6) 63) 128)
                           (logior (logand char 63) 128)))
                    (t (list (logior (ash char -18) 240)
                             (logior (logand (ash char -12) 63) 128)
                             (logior (logand (ash char -6) 63) 128)
                             (logior (logand char 63) 128)))))
    (new-bytes-rev (append (rev encoding) bytes-rev))
    (new-pstate (change-pristate pstate
                                 :bytes-rev new-bytes-rev)))
   new-pstate)))

Theorem: pristatep-of-print-char

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

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

(defthm print-char-of-pristate-fix-pstate
  (equal (print-char char (pristate-fix pstate))
         (print-char char pstate)))

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

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