Compatible with seq. Match any token that is not of the listed types. Causes an error on EOF.
(vl-match-any-except types &key (function '__function__) (tokstream 'tokstream)) → (mv errmsg? token new-tokstream)
Function:
(defun vl-match-any-except-fn (types function tokstream) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (and (true-listp types) (symbolp function)))) (let ((__function__ 'vl-match-any-except)) (declare (ignorable __function__)) (b* ((tokens (vl-tokstream->tokens)) ((when (atom tokens)) (vl-parse-error "Unexpected EOF." :function function)) (token1 (car tokens)) ((when (member-eq (vl-token->type token1) types)) (mv (make-vl-warning :type :vl-parse-error :msg "Parse error at ~a0: unexpected ~s1." :args (list (vl-token->loc token1) (vl-token->type token1)) :fn function :fatalp t) nil tokstream)) (tokstream (vl-tokstream-update-tokens (cdr tokens)))) (mv nil token1 tokstream))))
Theorem:
(defthm return-type-of-vl-match-any-except.errmsg? (b* (((mv ?errmsg? ?token ?new-tokstream) (vl-match-any-except-fn types function tokstream))) (iff (vl-warning-p errmsg?) errmsg?)) :rule-classes :rewrite)
Theorem:
(defthm vl-match-any-except-fails-when-vl-is-some-token? (iff (mv-nth 0 (vl-match-any-except types)) (or (atom (vl-tokstream->tokens)) (vl-is-some-token? types))))
Theorem:
(defthm vl-match-any-except-fails-gracefully (implies (or (atom (vl-tokstream->tokens)) (vl-is-some-token? types)) (equal (mv-nth 1 (vl-match-any-except types)) nil)))
Theorem:
(defthm vl-match-any-except-when-atom-of-tokens (implies (atom (vl-tokstream->tokens)) (equal (mv-nth 2 (vl-match-any-except types)) tokstream)))
Theorem:
(defthm vl-token-p-of-vl-match-any-except (implies (and (not (vl-is-some-token? types)) (consp (vl-tokstream->tokens))) (vl-token-p (mv-nth 1 (vl-match-any-except types)))))
Theorem:
(defthm vl-match-any-except-count-strong-on-value (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-match-any-except types))) (vl-tokstream-measure)) (implies (mv-nth 1 (vl-match-any-except types)) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-match-any-except types))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm equal-of-vl-match-any-except-fn-count (equal (equal (vl-tokstream-measure :tokstream (mv-nth 2 (vl-match-any-except types))) (vl-tokstream-measure)) (if (mv-nth 0 (vl-match-any-except types)) t nil)))