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:
Function:
(defun vl-parse-packeddimension-fn (tokstream config) (declare (xargs :measure-debug t)) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-packeddimension)) (declare (ignorable __function__)) (seq tokstream (:= (vl-match-token :vl-lbrack)) (when (vl-is-token? :vl-rbrack) (:= (vl-match)) (return :vl-unsized-dimension)) (msb :s= (vl-parse-expression)) (:= (vl-match-token :vl-colon)) (lsb := (vl-parse-expression)) (:= (vl-match-token :vl-rbrack)) (return (vl-range->dimension (make-vl-range :msb msb :lsb lsb))))))
Function:
(defun vl-parse-0+-packed-dimensions-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-0+-packed-dimensions)) (declare (ignorable __function__)) (seq tokstream (unless (vl-is-token? :vl-lbrack) (return nil)) (first :s= (vl-parse-packeddimension)) (rest := (vl-parse-0+-packed-dimensions)) (return (cons first rest)))))
Function:
(defun vl-parse-unpacked-dimension-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-unpacked-dimension)) (declare (ignorable __function__)) (seq tokstream (:= (vl-match-token :vl-lbrack)) (msb :s= (vl-parse-expression)) (when (vl-is-token? :vl-colon) (:= (vl-match)) (lsb := (vl-parse-expression))) (:= (vl-match-token :vl-rbrack)) (return (if lsb (make-vl-range :msb msb :lsb lsb) (make-vl-range :msb (vl-make-index 0) :lsb (make-vl-binary :op :vl-binary-minus :left msb :right (vl-make-index 1))))))))
Function:
(defun vl-parse-0+-unpacked-dimensions-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-0+-unpacked-dimensions)) (declare (ignorable __function__)) (seq tokstream (unless (vl-is-token? :vl-lbrack) (return nil)) (first :s= (vl-parse-unpacked-dimension)) (rest := (vl-parse-0+-unpacked-dimensions)) (return (cons first rest)))))
Function:
(defun vl-parse-queue-dimension-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-queue-dimension)) (declare (ignorable __function__)) (seq tokstream (:= (vl-match-token :vl-lbrack)) (:= (vl-match-token :vl-$)) (when (vl-is-token? :vl-colon) (:= (vl-match)) (maxsize := (vl-parse-expression))) (:= (vl-match-token :vl-rbrack)) (return (make-vl-dimension-queue :maxsize maxsize)))))
Function:
(defun vl-parse-core-data-type-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (declare (xargs :guard (vl-is-some-token? *vl-core-data-type-keywords*))) (let ((__function__ 'vl-parse-core-data-type)) (declare (ignorable __function__)) (b* ((entry (vl-coretypekwd->info (vl-token->type (car (vl-tokstream->tokens))))) ((vl-coredatatype-info entry) entry)) (seq tokstream (:= (vl-match-any)) (when (and entry.takes-signingp (vl-is-some-token? '(:vl-kwd-signed :vl-kwd-unsigned))) (signing := (vl-match))) (when entry.takes-dimensionsp (dims := (vl-parse-0+-packed-dimensions))) (return (let ((ans (make-vl-coretype :name entry.coretypename :signedp (if signing (if (eq (vl-token->type signing) :vl-kwd-signed) t nil) entry.default-signedp) :pdims dims))) (mbe :logic ans :exec (if (atom dims) (hons-copy ans) ans))))))))
Function:
(defun vl-parse-enum-base-type-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-enum-base-type)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-idtoken) (name := (vl-match)) (when (vl-is-token? :vl-lbrack) (dim := (vl-parse-packeddimension))) (return (make-vl-usertype :name (make-vl-scopeexpr-end :hid (make-vl-hidexpr-end :name (vl-idtoken->name name))) :pdims (and dim (list dim))))) (when (vl-is-some-token? '(:vl-kwd-bit :vl-kwd-logic :vl-kwd-reg)) (type := (vl-match)) (when (vl-is-some-token? '(:vl-kwd-signed :vl-kwd-unsigned)) (signing := (vl-match))) (when (vl-is-token? :vl-lbrack) (dim := (vl-parse-packeddimension))) (return (make-vl-coretype :name (case (vl-token->type type) (:vl-kwd-bit :vl-bit) (:vl-kwd-logic :vl-logic) (:vl-kwd-reg :vl-reg)) :signedp (and signing (eq (vl-token->type signing) :vl-kwd-signed)) :pdims (and dim (list dim))))) (type := (vl-match-some-token '(:vl-kwd-byte :vl-kwd-shortint :vl-kwd-int :vl-kwd-longint :vl-kwd-integer :vl-kwd-time))) (when (vl-is-some-token? '(:vl-kwd-signed :vl-kwd-unsigned)) (signing := (vl-match))) (return (make-vl-coretype :name (case (vl-token->type type) (:vl-kwd-byte :vl-byte) (:vl-kwd-shortint :vl-shortint) (:vl-kwd-int :vl-int) (:vl-kwd-longint :vl-longint) (:vl-kwd-integer :vl-integer) (:vl-kwd-time :vl-time)) :signedp (cond (signing (eq (vl-token->type signing) :vl-kwd-signed)) ((eq (vl-token->type type) :vl-kwd-time) nil) (t t)))))))
Function:
(defun vl-parse-enum-name-declaration-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-enum-name-declaration)) (declare (ignorable __function__)) (seq tokstream (name := (vl-match-token :vl-idtoken)) (when (vl-is-token? :vl-lbrack) (:= (vl-match)) (left := (vl-match-token :vl-inttoken)) (when (or (not (vl-inttoken->value left)) (member #\' (vl-echarlist->chars (vl-inttoken->etext left)))) (return-raw (vl-parse-error "Illegal enum index"))) (when (vl-is-token? :vl-colon) (:= (vl-match)) (right := (vl-match-token :vl-inttoken)) (when (or (not (vl-inttoken->value right)) (member #\' (vl-echarlist->chars (vl-inttoken->etext right)))) (return-raw (vl-parse-error "Illegal enum index")))) (:= (vl-match-token :vl-rbrack))) (when (vl-is-token? :vl-equalsign) (:= (vl-match)) (value := (vl-parse-expression))) (when (and left (not right) (equal (vl-inttoken->value left) 0)) (return-raw (vl-parse-error "Illegal enum item index [0]."))) (return (make-vl-enumitem :name (vl-idtoken->name name) :range (cond ((not left) nil) ((not right) (make-vl-range :msb (vl-make-index 0) :lsb (vl-make-index (- (vl-inttoken->value left) 1)))) (t (make-vl-range :msb (vl-make-index (vl-inttoken->value left)) :lsb (vl-make-index (vl-inttoken->value right))))) :value value)))))
Function:
(defun vl-parse-1+-enum-name-declarations-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+-enum-name-declarations-separated-by-commas)) (declare (ignorable __function__)) (seq tokstream (first :s= (vl-parse-enum-name-declaration)) (when (vl-is-token? :vl-comma) (:= (vl-match)) (rest := (vl-parse-1+-enum-name-declarations-separated-by-commas))) (return (cons first rest)))))
Function:
(defun vl-parse-rhs-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-rhs)) (declare (ignorable __function__)) (seq tokstream (unless (vl-is-token? :vl-kwd-new) (expr := (vl-parse-expression)) (return (make-vl-rhsexpr :guts expr))) (:= (vl-match)) (when (vl-is-token? :vl-lbrack) (:= (vl-match)) (arrsize :s= (vl-parse-expression)) (:= (vl-match-token :vl-rbrack)) (when (vl-is-token? :vl-lparen) (:= (vl-match)) (arg1 := (vl-parse-expression)) (:= (vl-match-token :vl-rparen)) (return (make-vl-rhsnew :arrsize arrsize :args (list arg1)))) (return (make-vl-rhsnew :arrsize arrsize))) (return-raw (b* ((backup (vl-tokstream-save)) ((mv err1 args tokstream) (seq tokstream (:= (vl-match-token :vl-lparen)) (args := (vl-parse-1+-expressions-separated-by-commas)) (:= (vl-match-token :vl-rparen)) (return args))) ((unless err1) (mv nil (make-vl-rhsnew :arrsize nil :args args) tokstream)) (tokstream (vl-tokstream-restore backup)) ((mv err2 arg1 tokstream) (vl-parse-expression)) ((unless err2) (mv nil (make-vl-rhsnew :arrsize nil :args (list arg1)) tokstream)) (tokstream (vl-tokstream-restore backup))) (mv nil (make-vl-rhsnew :arrsize nil :args nil) tokstream))))))
Function:
(defun vl-parse-range-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-range)) (declare (ignorable __function__)) (seq tokstream (:= (vl-match-token :vl-lbrack)) (msb :s= (vl-parse-expression)) (:= (vl-match-token :vl-colon)) (lsb := (vl-parse-expression)) (:= (vl-match-token :vl-rbrack)) (return (make-vl-range :msb msb :lsb lsb)))))
Function:
(defun vl-parse-0+-ranges-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-0+-ranges)) (declare (ignorable __function__)) (seq tokstream (unless (vl-plausible-start-of-range-p) (return nil)) (first :s= (vl-parse-range)) (rest := (vl-parse-0+-ranges)) (return (cons first rest)))))
Function:
(defun vl-parse-datatype-or-void-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-datatype-or-void)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-kwd-void) (:= (vl-match-any)) (return (make-vl-coretype :name :vl-void))) (type :s= (vl-parse-datatype)) (return type))))
Function:
(defun vl-parse-datatype-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-datatype)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-kwd-type) (return-raw (vl-parse-error "type references are not yet implemented."))) (when (vl-is-token? :vl-kwd-virtual) (when t (return-raw (vl-parse-error "Virtual interface datatypes are not supported"))) (:= (vl-match)) (id := (vl-match-token :vl-idtoken)) (when (vl-is-token? :vl-pound) (params := (vl-parse-parameter-value-assignment))) (return (make-vl-usertype :name (make-vl-scopeexpr-end :hid (make-vl-hidexpr-end :name (vl-idtoken->name id))) :virtual-intfc t :intfc-params params))) (when (vl-is-some-token? *vl-core-data-type-keywords*) (ret := (vl-parse-core-data-type)) (return ret)) (when (vl-is-some-token? '(:vl-kwd-struct :vl-kwd-union)) (kind := (vl-match)) (when (and (vl-is-token? :vl-kwd-tagged) (eq (vl-token->type kind) :vl-kwd-union)) (tagged := (vl-match))) (when (vl-is-token? :vl-kwd-packed) (packed := (vl-match)) (when (vl-is-some-token? '(:vl-kwd-signed :vl-kwd-unsigned)) (signed := (vl-match)))) (:= (vl-match-token :vl-lcurly)) (members :s= (vl-parse-structmembers)) (:= (vl-match-token :vl-rcurly)) (dims := (vl-parse-0+-packed-dimensions)) (return (b* ((packedp (acl2::bool-fix packed)) (signedp (and signed (eq (vl-token->type signed) :vl-kwd-signed))) ((when (eq (vl-token->type kind) :vl-kwd-struct)) (make-vl-struct :packedp packedp :signedp signedp :members members :pdims dims))) (make-vl-union :packedp packedp :signedp signedp :taggedp (acl2::bool-fix tagged) :members members :pdims dims)))) (when (vl-is-token? :vl-kwd-enum) (:= (vl-match)) (unless (vl-is-token? :vl-lcurly) (basetype :s= (vl-parse-enum-base-type))) (:= (vl-match-token :vl-lcurly)) (items :s= (vl-parse-1+-enum-name-declarations-separated-by-commas)) (:= (vl-match-token :vl-rcurly)) (dims := (vl-parse-0+-packed-dimensions)) (return (make-vl-enum :basetype (or basetype (make-vl-coretype :name :vl-int :signedp t)) :items items :pdims dims))) (type :s= (vl-parse-simple-type)) (dims := (vl-parse-0+-packed-dimensions)) (return (vl-datatype-update-pdims dims type)))))
Function:
(defun vl-parse-structmembers-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-structmembers)) (declare (ignorable __function__)) (seq tokstream (first :s= (vl-parse-structmember)) (when (vl-is-token? :vl-rcurly) (return first)) (rest := (vl-parse-structmembers)) (return (append first rest)))))
Function:
(defun vl-parse-structmember-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-structmember)) (declare (ignorable __function__)) (seq tokstream (atts :w= (vl-parse-0+-attribute-instances)) (when (vl-is-some-token? '(:vl-kwd-rand :vl-kwd-randc)) (rand := (vl-match))) (type :s= (vl-parse-datatype-or-void)) (decls := (vl-parse-1+-variable-decl-assignments-separated-by-commas)) (:= (vl-match-token :vl-semi)) (unless (vl-vardeclassignlist-newfree-p decls) (return-raw (vl-parse-error "Illegal use of 'new' in a struct or union member initial value"))) (return (let ((rand (and rand (case (vl-token->type rand) (:vl-kwd-rand :vl-rand) (:vl-kwd-randc :vl-randc))))) (vl-make-structmembers atts rand type decls))))))
Function:
(defun vl-parse-variable-dimension-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-variable-dimension)) (declare (ignorable __function__)) (seq tokstream (when (and (vl-is-token? :vl-lbrack) (vl-lookahead-is-token? :vl-rbrack (cdr (vl-tokstream->tokens)))) (:= (vl-match)) (:= (vl-match)) (return (make-vl-dimension-unsized))) (when (and (vl-is-token? :vl-lbrack) (vl-lookahead-is-token? :vl-$ (cdr (vl-tokstream->tokens)))) (ans := (vl-parse-queue-dimension)) (return ans)) (return-raw (b* ((backup (vl-tokstream-save)) ((mv erp val tokstream) (vl-parse-unpacked-dimension)) ((unless erp) (mv erp val tokstream)) (tokstream (vl-tokstream-restore backup))) (vl-parse-associative-dimension))))))
Function:
(defun vl-parse-associative-dimension-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-associative-dimension)) (declare (ignorable __function__)) (seq tokstream (:= (vl-match-token :vl-lbrack)) (when (vl-is-token? :vl-times) (:= (vl-match)) (:= (vl-match-token :vl-rbrack)) (return (make-vl-dimension-star))) (type := (vl-parse-datatype)) (:= (vl-match-token :vl-rbrack)) (return (make-vl-dimension-datatype :type type)))))
Function:
(defun vl-parse-0+-variable-dimensions-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-0+-variable-dimensions)) (declare (ignorable __function__)) (seq tokstream (unless (vl-is-token? :vl-lbrack) (return nil)) (first :s= (vl-parse-variable-dimension)) (rest := (vl-parse-0+-variable-dimensions)) (return (cons first rest)))))
Function:
(defun vl-parse-variable-decl-assignment-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-variable-decl-assignment)) (declare (ignorable __function__)) (seq tokstream (id := (vl-match-token :vl-idtoken)) (when (vl-is-token? :vl-lbrack) (dims :w= (vl-parse-0+-variable-dimensions))) (when (vl-is-token? :vl-equalsign) (:= (vl-match)) (rhs := (vl-parse-rhs))) (return (make-vl-vardeclassign :id (vl-idtoken->name id) :dims dims :rhs rhs)))))
Function:
(defun vl-parse-1+-variable-decl-assignments-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+-variable-decl-assignments-separated-by-commas)) (declare (ignorable __function__)) (seq tokstream (first :s= (vl-parse-variable-decl-assignment)) (when (vl-is-token? :vl-comma) (:= (vl-match)) (rest := (vl-parse-1+-variable-decl-assignments-separated-by-commas))) (return (cons first rest)))))
Function:
(defun vl-parse-param-expression-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-param-expression)) (declare (ignorable __function__)) (b* ((backup (vl-tokstream-save)) ((mv err expr tokstream) (vl-parse-mintypmax-expression)) ((unless err) (mv err (make-vl-paramvalue-expr :expr expr) tokstream)) (tokstream (vl-tokstream-restore backup))) (seq tokstream (type := (vl-parse-datatype)) (return (make-vl-paramvalue-type :type type))))))
Function:
(defun vl-parse-named-parameter-assignment-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-named-parameter-assignment)) (declare (ignorable __function__)) (seq tokstream (:= (vl-match-token :vl-dot)) (id := (vl-match-token :vl-idtoken)) (:= (vl-match-token :vl-lparen)) (unless (vl-is-token? :vl-rparen) (value := (vl-parse-param-expression))) (:= (vl-match-token :vl-rparen)) (return (make-vl-namedparamvalue :name (vl-idtoken->name id) :value value)))))
Function:
(defun vl-parse-list-of-named-parameter-assignments-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-list-of-named-parameter-assignments)) (declare (ignorable __function__)) (seq tokstream (first :s= (vl-parse-named-parameter-assignment)) (when (vl-is-token? :vl-comma) (:= (vl-match-token :vl-comma)) (rest := (vl-parse-list-of-named-parameter-assignments))) (return (cons first rest)))))
Function:
(defun vl-parse-list-of-ordered-parameter-assignments-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-list-of-ordered-parameter-assignments)) (declare (ignorable __function__)) (seq tokstream (first :s= (vl-parse-param-expression)) (when (vl-is-token? :vl-comma) (:= (vl-match-token :vl-comma)) (rest := (vl-parse-list-of-ordered-parameter-assignments))) (return (cons first rest)))))
Function:
(defun vl-parse-list-of-parameter-assignments-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-list-of-parameter-assignments)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-dot) (args := (vl-parse-list-of-named-parameter-assignments)) (return (make-vl-paramargs-named :args args))) (exprs := (if (eq (vl-loadconfig->edition config) :verilog-2005) (b* (((mv err val tokstream) (vl-parse-1+-expressions-separated-by-commas)) ((when err) (mv err nil tokstream))) (mv err (vl-expressions->paramvalues val) tokstream)) (vl-parse-list-of-ordered-parameter-assignments))) (return (make-vl-paramargs-plain :args exprs)))))
Function:
(defun vl-parse-parameter-value-assignment-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-parameter-value-assignment)) (declare (ignorable __function__)) (seq tokstream (:= (vl-match-token :vl-pound)) (unless (vl-is-token? :vl-lparen) (expr := (vl-parse-expression)) (return (make-vl-paramargs-plain :args (list (make-vl-paramvalue-expr :expr expr))))) (:= (vl-match)) (when (and (vl-is-token? :vl-rparen) (not (eq (vl-loadconfig->edition config) :verilog-2005))) (:= (vl-match)) (return (make-vl-paramargs-plain :args nil))) (args := (vl-parse-list-of-parameter-assignments)) (:= (vl-match-token :vl-rparen)) (return args))))
Function:
(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:
(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:
(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:
(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:
(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)) (linestart := (vl-linestart-indent)) (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__)) (atts (vl-extend-atts-with-linestart linestart atts)) (tokstream (vl-tokstream-add-warning w))) (mv nil atts tokstream))))))
Function:
(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:
(defun vl-parse-patternkey-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-patternkey)) (declare (ignorable __function__)) (b* (((when (vl-is-token? :vl-kwd-default)) (seq tokstream (:= (vl-match)) (return (make-vl-patternkey-default)))) (backup (vl-tokstream-save)) ((mv err expr tokstream) (vl-parse-expression)) ((unless err) (mv err (vl-initial-patternkey-from-expr expr) tokstream)) (tokstream (vl-tokstream-restore backup))) (seq tokstream (type := (vl-parse-simple-type)) (return (make-vl-patternkey-type :type type))))))
Function:
(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 (key :s= (vl-parse-patternkey)) (:= (vl-match-token :vl-colon)) (val :s= (vl-parse-expression)) (when (vl-is-token? :vl-comma) (:= (vl-match)) (rest := (vl-parse-1+-keyval-expression-pairs))) (return (cons (cons key val) rest)))))
Function:
(defun vl-parse-expression-without-failure-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-expression-without-failure)) (declare (ignorable __function__)) (b* ((backup (vl-tokstream-save)) ((mv err expr tokstream) (vl-parse-expression)) ((unless err) (mv err expr tokstream)) (tokstream (vl-tokstream-restore backup))) (mv nil nil tokstream))))
Function:
(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 (linestart := (vl-linestart-indent)) (fn := (vl-match-token :vl-sysidtoken)) (when (vl-is-token? :vl-lparen) (:= (vl-match)) (arg1 :w= (vl-parse-expression-without-failure)) (when (and (not arg1) (not (vl-is-token? :vl-rparen))) (typearg :w= (vl-parse-simple-type))) (when (vl-is-token? :vl-comma) (:= (vl-match)) (args := (vl-parse-sysfuncall-args))) (:= (vl-match-token :vl-rparen))) (return (let ((fname (vl-sysidtoken->name fn))) (make-vl-call :name (make-vl-scopeexpr-end :hid (make-vl-hidexpr-end :name fname)) :typearg typearg :plainargs (if arg1 (cons arg1 args) args) :systemp t :atts (vl-extend-atts-with-linestart linestart nil)))))))
Function:
(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-mintypmax :min min :typ typ :max max))) (when (eq (vl-loadconfig->edition config) :verilog-2005) (return min)) (linestart1 := (vl-linestart-indent)) (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)) (linestart2 := (vl-linestart-indent)) (rhs := (vl-parse-expression)) (return (b* ((atts nil) (atts (vl-extend-atts-with-linestart linestart2 atts)) (atts (vl-extend-atts-with-linestart linestart1 atts))) (make-vl-binary :op op :left min :right rhs :atts atts))))))
Function:
(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:
(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 (linestart := (vl-linestart-indent)) (:= (vl-match-token :vl-lcurly)) (args := (vl-parse-1+-expressions-separated-by-commas)) (:= (vl-match-token :vl-rcurly)) (return (make-vl-concat :parts args :atts (vl-extend-atts-with-linestart linestart nil))))))
Function:
(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 (make-vl-streamexpr :expr expr :part (make-vl-arrayrange-none)))) (:= (vl-match)) (:= (vl-match-token :vl-lbrack)) (range := (vl-parse-range-expression)) (:= (vl-match-token :vl-rbrack)) (return (vl-streamexpr-with expr range)))))
Function:
(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:
(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:
(defun vl-parse-pva-tail-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-pva-tail)) (declare (ignorable __function__)) (seq tokstream (:= (vl-match-token :vl-scope)) (head := (vl-match-token :vl-idtoken)) (when (vl-is-token? :vl-pound) (:= (vl-parse-parameter-value-assignment)) (return-raw (vl-parse-error "Implement PVAs."))) (unless (vl-is-token? :vl-scope) (return (make-vl-scopeexpr-end :hid (make-vl-hidexpr-end :name (vl-idtoken->name head))))) (tail := (vl-parse-pva-tail)) (return (make-vl-scopeexpr-colon :first (vl-idtoken->name head) :rest tail)))))
Function:
(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-usertype :name (make-vl-scopeexpr-colon :first :vl-local :rest (make-vl-scopeexpr-end :hid (make-vl-hidexpr-end :name (vl-idtoken->name tail))))))) (when (vl-is-token? :vl-$unit) (:= (vl-match)) (tail := (vl-parse-pva-tail)) (return (make-vl-usertype :name (make-vl-scopeexpr-colon :first :vl-$unit :rest 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)) (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-usertype :name (make-vl-scopeexpr-colon :first (vl-idtoken->name head) :rest tail)))) (hid := (vl-parse-hierarchical-identifier nil)) (return (make-vl-usertype :name (make-vl-scopeexpr-end :hid hid))))))
Function:
(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-expression)) ((unless err) (mv err (make-vl-slicesize-expr :expr expr) tokstream)) (tokstream (vl-tokstream-restore backup))) (seq tokstream (type := (vl-parse-simple-type)) (return (make-vl-slicesize-type :type type))))))
Function:
(defun vl-parse-any-sort-of-concatenation-aux-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-aux)) (declare (ignorable __function__)) (seq tokstream (linestart := (vl-linestart-indent)) (:= (vl-match-token :vl-lcurly)) (when (and (vl-is-token? :vl-rcurly) (not (eq (vl-loadconfig->edition config) :verilog-2005))) (:= (vl-match)) (return (vl-expr-update-atts (make-vl-special :key :vl-emptyqueue) (vl-extend-atts-with-linestart linestart nil)))) (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))) (make-vl-stream :dir (if (eq dir :vl-shl) :left :right) :size (or slicesize (make-vl-slicesize-none)) :parts args :atts (vl-extend-atts-with-linestart linestart nil))))) (e1 :s= (vl-parse-expression)) (when (vl-is-token? :vl-lcurly) (:= (vl-match)) (parts := (vl-parse-1+-expressions-separated-by-commas)) (:= (vl-match-token :vl-rcurly)) (:= (vl-match-token :vl-rcurly)) (return (make-vl-multiconcat :reps e1 :parts parts :atts (vl-extend-atts-with-linestart linestart nil)))) (when (vl-is-token? :vl-comma) (:= (vl-match)) (rest := (vl-parse-1+-expressions-separated-by-commas)) (:= (vl-match-token :vl-rcurly)) (return (make-vl-concat :parts (cons e1 rest) :atts (vl-extend-atts-with-linestart linestart nil)))) (:= (vl-match-token :vl-rcurly)) (return (make-vl-concat :parts (list e1) :atts (vl-extend-atts-with-linestart linestart nil))))))
Function:
(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 (concat :s= (vl-parse-any-sort-of-concatenation-aux)) (when (vl-is-token? :vl-lbrack) (:= (vl-match)) (range := (vl-parse-range-expression)) (:= (vl-match-token :vl-rbrack)) (return (b* (((vl-erange range))) (case range.type (:vl-index (make-vl-bitselect-expr :subexp concat :index range.left)) (:vl-colon (make-vl-partselect-expr :subexp concat :part (vl-range->partselect (make-vl-range :msb range.left :lsb range.right)))) (otherwise (make-vl-partselect-expr :subexp concat :part (vl-plusminus->partselect (make-vl-plusminus :base range.left :width range.right :minusp (eq range.type :vl-minuscolon))))))))) (return concat))))
Function:
(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 (make-vl-hidexpr-dot :first (make-vl-hidindex :name :vl-$root) :rest tail))) (id := (vl-match-token :vl-idtoken)) (when (vl-is-token? :vl-dot) (:= (vl-match)) (tail :s= (vl-parse-hierarchical-identifier t)) (return (make-vl-hidexpr-dot :first (make-vl-hidindex :name (vl-idtoken->name id)) :rest 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 (make-vl-hidexpr-dot :first (make-vl-hidindex :name (vl-idtoken->name id) :indices (list expr)) :rest tail))) (return (make-vl-hidexpr-end :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 (make-vl-hidexpr-dot :first (make-vl-hidindex :name (vl-idtoken->name id) :indices exprs) :rest tail))) (return (make-vl-hidexpr-end :name (vl-idtoken->name id)))))))
Function:
(defun vl-parse-scoped-hid-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-scoped-hid)) (declare (ignorable __function__)) (b* ((backup (vl-tokstream-save)) ((mv err first tokstream) (seq tokstream (name := (vl-parse-scopename)) (when (vl-is-some-token? '(:vl-pound :vl-scope)) (return name)) (return-raw (vl-parse-error "backup for hid")))) ((when err) (b* ((tokstream (vl-tokstream-restore backup))) (seq tokstream (hid := (vl-parse-hierarchical-identifier nil)) (return (make-vl-scopeexpr-end :hid hid)))))) (seq tokstream (when (vl-is-token? :vl-pound) (params :s= (vl-parse-parameter-value-assignment))) (:= (vl-match-token :vl-scope)) (rest := (vl-parse-scoped-hid)) (return (make-vl-scopeexpr-colon :first first :paramargs params :rest rest))))))
Function:
(defun vl-parse-call-namedarg-pair-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-call-namedarg-pair)) (declare (ignorable __function__)) (seq tokstream (:= (vl-match-token :vl-dot)) (id := (vl-match-token :vl-idtoken)) (:= (vl-match-token :vl-lparen)) (unless (vl-is-token? :vl-rparen) (expr :s= (vl-parse-expression))) (:= (vl-match-token :vl-rparen)) (return (cons (vl-idtoken->name id) expr)))))
Function:
(defun vl-parse-call-namedargs-aux-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-call-namedargs-aux)) (declare (ignorable __function__)) (seq tokstream (unless (vl-is-token? :vl-comma) (return nil)) (:= (vl-match)) (pair :s= (vl-parse-call-namedarg-pair)) (rest := (vl-parse-call-namedargs-aux)) (return (cons pair rest)))))
Function:
(defun vl-parse-call-namedargs-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-call-namedargs)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-rparen) (return nil)) (pair :s= (vl-parse-call-namedarg-pair)) (rest := (vl-parse-call-namedargs-aux)) (return (cons pair rest)))))
Function:
(defun vl-parse-call-plainargs-aux-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-call-plainargs-aux)) (declare (ignorable __function__)) (seq tokstream (unless (vl-is-token? :vl-comma) (return nil)) (:= (vl-match)) (when (vl-is-token? :vl-rparen) (return (list nil))) (when (vl-is-token? :vl-dot) (return nil)) (unless (vl-is-token? :vl-comma) (expr :s= (vl-parse-expression))) (rest := (vl-parse-call-plainargs-aux)) (return (cons expr rest)))))
Function:
(defun vl-parse-call-plainargs-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-call-plainargs)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-dot) (return nil)) (unless (vl-is-token? :vl-comma) (expr :s= (vl-parse-expression))) (rest := (vl-parse-call-plainargs-aux)) (return (cons expr rest)))))
Function:
(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 (linestart := (vl-linestart-indent)) (id :s= (vl-parse-scoped-hid)) (atts :w= (vl-parse-0+-attribute-instances)) (:= (vl-match-token :vl-lparen)) (when (and (not (eq (vl-loadconfig->edition config) :verilog-2005)) (vl-is-token? :vl-rparen)) (:= (vl-match-token :vl-rparen)) (return (make-vl-call :name id :systemp nil :atts (vl-extend-atts-with-linestart linestart atts)))) (plainargs :w= (vl-parse-call-plainargs)) (namedargs :w= (vl-parse-call-namedargs)) (:= (vl-match-token :vl-rparen)) (return (make-vl-call :name id :plainargs plainargs :namedargs namedargs :systemp nil :atts (vl-extend-atts-with-linestart linestart atts))))))
Function:
(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-plausible-start-of-range-p)) (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:
(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-scopenamelist-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-plausible-start-of-range-p) (:= (vl-match)) (range := (vl-parse-range-expression)) (:= (vl-match-token :vl-rbrack))) (return (let* ((ans (vl-tack-scopes-onto-hid scopes hid))) (if range (vl-build-range-select ans bexprs range) (make-vl-index :scope ans :indices bexprs :part (make-vl-partselect-none))))))))
Function:
(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 :vl-local) (:vl-$unit :vl-$unit)) morescopes) t))) (scopes := (vl-parse-0+-scope-prefixes)) (return-raw (vl-parse-indexed-id-2005 scopes (consp scopes))))))
Function:
(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__)) (seq tokstream (linestart := (vl-linestart-indent)) (ans := (if (eq (vl-loadconfig->edition config) :verilog-2005) (vl-parse-indexed-id-2005 nil nil) (vl-parse-indexed-id-2012))) (return (vl-extend-expr-with-linestart linestart ans)))))
Function:
(defun vl-parse-assignment-pattern-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-assignment-pattern)) (declare (ignorable __function__)) (b* ((backup (vl-tokstream-save)) ((mv expr-err first-expr tokstream) (seq tokstream (expr :w= (vl-parse-expression)) (return expr))) ((mv err first-key tokstream) (if expr-err (b* ((tokstream (vl-tokstream-restore backup))) (seq tokstream (key :w= (vl-parse-patternkey)) (return key))) (mv nil (vl-initial-patternkey-from-expr first-expr) tokstream))) ((when err) (mv err nil tokstream))) (seq tokstream (when (vl-is-token? :vl-colon) (:= (vl-match)) (firstval :s= (vl-parse-expression)) (when (vl-is-token? :vl-rcurly) (:= (vl-match)) (return (make-vl-assignpat-keyval :pairs (list (cons first-key firstval))))) (:= (vl-match-token :vl-comma)) (rest := (vl-parse-1+-keyval-expression-pairs)) (:= (vl-match-token :vl-rcurly)) (return (make-vl-assignpat-keyval :pairs (cons (cons first-key firstval) rest)))) (when expr-err (return-raw (mv expr-err nil tokstream))) (when (vl-is-token? :vl-rcurly) (:= (vl-match)) (return (make-vl-assignpat-positional :vals (list first-expr)))) (when (vl-is-token? :vl-comma) (:= (vl-match)) (rest := (vl-parse-1+-expressions-separated-by-commas)) (:= (vl-match-token :vl-rcurly)) (return (make-vl-assignpat-positional :vals (cons first-expr rest)))) (:= (vl-match-token :vl-lcurly)) (parts := (vl-parse-1+-expressions-separated-by-commas)) (:= (vl-match-token :vl-rcurly)) (:= (vl-match-token :vl-rcurly)) (return (make-vl-assignpat-repeat :reps first-expr :vals parts))))))
Function:
(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 (linestart := (vl-linestart-indent)) (:= (vl-match)) (:= (vl-match-token :vl-lcurly)) (pat := (vl-parse-assignment-pattern)) (return (make-vl-pattern :pat pat :atts (vl-extend-atts-with-linestart linestart nil)))))) (vl-parse-error "Failed to match a primary expression."))))
Function:
(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-cast :to (make-vl-casttype-size :size primary) :expr arg))) (:= (vl-match-token :vl-lcurly)) (pattern := (vl-parse-assignment-pattern)) (return-raw (b* ((type (vl-interpret-expr-as-type primary)) ((unless type) (vl-parse-error "Couldn't interpret cast expression as datatype."))) (mv nil (make-vl-pattern :pattype type :pat pattern) tokstream)))) (return primary))))
Function:
(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 (make-vl-casttype-signedness :signedp t)) (:vl-kwd-unsigned (make-vl-casttype-signedness :signedp nil)) (:vl-kwd-string (make-vl-casttype-type :type (make-vl-coretype :name :vl-string))) (:vl-kwd-const (make-vl-casttype-const))))) (make-vl-cast :to casting-type :expr 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-cast :to (make-vl-casttype-type :type type) :expr arg)))))
Function:
(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:
(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 (linestart := (vl-linestart-indent)) (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 (vl-expr-update-atts (make-vl-unary :op post :arg primary) atts)))) ((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 := (if (member-eq op '(:vl-unary-lognot :vl-unary-bitnot)) (vl-parse-unary-expression) (vl-parse-primary))) (return (make-vl-unary :op op :atts (vl-extend-atts-with-linestart linestart atts) :arg primary)))))
Function:
(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))) (linestart1 := (vl-linestart-indent)) (:= (vl-match)) (linestart2 := (vl-linestart-indent)) (atts :w= (vl-parse-0+-attribute-instances)) (tail := (vl-parse-power-expression-aux)) (return (b* ((atts (vl-extend-atts-with-linestart linestart2 atts)) (atts (vl-extend-atts-with-linestart linestart1 atts))) (list* first :vl-binary-power atts tail))))))
Function:
(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:
(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)) (linestart1 := (vl-linestart-indent)) (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))) (linestart2 := (vl-linestart-indent)) (atts :w= (vl-parse-0+-attribute-instances)) (tail := (vl-parse-mult-expression-aux)) (return (b* ((atts (vl-extend-atts-with-linestart linestart2 atts)) (atts (vl-extend-atts-with-linestart linestart1 atts))) (list* first op atts tail))))))
Function:
(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:
(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)) (linestart1 := (vl-linestart-indent)) (op := (vl-parse-op 2 '((:vl-plus . :vl-binary-plus) (:vl-minus . :vl-binary-minus)))) (unless op (return (list first))) (linestart2 := (vl-linestart-indent)) (atts :w= (vl-parse-0+-attribute-instances)) (tail := (vl-parse-add-expression-aux)) (return (b* ((atts (vl-extend-atts-with-linestart linestart2 atts)) (atts (vl-extend-atts-with-linestart linestart1 atts))) (list* first op atts tail))))))
Function:
(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:
(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)) (linestart1 := (vl-linestart-indent)) (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))) (linestart2 := (vl-linestart-indent)) (atts :w= (vl-parse-0+-attribute-instances)) (tail := (vl-parse-shift-expression-aux)) (return (b* ((atts (vl-extend-atts-with-linestart linestart2 atts)) (atts (vl-extend-atts-with-linestart linestart1 atts))) (list* first op atts tail))))))
Function:
(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:
(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)) (when (vl-is-token? :vl-kwd-inside) (linestart1 := (vl-linestart-indent)) (:= (vl-match)) (linestart2 := (vl-linestart-indent)) (:= (vl-match-token :vl-lcurly)) (set := (vl-parse-1+-open-value-ranges)) (:= (vl-match-token :vl-rcurly)) (return (b* ((atts nil) (atts (vl-extend-atts-with-linestart linestart2 atts)) (atts (vl-extend-atts-with-linestart linestart1 atts))) (list (make-vl-inside :elem first :set set :atts atts))))) (linestart1 := (vl-linestart-indent)) (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)))) (unless op (return (list first))) (linestart2 := (vl-linestart-indent)) (atts :w= (vl-parse-0+-attribute-instances)) (tail := (vl-parse-compare-expression-aux)) (return (b* ((atts (vl-extend-atts-with-linestart linestart2 atts)) (atts (vl-extend-atts-with-linestart linestart1 atts))) (list* first op atts tail))))))
Function:
(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:
(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-plausible-start-of-range-p) (:= (vl-match)) (low :w= (vl-parse-expression)) (:= (vl-match-token :vl-colon)) (high := (vl-parse-expression)) (:= (vl-match-token :vl-rbrack)) (return (make-vl-valuerange-range :low low :high high))) (expr := (vl-parse-expression)) (return (make-vl-valuerange-single :expr expr)))))
Function:
(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:
(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)) (linestart1 := (vl-linestart-indent)) (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))) (linestart2 := (vl-linestart-indent)) (atts :w= (vl-parse-0+-attribute-instances)) (tail := (vl-parse-equality-expression-aux)) (return (b* ((atts (vl-extend-atts-with-linestart linestart2 atts)) (atts (vl-extend-atts-with-linestart linestart1 atts))) (list* first op atts tail))))))
Function:
(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:
(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))) (linestart1 := (vl-linestart-indent)) (:= (vl-match)) (linestart2 := (vl-linestart-indent)) (atts :w= (vl-parse-0+-attribute-instances)) (tail := (vl-parse-bitand-expression-aux)) (return (b* ((atts (vl-extend-atts-with-linestart linestart2 atts)) (atts (vl-extend-atts-with-linestart linestart1 atts))) (list* first :vl-binary-bitand atts tail))))))
Function:
(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:
(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)) (linestart1 := (vl-linestart-indent)) (op := (vl-parse-op 2 '((:vl-xor . :vl-binary-xor) (:vl-xnor . :vl-binary-xnor)))) (linestart2 := (vl-linestart-indent)) (unless op (return (list first))) (atts :w= (vl-parse-0+-attribute-instances)) (tail := (vl-parse-bitxor-expression-aux)) (return (b* ((atts (vl-extend-atts-with-linestart linestart2 atts)) (atts (vl-extend-atts-with-linestart linestart1 atts))) (list* first op atts tail))))))
Function:
(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:
(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))) (linestart1 := (vl-linestart-indent)) (:= (vl-match)) (linestart2 := (vl-linestart-indent)) (atts :w= (vl-parse-0+-attribute-instances)) (tail := (vl-parse-bitor-expression-aux)) (return (b* ((atts (vl-extend-atts-with-linestart linestart2 atts)) (atts (vl-extend-atts-with-linestart linestart1 atts))) (list* first :vl-binary-bitor atts tail))))))
Function:
(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:
(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))) (linestart1 := (vl-linestart-indent)) (:= (vl-match)) (linestart2 := (vl-linestart-indent)) (atts :w= (vl-parse-0+-attribute-instances)) (tail := (vl-parse-logand-expression-aux)) (return (b* ((atts (vl-extend-atts-with-linestart linestart2 atts)) (atts (vl-extend-atts-with-linestart linestart1 atts))) (list* first :vl-binary-logand atts tail))))))
Function:
(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:
(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))) (linestart1 := (vl-linestart-indent)) (:= (vl-match)) (linestart2 := (vl-linestart-indent)) (atts :w= (vl-parse-0+-attribute-instances)) (tail := (vl-parse-logor-expression-aux)) (return (b* ((atts (vl-extend-atts-with-linestart linestart2 atts)) (atts (vl-extend-atts-with-linestart linestart1 atts))) (list* first :vl-binary-logor atts tail))))))
Function:
(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:
(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)) (qmark-linestart1 := (vl-linestart-indent)) (:= (vl-match)) (qmark-linestart2 := (vl-linestart-indent)) (atts :w= (vl-parse-0+-attribute-instances)) (second :s= (vl-parse-expression)) (colon-linestart1 := (vl-linestart-indent)) (:= (vl-match-token :vl-colon)) (colon-linestart2 := (vl-linestart-indent)) (third := (vl-parse-qmark-expression)) (return (b* ((qmark-linestart (or qmark-linestart1 qmark-linestart2)) (colon-linestart (or colon-linestart1 colon-linestart2)) (atts (if qmark-linestart (cons (hons "VL_QMARK_LINESTART" (vl-make-index qmark-linestart)) atts) atts)) (atts (if colon-linestart (cons (hons "VL_COLON_LINESTART" (vl-make-index colon-linestart)) atts) atts))) (make-vl-qmark :test first :then second :else third :atts atts))))))
Function:
(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)) (linestart1 := (vl-linestart-indent)) (op := (vl-parse-op 2 '((:vl-arrow . :vl-implies) (:vl-equiv . :vl-equiv)))) (unless op (return first)) (linestart2 := (vl-linestart-indent)) (atts :w= (vl-parse-0+-attribute-instances)) (second :s= (vl-parse-impl-expression)) (return (b* ((atts (vl-extend-atts-with-linestart linestart2 atts)) (atts (vl-extend-atts-with-linestart linestart1 atts))) (make-vl-binary :op op :left first :right second :atts atts))))))
Function:
(defun vl-parse-event-expression-2005-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-event-expression-2005)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-some-token? '(:vl-kwd-posedge :vl-kwd-negedge)) (edge := (vl-match))) (expr :s= (vl-parse-expression)) (when (vl-is-some-token? '(:vl-kwd-or :vl-comma)) (:= (vl-match)) (rest := (vl-parse-event-expression-2005))) (return (let ((edgetype (if (not edge) :vl-noedge (case (vl-token->type edge) (:vl-kwd-posedge :vl-posedge) (:vl-kwd-negedge :vl-negedge) (t (impossible)))))) (cons (make-vl-evatom :type edgetype :expr expr) rest))))))
Function:
(defun vl-parse-event-expression-2012-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-event-expression-2012)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-lparen) (:= (vl-match)) (nested :w= (vl-parse-event-expression-2012)) (:= (vl-match-token :vl-rparen))) (unless nested (edge :w= (vl-parse-optional-edge-identifier)) (expr :s= (vl-parse-expression))) (when (vl-is-token? :vl-kwd-iff) (return-raw (vl-parse-error "BOZO need to implement event_expressions with 'iff' clauses."))) (when (vl-is-some-token? '(:vl-kwd-or :vl-comma)) (:= (vl-match)) (rest := (vl-parse-event-expression-2012))) (return (if nested (append-without-guard nested rest) (cons (make-vl-evatom :type edge :expr expr) rest))))))
Function:
(defun vl-parse-event-expression-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-event-expression)) (declare (ignorable __function__)) (seq tokstream (when (eq (vl-loadconfig->edition config) :verilog-2005) (ret := (vl-parse-event-expression-2005)) (return ret)) (ret := (vl-parse-event-expression-2012)) (return ret))))
Function:
(defun vl-parse-clocking-event-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-clocking-event)) (declare (ignorable __function__)) (seq tokstream (:= (vl-match-token :vl-atsign)) (when (vl-is-token? :vl-idtoken) (id := (vl-match)) (return (list (make-vl-evatom :type :vl-noedge :expr (vl-idexpr (vl-idtoken->name id)))))) (:= (vl-match-token :vl-lparen)) (evatoms := (vl-parse-event-expression)) (:= (vl-match-token :vl-rparen)) (return evatoms))))
Function:
(defun vl-parse-expr-or-clocking-event-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-expr-or-clocking-event)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-atsign) (evatoms := (vl-parse-clocking-event)) (return (make-vl-eventexpr :atoms evatoms))) (expr := (vl-parse-expression)) (return expr))))
Function:
(defun vl-parse-sysfuncall-args-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-sysfuncall-args)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-rparen) (return nil)) (when (vl-is-token? :vl-comma) (:= (vl-match)) (rest := (vl-parse-sysfuncall-args)) (return (cons nil rest))) (first :s= (vl-parse-expr-or-clocking-event)) (when (vl-is-token? :vl-comma) (:= (vl-match)) (rest := (vl-parse-sysfuncall-args))) (return (cons first rest)))))
Function:
(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)) (linestart := (vl-linestart-indent)) (:= (vl-match)) (id := (vl-match-token :vl-idtoken)) (return-raw (b* ((tag (vl-idtoken->name id)) (atts (vl-extend-atts-with-linestart linestart nil)) (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-tagged :tag tag :atts atts) tokstream))) ((unless (or (hons-assoc-equal "VL_EXPLICIT_PARENS" (vl-expr->atts expr)) (vl-expr-case expr :vl-binary nil :vl-qmark nil :otherwise t))) (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-tagged :tag tag :expr expr :atts atts))) (mv nil ans tokstream))))))