Parse
(vl-parse-0+-assertion-variable-declarations &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
In
assertion_variable_declaration ::= var_data_type list_of_variable_decl_assignments ';' var_data_type ::= data_type | 'var' data_type_or_implicit
Function:
(defun vl-parse-0+-assertion-variable-declarations-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-0+-assertion-variable-declarations)) (declare (ignorable __function__)) (b* ((loc (if (consp (vl-tokstream->tokens)) (vl-token->loc (car (vl-tokstream->tokens))) *vl-fakeloc*)) ((when (vl-is-token? :vl-kwd-var)) (seq tokstream (:= (vl-match)) (type := (vl-parse-datatype-or-implicit)) (vars := (vl-parse-1+-variable-decl-assignments-separated-by-commas)) (:= (vl-match-token :vl-semi)) (rest := (vl-parse-0+-assertion-variable-declarations)) (return (append (vl-make-assertion-vardecls type vars loc) rest)))) (backup (vl-tokstream-save)) ((mv err type tokstream) (vl-parse-datatype)) ((when (and (not err) (vl-is-token? :vl-idtoken))) (seq tokstream (vars := (vl-parse-1+-variable-decl-assignments-separated-by-commas)) (:= (vl-match-token :vl-semi)) (return (vl-make-assertion-vardecls type vars loc)))) (tokstream (vl-tokstream-restore backup))) (mv nil nil tokstream))))
Theorem:
(defthm vl-parse-0+-assertion-variable-declarations-fails-gracefully (implies (mv-nth 0 (vl-parse-0+-assertion-variable-declarations)) (not (mv-nth 1 (vl-parse-0+-assertion-variable-declarations)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-0+-assertion-variable-declarations (iff (vl-warning-p (mv-nth 0 (vl-parse-0+-assertion-variable-declarations))) (mv-nth 0 (vl-parse-0+-assertion-variable-declarations))))
Theorem:
(defthm vl-parse-0+-assertion-variable-declarations-result (implies (and t) (vl-vardecllist-p (mv-nth 1 (vl-parse-0+-assertion-variable-declarations)))))
Theorem:
(defthm vl-parse-0+-assertion-variable-declarations-true-listp (true-listp (mv-nth 1 (vl-parse-0+-assertion-variable-declarations))) :rule-classes :type-prescription)
Theorem:
(defthm vl-parse-0+-assertion-variable-declarations-count-weak (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-0+-assertion-variable-declarations))) (vl-tokstream-measure)) :rule-classes ((:rewrite) (:linear)))