		Search-engine friendly clone of the ACL2 documentation.

Vl-lex-simple-identifier-or-keyword

Match either a keyword or an ordinary, simple identifier.

Signature
(vl-lex-simple-identifier-or-keyword echars table) → (mv token/nil remainder)
Arguments: echars — The characters we're lexing.
Guard (vl-echarlist-p echars).; table — The table of keywords we're currently using.
Guard (vl-keyword-table-p table).

Definitions and Theorems

Function: vl-lex-simple-identifier-or-keyword

(defun vl-lex-simple-identifier-or-keyword (echars table)
  (declare (xargs :guard (and (vl-echarlist-p echars)
                              (vl-keyword-table-p table))))
  (let ((__function__ 'vl-lex-simple-identifier-or-keyword))
    (declare (ignorable __function__))
    (b* (((unless (and (consp echars)
                       (vl-simple-id-head-echar-p (car echars))))
          (mv nil echars))
         ((mv prefix remainder)
          (vl-read-simple-identifier echars))
         (str (hons-copy (vl-echarlist->string prefix)))
         (lookup (vl-keyword-lookup str table))
         (token (if lookup (make-vl-plaintoken :etext prefix
                                               :type lookup)
                  (make-vl-idtoken :etext prefix
                                   :name str))))
      (mv token remainder))))

Subtopics

Vl-lex-simple-identifier-or-keyword-token/remainder-thms: Token and remainder theorems for vl-lex-simple-identifier-or-keyword, automatically generated by def-token/remainder-thms.