|
|
|---|
|
|
|
|---|
Check if an ASCII character is ignorable in identifiers.
[JLS14:3.8] introduces the notion of `ignorable' character in identifiers:
two identifiers are considered `equal' when,
after ignoring (i.e. removing) the ignorable characters,
the two identifiers are the same (i.e. same characters in the same order).
[JLS14:3.8] defines this notion in terms of
the API method
Running OpenJDK 14's implementation of this API method
on all the ASCII codes (i.e. the integers from 0 to 127),
reveals that the ignorable ASCII characters are the ones with the codes
0 to 8, 14 to 27, and 127, and no others.
Ideally, this should be confirmed with the Unicode standard,
in regard to the
Function:
(defun ascii-identifier-ignore-p (char) (declare (xargs :guard (asciip char))) (let ((__function__ 'ascii-identifier-ignore-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 127)))))
Theorem:
(defthm booleanp-of-ascii-identifier-ignore-p (b* ((yes/no (ascii-identifier-ignore-p char))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm ascii-identifier-ignore-p-of-ascii-fix-char (equal (ascii-identifier-ignore-p (ascii-fix char)) (ascii-identifier-ignore-p char)))
Theorem:
(defthm ascii-identifier-ignore-p-ascii-equiv-congruence-on-char (implies (ascii-equiv char char-equiv) (equal (ascii-identifier-ignore-p char) (ascii-identifier-ignore-p char-equiv))) :rule-classes :congruence)