		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-expressions

Parser for Verilog and SystemVerilog expressions.

This is very complicated because everything about expressions is mutually recursive. Most of the functions here correspond to particular productions in the grammars of the Verilog-2005 or SystemVerilog-2012. A few high-level notes:

The documentation for each function generally describes the grammar productions that are being implemented.
We generally simplify the grammar rules by removing any bare "aliases" such as base_expression ::= expression and attr_name ::= identifier.
We do not try to implement any separation between "ordinary" expressions and "constant" expressions. I think the whole treatment of constant expressions as a syntactic construct is somewhat misguided. It is difficult to imagine truly handling constant expressions at parse time. For instance, in a parameterized module with, say, a width parameter, you really want to resolve expressions like width-1 into constants and treat them as constant indexes. But you can't do this until you know the values for these parameters, which you don't know until you've read all the instances of the module, etc.

Definitions and Theorems

Function: vl-parse-attr-spec-fn

(defun vl-parse-attr-spec-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-attr-spec))
  (declare (ignorable __function__))
  (seq
   tokstream
   (id := (vl-match-token :vl-idtoken))
   (when (vl-is-token? :vl-equalsign)
         (:= (vl-match))
         (expr := (vl-parse-expression)))
   (when
     (and expr (vl-expr-has-any-atts-p expr))
     (return-raw (vl-parse-error "Nested attributes are illegal.")))
   (return (list (cons (vl-idtoken->name id) expr))))))

Function: vl-parse-attribute-instance-aux-fn

(defun vl-parse-attribute-instance-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-attribute-instance-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-attr-spec))
         (when (vl-is-token? :vl-comma)
               (:= (vl-match))
               (rest := (vl-parse-attribute-instance-aux)))
         (return (append first rest)))))

Function: vl-parse-attribute-instance-fn

(defun vl-parse-attribute-instance-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-attribute-instance))
    (declare (ignorable __function__))
    (seq tokstream
         (:= (vl-match-token :vl-beginattr))
         (data := (vl-parse-attribute-instance-aux))
         (:= (vl-match-token :vl-endattr))
         (return data))))

Function: vl-parse-0+-attribute-instances-aux-fn

(defun vl-parse-0+-attribute-instances-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-0+-attribute-instances-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (when (not (vl-is-token? :vl-beginattr))
               (return nil))
         (first :s= (vl-parse-attribute-instance))
         (rest := (vl-parse-0+-attribute-instances-aux))
         (return (append first rest)))))

Function: vl-parse-0+-attribute-instances-fn

(defun vl-parse-0+-attribute-instances-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-0+-attribute-instances))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when (not (vl-is-token? :vl-beginattr))
         (return nil))
   (loc := (vl-current-loc))
   (original-atts := (vl-parse-0+-attribute-instances-aux))
   (return-raw
    (b*
     ((atts (fast-alist-free (hons-shrink-alist (rev original-atts)
                                                nil)))
      ((when (same-lengthp atts original-atts))
       (mv nil atts tokstream))
      (w
       (make-vl-warning
        :type :vl-warn-shadowed-atts
        :msg
        "~l0: Found multiple occurrences of ~&1 in ~
                          attributes.  Later occurrences take precedence."
        :args (list loc
                    (duplicated-members (alist-keys original-atts)))
        :fatalp nil
        :fn __function__))
      (tokstream (vl-tokstream-add-warning w)))
     (mv nil atts tokstream))))))

Function: vl-parse-1+-expressions-separated-by-commas-fn

(defun vl-parse-1+-expressions-separated-by-commas-fn
       (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-1+-expressions-separated-by-commas))
  (declare (ignorable __function__))
  (seq
      tokstream
      (first :s= (vl-parse-expression))
      (when (vl-is-token? :vl-comma)
            (:= (vl-match))
            (rest := (vl-parse-1+-expressions-separated-by-commas)))
      (return (cons first rest)))))

Function: vl-parse-1+-keyval-expression-pairs-fn

(defun vl-parse-1+-keyval-expression-pairs-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-1+-keyval-expression-pairs))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-expression))
         (:= (vl-match-token :vl-colon))
         (second :s= (vl-parse-expression))
         (when (vl-is-token? :vl-comma)
               (:= (vl-match))
               (rest := (vl-parse-1+-keyval-expression-pairs)))
         (return (cons (make-vl-nonatom :op :vl-keyvalue
                                        :args (list first second))
                       rest)))))

Function: vl-parse-system-function-call-fn

(defun vl-parse-system-function-call-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-system-function-call))
  (declare (ignorable __function__))
  (seq
   tokstream
   (fn := (vl-match-token :vl-sysidtoken))
   (when (vl-is-token? :vl-lparen)
         (:= (vl-match))
         (args := (vl-parse-1+-expressions-separated-by-commas))
         (:= (vl-match-token :vl-rparen)))
   (return
     (let
       ((fname (make-vl-sysfunname :name (vl-sysidtoken->name fn))))
       (make-vl-nonatom :op :vl-syscall
                        :args (cons (make-vl-atom :guts fname)
                                    args)))))))

Function: vl-parse-mintypmax-expression-fn

(defun vl-parse-mintypmax-expression-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-mintypmax-expression))
  (declare (ignorable __function__))
  (seq tokstream
       (min :s= (vl-parse-expression))
       (when (vl-is-token? :vl-colon)
             (:= (vl-match))
             (typ :s= (vl-parse-expression))
             (:= (vl-match-token :vl-colon))
             (max := (vl-parse-expression))
             (return (make-vl-nonatom :op :vl-mintypmax
                                      :args (list min typ max))))
       (when (eq (vl-loadconfig->edition config)
                 :verilog-2005)
             (return min))
       (op := (vl-parse-op 2
                           '((:vl-equalsign . :vl-binary-assign)
                             (:vl-pluseq . :vl-binary-plusassign)
                             (:vl-minuseq . :vl-binary-minusassign)
                             (:vl-timeseq . :vl-binary-timesassign)
                             (:vl-diveq . :vl-binary-divassign)
                             (:vl-remeq . :vl-binary-remassign)
                             (:vl-andeq . :vl-binary-andassign)
                             (:vl-oreq . :vl-binary-orassign)
                             (:vl-xoreq . :vl-binary-xorassign)
                             (:vl-shleq . :vl-binary-shlassign)
                             (:vl-shreq . :vl-binary-shrassign)
                             (:vl-ashleq . :vl-binary-ashlassign)
                             (:vl-ashreq . :vl-binary-ashrassign))))
       (unless op (return min))
       (rhs := (vl-parse-expression))
       (return (make-vl-nonatom :op op
                                :args (list min rhs))))))

Function: vl-parse-range-expression-fn

(defun vl-parse-range-expression-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-range-expression))
  (declare (ignorable __function__))
  (seq
   tokstream (e1 :s= (vl-parse-expression))
   (unless
       (vl-is-some-token? '(:vl-colon :vl-pluscolon :vl-minuscolon))
       (return (vl-erange :vl-index e1 e1)))
   (sep := (vl-match))
   (e2 := (vl-parse-expression))
   (return (vl-erange (vl-token->type sep)
                      e1 e2)))))

Function: vl-parse-concatenation-fn

(defun vl-parse-concatenation-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-concatenation))
    (declare (ignorable __function__))
    (seq tokstream
         (:= (vl-match-token :vl-lcurly))
         (args := (vl-parse-1+-expressions-separated-by-commas))
         (:= (vl-match-token :vl-rcurly))
         (return (make-vl-nonatom :op :vl-concat
                                  :args args)))))

Function: vl-parse-stream-expression-fn

(defun vl-parse-stream-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-stream-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (expr :s= (vl-parse-expression))
         (unless (vl-is-token? :vl-kwd-with)
                 (return expr))
         (:= (vl-match))
         (:= (vl-match-token :vl-lbrack))
         (range := (vl-parse-range-expression))
         (:= (vl-match-token :vl-rbrack))
         (return (vl-build-range-select-with expr range)))))

Function: vl-parse-1+-stream-expressions-separated-by-commas-fn

(defun vl-parse-1+-stream-expressions-separated-by-commas-fn
       (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__
            'vl-parse-1+-stream-expressions-separated-by-commas))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-stream-expression))
   (when
     (vl-is-token? :vl-comma)
     (:= (vl-match))
     (rest := (vl-parse-1+-stream-expressions-separated-by-commas)))
   (return (cons first rest)))))

Function: vl-parse-stream-concatenation-fn

(defun vl-parse-stream-concatenation-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-stream-concatenation))
  (declare (ignorable __function__))
  (seq
      tokstream
      (:= (vl-match-token :vl-lcurly))
      (args := (vl-parse-1+-stream-expressions-separated-by-commas))
      (:= (vl-match-token :vl-rcurly))
      (return args))))

Function: vl-parse-simple-type-fn

(defun vl-parse-simple-type-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-simple-type))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when
    (vl-is-token? :vl-kwd-local)
    (:= (vl-match))
    (:= (vl-match-token :vl-scope))
    (tail := (vl-match-token :vl-idtoken))
    (return
     (make-vl-nonatom
      :op :vl-scope
      :args
      (list
       (make-vl-atom :guts (make-vl-keyguts :type :vl-local))
       (make-vl-atom
         :guts (make-vl-hidpiece :name (vl-idtoken->name tail)))))))
   (when
    (vl-is-token? :vl-$unit)
    (:= (vl-match))
    (tail := (vl-parse-pva-tail))
    (return
     (make-vl-nonatom
        :op :vl-scope
        :args
        (list (make-vl-atom :guts (make-vl-keyguts :type :vl-$unit))
              tail))))
   (unless (vl-is-token? :vl-idtoken)
           (return-raw (vl-parse-very-simple-type)))
   (when
     (vl-lookahead-is-token? :vl-pound (cdr (vl-tokstream->tokens)))
     (:= (vl-match))
     (:= (vl-parse-parameter-value-assignment-hack))
     (return-raw (vl-parse-error "Implement PVAs.")))
   (when
    (vl-lookahead-is-token? :vl-scope (cdr (vl-tokstream->tokens)))
    (head := (vl-match))
    (tail := (vl-parse-pva-tail))
    (return
     (make-vl-nonatom
      :op :vl-scope
      :args
      (list
        (make-vl-atom
             :guts (make-vl-hidpiece :name (vl-idtoken->name head)))
        tail))))
   (id := (vl-parse-hierarchical-identifier nil))
   (when (and (vl-idexpr-p id)
              (not (vl-parsestate-is-user-defined-type-p
                        (vl-idexpr->name id)
                        (vl-tokstream->pstate))))
         (return-raw (vl-parse-error (cat "Not a known type: "
                                          (vl-idexpr->name id)))))
   (return id))))

Function: vl-parse-slice-size-fn

(defun vl-parse-slice-size-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-slice-size))
    (declare (ignorable __function__))
    (b* ((backup (vl-tokstream-save))
         ((mv err expr tokstream)
          (vl-parse-simple-type))
         ((unless err) (mv err expr tokstream))
         (tokstream (vl-tokstream-restore backup)))
      (vl-parse-expression))))

Function: vl-parse-any-sort-of-concatenation-fn

(defun vl-parse-any-sort-of-concatenation-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-any-sort-of-concatenation))
  (declare (ignorable __function__))
  (seq
   tokstream
   (:= (vl-match-token :vl-lcurly))
   (when
    (and (vl-is-token? :vl-rcurly)
         (not (eq (vl-loadconfig->edition config)
                  :verilog-2005)))
    (:= (vl-match))
    (return
       (make-vl-atom :guts (make-vl-keyguts :type :vl-emptyqueue))))
   (when (and (vl-is-some-token? '(:vl-shl :vl-shr))
              (not (eq (vl-loadconfig->edition config)
                       :verilog-2005)))
         (op := (vl-match))
         (unless (vl-is-token? :vl-lcurly)
                 (slicesize :s= (vl-parse-slice-size)))
         (args := (vl-parse-stream-concatenation))
         (:= (vl-match-token :vl-rcurly))
         (return (b* ((dir (vl-token->type op))
                      ((unless slicesize)
                       (make-vl-nonatom :op
                                        (if (eq dir :vl-shl)
                                            :vl-stream-left
                                          :vl-stream-right)
                                        :args args)))
                   (make-vl-nonatom :op
                                    (if (eq dir :vl-shl)
                                        :vl-stream-left-sized
                                      :vl-stream-right-sized)
                                    :args (cons slicesize args)))))
   (e1 :s= (vl-parse-expression))
   (when (vl-is-token? :vl-lcurly)
         (concat := (vl-parse-concatenation))
         (:= (vl-match-token :vl-rcurly))
         (return (make-vl-nonatom :op :vl-multiconcat
                                  :args (list e1 concat))))
   (when (vl-is-token? :vl-comma)
         (:= (vl-match))
         (rest := (vl-parse-1+-expressions-separated-by-commas))
         (:= (vl-match-token :vl-rcurly))
         (return (make-vl-nonatom :op :vl-concat
                                  :args (cons e1 rest))))
   (:= (vl-match-token :vl-rcurly))
   (return (make-vl-nonatom :op :vl-concat
                            :args (list e1))))))

Function: vl-parse-hierarchical-identifier-fn

(defun vl-parse-hierarchical-identifier-fn
       (recursivep tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-hierarchical-identifier))
  (declare (ignorable __function__))
  (b* ((sys-p (not (eq (vl-loadconfig->edition config)
                       :verilog-2005))))
   (seq
    tokstream
    (when (and sys-p (not recursivep)
               (vl-is-token? :vl-$root))
          (:= (vl-match))
          (:= (vl-match-token :vl-dot))
          (tail := (vl-parse-hierarchical-identifier t))
          (return (b* ((guts (make-vl-keyguts :type :vl-$root))
                       (head (make-vl-atom :guts guts)))
                    (make-vl-nonatom :op :vl-hid-dot
                                     :args (list head tail)))))
    (id := (vl-match-token :vl-idtoken))
    (when
     (vl-parsestate-is-user-defined-type-p (vl-idtoken->name id)
                                           (vl-tokstream->pstate))
     (return
        (make-vl-atom
             :guts (make-vl-typename :name (vl-idtoken->name id)))))
    (when
     (vl-is-token? :vl-dot)
     (:= (vl-match))
     (tail :s= (vl-parse-hierarchical-identifier t))
     (return
          (b* ((guts (make-vl-hidpiece :name (vl-idtoken->name id)))
               (head (make-vl-atom :guts guts)))
            (make-vl-nonatom :op :vl-hid-dot
                             :args (list head tail)))))
    (unless
     sys-p
     (when (vl-is-token? :vl-lbrack)
           (expr :=
                 (b* ((backup (vl-tokstream-save))
                      ((mv err expr tokstream)
                       (seq tokstream (:= (vl-match))
                            (expr :s= (vl-parse-expression))
                            (:= (vl-match-token :vl-rbrack))
                            (:= (vl-match-token :vl-dot))
                            (return expr)))
                      ((unless err) (mv nil expr tokstream))
                      (tokstream (vl-tokstream-restore backup)))
                   (mv nil nil tokstream))))
     (when
      expr
      (tail := (vl-parse-hierarchical-identifier t))
      (return
        (b*
         ((from-guts (make-vl-hidpiece :name (vl-idtoken->name id)))
          (from-expr (make-vl-atom :guts from-guts))
          (sel-expr (make-vl-nonatom :op :vl-index
                                     :args (list from-expr expr))))
         (make-vl-nonatom :op :vl-hid-dot
                          :args (list sel-expr tail)))))
     (return
      (make-vl-atom
       :guts
       (if recursivep (make-vl-hidpiece :name (vl-idtoken->name id))
         (make-vl-id :name (vl-idtoken->name id))))))
    (when
      (vl-is-token? :vl-lbrack)
      (exprs
           :w=
           (b* ((backup (vl-tokstream-save))
                ((mv err exprs tokstream)
                 (seq tokstream
                      (exprs := (vl-parse-0+-bracketed-expressions))
                      (:= (vl-match-token :vl-dot))
                      (return exprs)))
                ((unless err) (mv nil exprs tokstream))
                (tokstream (vl-tokstream-restore backup)))
             (mv nil nil tokstream))))
    (when
     exprs
     (tail := (vl-parse-hierarchical-identifier t))
     (return
       (b*
         ((from-guts (make-vl-hidpiece :name (vl-idtoken->name id)))
          (from-expr (make-vl-atom :guts from-guts))
          (sel-expr (vl-build-indexing-nest from-expr exprs)))
         (make-vl-nonatom :op :vl-hid-dot
                          :args (list sel-expr tail)))))
    (return
     (make-vl-atom
       :guts
       (if recursivep (make-vl-hidpiece :name (vl-idtoken->name id))
         (make-vl-id :name (vl-idtoken->name id)))))))))

Function: vl-parse-function-call-fn

(defun vl-parse-function-call-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-function-call))
  (declare (ignorable __function__))
  (seq
   tokstream
   (id :s= (vl-parse-hierarchical-identifier nil))
   (atts :w= (vl-parse-0+-attribute-instances))
   (:= (vl-match-token :vl-lparen))
   (args := (vl-parse-1+-expressions-separated-by-commas))
   (:= (vl-match-token :vl-rparen))
   (return
    (cond
     ((and (vl-fast-atom-p id)
           (vl-fast-id-p (vl-atom->guts id)))
      (let
       ((fname
          (make-vl-funname :name (vl-id->name (vl-atom->guts id)))))
       (make-vl-nonatom :op :vl-funcall
                        :atts atts
                        :args (cons (make-vl-atom :guts fname)
                                    args))))
     (t (make-vl-nonatom :op :vl-funcall
                         :atts atts
                         :args (cons id args))))))))

Function: vl-parse-0+-bracketed-expressions-fn

(defun vl-parse-0+-bracketed-expressions-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-0+-bracketed-expressions))
   (declare (ignorable __function__))
   (b*
     (((unless (vl-is-token? :vl-lbrack))
       (mv nil nil tokstream))
      (backup (vl-tokstream-save))
      ((mv err first tokstream)
       (seq tokstream (:= (vl-match))
            (expr := (vl-parse-expression))
            (:= (vl-match-token :vl-rbrack))
            (return expr)))
      ((when (or err (not first)))
       (b* ((tokstream (vl-tokstream-restore backup)))
         (mv nil nil tokstream)))
      ((unless (mbt (< (vl-tokstream-measure)
                       (len (vl-tokstream-backup->tokens backup)))))
       (raise "termination failure")
       (vl-parse-error "termination failure"))
      ((mv erp rest tokstream)
       (vl-parse-0+-bracketed-expressions))
      ((when erp) (mv erp rest tokstream)))
     (mv nil (cons first rest) tokstream))))

Function: vl-parse-indexed-id-2005-fn

(defun vl-parse-indexed-id-2005-fn
       (scopes recursivep tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (declare (xargs :guard (vl-exprlist-p scopes)))
  (let ((__function__ 'vl-parse-indexed-id-2005))
    (declare (ignorable __function__))
    (seq tokstream
         (hid :s= (vl-parse-hierarchical-identifier recursivep))
         (bexprs :w= (vl-parse-0+-bracketed-expressions))
         (when (vl-is-token? :vl-lbrack)
               (:= (vl-match))
               (range := (vl-parse-range-expression))
               (:= (vl-match-token :vl-rbrack)))
         (return (let* ((ans (vl-tack-scopes-onto-hid scopes hid))
                        (ans (vl-build-indexing-nest ans bexprs)))
                   (if range (vl-build-range-select ans range)
                     ans))))))

Function: vl-parse-indexed-id-2012-fn

(defun vl-parse-indexed-id-2012-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-indexed-id-2012))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when
    (vl-is-some-token? '(:vl-kwd-local :vl-$unit))
    (first := (vl-match))
    (:= (vl-match-token :vl-scope))
    (morescopes := (vl-parse-0+-scope-prefixes))
    (return-raw
     (vl-parse-indexed-id-2005
      (cons
       (case
        (vl-token->type first)
        (:vl-kwd-local
             (make-vl-atom :guts (make-vl-keyguts :type :vl-local)))
        (:vl-$unit
            (make-vl-atom :guts (make-vl-keyguts :type :vl-$unit))))
       morescopes)
      t)))
   (scopes := (vl-parse-0+-scope-prefixes))
   (return-raw (vl-parse-indexed-id-2005 scopes (consp scopes))))))

Function: vl-parse-indexed-id-fn

(defun vl-parse-indexed-id-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-indexed-id))
    (declare (ignorable __function__))
    (if (eq (vl-loadconfig->edition config)
            :verilog-2005)
        (vl-parse-indexed-id-2005 nil nil)
      (vl-parse-indexed-id-2012))))

Function: vl-parse-assignment-pattern-fn

(defun vl-parse-assignment-pattern-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (xargs :measure-debug t))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-assignment-pattern))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-expression))
   (when (vl-is-token? :vl-rcurly)
         (:= (vl-match))
         (return (make-vl-nonatom :op :vl-pattern-positional
                                  :args (list first))))
   (when (vl-is-token? :vl-comma)
         (:= (vl-match))
         (rest := (vl-parse-1+-expressions-separated-by-commas))
         (:= (vl-match-token :vl-rcurly))
         (return (make-vl-nonatom :op :vl-pattern-positional
                                  :args (cons first rest))))
   (when
    (vl-is-token? :vl-colon)
    (:= (vl-match))
    (firstval :s= (vl-parse-expression))
    (when
     (vl-is-token? :vl-rcurly)
     (:= (vl-match))
     (return
      (make-vl-nonatom
       :op :vl-pattern-keyvalue
       :args (list (make-vl-nonatom :op :vl-keyvalue
                                    :args (list first firstval))))))
    (:= (vl-match-token :vl-comma))
    (rest := (vl-parse-1+-keyval-expression-pairs))
    (:= (vl-match-token :vl-rcurly))
    (return
      (make-vl-nonatom
           :op :vl-pattern-keyvalue
           :args (cons (make-vl-nonatom :op :vl-keyvalue
                                        :args (list first firstval))
                       rest))))
   (concat := (vl-parse-concatenation))
   (:= (vl-match-token :vl-rcurly))
   (return (make-vl-nonatom :op :vl-pattern-multi
                            :args (list first concat))))))

Function: vl-parse-primary-main-fn

(defun vl-parse-primary-main-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-primary-main))
    (declare (ignorable __function__))
    (b* ((backup (vl-tokstream-save))
         ((mv errmsg? expr tokstream)
          (vl-maybe-parse-base-primary))
         ((when (or errmsg? expr))
          (mv errmsg? expr tokstream))
         (tokstream (vl-tokstream-restore backup))
         (tokens (vl-tokstream->tokens))
         ((when (atom tokens))
          (vl-parse-error "Unexpected EOF."))
         (type (vl-token->type (car tokens)))
         ((when (or (eq type :vl-idtoken)
                    (eq type :vl-$root)
                    (eq type :vl-$unit)
                    (eq type :vl-kwd-local)))
          (b* (((mv err funcall tokstream)
                (vl-parse-function-call))
               ((unless err)
                (mv err funcall tokstream))
               (tokstream (vl-tokstream-restore backup)))
            (vl-parse-indexed-id)))
         ((when (eq type :vl-lcurly))
          (vl-parse-any-sort-of-concatenation))
         ((when (eq type :vl-sysidtoken))
          (vl-parse-system-function-call))
         ((when (eq type :vl-lparen))
          (seq tokstream (:= (vl-match))
               (expr := (vl-parse-mintypmax-expression))
               (:= (vl-match-token :vl-rparen))
               (return (vl-mark-as-explicit-parens expr))))
         ((when (eq type :vl-quote))
          (seq tokstream (:= (vl-match))
               (:= (vl-match-token :vl-lcurly))
               (return-raw (vl-parse-assignment-pattern)))))
      (vl-parse-error "Failed to match a primary expression."))))

Function: vl-parse-primary-cast-fn

(defun vl-parse-primary-cast-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-primary-cast))
  (declare (ignorable __function__))
  (seq
    tokstream
    (primary :s= (vl-parse-primary-main))
    (when (vl-is-token? :vl-quote)
          (:= (vl-match))
          (when (vl-is-token? :vl-lparen)
                (:= (vl-match))
                (arg := (vl-parse-expression))
                (:= (vl-match-token :vl-rparen))
                (return (make-vl-nonatom :op :vl-binary-cast
                                         :args (list primary arg))))
          (:= (vl-match-token :vl-lcurly))
          (pattern := (vl-parse-assignment-pattern))
          (return (make-vl-nonatom :op :vl-pattern-type
                                   :args (list primary pattern))))
    (return primary))))

Function: vl-parse-nonprimary-cast-fn

(defun vl-parse-nonprimary-cast-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-nonprimary-cast))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when
    (vl-is-some-token?
         '(:vl-kwd-signed :vl-kwd-unsigned
                          :vl-kwd-string :vl-kwd-const))
    (type := (vl-match))
    (:= (vl-match-token :vl-quote))
    (:= (vl-match-token :vl-lparen))
    (arg := (vl-parse-expression))
    (:= (vl-match-token :vl-rparen))
    (return
      (b* ((casting-type (case (vl-token->type type)
                               (:vl-kwd-signed :vl-signed)
                               (:vl-kwd-unsigned :vl-unsigned)
                               (:vl-kwd-string :vl-string)
                               (:vl-kwd-const :vl-const)))
           (type-atom
                (make-vl-atom
                     :guts (make-vl-basictype :kind casting-type))))
        (make-vl-nonatom :op :vl-binary-cast
                         :args (list type-atom arg)))))
   (type :s= (vl-parse-simple-type))
   (:= (vl-match-token :vl-quote))
   (:= (vl-match-token :vl-lparen))
   (arg := (vl-parse-expression))
   (:= (vl-match-token :vl-rparen))
   (return (make-vl-nonatom :op :vl-binary-cast
                            :args (list type arg))))))

Function: vl-parse-primary-fn

(defun vl-parse-primary-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-primary))
    (declare (ignorable __function__))
    (b* (((when (eq (vl-loadconfig->edition config)
                    :verilog-2005))
          (vl-parse-primary-main))
         (backup (vl-tokstream-save))
         ((mv errmsg expr tokstream)
          (vl-parse-primary-cast))
         ((unless errmsg)
          (mv errmsg expr tokstream))
         (tokstream (vl-tokstream-restore backup))
         ((mv errmsg expr tokstream)
          (vl-parse-nonprimary-cast))
         ((unless errmsg)
          (mv errmsg expr tokstream))
         (tokstream (vl-tokstream-restore backup)))
      (vl-parse-error "Failed to match a primary expression."))))

Function: vl-parse-unary-expression-fn

(defun vl-parse-unary-expression-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-unary-expression))
  (declare (ignorable __function__))
  (seq
   tokstream
   (op :=
       (if (eq (vl-loadconfig->edition config)
               :verilog-2005)
           (vl-parse-op 1
                        '((:vl-plus . :vl-unary-plus)
                          (:vl-minus . :vl-unary-minus)
                          (:vl-lognot . :vl-unary-lognot)
                          (:vl-bitnot . :vl-unary-bitnot)
                          (:vl-bitand . :vl-unary-bitand)
                          (:vl-nand . :vl-unary-nand)
                          (:vl-bitor . :vl-unary-bitor)
                          (:vl-nor . :vl-unary-nor)
                          (:vl-xor . :vl-unary-xor)
                          (:vl-xnor . :vl-unary-xnor)))
         (vl-parse-op 1
                      '((:vl-plus . :vl-unary-plus)
                        (:vl-minus . :vl-unary-minus)
                        (:vl-lognot . :vl-unary-lognot)
                        (:vl-bitnot . :vl-unary-bitnot)
                        (:vl-bitand . :vl-unary-bitand)
                        (:vl-nand . :vl-unary-nand)
                        (:vl-bitor . :vl-unary-bitor)
                        (:vl-nor . :vl-unary-nor)
                        (:vl-xor . :vl-unary-xor)
                        (:vl-xnor . :vl-unary-xnor)
                        (:vl-plusplus . :vl-unary-preinc)
                        (:vl-minusminus . :vl-unary-predec)))))
   (unless
    op (primary :s= (vl-parse-primary))
    (when (eq (vl-loadconfig->edition config)
              :verilog-2005)
          (return primary))
    (return-raw
     (b*
      ((backup (vl-tokstream-save))
       ((mv err val tokstream)
        (seq
         tokstream
         (atts := (vl-parse-0+-attribute-instances))
         (post
           := (vl-parse-op 1
                           '((:vl-plusplus . :vl-unary-postinc)
                             (:vl-minusminus . :vl-unary-postdec))))
         (unless post (return nil))
         (return (make-vl-nonatom :op post
                                  :atts atts
                                  :args (list primary)))))
       ((when (and (not err) val))
        (mv nil val tokstream))
       (tokstream (vl-tokstream-restore backup)))
      (mv nil primary tokstream))))
   (atts :w= (vl-parse-0+-attribute-instances))
   (primary := (vl-parse-primary))
   (return (make-vl-nonatom :op op
                            :atts atts
                            :args (list primary))))))

Function: vl-parse-power-expression-aux-fn

(defun vl-parse-power-expression-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-power-expression-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-unary-expression))
         (unless (vl-is-token? :vl-power)
                 (return (list first)))
         (:= (vl-match))
         (atts :w= (vl-parse-0+-attribute-instances))
         (tail := (vl-parse-power-expression-aux))
         (return (list* first :vl-binary-power atts tail)))))

Function: vl-parse-power-expression-fn

(defun vl-parse-power-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-power-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-power-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-mult-expression-aux-fn

(defun vl-parse-mult-expression-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-mult-expression-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-power-expression))
         (op := (vl-parse-op 2
                             '((:vl-times . :vl-binary-times)
                               (:vl-div . :vl-binary-div)
                               (:vl-rem . :vl-binary-rem))))
         (unless op (return (list first)))
         (atts :w= (vl-parse-0+-attribute-instances))
         (tail := (vl-parse-mult-expression-aux))
         (return (list* first op atts tail)))))

Function: vl-parse-mult-expression-fn

(defun vl-parse-mult-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-mult-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-mult-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-add-expression-aux-fn

(defun vl-parse-add-expression-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-add-expression-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-mult-expression))
         (op := (vl-parse-op 2
                             '((:vl-plus . :vl-binary-plus)
                               (:vl-minus . :vl-binary-minus))))
         (unless op (return (list first)))
         (atts :w= (vl-parse-0+-attribute-instances))
         (tail := (vl-parse-add-expression-aux))
         (return (list* first op atts tail)))))

Function: vl-parse-add-expression-fn

(defun vl-parse-add-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-add-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-add-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-shift-expression-aux-fn

(defun vl-parse-shift-expression-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-shift-expression-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-add-expression))
         (op := (vl-parse-op 2
                             '((:vl-shl . :vl-binary-shl)
                               (:vl-shr . :vl-binary-shr)
                               (:vl-ashl . :vl-binary-ashl)
                               (:vl-ashr . :vl-binary-ashr))))
         (unless op (return (list first)))
         (atts :w= (vl-parse-0+-attribute-instances))
         (tail := (vl-parse-shift-expression-aux))
         (return (list* first op atts tail)))))

Function: vl-parse-shift-expression-fn

(defun vl-parse-shift-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-shift-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-shift-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-compare-expression-aux-fn

(defun vl-parse-compare-expression-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-compare-expression-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-shift-expression))
         (op := (vl-parse-op 2
                             '((:vl-lt . :vl-binary-lt)
                               (:vl-lte . :vl-binary-lte)
                               (:vl-gt . :vl-binary-gt)
                               (:vl-gte . :vl-binary-gte)
                               (:vl-kwd-inside . :vl-inside))))
         (unless op (return (list first)))
         (unless (eq op :vl-inside)
                 (atts :w= (vl-parse-0+-attribute-instances))
                 (tail := (vl-parse-compare-expression-aux))
                 (return (list* first op atts tail)))
         (:= (vl-match-token :vl-lcurly))
         (args := (vl-parse-1+-open-value-ranges))
         (:= (vl-match-token :vl-rcurly))
         (return (b* ((tail (make-vl-nonatom :op :vl-valuerangelist
                                             :args args)))
                   (list* first op atts (list tail)))))))

Function: vl-parse-compare-expression-fn

(defun vl-parse-compare-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-compare-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-compare-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-open-value-range-fn

(defun vl-parse-open-value-range-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-open-value-range))
    (declare (ignorable __function__))
    (seq tokstream
         (when (vl-is-token? :vl-lbrack)
               (:= (vl-match))
               (a :w= (vl-parse-expression))
               (:= (vl-match-token :vl-colon))
               (b := (vl-parse-expression))
               (:= (vl-match-token :vl-rbrack))
               (return (make-vl-nonatom :op :vl-valuerange
                                        :args (list a b))))
         (return-raw (vl-parse-expression)))))

Function: vl-parse-1+-open-value-ranges-fn

(defun vl-parse-1+-open-value-ranges-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-1+-open-value-ranges))
    (declare (ignorable __function__))
    (seq tokstream
         (range1 :s= (vl-parse-open-value-range))
         (when (vl-is-token? :vl-comma)
               (:= (vl-match))
               (rest := (vl-parse-1+-open-value-ranges)))
         (return (cons range1 rest)))))

Function: vl-parse-equality-expression-aux-fn

(defun vl-parse-equality-expression-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-equality-expression-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-compare-expression))
         (op := (vl-parse-op 2
                             '((:vl-eq . :vl-binary-eq)
                               (:vl-neq . :vl-binary-neq)
                               (:vl-ceq . :vl-binary-ceq)
                               (:vl-cne . :vl-binary-cne)
                               (:vl-wildeq . :vl-binary-wildeq)
                               (:vl-wildneq . :vl-binary-wildneq))))
         (unless op (return (list first)))
         (atts :w= (vl-parse-0+-attribute-instances))
         (tail := (vl-parse-equality-expression-aux))
         (return (list* first op atts tail)))))

Function: vl-parse-equality-expression-fn

(defun vl-parse-equality-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-equality-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-equality-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-bitand-expression-aux-fn

(defun vl-parse-bitand-expression-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-bitand-expression-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-equality-expression))
         (unless (vl-is-token? :vl-bitand)
                 (return (list first)))
         (:= (vl-match))
         (atts :w= (vl-parse-0+-attribute-instances))
         (tail := (vl-parse-bitand-expression-aux))
         (return (list* first :vl-binary-bitand atts tail)))))

Function: vl-parse-bitand-expression-fn

(defun vl-parse-bitand-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-bitand-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-bitand-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-bitxor-expression-aux-fn

(defun vl-parse-bitxor-expression-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-bitxor-expression-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-bitand-expression))
         (op := (vl-parse-op 2
                             '((:vl-xor . :vl-binary-xor)
                               (:vl-xnor . :vl-binary-xnor))))
         (unless op (return (list first)))
         (atts :w= (vl-parse-0+-attribute-instances))
         (tail := (vl-parse-bitxor-expression-aux))
         (return (list* first op atts tail)))))

Function: vl-parse-bitxor-expression-fn

(defun vl-parse-bitxor-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-bitxor-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-bitxor-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-bitor-expression-aux-fn

(defun vl-parse-bitor-expression-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-bitor-expression-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-bitxor-expression))
         (unless (vl-is-token? :vl-bitor)
                 (return (list first)))
         (:= (vl-match))
         (atts :w= (vl-parse-0+-attribute-instances))
         (tail := (vl-parse-bitor-expression-aux))
         (return (list* first :vl-binary-bitor atts tail)))))

Function: vl-parse-bitor-expression-fn

(defun vl-parse-bitor-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-bitor-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-bitor-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-logand-expression-aux-fn

(defun vl-parse-logand-expression-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-logand-expression-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-bitor-expression))
         (unless (vl-is-token? :vl-logand)
                 (return (list first)))
         (:= (vl-match))
         (atts :w= (vl-parse-0+-attribute-instances))
         (tail := (vl-parse-logand-expression-aux))
         (return (list* first :vl-binary-logand atts tail)))))

Function: vl-parse-logand-expression-fn

(defun vl-parse-logand-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-logand-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-logand-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-logor-expression-aux-fn

(defun vl-parse-logor-expression-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-logor-expression-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-logand-expression))
         (unless (vl-is-token? :vl-logor)
                 (return (list first)))
         (:= (vl-match))
         (atts :w= (vl-parse-0+-attribute-instances))
         (tail := (vl-parse-logor-expression-aux))
         (return (list* first :vl-binary-logor atts tail)))))

Function: vl-parse-logor-expression-fn

(defun vl-parse-logor-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-logor-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-logor-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-qmark-expression-fn

(defun vl-parse-qmark-expression-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-qmark-expression))
  (declare (ignorable __function__))
  (seq tokstream
       (first :s= (vl-parse-logor-expression))
       (unless (vl-is-token? :vl-qmark)
               (return first))
       (:= (vl-match))
       (atts :w= (vl-parse-0+-attribute-instances))
       (second :s= (vl-parse-expression))
       (:= (vl-match-token :vl-colon))
       (third := (vl-parse-qmark-expression))
       (return (make-vl-nonatom :op :vl-qmark
                                :atts atts
                                :args (list first second third))))))

Function: vl-parse-impl-expression-fn

(defun vl-parse-impl-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-impl-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-qmark-expression))
         (when (eq (vl-loadconfig->edition config)
                   :verilog-2005)
               (return first))
         (op := (vl-parse-op 2
                             '((:vl-arrow . :vl-implies)
                               (:vl-equiv . :vl-equiv))))
         (unless op (return first))
         (atts :w= (vl-parse-0+-attribute-instances))
         (second :s= (vl-parse-impl-expression))
         (return (make-vl-nonatom :op op
                                  :args (list first second)
                                  :atts atts)))))

Function: vl-parse-expression-fn

(defun vl-parse-expression-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-expression))
  (declare (ignorable __function__))
  (seq
   tokstream
   (unless (and (vl-is-token? :vl-kwd-tagged)
                (not (eq (vl-loadconfig->edition config)
                         :verilog-2005)))
           (expr :s= (vl-parse-impl-expression))
           (return expr))
   (:= (vl-match))
   (id := (vl-match-token :vl-idtoken))
   (return-raw
    (b*
     ((tagexpr
          (make-vl-atom
               :guts (make-vl-tagname :name (vl-idtoken->name id))))
      (backup (vl-tokstream-save))
      ((mv err expr tokstream)
       (seq tokstream
            (expr :s= (vl-parse-expression))
            (return expr)))
      ((when err)
       (b* ((tokstream (vl-tokstream-restore backup)))
         (mv nil
             (make-vl-nonatom :op :vl-tagged
                              :args (list tagexpr))
             tokstream)))
      ((unless (or (vl-fast-atom-p expr)
                   (hons-assoc-equal "VL_EXPLICIT_PARENS"
                                     (vl-nonatom->atts expr))))
       (vl-parse-error
        "Cowardly refusing to support tagged union expression such as
                   'tagged foo 1 + 2' due to unclear precedence.  Workaround:
                   add explicit parens, e.g., write 'tagged foo (1 + 2)'
                   instead."))
      (ans (make-vl-nonatom :op :vl-tagged
                            :args (list tagexpr expr))))
     (mv nil ans tokstream))))))

Subtopics

Vl-parse-parameter-value-assignment-hack: Ostensibly match a parameter_value_assignment within an expression.
Vl-erange-p: An expression range is a temporary internal representation of the ranges for select-like expressions (bit selects, array indexes, part selects, +: and -: expressions.
Vl-mixed-binop-list-p: A list of alternating expressions, operators, and attributes.
Vl-parse-very-simple-type: Match the very simplest simple_type keywords, return an expression.
Vl-mark-as-explicit-parens: Annotate an expression as having explicit parentheses.
Vl-parse-0+-scope-prefixes: Match { id '::' } and return an expression list with all of the ids that have been matched.
Vl-parse-0+-attribute-instances: Top level parser for { attribute_instance } with proper duplicity checking and warnings. Returns a vl-atts-p.
Vl-parse-op: Compatible with seq. Match any of the tokens specified in this alist, and return the corresponding vl-op-p for it.
Vl-parse-hierarchical-identifier: Match a hierarchical_identifier.
Vl-parse-pva-tail: Match { '::' identifier [parameter_value_assignment] } '::' identifier and return an expression.
Vl-parse-expression-top
Vl-parse-any-sort-of-concatenation: Match single, multiple, or streaming concatenations, or empty queues.
Vl-build-indexing-nest: Build the proper expression for successive indexing operations.
Vl-erangetypelist-p: (vl-erangetypelist-p x) recognizes lists where every element satisfies vl-erangetype-p.
Vl-build-range-select-with
Vl-build-range-select
Vl-parse-simple-type: Match simple_type and return an expression.
Vl-expr-has-any-atts-p: Check whether an expression has any attributes.
Vl-left-associate-mixed-binop-list
Vl-tack-scopes-onto-hid
Vl-parse-op-alist-p
Vl-make-guts-from-inttoken
Vl-parse-range-expression: Match range_expression, returning an vl-erange-p.
Vl-parse-slice-size: Match slice_size ::= simple_type | expression and return it as an expression.
Vl-parse-concatenation: Match concatenation ::= '{' expression { ',' expression } '}' and return a single :vl-concat expression.
Vl-parse-stream-expression: Match stream_expression, returning a single expression.
Vl-parse-1+-stream-expressions-separated-by-commas: Match at least one (but perhaps more) stream expressions, return them as an expression list.
Vl-parse-stream-concatenation: Match stream_concatenation, return an expression list.
Vl-parse-primary
Vl-parse-0+-bracketed-expressions: Match { '[' expression '] }'), return an expression list.
Vl-parse-system-function-call
Vl-parse-shift-expression-aux
Vl-parse-power-expression-aux
Vl-parse-mult-expression-aux
Vl-parse-mintypmax-expression
Vl-parse-logor-expression-aux
Vl-parse-logand-expression-aux
Vl-parse-indexed-id-2012
Vl-parse-indexed-id-2005
Vl-parse-equality-expression-aux
Vl-parse-equality-expression
Vl-parse-compare-expression-aux
Vl-parse-bitxor-expression-aux
Vl-parse-bitor-expression-aux
Vl-parse-bitand-expression-aux
Vl-parse-1+-open-value-ranges
Vl-parse-1+-keyval-expression-pairs
Vl-parse-unary-expression
Vl-parse-shift-expression
Vl-parse-qmark-expression
Vl-parse-primary-main
Vl-parse-primary-cast
Vl-parse-power-expression
Vl-parse-open-value-range
Vl-parse-nonprimary-cast
Vl-parse-mult-expression
Vl-parse-logor-expression
Vl-parse-logand-expression
Vl-parse-indexed-id
Vl-parse-impl-expression
Vl-parse-function-call
Vl-parse-expression
Vl-parse-compare-expression
Vl-parse-bitxor-expression
Vl-parse-bitor-expression
Vl-parse-bitand-expression
Vl-parse-assignment-pattern
Vl-parse-add-expression-aux
Vl-parse-add-expression
Vl-parse-1+-expressions-separated-by-commas