		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-s-char

Validate a character of a string literal.

Signature
(valid-s-char schar prefix? ienv) → (mv erp code)
Arguments: schar — Guard (s-char-p schar).; prefix? — Guard (eprefix-optionp prefix?).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; code — Type (natp code).

If validation succeeds, we return the character code. [C17:6.4.5/4] says that the same restrictions that apply to c-chars in character constants also apply to s-chars in string literals. So this function is similar to valid-c-char, except that we prohibit double quote instead of single quote, based on the grammar in [C17:6.4.5/1].

Definitions and Theorems

Function: valid-s-char

(defun valid-s-char (schar prefix? ienv)
 (declare (xargs :guard (and (s-char-p schar)
                             (eprefix-optionp prefix?)
                             (ienvp ienv))))
 (b* (((reterr) 0)
      (max (if prefix? 1114111
             (ienv->uchar-max ienv))))
  (s-char-case
   schar
   :char
   (cond
    ((= schar.code (char-code #\"))
     (retmsg$
      "Double quote cannot be used directly ~
                            in a string literal."))
    ((= schar.code 10)
     (retmsg$
      "Line feed cannot be used directly ~
                            in a character constant."))
    ((= schar.code 13)
     (retmsg$
      "Carriage return cannot be used directly ~
                            in a character constant."))
    ((> schar.code max)
     (retmsg$
      "The character with code ~x0 ~
                            exceeds the maximum ~x1 allowed for ~
                            a character constant with prefix ~x2."
      schar.code
      max (eprefix-option-fix prefix?)))
    (t (retok schar.code)))
   :escape (valid-escape schar.escape max))))

Theorem: maybe-msgp-of-valid-s-char.erp

(defthm maybe-msgp-of-valid-s-char.erp
  (b* (((mv acl2::?erp ?code)
        (valid-s-char schar prefix? ienv)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: natp-of-valid-s-char.code

(defthm natp-of-valid-s-char.code
  (b* (((mv acl2::?erp ?code)
        (valid-s-char schar prefix? ienv)))
    (natp code))
  :rule-classes :rewrite)

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

(defthm valid-s-char-of-s-char-fix-schar
  (equal (valid-s-char (s-char-fix schar)
                       prefix? ienv)
         (valid-s-char schar prefix? ienv)))

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

(defthm valid-s-char-s-char-equiv-congruence-on-schar
  (implies (s-char-equiv schar schar-equiv)
           (equal (valid-s-char schar prefix? ienv)
                  (valid-s-char schar-equiv prefix? ienv)))
  :rule-classes :congruence)

Theorem: valid-s-char-of-eprefix-option-fix-prefix?

(defthm valid-s-char-of-eprefix-option-fix-prefix?
  (equal (valid-s-char schar (eprefix-option-fix prefix?)
                       ienv)
         (valid-s-char schar prefix? ienv)))

Theorem: valid-s-char-eprefix-option-equiv-congruence-on-prefix?

(defthm valid-s-char-eprefix-option-equiv-congruence-on-prefix?
  (implies (eprefix-option-equiv prefix? prefix?-equiv)
           (equal (valid-s-char schar prefix? ienv)
                  (valid-s-char schar prefix?-equiv ienv)))
  :rule-classes :congruence)

Theorem: valid-s-char-of-ienv-fix-ienv

(defthm valid-s-char-of-ienv-fix-ienv
  (equal (valid-s-char schar prefix? (ienv-fix ienv))
         (valid-s-char schar prefix? ienv)))

Theorem: valid-s-char-ienv-equiv-congruence-on-ienv

(defthm valid-s-char-ienv-equiv-congruence-on-ienv
  (implies (ienv-equiv ienv ienv-equiv)
           (equal (valid-s-char schar prefix? ienv)
                  (valid-s-char schar prefix? ienv-equiv)))
  :rule-classes :congruence)