		Search-engine friendly clone of the ACL2 documentation.

Static-identifier-checking

Check-identifier

Check if an identifier is well-formed.

Signature
(check-identifier iden) → _
Arguments: iden — Guard (identifierp iden).
Returns: _ — Type (reserr-optionp _).

It must consists of only letters (lowercase and uppercase), (decimal) digits, underscores, and dollars. It must be non-empty and not start with a digit.

We may move these requirements into an invariant of identifier, but for now we state them as part of the static semantics.

Definitions and Theorems

Function: check-identifier

(defun check-identifier (iden)
 (declare (xargs :guard (identifierp iden)))
 (let ((__function__ 'check-identifier))
  (declare (ignorable __function__))
  (b* ((chars (acl2::explode (identifier->get iden))))
    (if
      (and (consp chars)
           (str::letter/uscore/dollar-char-p (car chars))
           (str::letter/digit/uscore/dollar-charlist-p (cdr chars)))
      nil
      (reserrf (list :bad-identifier (identifier-fix iden)))))))

Theorem: reserr-optionp-of-check-identifier

(defthm reserr-optionp-of-check-identifier
  (b* ((_ (check-identifier iden)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: check-identifier-of-identifier-fix-iden

(defthm check-identifier-of-identifier-fix-iden
  (equal (check-identifier (identifier-fix iden))
         (check-identifier iden)))

Theorem: check-identifier-identifier-equiv-congruence-on-iden

(defthm check-identifier-identifier-equiv-congruence-on-iden
  (implies (identifier-equiv iden iden-equiv)
           (equal (check-identifier iden)
                  (check-identifier iden-equiv)))
  :rule-classes :congruence)