		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-univ-char-name

Validate a universal character name.

Signature
(valid-univ-char-name ucn max) → (mv erp code)
Arguments: ucn — Guard (univ-char-name-p ucn).; max — Guard (natp max).
Returns: code — Type (natp code).

If validation is successful, we return the numeric code of the character.

[C:6.4.3/2] states some restriction on the character code. [C:6.4.4.4/4] and (implicitly) [C:6.4.5/4] state type-based restrictions on the character codes of octal and hexadecimal escapes, based on the (possibly absent) prefix of the character constant or string literal. But it seems reasonable that the same range restrictions should also apply to universal character names; some experiments with the C compiler on Mac confirms this.

Definitions and Theorems

Function: valid-univ-char-name

(defun valid-univ-char-name (ucn max)
 (declare (xargs :guard (and (univ-char-name-p ucn)
                             (natp max))))
 (let ((__function__ 'valid-univ-char-name))
  (declare (ignorable __function__))
  (b*
   (((reterr) 0)
    (code
     (univ-char-name-case
        ucn
        :locase-u
        (str::hex-digit-chars-value (list (hex-quad->1st ucn.quad)
                                          (hex-quad->2nd ucn.quad)
                                          (hex-quad->3rd ucn.quad)
                                          (hex-quad->4th ucn.quad)))
        :upcase-u (str::hex-digit-chars-value
                       (list (hex-quad->1st ucn.quad1)
                             (hex-quad->2nd ucn.quad1)
                             (hex-quad->3rd ucn.quad1)
                             (hex-quad->4th ucn.quad1)
                             (hex-quad->1st ucn.quad2)
                             (hex-quad->2nd ucn.quad2)
                             (hex-quad->3rd ucn.quad2)
                             (hex-quad->4th ucn.quad2)))))
    ((when (and (< code 160)
                (not (= code 36))
                (not (= code 64))
                (not (= code 96))))
     (reterr
      (msg
       "The universal character name ~x0 ~
                      has a code ~x1 that is below A0h ~
                      but is not 24h or 40h or 60h."
       (univ-char-name-fix ucn)
       code)))
    ((when (and (<= 55296 code) (<= code 57343)))
     (reterr
      (msg
       "The universal character name ~x0 ~
                      has a code ~x1 between D800h and DFFFh."
       (univ-char-name-fix ucn)
       code)))
    ((when (> code (nfix max)))
     (reterr
      (msg
       "The universal character name ~x0 ~
                      has a code ~x1 above ~x2."
       (univ-char-name-fix ucn)
       code (nfix max)))))
   (retok code))))

Theorem: natp-of-valid-univ-char-name.code

(defthm natp-of-valid-univ-char-name.code
  (b* (((mv acl2::?erp ?code)
        (valid-univ-char-name ucn max)))
    (natp code))
  :rule-classes :rewrite)

Theorem: valid-univ-char-name-of-univ-char-name-fix-ucn

(defthm valid-univ-char-name-of-univ-char-name-fix-ucn
  (equal (valid-univ-char-name (univ-char-name-fix ucn)
                               max)
         (valid-univ-char-name ucn max)))

Theorem: valid-univ-char-name-univ-char-name-equiv-congruence-on-ucn

(defthm valid-univ-char-name-univ-char-name-equiv-congruence-on-ucn
  (implies (univ-char-name-equiv ucn ucn-equiv)
           (equal (valid-univ-char-name ucn max)
                  (valid-univ-char-name ucn-equiv max)))
  :rule-classes :congruence)

Theorem: valid-univ-char-name-of-nfix-max

(defthm valid-univ-char-name-of-nfix-max
  (equal (valid-univ-char-name ucn (nfix max))
         (valid-univ-char-name ucn max)))

Theorem: valid-univ-char-name-nat-equiv-congruence-on-max

(defthm valid-univ-char-name-nat-equiv-congruence-on-max
  (implies (acl2::nat-equiv max max-equiv)
           (equal (valid-univ-char-name ucn max)
                  (valid-univ-char-name ucn max-equiv)))
  :rule-classes :congruence)