Match
(vl-parse-0+-scope-prefixes &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
See also vl-parse-indexed-id-2012 and vl-scopeexpr. We use this in the tricky case of parsing:
{ id '::' } hierarchical_identifier select
But per our desired scope expression representation, we want to keep all of the scoping stuff bundled up together, so we prefer to match it first, if it exists.
Function:
(defun vl-parse-0+-scope-prefixes-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-0+-scope-prefixes)) (declare (ignorable __function__)) (seq tokstream (unless (and (vl-is-token? :vl-idtoken) (vl-lookahead-is-token? :vl-scope (cdr (vl-tokstream->tokens)))) (return nil)) (first := (vl-match)) (:= (vl-match)) (rest := (vl-parse-0+-scope-prefixes)) (return (cons (vl-idtoken->name first) rest)))))
Theorem:
(defthm vl-parse-0+-scope-prefixes-never-fails (not (mv-nth 0 (vl-parse-0+-scope-prefixes))))
Theorem:
(defthm vl-parse-0+-scope-prefixes-result (implies (and (not (mv-nth 0 (vl-parse-0+-scope-prefixes))) (and t)) (string-listp (mv-nth 1 (vl-parse-0+-scope-prefixes)))))
Theorem:
(defthm vl-parse-0+-scope-prefixes-true-listp (true-listp (mv-nth 1 (vl-parse-0+-scope-prefixes))) :rule-classes :type-prescription)
Theorem:
(defthm vl-parse-0+-scope-prefixes-count-strong-on-value (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-0+-scope-prefixes))) (vl-tokstream-measure)) (implies (mv-nth 1 (vl-parse-0+-scope-prefixes)) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-0+-scope-prefixes))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm vl-parse-0+-scope-prefixes-on-eof (implies (not (consp (vl-tokstream->tokens))) (b* (((mv & val new-tokstream) (vl-parse-0+-scope-prefixes))) (and (not val) (not (consp (vl-tokstream->tokens :tokstream new-tokstream)))))))