Matches
(vl-parse-boolean-abbrev &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Relevant grammar rules:
boolean_abbrev ::= consecutive_repetition | non_consecutive_repetition | goto_repetition consecutive_repetition ::= '[*' const_or_range_expression ']' | '[*]' | '[+]' non_consecutive_repetition ::= ['=' const_or_range_expression ] goto_repetition ::= ['->' const_or_range_expression ] const_or_range_expression ::= constant_expression | cycle_delay_const_range_expression cycle_delay_const_range_expression ::= constant_expression ':' constant_expression | constant_expression ':' '$'
Function:
(defun vl-parse-boolean-abbrev-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-boolean-abbrev)) (declare (ignorable __function__)) (seq tokstream (:= (vl-match-token :vl-lbrack)) (when (vl-is-token? :vl-plus) (:= (vl-match)) (:= (vl-match-token :vl-rbrack)) (return (make-vl-repetition :type :vl-repetition-consecutive :left (vl-make-index 1) :right *vl-end-of-sequence-$*))) (type := (vl-match-some-token '(:vl-times :vl-arrow :vl-equalsign))) (when (and (eq (vl-token->type type) :vl-times) (vl-is-token? :vl-rbrack)) (:= (vl-match)) (return (make-vl-repetition :type :vl-repetition-consecutive :left (vl-make-index 0) :right *vl-end-of-sequence-$*))) (left := (vl-parse-expression)) (when (vl-is-token? :vl-colon) (:= (vl-match)) (right := (vl-parse-expression))) (:= (vl-match-token :vl-rbrack)) (return (make-vl-repetition :type (case (vl-token->type type) (:vl-times :vl-repetition-consecutive) (:vl-arrow :vl-repetition-goto) (:vl-equalsign :vl-repetition-nonconsecutive)) :left left :right right)))))
Theorem:
(defthm vl-parse-boolean-abbrev-fails-gracefully (implies (mv-nth 0 (vl-parse-boolean-abbrev)) (not (mv-nth 1 (vl-parse-boolean-abbrev)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-boolean-abbrev (iff (vl-warning-p (mv-nth 0 (vl-parse-boolean-abbrev))) (mv-nth 0 (vl-parse-boolean-abbrev))))
Theorem:
(defthm vl-parse-boolean-abbrev-result (implies (and t) (equal (vl-repetition-p (mv-nth 1 (vl-parse-boolean-abbrev))) (not (mv-nth 0 (vl-parse-boolean-abbrev))))))
Theorem:
(defthm vl-parse-boolean-abbrev-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-boolean-abbrev))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-boolean-abbrev))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-boolean-abbrev))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))