		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Uniescape-candidate-valid-p

Check if a candidate Unicode escape is valid.

Signature
(uniescape-candidate-valid-p pos unicodes) → yes/no
Arguments: pos — Guard (natp pos).; unicodes — Guard (unicode-listp unicodes).
Returns: yes/no — Type (booleanp yes/no).

That is, check if the candidate is an actual Unicode escape. This is the case when there are four hexadecimal digits just after the last `u' letter.

Here we use the fact that the witness of nonzero-uletters-after-p returns the total number n of `u' letters: the hexadecimal digits must be at positions (+ pos n 1), (+ pos n 2), (+ pos n 3), and (+ pos n 4).

Definitions and Theorems

Function: uniescape-candidate-valid-p

(defun uniescape-candidate-valid-p (pos unicodes)
 (declare (xargs :guard (and (natp pos)
                             (unicode-listp unicodes))))
 (declare (xargs :guard (and (< pos (len unicodes))
                             (uniescape-candidate-p pos unicodes))))
 (b* ((n-uletters (number-of-nonzero-uletters-after pos unicodes))
      (pos-hex (+ pos 1 n-uletters)))
   (and (<= (+ pos-hex 4) (len unicodes))
        (hex-digitp (nth pos-hex unicodes))
        (hex-digitp (nth (+ pos-hex 1) unicodes))
        (hex-digitp (nth (+ pos-hex 2) unicodes))
        (hex-digitp (nth (+ pos-hex 3) unicodes)))))

Theorem: booleanp-of-uniescape-candidate-valid-p

(defthm booleanp-of-uniescape-candidate-valid-p
  (b* ((yes/no (uniescape-candidate-valid-p pos unicodes)))
    (booleanp yes/no))
  :rule-classes :rewrite)