(vl-parse-define-formal-arguments text config starting-loc) → (mv successp formals body)
Function:
(defun vl-parse-define-formal-arguments (text config starting-loc) (declare (xargs :guard (and (vl-echarlist-p text) (vl-loadconfig-p config) (vl-location-p starting-loc)))) (let ((__function__ 'vl-parse-define-formal-arguments)) (declare (ignorable __function__)) (b* (((when (atom text)) (mv (cw "Preprocessor error (~s0): `define arguments are not closed.~%" (vl-location-string starting-loc)) nil nil)) ((mv ?ws rest) (vl-read-while-whitespace text)) ((mv id rest) (vl-read-simple-identifier rest)) ((unless id) (mv (cw "Preprocessor error (~s0): invalid `define argument name~%" (vl-location-string (vl-echar->loc (car text)))) nil nil)) (name1 (vl-echarlist->string id)) ((when (vl-keyword-lookup name1 (vl-lexstate->kwdtable (vl-lexstate-init config)))) (mv (cw "Preprocessor error (~s0): keyword ~s1 not permitted as `define argument~%" (vl-location-string (vl-echar->loc (car text))) name1) nil nil)) ((mv ?ws rest) (vl-read-while-whitespace rest)) (formal1 (make-vl-define-formal :name name1 :default "")) ((when (and (consp rest) (eql (vl-echar->char (car rest)) #\)))) (mv t (list formal1) (cdr rest))) ((unless (and (consp rest) (eql (vl-echar->char (car rest)) #\,))) (mv (cw "Preprocessor error (~s0): expected next `define argument or end of arguments.~%" (vl-location-string (if (consp rest) (vl-echar->loc (car rest)) (vl-echar->loc (car text))))) nil nil)) (starting-loc (vl-echar->loc (car rest))) (rest (cdr rest)) ((mv rest-okp rest-formals body) (vl-parse-define-formal-arguments rest config starting-loc)) ((unless rest-okp) (mv nil nil nil)) (formals (cons formal1 rest-formals))) (mv t formals body))))
Theorem:
(defthm booleanp-of-vl-parse-define-formal-arguments.successp (b* (((mv ?successp ?formals ?body) (vl-parse-define-formal-arguments text config starting-loc))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-define-formallist-p-of-vl-parse-define-formal-arguments.formals (b* (((mv ?successp ?formals ?body) (vl-parse-define-formal-arguments text config starting-loc))) (vl-define-formallist-p formals)) :rule-classes :rewrite)
Theorem:
(defthm vl-echarlist-p-of-vl-parse-define-formal-arguments.body (implies (force (vl-echarlist-p text)) (b* (((mv ?successp ?formals ?body) (vl-parse-define-formal-arguments text config starting-loc))) (vl-echarlist-p body))) :rule-classes :rewrite)