		Search-engine friendly clone of the ACL2 documentation.

Ascii-identifiers

Ascii-ident-stringp

Recognize an ACL2 string that is a C ASCII identifier.

Signature
(ascii-ident-stringp x gcc) → yes/no
Arguments: gcc — Guard (booleanp gcc).
Returns: yes/no — Type (booleanp yes/no).

The gcc flag determines whether GCC extensions should be considered or not, since the notion varies slightly, as explained shortly.

For standard C (i.e. no GCC extensions), this notion is the same as the one of portable ASCII identifiers defined in the language formalization; in fact, we use a function defined here as part of the definition here. The notion is that the string must start with a letter or underscore, consists of only letters, digits, and underscores, and be distinct from the standard C keywords.

With GCC extensions, the notion is strenghtened to also exclude the GCC keywords.

Definitions and Theorems

Function: ascii-ident-stringp

(defun ascii-ident-stringp (x gcc)
  (declare (xargs :guard (booleanp gcc)))
  (let ((__function__ 'ascii-ident-stringp))
    (declare (ignorable __function__))
    (and (stringp x)
         (c::paident-char-listp (acl2::explode x))
         (not (member-equal x *keywords*))
         (or (not gcc)
             (not (member-equal x *gcc-keywords*))))))

Theorem: booleanp-of-ascii-ident-stringp

(defthm booleanp-of-ascii-ident-stringp
  (b* ((yes/no (ascii-ident-stringp x gcc)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: ascii-ident-stringp-of-bool-fix-gcc

(defthm ascii-ident-stringp-of-bool-fix-gcc
  (equal (ascii-ident-stringp x (bool-fix gcc))
         (ascii-ident-stringp x gcc)))

Theorem: ascii-ident-stringp-iff-congruence-on-gcc

(defthm ascii-ident-stringp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (ascii-ident-stringp x gcc)
                  (ascii-ident-stringp x gcc-equiv)))
  :rule-classes :congruence)