|
|
|---|
|
|
|
|---|
Check if an ASCII character can start identifiers.
[JLS14:3.8] introduces the notion of `Java letter'
as a character that can be used to start an identifier.
[JLS14:3.8] defines this notion in terms of
the API method
[JLS14:3.8] says that this notion includes the ASCII
uppercase and lowercase Latin letters, as well as dollar and underscore.
Running OpenJDK 14's
implementation of
Function:
(defun ascii-identifier-start-p (char) (declare (xargs :guard (asciip char))) (let ((__function__ 'ascii-identifier-start-p)) (declare (ignorable __function__)) (b* ((char (mbe :logic (ascii-fix char) :exec char))) (or (= char (char-code #\$)) (and (<= (char-code #\A) char) (<= char (char-code #\Z))) (= char (char-code #\_)) (and (<= (char-code #\a) char) (<= char (char-code #\z)))))))
Theorem:
(defthm booleanp-of-ascii-identifier-start-p (b* ((yes/no (ascii-identifier-start-p char))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm ascii-identifier-start-p-of-ascii-fix-char (equal (ascii-identifier-start-p (ascii-fix char)) (ascii-identifier-start-p char)))
Theorem:
(defthm ascii-identifier-start-p-ascii-equiv-congruence-on-char (implies (ascii-equiv char char-equiv) (equal (ascii-identifier-start-p char) (ascii-identifier-start-p char-equiv))) :rule-classes :congruence)