Horrible. To support edge_indicator, match two
(vl-parse-two-level-symbols &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Function:
(defun vl-parse-two-level-symbols-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-two-level-symbols)) (declare (ignorable __function__)) (seq tokstream (when (and (consp (vl-tokstream->tokens)) (vl-udp-level-symbol-token-p (car (vl-tokstream->tokens)))) (prev := (vl-parse-level-symbol)) (next := (vl-parse-level-symbol)) (return (make-vl-udpedge :prev prev :next next))) (when (and (consp (vl-tokstream->tokens)) (vl-01-integer-token-p (car (vl-tokstream->tokens)))) (:= (vl-match)) (return (make-vl-udpedge :prev :vl-udp-0 :next :vl-udp-1))) (when (and (consp (vl-tokstream->tokens)) (vl-10-integer-token-p (car (vl-tokstream->tokens)))) (:= (vl-match)) (return (make-vl-udpedge :prev :vl-udp-1 :next :vl-udp-0))) (return-raw (vl-parse-error "Unsupported two level_symbols")))))
Theorem:
(defthm vl-parse-two-level-symbols-fails-gracefully (implies (mv-nth 0 (vl-parse-two-level-symbols)) (not (mv-nth 1 (vl-parse-two-level-symbols)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-two-level-symbols (iff (vl-warning-p (mv-nth 0 (vl-parse-two-level-symbols))) (mv-nth 0 (vl-parse-two-level-symbols))))
Theorem:
(defthm vl-parse-two-level-symbols-result (implies (and t) (equal (vl-udpentry-p (mv-nth 1 (vl-parse-two-level-symbols))) (not (mv-nth 0 (vl-parse-two-level-symbols))))))
Theorem:
(defthm vl-parse-two-level-symbols-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-two-level-symbols))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-two-level-symbols))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-two-level-symbols))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))