Matches
(vl-parse-function-data-type-and-name void-allowed-p &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
This matches the part of a function body consisting of:
function_data_type_or_implicit [ interface_identifier '.' | class_scope ] identifier
Except that we're going to ignore the interface_identifier and class_scope part.
The following grammar rules are relevant:
function_data_type_or_implicit ::= data_type_or_void | implicit_data_type data_type_or_void ::= data_type | 'void' implicit_data_type ::= [ signing ] { packed_dimension }
So really what we're parsing is:
'void' identifier | data_type identifier | [ signing ] { packed_dimension } identifier.
This requires backtracking because if an identifier is first, we don't know if we're in the data type or implicit case. The way we resolve this is to first try the datatype case. If that works, it's definitely the right one, because in all cases our final identifier is going to be followed by some punctuation, and so if we parse both a data type and an identifier, we know the third option wouldn't have worked (we would've just gotten an identifier and then a semicolon or left-paren).
Function:
(defun vl-parse-function-data-type-and-name-fn (void-allowed-p tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-function-data-type-and-name)) (declare (ignorable __function__)) (b* (((when (and void-allowed-p (vl-is-token? :vl-kwd-void))) (seq tokstream (:= (vl-match)) (name := (vl-match-token :vl-idtoken)) (return (cons (make-vl-datatype-or-implicit :type (make-vl-coretype :name :vl-void) :implicitp nil) name)))) (backup (vl-tokstream-save)) ((mv err1 val tokstream) (seq tokstream (type := (vl-parse-datatype)) (name := (vl-match-token :vl-idtoken)) (return (cons (make-vl-datatype-or-implicit :type type :implicitp nil) name)))) ((unless err1) (mv nil val tokstream)) (pos1 (vl-tokstream->position)) (tokstream (vl-tokstream-restore backup)) ((mv err2 val tokstream) (seq tokstream (when (vl-is-some-token? '(:vl-kwd-signed :vl-kwd-unsigned)) (signing := (vl-match))) (pdims := (vl-parse-0+-packed-dimensions)) (name := (vl-match-token :vl-idtoken)) (return (cons (make-vl-datatype-or-implicit :type (make-vl-coretype :name :vl-logic :signedp (and signing (eq (vl-token->type signing) :vl-kwd-signed)) :pdims pdims) :implicitp t) name)))) ((unless err2) (mv nil val tokstream)) (pos2 (vl-tokstream->position)) ((mv pos err) (vl-choose-parse-error pos1 err1 pos2 err2)) (tokstream (vl-tokstream-update-position pos))) (mv err nil tokstream))))
Theorem:
(defthm vl-parse-function-data-type-and-name-fails-gracefully (implies (mv-nth 0 (vl-parse-function-data-type-and-name void-allowed-p)) (not (mv-nth 1 (vl-parse-function-data-type-and-name void-allowed-p)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-function-data-type-and-name (iff (vl-warning-p (mv-nth 0 (vl-parse-function-data-type-and-name void-allowed-p))) (mv-nth 0 (vl-parse-function-data-type-and-name void-allowed-p))))
Theorem:
(defthm vl-parse-function-data-type-and-name-result (implies (and (not (mv-nth 0 (vl-parse-function-data-type-and-name void-allowed-p))) (and t)) (and (consp (mv-nth 1 (vl-parse-function-data-type-and-name void-allowed-p))) (vl-datatype-or-implicit-p (car (mv-nth 1 (vl-parse-function-data-type-and-name void-allowed-p)))) (vl-idtoken-p (cdr (mv-nth 1 (vl-parse-function-data-type-and-name void-allowed-p)))))))
Theorem:
(defthm vl-parse-function-data-type-and-name-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-function-data-type-and-name void-allowed-p))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-function-data-type-and-name void-allowed-p))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-function-data-type-and-name void-allowed-p))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))