		Search-engine friendly clone of the ACL2 documentation.

Lex-identifiers

Vl-lex-system-identifier

Try to match a system identifier (or some other special token like $ or $root.

Signature
(vl-lex-system-identifier echars dollarops) → (mv token/nil remainder)
Arguments: echars — The characters we're lexing.
Guard (vl-echarlist-p echars).; dollarops — Any special $ tokens.
Guard (vl-plaintoken-alistp dollarops).

The order here is subtle. We check for a hit in dollarops first, before even checking if there are any characters at all in the tail, because $ is a valid token with special meaning in SystemVerilog, but is just invalid in Verilog-2005.

Definitions and Theorems

Function: vl-lex-system-identifier

(defun vl-lex-system-identifier (echars dollarops)
  (declare (xargs :guard (and (vl-echarlist-p echars)
                              (vl-plaintoken-alistp dollarops))))
  (let ((__function__ 'vl-lex-system-identifier))
    (declare (ignorable __function__))
    (b* (((unless (and (consp echars)
                       (eql (vl-echar->char (car echars))
                            #\$)))
          (mv nil echars))
         ((mv tail remainder)
          (vl-read-while-simple-id-tail (cdr echars)))
         (etext (cons (car echars) tail))
         (name (hons-copy (vl-echarlist->string etext)))
         (look (hons-assoc-equal name dollarops))
         ((when look)
          (mv (make-vl-plaintoken :type (cdr look)
                                  :etext etext)
              remainder))
         ((unless tail) (mv nil echars)))
      (mv (make-vl-sysidtoken :etext etext
                              :name name)
          remainder))))

Subtopics

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