Matches
(vl-parse-scoped-or-hierarchical-identifier &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
These seem to be a subset of scoped identifiers, so that's what I'll return.
Relevant grammar rules for
ps_or_hierarchical_sequence_identifier ::= [package_scope] sequence_identifier | hierarchical_sequence_identifier package_scope ::= package_identifier '::' | '$unit' '::' sequence_identifier ::= identifier package_identifier ::= identifier hierarchical_sequence_identifier ::= hierarchical_identifier hierarchical_identifier ::= [ '$root' '.' ] { identifier constant_bit_select '.'} identifier
Analogous rules for
ps_or_hierarchical_tf_identifier ::= [package_scope] tf_identifier | hierarchical_tf_identifier hierarchical_tf_identifier ::= hierarchical_identifier tf_identifier ::= identifier
Function:
(defun vl-parse-scoped-or-hierarchical-identifier-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-scoped-or-hierarchical-identifier)) (declare (ignorable __function__)) (seq tokstream (when (and (vl-is-token? :vl-idtoken) (vl-lookahead-is-token? :vl-scope (cdr (vl-tokstream->tokens)))) (id1 := (vl-match)) (:= (vl-match)) (id2 := (vl-match-token :vl-idtoken)) (return (make-vl-scopeexpr-colon :first (vl-idtoken->name id1) :rest (make-vl-scopeexpr-end :hid (make-vl-hidexpr-end :name (vl-idtoken->name id2)))))) (hid := (vl-parse-hierarchical-identifier nil)) (return (make-vl-scopeexpr-end :hid hid)))))
Theorem:
(defthm vl-parse-scoped-or-hierarchical-identifier-fails-gracefully (implies (mv-nth 0 (vl-parse-scoped-or-hierarchical-identifier)) (not (mv-nth 1 (vl-parse-scoped-or-hierarchical-identifier)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-scoped-or-hierarchical-identifier (iff (vl-warning-p (mv-nth 0 (vl-parse-scoped-or-hierarchical-identifier))) (mv-nth 0 (vl-parse-scoped-or-hierarchical-identifier))))
Theorem:
(defthm vl-parse-scoped-or-hierarchical-identifier-result (implies (and t) (equal (vl-scopeexpr-p (mv-nth 1 (vl-parse-scoped-or-hierarchical-identifier))) (not (mv-nth 0 (vl-parse-scoped-or-hierarchical-identifier))))))
Theorem:
(defthm vl-parse-scoped-or-hierarchical-identifier-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-scoped-or-hierarchical-identifier))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-scoped-or-hierarchical-identifier))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-scoped-or-hierarchical-identifier))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))