Print a character or escape sequence usable in character constants.
The abstract syntax puts no limitation on the character (code), but here we check that it satisfies the requirements in the concrete syntax. It must be a character in the grammar, and in addition it must not be a single quote, a backslash, or a new-line character. The latter check encompasses not only line feed, but also carriage return: recall that both are allowed in our grammar, and that we allow three kinds of new-line characters (line feed alone, carriage return alone, or line feed followed by carriage return).
Function:
(defun print-c-char (cchar pstate) (declare (xargs :guard (and (c-char-p cchar) (pristatep pstate)))) (let ((__function__ 'print-c-char)) (declare (ignorable __function__)) (c-char-case cchar :char (b* (((unless (and (grammar-character-p cchar.unwrap) (not (= cchar.unwrap (char-code #\'))) (not (= cchar.unwrap (char-code #\\))) (not (= cchar.unwrap 10)) (not (= cchar.unwrap 13)))) (raise "Misusage error: ~ the character code ~x0 is disallowed ~ in a character constant." cchar.unwrap) (pristate-fix pstate))) (print-char cchar.unwrap pstate)) :escape (print-escape cchar.unwrap pstate))))
Theorem:
(defthm pristatep-of-print-c-char (b* ((new-pstate (print-c-char cchar pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-c-char-of-c-char-fix-cchar (equal (print-c-char (c-char-fix cchar) pstate) (print-c-char cchar pstate)))
Theorem:
(defthm print-c-char-c-char-equiv-congruence-on-cchar (implies (c-char-equiv cchar cchar-equiv) (equal (print-c-char cchar pstate) (print-c-char cchar-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-c-char-of-pristate-fix-pstate (equal (print-c-char cchar (pristate-fix pstate)) (print-c-char cchar pstate)))
Theorem:
(defthm print-c-char-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-c-char cchar pstate) (print-c-char cchar pstate-equiv))) :rule-classes :congruence)