Match the very simplest
(vl-parse-very-simple-type &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
The rule from SystemVerilog-2012 is:
simple_type ::= integer_type | non_integer_type | ps_type_identifier | ps_parameter_identifier
This function matches only the first two variants, which are completely trivial:
integer_type ::= integer_vector_type | integer_atom_type integer_vector_type ::= 'bit' | 'logic' | 'reg' integer_atom_type ::= 'byte' | 'shortint' | 'int' | 'longint' | 'integer' | 'time' non_integer_type ::= 'shortreal' | 'real' | 'realtime'
Function:
(defun vl-parse-very-simple-type-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-very-simple-type)) (declare (ignorable __function__)) (seq tokstream (type := (vl-match-some-token *vl-very-simple-type-tokens*)) (return (cdr (assoc (vl-token->type type) *vl-very-simple-type-table*))))))
Theorem:
(defthm vl-parse-very-simple-type-fails-gracefully (implies (mv-nth 0 (vl-parse-very-simple-type)) (not (mv-nth 1 (vl-parse-very-simple-type)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-very-simple-type (iff (vl-warning-p (mv-nth 0 (vl-parse-very-simple-type))) (mv-nth 0 (vl-parse-very-simple-type))))
Theorem:
(defthm vl-parse-very-simple-type-result (implies (and t) (equal (vl-expr-p (mv-nth 1 (vl-parse-very-simple-type))) (not (mv-nth 0 (vl-parse-very-simple-type))))))
Theorem:
(defthm vl-parse-very-simple-type-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-very-simple-type))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-very-simple-type))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-very-simple-type))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm vl-parse-very-simple-type-when-eof (b* (((mv errmsg ?val ?new-tokstream) (vl-parse-very-simple-type))) (implies (atom (vl-tokstream->tokens)) errmsg)))