		Search-engine friendly clone of the ACL2 documentation.

Atj-library-extensions

Atj-string-ascii-java-identifier-p

Check if an ACL2 string is a valid ASCII Java identifier.

Signature
(atj-string-ascii-java-identifier-p string) → yes/no
Arguments: string — Guard (stringp string).
Returns: yes/no — Type (booleanp yes/no).

The string must be non-empty, start with a letter or underscore or dollar sign, and continue with zero or more letters, digits, underscores, and dollar signs. It must also be different from Java keywords and from the boolean and null literals.

Here for simplicity we disallow ignorable characters. See the formalization of identifiers for more details. It is expected that (perhaps an extension of) that formalization will replace this function here, but for now this function is adequate to ATJ's needs.

Definitions and Theorems

Function: atj-string-ascii-java-identifier-p

(defun atj-string-ascii-java-identifier-p (string)
 (declare (xargs :guard (stringp string)))
 (let ((__function__ 'atj-string-ascii-java-identifier-p))
  (declare (ignorable __function__))
  (and
   (not (member-equal string *reserved-keywords*))
   (not (member-equal string *boolean-literals*))
   (not (equal string *null-literal*))
   (b* ((chars (explode string)))
    (and
       (consp chars)
       (str::letter/uscore/dollar-char-p (car chars))
       (str::letter/digit/uscore/dollar-charlist-p (cdr chars)))))))

Theorem: booleanp-of-atj-string-ascii-java-identifier-p

(defthm booleanp-of-atj-string-ascii-java-identifier-p
  (b* ((yes/no (atj-string-ascii-java-identifier-p string)))
    (booleanp yes/no))
  :rule-classes :rewrite)