Match the start of a ``proper''
(vl-match-proper-header-file-start-1 x) → (mv controller loc resume-point)
Here
`ifndef included_foo `define included_foo ... `endif
except that we're a bit more permissive than this because we allow for whitespace and comments before the leading `ifndef and so forth.
Here we only examine the start of the file and, if we match the above
template through
Function:
(defun vl-match-proper-header-file-start-1 (x) (declare (xargs :guard (vl-echarlist-p x))) (let ((__function__ 'vl-match-proper-header-file-start-1)) (declare (ignorable __function__)) (b* ((x (vl-echarlist-fix x)) (x (vl-skip-whitespace/comments x)) (loc (if (consp x) (vl-echar->loc (car x)) *vl-fakeloc*)) ((mv prefix x) (vl-read-literal "`ifndef" x)) ((unless prefix) (mv nil loc nil)) ((mv ws x) (vl-read-while-whitespace x)) ((unless ws) (mv nil loc nil)) ((mv ifndef-name & x) (vl-read-identifier x)) ((unless ifndef-name) (mv nil loc nil)) (x (vl-skip-whitespace/comments x)) (resume-point x) ((mv prefix x) (vl-read-literal "`define" x)) ((unless prefix) (mv nil loc nil)) ((mv ws x) (vl-read-while-whitespace x)) ((unless ws) (mv nil loc nil)) ((mv define-name ?prefix ?remainder) (vl-read-identifier x)) ((unless define-name) (mv nil loc nil)) ((unless (equal ifndef-name define-name)) (mv nil loc nil))) (mv (string-fix ifndef-name) loc resume-point))))
Theorem:
(defthm maybe-stringp-of-vl-match-proper-header-file-start-1.controller (b* (((mv ?controller ?loc ?resume-point) (vl-match-proper-header-file-start-1 x))) (maybe-stringp controller)) :rule-classes :type-prescription)
Theorem:
(defthm vl-location-p-of-vl-match-proper-header-file-start-1.loc (b* (((mv ?controller ?loc ?resume-point) (vl-match-proper-header-file-start-1 x))) (vl-location-p loc)) :rule-classes :rewrite)
Theorem:
(defthm vl-echarlist-p-of-vl-match-proper-header-file-start-1.resume-point (implies (and (vl-echarlist-p x)) (b* (((mv ?controller ?loc ?resume-point) (vl-match-proper-header-file-start-1 x))) (vl-echarlist-p resume-point))) :rule-classes :rewrite)