Print a character or escape sequence usable in string literals.
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 double 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-s-char (schar pstate) (declare (xargs :guard (and (s-char-p schar) (pristatep pstate)))) (let ((__function__ 'print-s-char)) (declare (ignorable __function__)) (s-char-case schar :char (b* (((unless (and (grammar-character-p schar.unwrap) (not (= schar.unwrap (char-code #\"))) (not (= schar.unwrap (char-code #\\))) (not (= schar.unwrap 10)) (not (= schar.unwrap 13)))) (raise "Misusage error: ~ the character code ~x0 is disallowed ~ in a string literal." schar.unwrap) (pristate-fix pstate))) (print-char schar.unwrap pstate)) :escape (print-escape schar.unwrap pstate))))
Theorem:
(defthm pristatep-of-print-s-char (b* ((new-pstate (print-s-char schar pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-s-char-of-s-char-fix-schar (equal (print-s-char (s-char-fix schar) pstate) (print-s-char schar pstate)))
Theorem:
(defthm print-s-char-s-char-equiv-congruence-on-schar (implies (s-char-equiv schar schar-equiv) (equal (print-s-char schar pstate) (print-s-char schar-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-s-char-of-pristate-fix-pstate (equal (print-s-char schar (pristate-fix pstate)) (print-s-char schar pstate)))
Theorem:
(defthm print-s-char-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-s-char schar pstate) (print-s-char schar pstate-equiv))) :rule-classes :congruence)