(vl-parse-package-declaration atts &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Function:
(defun vl-parse-package-declaration-fn (atts tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (declare (xargs :guard (vl-atts-p atts))) (let ((__function__ 'vl-parse-package-declaration)) (declare (ignorable __function__)) (seq tokstream (startkwd := (vl-match-token :vl-kwd-package)) (lifetime := (vl-maybe-parse-lifetime)) (name := (vl-match-token :vl-idtoken)) (return-raw (b* ((backup (vl-tokstream-save)) (orig-warnings (vl-parsestate->warnings (vl-tokstream->pstate))) (tokstream (vl-tokstream-update-pstate (change-vl-parsestate (vl-tokstream->pstate) :warnings nil))) ((mv err pkg tokstream) (seq tokstream (:= (vl-match-token :vl-semi)) (items := (vl-parse-genelements-or-classes-until :vl-kwd-endpackage)) (endkwd := (vl-match-token :vl-kwd-endpackage)) (:= (vl-parse-endblock-name (vl-idtoken->name name) "package/endpackage")) (return (b* ((warnings (vl-parsestate->warnings (vl-tokstream->pstate))) (bad-item (vl-genelementlist-findbad items '(:vl-vardecl :vl-paramdecl :vl-fundecl :vl-taskdecl :vl-typedef :vl-import :vl-letdecl :vl-dpiimport :vl-dpiexport :vl-class :vl-property))) (warnings (if (not bad-item) warnings (fatal :type :vl-bad-package-item :msg "~a0: a package may not contain a ~s1." :args (list bad-item (vl-genelement->short-kind-string bad-item))))) ((vl-genblob c) (vl-sort-genelements items))) (make-vl-package :name (vl-idtoken->name name) :minloc (vl-token->loc startkwd) :maxloc (vl-token->loc endkwd) :lifetime lifetime :vardecls c.vardecls :paramdecls c.paramdecls :fundecls c.fundecls :taskdecls c.taskdecls :typedefs c.typedefs :imports c.imports :classes c.classes :dpiimports c.dpiimports :dpiexports c.dpiexports :warnings warnings :atts atts))))) ((unless err) (let ((tokstream (vl-tokstream-update-pstate (change-vl-parsestate (vl-tokstream->pstate) :warnings orig-warnings)))) (mv nil pkg tokstream))) (errtokens (vl-tokstream->tokens)) (tokstream (vl-tokstream-restore backup))) (seq tokstream (endkwd := (vl-skip-through-endpackage (vl-idtoken->name name))) (return (vl-make-package-with-parse-error (vl-idtoken->name name) (vl-token->loc startkwd) (vl-token->loc endkwd) err errtokens))))))))
Theorem:
(defthm vl-parse-package-declaration-fails-gracefully (implies (mv-nth 0 (vl-parse-package-declaration atts)) (not (mv-nth 1 (vl-parse-package-declaration atts)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-package-declaration (iff (vl-warning-p (mv-nth 0 (vl-parse-package-declaration atts))) (mv-nth 0 (vl-parse-package-declaration atts))))
Theorem:
(defthm vl-parse-package-declaration-result (implies (and (force (vl-atts-p atts))) (equal (vl-package-p (mv-nth 1 (vl-parse-package-declaration atts))) (not (mv-nth 0 (vl-parse-package-declaration atts))))))
Theorem:
(defthm vl-parse-package-declaration-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-package-declaration atts))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-package-declaration atts))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-package-declaration atts))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))