Match any kind of
(vl-parse-type-declaration atts &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
The grammar mixes both forward and regular type declarations:
type_declaration ::= 'typedef' data_type type_identifier { variable_dimension } ';' | 'typedef' interface_instance_identifier constant_bit_select '.' type_identifier type_identifier ';' | 'typedef' [ 'enum' | 'struct' | 'union' | 'class' | 'interface class' ] type_identifier ';'
We match either kind of type declaration and return it as a vl-description-p.
Function:
(defun vl-parse-type-declaration-fn (atts tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (declare (xargs :guard (and (vl-atts-p atts) (vl-is-token? :vl-kwd-typedef)))) (let ((__function__ 'vl-parse-type-declaration)) (declare (ignorable __function__)) (b* ((backup (vl-tokstream-save)) ((mv erp fwd tokstream) (vl-parse-fwd-typedef atts)) ((unless erp) (mv erp fwd tokstream)) (tokstream (vl-tokstream-restore backup))) (seq tokstream (typedef := (vl-match)) (datatype := (vl-parse-datatype)) (id := (vl-match-token :vl-idtoken)) (udims := (vl-parse-0+-variable-dimensions)) (semi := (vl-match-token :vl-semi)) (return-raw (b* ((val (make-vl-typedef :name (vl-idtoken->name id) :type (vl-datatype-update-udims udims datatype) :minloc (vl-token->loc typedef) :maxloc (vl-token->loc semi) :atts atts))) (mv nil val tokstream)))))))
Theorem:
(defthm vl-parse-type-declaration-fails-gracefully (implies (mv-nth 0 (vl-parse-type-declaration atts)) (not (mv-nth 1 (vl-parse-type-declaration atts)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-type-declaration (iff (vl-warning-p (mv-nth 0 (vl-parse-type-declaration atts))) (mv-nth 0 (vl-parse-type-declaration atts))))
Theorem:
(defthm vl-parse-type-declaration-result (implies (and (and (force (vl-atts-p atts)) (force (vl-is-token? :vl-kwd-typedef)))) (equal (vl-description-p (mv-nth 1 (vl-parse-type-declaration atts))) (not (mv-nth 0 (vl-parse-type-declaration atts))))))
Theorem:
(defthm vl-parse-type-declaration-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-type-declaration atts))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-type-declaration atts))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-type-declaration atts))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm vl-typedef-p-of-vl-parse-type-declaration (b* (((mv err val ?tokstream) (vl-parse-type-declaration atts))) (implies (not err) (equal (vl-typedef-p val) (eq (tag val) :vl-typedef)))))