		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lex-numeric-literal

Lex an atomic-literal that is a numeric literal.

Signature
(lex-numeric-literal 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).

More precisely, lex an integer-literal, field-literal, product-group-literal, or scalar-literal. Return a numeric-literal tree that wraps that tree if successful.

It is convenient to have this lexing function, called when lexing a token, since numeric literals all start with a decimal digit, and also share some structure that may enable future optimizations. Currently this lexing function is not very optimized, as it tries each kind of literal independently.

Definitions and Theorems

Function: lex-numeric-literal

(defun lex-numeric-literal (input)
  (declare (xargs :guard (nat-listp input)))
  (let ((__function__ 'lex-numeric-literal))
    (declare (ignorable __function__))
    (b* (((mv tree input)
          (b* (((mv tree input1)
                (lex-integer-literal input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (lex-field-literal input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (lex-product-group-literal input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (lex-scalar-literal input))
               ((when (not (reserrp tree)))
                (mv tree input1)))
            (mv (reserrf :no-numeric-literal)
                (nat-list-fix input))))
         ((when (reserrp tree)) (mv tree input)))
      (mv (abnf-tree-wrap tree "numeric-literal")
          input))))

Theorem: tree-resultp-of-lex-numeric-literal.tree

(defthm tree-resultp-of-lex-numeric-literal.tree
  (b* (((mv ?tree ?rest-input)
        (lex-numeric-literal input)))
    (abnf::tree-resultp tree))
  :rule-classes :rewrite)

Theorem: nat-listp-of-lex-numeric-literal.rest-input

(defthm nat-listp-of-lex-numeric-literal.rest-input
  (b* (((mv ?tree ?rest-input)
        (lex-numeric-literal input)))
    (nat-listp rest-input))
  :rule-classes :rewrite)

Theorem: len-of-lex-numeric-literal-<=

(defthm len-of-lex-numeric-literal-<=
  (b* (((mv ?tree ?rest-input)
        (lex-numeric-literal input)))
    (<= (len rest-input) (len input)))
  :rule-classes :linear)

Theorem: len-of-lex-numeric-literal-<

(defthm len-of-lex-numeric-literal-<
  (b* (((mv ?tree ?rest-input)
        (lex-numeric-literal input)))
    (implies (not (reserrp tree))
             (< (len rest-input) (len input))))
  :rule-classes :linear)

Theorem: lex-numeric-literal-of-nat-list-fix-input

(defthm lex-numeric-literal-of-nat-list-fix-input
  (equal (lex-numeric-literal (nat-list-fix input))
         (lex-numeric-literal input)))

Theorem: lex-numeric-literal-nat-list-equiv-congruence-on-input

(defthm lex-numeric-literal-nat-list-equiv-congruence-on-input
  (implies (acl2::nat-list-equiv input input-equiv)
           (equal (lex-numeric-literal input)
                  (lex-numeric-literal input-equiv)))
  :rule-classes :congruence)