		Search-engine friendly clone of the ACL2 documentation.

Identifiers

Ascii-identifier-part-p

Check if an ASCII character can be non-starting part of identifiers.

Signature
(ascii-identifier-part-p char) → yes/no
Arguments: char — Guard (asciip char).
Returns: yes/no — Type (booleanp yes/no).

[JLS14:3.8] introduces the notion of `Java letter or digit' as a character that can be used in an identifier, not at the start. [JLS14:3.8] defines this notion in terms of the API method Character.isJavaIdentifierPart(int). [JCAPIS] specifies this method in terms of Unicode notions, and mentions that it includes ignorable characters (see ascii-identifier-ignore-p). [JLS14:3.8] says that a `Java digit' includes the ASCII decimal digits; this, together with the statement made by [JLS14:3.8] about `Java letters' (see ascii-identifier-start-p), implies that `Java letters and digits' include uppercase and lowercase Latin letters, decimal digits, dollar, and underscore.

Running OpenJDK 14's implementation of Character.isJavaIdentifierPart(int) on all the ASCII codes (i.e. the integers from 0 to 127) returns true for the characters with the codes 0 to 8, 14 to 27, 36 (dollar), 48 to 57 (decimal digits), 65 to 90 (uppercase letters), 95 (underscore), 97-122 (lowercase letters), 127, and no others; these are exactly the ASCII characters mentioned by [JLS14:3.8], plus the ignorable ASCII characters (see ascii-identifier-ignore-p). Ideally, this should be confirmed with the Unicode standard.

Definitions and Theorems

Function: ascii-identifier-part-p

(defun ascii-identifier-part-p (char)
  (declare (xargs :guard (asciip char)))
  (let ((__function__ 'ascii-identifier-part-p))
    (declare (ignorable __function__))
    (b* ((char (mbe :logic (ascii-fix char)
                    :exec char)))
      (or (and (<= 0 char) (<= char 8))
          (and (<= 14 char) (<= char 27))
          (= char (char-code #\$))
          (and (<= (char-code #\A) char)
               (<= char (char-code #\Z)))
          (= char (char-code #\_))
          (and (<= (char-code #\a) char)
               (<= char (char-code #\z)))
          (and (<= (char-code #\0) char)
               (<= char (char-code #\9)))
          (= char 127)))))

Theorem: booleanp-of-ascii-identifier-part-p

(defthm booleanp-of-ascii-identifier-part-p
  (b* ((yes/no (ascii-identifier-part-p char)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: ascii-identifier-part-p-of-ascii-fix-char

(defthm ascii-identifier-part-p-of-ascii-fix-char
  (equal (ascii-identifier-part-p (ascii-fix char))
         (ascii-identifier-part-p char)))

Theorem: ascii-identifier-part-p-ascii-equiv-congruence-on-char

(defthm ascii-identifier-part-p-ascii-equiv-congruence-on-char
  (implies (ascii-equiv char char-equiv)
           (equal (ascii-identifier-part-p char)
                  (ascii-identifier-part-p char-equiv)))
  :rule-classes :congruence)