Parses, e.g.,
(vl-parse-operator-assignment/inc/dec &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Function:
(defun vl-parse-operator-assignment/inc/dec-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-operator-assignment/inc/dec)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-some-token? '(:vl-plusplus :vl-minusminus)) (op := (vl-match)) (var := (vl-parse-variable-lvalue)) (return (cons var (vl-inc-or-dec-expr var (vl-token->type op))))) (var := (vl-parse-variable-lvalue)) (when (vl-is-some-token? '(:vl-plusplus :vl-minusminus)) (op := (vl-match)) (return (cons var (vl-inc-or-dec-expr var (vl-token->type op))))) (eq := (vl-match-some-token *vl-assignment-operators*)) (rhs := (vl-parse-expression)) (return (cons var (vl-assign-op-expr var (vl-token->type eq) rhs))))))
Theorem:
(defthm vl-parse-operator-assignment/inc/dec-fails-gracefully (implies (mv-nth 0 (vl-parse-operator-assignment/inc/dec)) (not (mv-nth 1 (vl-parse-operator-assignment/inc/dec)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-operator-assignment/inc/dec (iff (vl-warning-p (mv-nth 0 (vl-parse-operator-assignment/inc/dec))) (mv-nth 0 (vl-parse-operator-assignment/inc/dec))))
Theorem:
(defthm vl-parse-operator-assignment/inc/dec-result (implies (and (not (mv-nth 0 (vl-parse-operator-assignment/inc/dec))) (and t)) (and (consp (mv-nth 1 (vl-parse-operator-assignment/inc/dec))) (vl-expr-p (car (mv-nth 1 (vl-parse-operator-assignment/inc/dec)))) (vl-expr-p (cdr (mv-nth 1 (vl-parse-operator-assignment/inc/dec)))))))
Theorem:
(defthm vl-parse-operator-assignment/inc/dec-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-operator-assignment/inc/dec))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-operator-assignment/inc/dec))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-operator-assignment/inc/dec))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))