		Search-engine friendly clone of the ACL2 documentation.

Lexing-and-parsing

Identifier-lexp

Lexing of Identifiers.

Signature
(identifier-lexp tree) → yes/no
Arguments: tree — Guard (abnf::treep tree).
Returns: yes/no — Type (booleanp yes/no).

The ambiguity, mentioned in longest-lexp, deriving from the fact that, grammatically, keywords and boolean literals are also identifiers, and that identifiers may be or start with aleo1, is eliminated by imposing the extra-grammatical requirement that identifiers are not keywords or boolean literals and are not and do not start with aleo1. This is formalized by this predicate, which holds on ((sequences of) sequences of) CSTs that are not, and do not contain any, identifier CSTs whose fringe is the same as the CST of some keyword or boolean literal, or has aleo1 as prefix.

Theorem: return-type-of-identifier-lexp.yes/no

(defthm return-type-of-identifier-lexp.yes/no
  (b* ((?yes/no (identifier-lexp tree)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: return-type-of-identifier-lexp-list.yes/no

(defthm return-type-of-identifier-lexp-list.yes/no
  (b* ((?yes/no (identifier-lexp-list trees)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: return-type-of-identifier-lexp-list-list.yes/no

(defthm return-type-of-identifier-lexp-list-list.yes/no
  (b* ((?yes/no (identifier-lexp-list-list treess)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: identifier-lexp-of-tree-fix-tree

(defthm identifier-lexp-of-tree-fix-tree
  (equal (identifier-lexp (abnf::tree-fix tree))
         (identifier-lexp tree)))

Theorem: identifier-lexp-list-of-tree-list-fix-trees

(defthm identifier-lexp-list-of-tree-list-fix-trees
  (equal (identifier-lexp-list (abnf::tree-list-fix trees))
         (identifier-lexp-list trees)))

Theorem: identifier-lexp-list-list-of-tree-list-list-fix-treess

(defthm identifier-lexp-list-list-of-tree-list-list-fix-treess
  (equal
       (identifier-lexp-list-list (abnf::tree-list-list-fix treess))
       (identifier-lexp-list-list treess)))

Theorem: identifier-lexp-tree-equiv-congruence-on-tree

(defthm identifier-lexp-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv tree tree-equiv)
           (equal (identifier-lexp tree)
                  (identifier-lexp tree-equiv)))
  :rule-classes :congruence)

Theorem: identifier-lexp-list-tree-list-equiv-congruence-on-trees

(defthm identifier-lexp-list-tree-list-equiv-congruence-on-trees
  (implies (abnf::tree-list-equiv trees trees-equiv)
           (equal (identifier-lexp-list trees)
                  (identifier-lexp-list trees-equiv)))
  :rule-classes :congruence)

Theorem: identifier-lexp-list-list-tree-list-list-equiv-congruence-on-treess

(defthm
 identifier-lexp-list-list-tree-list-list-equiv-congruence-on-treess
 (implies (abnf::tree-list-list-equiv treess treess-equiv)
          (equal (identifier-lexp-list-list treess)
                 (identifier-lexp-list-list treess-equiv)))
 :rule-classes :congruence)

Subtopics

Identifier-lexp-list-list
Identifier-lexp-list