Matches
(vl-parse-dist-item &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
See vl-distitem. Grammar rules:
dist_item ::= value_range [ dist_weight ] dist_weight ::= ':=' expression | ':/' expression value_range ::= expression | [ expression : expression ]
Function:
(defun vl-parse-dist-item-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-dist-item)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-lbrack) (lbrack := (vl-match))) (left := (vl-parse-expression)) (when lbrack (:= (vl-match-token :vl-colon)) (right := (vl-parse-expression)) (:= (vl-match-token :vl-rbrack))) (when (vl-is-some-token? '(:vl-coloneq :vl-colonslash)) (type := (vl-match)) (weight := (vl-parse-expression))) (return (make-vl-distitem :left left :right right :type (cond ((not type) :vl-weight-each) ((eq (vl-token->type type) :vl-coloneq) :vl-weight-each) ((eq (vl-token->type type) :vl-colonslash) :vl-weight-total) (t (progn$ (impossible) :vl-weight-each))) :weight (or weight (vl-make-index 1)))))))
Theorem:
(defthm vl-parse-dist-item-fails-gracefully (implies (mv-nth 0 (vl-parse-dist-item)) (not (mv-nth 1 (vl-parse-dist-item)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-dist-item (iff (vl-warning-p (mv-nth 0 (vl-parse-dist-item))) (mv-nth 0 (vl-parse-dist-item))))
Theorem:
(defthm vl-parse-dist-item-result (implies (and t) (equal (vl-distitem-p (mv-nth 1 (vl-parse-dist-item))) (not (mv-nth 0 (vl-parse-dist-item))))))
Theorem:
(defthm vl-parse-dist-item-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-dist-item))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-dist-item))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-dist-item))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))