		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lex-symbol

Lex a symbol.

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

It is critical that symbols that are prefixes of other symbols are tried after trying the longer ones, to satisfy the longest lexing requirement.

Definitions and Theorems

Function: lex-symbol

(defun lex-symbol (input)
  (declare (xargs :guard (nat-listp input)))
  (let ((__function__ 'lex-symbol))
    (declare (ignorable __function__))
    (b* (((mv tree input)
          (b* (((mv tree input1)
                (abnf::parse-schars ")group" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "(" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars ")" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "[" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "]" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "{" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "}" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "&&=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "&&" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "||=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "||" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "&=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "&" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "|=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "|" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "^=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "^" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "_" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "?" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "," input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars ";" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars ".." input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "." input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "::" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars ":" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "!=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "!" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "<<=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "<<" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars ">>=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars ">>" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "=>" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "==" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "<=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "<" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars ">=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars ">" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "+=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "+" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "/=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "/" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "%=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "%" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "->" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "-=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "-" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "**=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "**" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "*=" input))
               ((when (not (reserrp tree)))
                (mv tree input1))
               ((mv tree input1)
                (abnf::parse-ichars "*" input))
               ((when (not (reserrp tree)))
                (mv tree input1)))
            (mv (reserrf :no-symbol)
                (nat-list-fix input))))
         ((when (reserrp tree)) (mv tree input)))
      (mv (abnf-tree-wrap tree "symbol")
          input))))

Theorem: tree-resultp-of-lex-symbol.tree

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

Theorem: nat-listp-of-lex-symbol.rest-input

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

Theorem: len-of-lex-symbol-<=

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

Theorem: len-of-lex-symbol-<

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

Theorem: lex-symbol-of-nat-list-fix-input

(defthm lex-symbol-of-nat-list-fix-input
  (equal (lex-symbol (nat-list-fix input))
         (lex-symbol input)))

Theorem: lex-symbol-nat-list-equiv-congruence-on-input

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