		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lex-1*6-hexadecimal-digit

Lex a 1*6hexadecimal-digit.

Signature
(lex-1*6-hexadecimal-digit input) → (mv trees rest-input)
Arguments: input — Guard (nat-listp input).
Returns: trees — Type (abnf::tree-list-resultp trees).; rest-input — Type (nat-listp rest-input).

This is used to lex Unicode escape sequences. We just lex any number of hexadecimal digits, and we ensure that we find between one and six. If we read none, it is clearly a failure. If we read more than six, there is no point in just considering the first six and continuing the lexing, because the six hexadecimal digits must be followed by a closing brace: so, if instead there is a seventh hexadecimal digit, this cannot be part of a valid Unicode character escape.

Definitions and Theorems

Function: lex-1*6-hexadecimal-digit

(defun lex-1*6-hexadecimal-digit (input)
  (declare (xargs :guard (nat-listp input)))
  (let ((__function__ 'lex-1*6-hexadecimal-digit))
    (declare (ignorable __function__))
    (b* (((mv trees input1)
          (lex-*-hexadecimal-digit input))
         ((unless (and (<= 1 (len trees))
                       (<= (len trees) 6)))
          (mv (reserrf (list :found trees))
              (nat-list-fix input))))
      (mv trees input1))))

Theorem: tree-list-resultp-of-lex-1*6-hexadecimal-digit.trees

(defthm tree-list-resultp-of-lex-1*6-hexadecimal-digit.trees
  (b* (((mv ?trees ?rest-input)
        (lex-1*6-hexadecimal-digit input)))
    (abnf::tree-list-resultp trees))
  :rule-classes :rewrite)

Theorem: nat-listp-of-lex-1*6-hexadecimal-digit.rest-input

(defthm nat-listp-of-lex-1*6-hexadecimal-digit.rest-input
  (b* (((mv ?trees ?rest-input)
        (lex-1*6-hexadecimal-digit input)))
    (nat-listp rest-input))
  :rule-classes :rewrite)

Theorem: len-of-lex-1*6-hexadecimal-digit-<=

(defthm len-of-lex-1*6-hexadecimal-digit-<=
  (b* (((mv ?trees ?rest-input)
        (lex-1*6-hexadecimal-digit input)))
    (<= (len rest-input) (len input)))
  :rule-classes :linear)

Theorem: lex-1*6-hexadecimal-digit-of-nat-list-fix-input

(defthm lex-1*6-hexadecimal-digit-of-nat-list-fix-input
  (equal (lex-1*6-hexadecimal-digit (nat-list-fix input))
         (lex-1*6-hexadecimal-digit input)))

Theorem: lex-1*6-hexadecimal-digit-nat-list-equiv-congruence-on-input

(defthm lex-1*6-hexadecimal-digit-nat-list-equiv-congruence-on-input
  (implies (acl2::nat-list-equiv input input-equiv)
           (equal (lex-1*6-hexadecimal-digit input)
                  (lex-1*6-hexadecimal-digit input-equiv)))
  :rule-classes :congruence)