(vl-parse-core-data-type &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Function:
(defun vl-parse-core-data-type-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (declare (xargs :guard (vl-is-some-token? *vl-core-data-type-keywords*))) (let ((__function__ 'vl-parse-core-data-type)) (declare (ignorable __function__)) (b* ((entry (vl-coretypekwd->info (vl-token->type (car (vl-tokstream->tokens))))) ((vl-coredatatype-info entry) entry)) (seq tokstream (:= (vl-match-any)) (when (and entry.takes-signingp (vl-is-some-token? '(:vl-kwd-signed :vl-kwd-unsigned))) (signing := (vl-match))) (when entry.takes-dimensionsp (dims := (vl-parse-0+-packed-dimensions))) (return (make-vl-coretype :name entry.coretypename :signedp (if signing (if (eq (vl-token->type signing) :vl-kwd-signed) t nil) entry.default-signedp) :pdims dims))))))
Theorem:
(defthm vl-parse-core-data-type-fails-gracefully (implies (mv-nth 0 (vl-parse-core-data-type)) (not (mv-nth 1 (vl-parse-core-data-type)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-core-data-type (iff (vl-warning-p (mv-nth 0 (vl-parse-core-data-type))) (mv-nth 0 (vl-parse-core-data-type))))
Theorem:
(defthm vl-parse-core-data-type-result (implies (and (force (vl-is-some-token? *vl-core-data-type-keywords*))) (equal (vl-datatype-p (mv-nth 1 (vl-parse-core-data-type))) (not (mv-nth 0 (vl-parse-core-data-type))))))
Theorem:
(defthm vl-parse-core-data-type-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-core-data-type))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-core-data-type))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-core-data-type))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))