(vl-parse-1+-id=expr-pairs type varp &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Function:
(defun vl-parse-1+-id=expr-pairs-fn (type varp tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (declare (xargs :guard (and (vl-datatype-p type) (booleanp varp)))) (let ((__function__ 'vl-parse-1+-id=expr-pairs)) (declare (ignorable __function__)) (seq tokstream (id := (vl-match-token :vl-idtoken)) (:= (vl-match-token :vl-equalsign)) (initval := (vl-parse-rhs)) (return-raw (b* ((vardecl1 (make-vl-vardecl :name (vl-idtoken->name id) :type type :varp varp :initval initval :loc (vl-token->loc id))) (backup (vl-tokstream-save)) ((mv erp rest tokstream) (seq tokstream (:= (vl-match-token :vl-comma)) (return-raw (vl-parse-1+-id=expr-pairs type varp)))) ((unless erp) (mv nil (cons vardecl1 rest) tokstream)) (tokstream (vl-tokstream-restore backup))) (mv nil (list vardecl1) tokstream))))))
Theorem:
(defthm vl-parse-1+-id=expr-pairs-fails-gracefully (implies (mv-nth 0 (vl-parse-1+-id=expr-pairs type varp)) (not (mv-nth 1 (vl-parse-1+-id=expr-pairs type varp)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-1+-id=expr-pairs (iff (vl-warning-p (mv-nth 0 (vl-parse-1+-id=expr-pairs type varp))) (mv-nth 0 (vl-parse-1+-id=expr-pairs type varp))))
Theorem:
(defthm vl-parse-1+-id=expr-pairs-result (implies (and (and (force (vl-datatype-p type)) (force (booleanp varp)))) (vl-vardecllist-p (mv-nth 1 (vl-parse-1+-id=expr-pairs type varp)))))
Theorem:
(defthm vl-parse-1+-id=expr-pairs-true-listp (true-listp (mv-nth 1 (vl-parse-1+-id=expr-pairs type varp))) :rule-classes :type-prescription)
Theorem:
(defthm vl-parse-1+-id=expr-pairs-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-1+-id=expr-pairs type varp))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-1+-id=expr-pairs type varp))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-1+-id=expr-pairs type varp))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))