		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-escape

Validate an escape sequence.

Signature
(valid-escape esc max) → (mv erp code)
Arguments: esc — Guard (escapep esc).; max — Guard (natp max).
Returns: erp — Type (maybe-msgp erp).; code — Type (natp code).

If the escape sequence is valid, we return its character code. For simple and octal escapes, and for universal character names, we use separate validation functions. For a hexadecimal escape, we calculate the numeric value, and we subject them to same restrictions as octal escapes [C17:6.4.4.4/9] [C17:6.4.5/4].

Although [C17] does not seem to state that explicitly, it seems reasonable that the same restriction applies to universal character names; we will revise this if that turns out to be not the case.

Definitions and Theorems

Function: valid-escape

(defun valid-escape (esc max)
 (declare (xargs :guard (and (escapep esc) (natp max))))
 (let ((__function__ 'valid-escape))
  (declare (ignorable __function__))
  (b* (((reterr) 0))
   (escape-case
    esc :simple
    (retok (valid-simple-escape esc.unwrap))
    :oct (valid-oct-escape esc.unwrap max)
    :hex
    (b* ((code (str::hex-digit-chars-value esc.unwrap)))
     (if (<= code (nfix max))
         (retok code)
      (retmsg$
       "The hexadecimal escape sequence ~x0 has value ~x1, ~
                        which exceeds the maximum allowed ~x2, ~
                        required in the context where ~
                        this hexadecimal escape occurs."
       (escape-fix esc)
       code (nfix max))))
    :univ (valid-univ-char-name esc.unwrap max)))))

Theorem: maybe-msgp-of-valid-escape.erp

(defthm maybe-msgp-of-valid-escape.erp
  (b* (((mv acl2::?erp ?code)
        (valid-escape esc max)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: natp-of-valid-escape.code

(defthm natp-of-valid-escape.code
  (b* (((mv acl2::?erp ?code)
        (valid-escape esc max)))
    (natp code))
  :rule-classes :rewrite)

Theorem: valid-escape-of-escape-fix-esc

(defthm valid-escape-of-escape-fix-esc
  (equal (valid-escape (escape-fix esc) max)
         (valid-escape esc max)))

Theorem: valid-escape-escape-equiv-congruence-on-esc

(defthm valid-escape-escape-equiv-congruence-on-esc
  (implies (escape-equiv esc esc-equiv)
           (equal (valid-escape esc max)
                  (valid-escape esc-equiv max)))
  :rule-classes :congruence)

Theorem: valid-escape-of-nfix-max

(defthm valid-escape-of-nfix-max
  (equal (valid-escape esc (nfix max))
         (valid-escape esc max)))

Theorem: valid-escape-nat-equiv-congruence-on-max

(defthm valid-escape-nat-equiv-congruence-on-max
  (implies (acl2::nat-equiv max max-equiv)
           (equal (valid-escape esc max)
                  (valid-escape esc max-equiv)))
  :rule-classes :congruence)