		Search-engine friendly clone of the ACL2 documentation.

Lexer

Vl-lex

Top level lexing function.

Signature
(vl-lex echars &key warnings config) → (mv successp tokens warnings)
Arguments: echars — The extended-characters to tokenize.
Guard (vl-echarlist-p echars).; warnings — A warnings accumulator to extend with any warnings, which are mainly about overflows or potential incompatibilities ~ involving integer literals.
Guard (vl-warninglist-p warnings).; config — Options about which keywords and operators to accept, i.e., for implementing different Verilog editions.
Guard (vl-loadconfig-p config).
Returns: successp — Did we successfully tokenize the input? Note that even on success there may be some warnings.
Type (booleanp successp).; tokens — The resulting tokens, including any comment or whitespace tokens.
Type (vl-tokenlist-p tokens), given (force (vl-echarlist-p echars)).; warnings — Extended warnings accumulator.
Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-lex-fn

(defun vl-lex-fn (echars warnings config)
  (declare (xargs :guard (and (vl-echarlist-p echars)
                              (vl-warninglist-p warnings)
                              (vl-loadconfig-p config))))
  (let ((__function__ 'vl-lex))
    (declare (ignorable __function__))
    (b* ((st (vl-lexstate-init config))
         ((mv okp tokens warnings)
          (vl-lex-main echars t st warnings)))
      (mv okp tokens warnings))))

Theorem: booleanp-of-vl-lex.successp

(defthm booleanp-of-vl-lex.successp
  (b* (((mv ?successp ?tokens ?warnings)
        (vl-lex-fn echars warnings config)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-tokenlist-p-of-vl-lex.tokens

(defthm vl-tokenlist-p-of-vl-lex.tokens
  (implies (force (vl-echarlist-p echars))
           (b* (((mv ?successp ?tokens ?warnings)
                 (vl-lex-fn echars warnings config)))
             (vl-tokenlist-p tokens)))
  :rule-classes :rewrite)

Theorem: vl-warninglist-p-of-vl-lex.warnings

(defthm vl-warninglist-p-of-vl-lex.warnings
  (b* (((mv ?successp ?tokens ?warnings)
        (vl-lex-fn echars warnings config)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-tokenlist->etext-of-vl-lex

(defthm vl-tokenlist->etext-of-vl-lex
  (b* (((mv okp tokens ?warnings)
        (vl-lex echars
                :warnings warnings
                :config config)))
    (implies (and okp (force (vl-echarlist-p echars))
                  (force (true-listp echars)))
             (equal (vl-tokenlist->etext tokens)
                    echars))))

Subtopics

Vl-lex-token1: Try to parse a single token at the front of echars.
Vl-lex-1step-or-number: Match any integral_number or 1step.
Vl-lex-timescale: Try to read a `timescale directive and turn it into a whitespace token.
Vl-lex-plain: Try to match a particular string literal corresponding to some plain token.
Vl-lex-plain-alist
Vl-lex-token
Vl-lex-main
Vl-lex-main-exec: Tail recursive implementation.