		Search-engine friendly clone of the ACL2 documentation.

Identifiers

Midentifier

Fixtype of Java identifiers, for module-related contexts.

These are Java identifiers that exclude all the keywords (non-restricted and restricted, with one exception discussed below), as discussed in the topic on identifiers. Since these are used in module-related contexts, we prepend the name of this recognizer with m. See identifierp for the kind of identifiers used in the other contexts.

We model these Java identifiers as regular Java identifiers (the kinds used in most contexts) that differ from all non-restricted and restricted keywords, with one exception discussed below. Note that this notion of identifiers for module-related contexts is not explicit in the grammar in [JLS14].

The exception mentioned above is that we allow transitive to be an identifier even though it is also a restricted keyword. The reason is that, as noted in [JLS14:3.9], transitive is sometimes tokenized as a keyword, other times as an identifier, based on some surrounding context. Thus, it can be an identifier in a module context. Here we are defining a recognizer that has no information about the surrounding context. Additional predicates can be used to impose restrictions based on the surrounding context.

Definitions and Theorems

Function: midentifierp

(defun midentifierp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'midentifierp))
    (declare (ignorable __function__))
    (and (identifierp x)
         (or (not (restricted-jkeywordp x))
             (equal x (string=>unicode "transitive"))))))

Theorem: booleanp-of-midentifierp

(defthm booleanp-of-midentifierp
  (b* ((yes/no (midentifierp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Function: midentifier-fix

(defun midentifier-fix (x)
  (declare (xargs :guard (midentifierp x)))
  (mbe :logic
       (if (midentifierp x)
           x
         (list (char-code #\$)))
       :exec x))

Theorem: midentifierp-of-midentifier-fix

(defthm midentifierp-of-midentifier-fix
  (b* ((fixed-x (midentifier-fix x)))
    (midentifierp fixed-x))
  :rule-classes :rewrite)

Theorem: midentifier-fix-when-midentifierp

(defthm midentifier-fix-when-midentifierp
  (implies (midentifierp x)
           (equal (midentifier-fix x) x)))

Function: midentifier-equiv$inline

(defun midentifier-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (midentifierp acl2::x)
                              (midentifierp acl2::y))))
  (equal (midentifier-fix acl2::x)
         (midentifier-fix acl2::y)))

Theorem: midentifier-equiv-is-an-equivalence

(defthm midentifier-equiv-is-an-equivalence
  (and (booleanp (midentifier-equiv x y))
       (midentifier-equiv x x)
       (implies (midentifier-equiv x y)
                (midentifier-equiv y x))
       (implies (and (midentifier-equiv x y)
                     (midentifier-equiv y z))
                (midentifier-equiv x z)))
  :rule-classes (:equivalence))

Theorem: midentifier-equiv-implies-equal-midentifier-fix-1

(defthm midentifier-equiv-implies-equal-midentifier-fix-1
  (implies (midentifier-equiv acl2::x x-equiv)
           (equal (midentifier-fix acl2::x)
                  (midentifier-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: midentifier-fix-under-midentifier-equiv

(defthm midentifier-fix-under-midentifier-equiv
  (midentifier-equiv (midentifier-fix acl2::x)
                     acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-midentifier-fix-1-forward-to-midentifier-equiv

(defthm equal-of-midentifier-fix-1-forward-to-midentifier-equiv
  (implies (equal (midentifier-fix acl2::x)
                  acl2::y)
           (midentifier-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-midentifier-fix-2-forward-to-midentifier-equiv

(defthm equal-of-midentifier-fix-2-forward-to-midentifier-equiv
  (implies (equal acl2::x (midentifier-fix acl2::y))
           (midentifier-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: midentifier-equiv-of-midentifier-fix-1-forward

(defthm midentifier-equiv-of-midentifier-fix-1-forward
  (implies (midentifier-equiv (midentifier-fix acl2::x)
                              acl2::y)
           (midentifier-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: midentifier-equiv-of-midentifier-fix-2-forward

(defthm midentifier-equiv-of-midentifier-fix-2-forward
  (implies (midentifier-equiv acl2::x (midentifier-fix acl2::y))
           (midentifier-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)