		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lex-identifier/keyword/boolean/address

Lex an identifier or a keyword or a boolean-literal or an address-literal.

Signature
(lex-identifier/keyword/boolean/address input) → (mv tree rest-input)
Arguments: input — Guard (nat-listp input).
Returns: tree — Type (abnf::tree-resultp tree).; rest-input — Type (nat-listp rest-input).

Lexically, these are all identifiers, in the sense that they are instances of the identifier rule, on a purely grammatical basis. Thus, we start by lexing a (grammatical) identifier. Then we check whether it is a keyword, in which case we re-classify the ABNF tree as a keyword tree. Otherwise, we check whether it is a boolean literal, in which case we re-classify the ABNF tree as a boolean-literal). Otherwise, we check whether it is an address: in this case, we need to re-lex it, so that we can construct and return an @('address-literal. Otherwise, we return the identifier tree, unless it is or starts with aleo1.

Note that keywords, boolean literals, and address literals are all disjoint.

Definitions and Theorems

Function: lex-identifier/keyword/boolean/address

(defun lex-identifier/keyword/boolean/address (input)
  (declare (xargs :guard (nat-listp input)))
  (let ((__function__ 'lex-identifier/keyword/boolean/address))
    (declare (ignorable __function__))
    (b* (((mv tree input1)
          (lex-identifier input))
         ((when (reserrp tree))
          (mv (reserrf-push tree) input1))
         (nats (abnf::tree->string tree))
         ((unless (unsigned-byte-listp 8 nats))
          (mv (reserrf :impossible) input1))
         (str (nats=>string nats))
         ((when (member-equal str *keywords*))
          (mv (abnf-tree-wrap (abnf::tree-leafterm nats)
                              "keyword")
              input1))
         ((when (member-equal str (list "true" "false")))
          (mv (abnf-tree-wrap (abnf::tree-leafterm nats)
                              "boolean-literal")
              input1))
         ((when (address-string-p str))
          (b* (((mv tree input)
                (lex-address-literal input))
               ((when (reserrp tree))
                (mv (reserrf :impossible) input)))
            (mv tree input)))
         ((when (and (>= (length str) 5)
                     (equal (subseq str 0 5) "aleo1")))
          (mv (reserrf (list :found str))
              input1)))
      (mv tree input1))))

Theorem: tree-resultp-of-lex-identifier/keyword/boolean/address.tree

(defthm tree-resultp-of-lex-identifier/keyword/boolean/address.tree
  (b* (((mv ?tree ?rest-input)
        (lex-identifier/keyword/boolean/address input)))
    (abnf::tree-resultp tree))
  :rule-classes :rewrite)

Theorem: nat-listp-of-lex-identifier/keyword/boolean/address.rest-input

(defthm
     nat-listp-of-lex-identifier/keyword/boolean/address.rest-input
  (b* (((mv ?tree ?rest-input)
        (lex-identifier/keyword/boolean/address input)))
    (nat-listp rest-input))
  :rule-classes :rewrite)

Theorem: len-of-lex-identifier/keyword/boolean/address-<=

(defthm len-of-lex-identifier/keyword/boolean/address-<=
  (b* (((mv ?tree ?rest-input)
        (lex-identifier/keyword/boolean/address input)))
    (<= (len rest-input) (len input)))
  :rule-classes :linear)

Theorem: len-of-lex-identifier/keyword/boolean/address-<

(defthm len-of-lex-identifier/keyword/boolean/address-<
  (b* (((mv ?tree ?rest-input)
        (lex-identifier/keyword/boolean/address input)))
    (implies (not (reserrp tree))
             (< (len rest-input) (len input))))
  :rule-classes :linear)

Theorem: lex-identifier/keyword/boolean/address-of-nat-list-fix-input

(defthm lex-identifier/keyword/boolean/address-of-nat-list-fix-input
  (equal
       (lex-identifier/keyword/boolean/address (nat-list-fix input))
       (lex-identifier/keyword/boolean/address input)))

Theorem: lex-identifier/keyword/boolean/address-nat-list-equiv-congruence-on-input

(defthm
 lex-identifier/keyword/boolean/address-nat-list-equiv-congruence-on-input
 (implies
      (acl2::nat-list-equiv input input-equiv)
      (equal (lex-identifier/keyword/boolean/address input)
             (lex-identifier/keyword/boolean/address input-equiv)))
 :rule-classes :congruence)