		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-s-char

Print a character or escape sequence usable in string literals.

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

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

Definitions and Theorems

Function: print-s-char

(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.code)
                   (not (= schar.code (char-code #\")))
                   (not (= schar.code (char-code #\\)))
                   (not (= schar.code 10))
                   (not (= schar.code 13))))
      (raise
       "Misusage error: ~
                       the character code ~x0 is disallowed ~
                       in a string literal."
       schar.code)
      (pristate-fix pstate)))
    (print-char schar.code pstate))
   :escape (print-escape schar.escape pstate))))

Theorem: pristatep-of-print-s-char

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

Theorem: pristate->gcc-of-print-s-char

(defthm pristate->gcc-of-print-s-char
  (b* ((?new-pstate (print-s-char schar pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: print-s-char-of-s-char-fix-schar

(defthm print-s-char-of-s-char-fix-schar
  (equal (print-s-char (s-char-fix schar) pstate)
         (print-s-char schar pstate)))

Theorem: print-s-char-s-char-equiv-congruence-on-schar

(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: print-s-char-of-pristate-fix-pstate

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

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

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