Compatible with seq. Consume and return a token if it is of the given type, but if not, don't consume anything and return nil.
(vl-maybe-match-token type &key (tokstream 'tokstream)) → (mv errmsg? token new-tokstream)
Function:
(defun vl-maybe-match-token-fn (type tokstream) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-tokentype-p type))) (let ((__function__ 'vl-maybe-match-token)) (declare (ignorable __function__)) (b* ((tokens (vl-tokstream->tokens)) ((when (atom tokens)) (mv nil nil tokstream)) (token1 (car tokens)) ((unless (eq type (vl-token->type token1))) (mv nil nil tokstream)) (tokstream (vl-tokstream-pop))) (mv nil token1 tokstream))))
Theorem:
(defthm return-type-of-vl-maybe-match-token.errmsg? (b* (((mv ?errmsg? ?token ?new-tokstream) (vl-maybe-match-token-fn type tokstream))) (equal errmsg? nil)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-maybe-match-token.token (b* (((mv ?errmsg? ?token ?new-tokstream) (vl-maybe-match-token-fn type tokstream))) (and (iff (vl-token-p token) (vl-is-token? type)) (iff token (vl-is-token? type)))) :rule-classes :rewrite)
Theorem:
(defthm vl-maybe-match-token-fails-gracefully (implies (not (vl-is-token? type)) (equal (mv-nth 1 (vl-maybe-match-token type)) nil)))
Theorem:
(defthm vl-token->type-of-vl-maybe-match-token (implies (vl-is-token? type) (equal (vl-token->type (mv-nth 1 (vl-maybe-match-token type))) type)))
Theorem:
(defthm vl-maybe-match-token-count-strong-on-value (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-maybe-match-token type))) (vl-tokstream-measure)) (implies (mv-nth 1 (vl-maybe-match-token type)) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-maybe-match-token type))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))