Parse
(vl-parse-property-formal-type-and-id &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Relevant grammar rules
sequence_formal_type ::= 'untyped' | 'sequence' | data_type_or_implicit property_formal_type ::= sequence_formal_type | 'property'
We match
Function:
(defun vl-parse-property-formal-type-and-id-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-property-formal-type-and-id)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-some-token? '(:vl-kwd-untyped :vl-kwd-sequence :vl-kwd-property)) (type := (vl-match)) (id := (vl-match-token :vl-idtoken)) (return (cons (make-vl-coretype :name (case (vl-token->type type) (:vl-kwd-untyped :vl-untyped) (:vl-kwd-sequence :vl-sequence) (:vl-kwd-property :vl-property))) id))) (return-raw (b* ((backup (vl-tokstream-save)) ((mv erp ans tokstream) (seq tokstream (type := (vl-parse-datatype-or-implicit)) (id := (vl-match-token :vl-idtoken)) (return (cons type id)))) ((unless erp) (mv erp ans tokstream)) (tokstream (vl-tokstream-restore backup))) (seq tokstream (id := (vl-match-token :vl-idtoken)) (return (cons (make-vl-coretype :name :vl-logic) id))))))))
Theorem:
(defthm vl-parse-property-formal-type-and-id-fails-gracefully (implies (mv-nth 0 (vl-parse-property-formal-type-and-id)) (not (mv-nth 1 (vl-parse-property-formal-type-and-id)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-property-formal-type-and-id (iff (vl-warning-p (mv-nth 0 (vl-parse-property-formal-type-and-id))) (mv-nth 0 (vl-parse-property-formal-type-and-id))))
Theorem:
(defthm vl-parse-property-formal-type-and-id-result (implies (and (not (mv-nth 0 (vl-parse-property-formal-type-and-id))) (and t)) (and (consp (mv-nth 1 (vl-parse-property-formal-type-and-id))) (vl-datatype-p (car (mv-nth 1 (vl-parse-property-formal-type-and-id)))) (vl-idtoken-p (cdr (mv-nth 1 (vl-parse-property-formal-type-and-id)))))))
Theorem:
(defthm vl-parse-property-formal-type-and-id-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-property-formal-type-and-id))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-property-formal-type-and-id))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-property-formal-type-and-id))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))