Read from
(vl-read-until-end-of-define echars config) → (mv successp prefix remainder)
This is really tricky! See preprocessor-ifdef-minutia.
The initial
`define foo blah...
the initial
`define max(a,b) blah...
the initial
`define sum(a, b) a+b
But VCS rejects this. I think it's reasonable to reject this, too, so we basically just read the whole line, then split it up into any arguments versus non-arguments pieces.
Function:
(defun vl-read-until-end-of-define (echars config) (declare (xargs :guard (and (vl-echarlist-p echars) (vl-loadconfig-p config)))) (let ((__function__ 'vl-read-until-end-of-define)) (declare (ignorable __function__)) (b* (((when (atom echars)) (mv t nil echars)) (char1 (vl-echar->char (first echars))) ((when (eql char1 #\Newline)) (mv t nil echars)) ((when (eql char1 #\`)) (b* (((mv name prefix remainder) (vl-read-identifier (cdr echars))) ((unless name) (mv (cw "Preprocessor error (~s0): no name following ~ back-quote/grave character (`).~%" (vl-location-string (vl-echar->loc (car echars)))) nil echars)) ((when (vl-is-compiler-directive-p name)) (mv (cw "Preprocessor error (~s0): we cowardly do not allow ~ `~s1 in defines.~%" (vl-location-string (vl-echar->loc (car echars))) name) nil echars)) ((mv successp text remainder) (vl-read-until-end-of-define remainder config)) ((unless successp) (mv nil nil echars))) (mv t (cons (car echars) (append prefix text)) remainder))) ((when (eql char1 #\")) (b* (((mv string prefix remainder) (vl-read-string echars (vl-lexstate-init config))) ((unless string) (mv nil nil echars)) ((mv successp text remainder) (vl-read-until-end-of-define remainder config)) ((unless successp) (mv nil nil echars))) (mv t (append prefix text) remainder))) ((when (eql char1 #\\)) (b* (((when (vl-matches-string-p "//" (cdr echars))) (mv (cw "Preprocessor error (~s0): we cowardly do not allow ~ '//' in defines.~%" (vl-location-string (vl-echar->loc (car echars)))) nil echars)) ((when (vl-matches-string-p "/*" (cdr echars))) (mv (cw "Preprocessor error (~s0): we cowardly do not allow ~ '/*' in defines.~%" (vl-location-string (vl-echar->loc (car echars)))) nil echars)) ((when (vl-matches-string-p *nls* (cdr echars))) (b* (((mv successp text remainder) (vl-read-until-end-of-define (cddr echars) config)) ((unless successp) (mv nil nil echars))) (mv t (cons (change-vl-echar (second echars) :char #\Space) text) remainder))) ((mv name prefix remainder) (vl-read-escaped-identifier echars)) ((unless name) (mv (cw "Preprocessor error (~s0): stray backslash?~%" (vl-location-string (vl-echar->loc (car echars)))) nil echars)) ((mv successp text remainder) (vl-read-until-end-of-define remainder config)) ((unless successp) (mv nil nil echars))) (mv t (append prefix text) remainder))) ((when (eql char1 #\/)) (cond ((vl-matches-string-p "//" echars) (b* (((mv successp prefix remainder) (vl-read-until-literal *nls* echars)) ((unless successp) (mv t nil remainder)) ((when (and (consp prefix) (eql (vl-echar->char (car (last prefix))) #\\))) (mv (cw "Preprocessor error (~s0): we cowardly do not allow ~ single-line comments inside defines to end with .~%" (vl-location-string (vl-echar->loc (car echars)))) nil echars))) (mv t nil remainder))) ((vl-matches-string-p "/*" echars) (b* (((mv successp prefix remainder) (vl-read-through-literal "*/" (cddr echars))) ((unless successp) (mv (cw "Preprocessor error (~s0): block comment is never ~ closed.~%" (vl-location-string (vl-echar->loc (car echars)))) nil echars)) ((when (member #\Newline (vl-echarlist->chars prefix))) (mv (cw "Preprocessor error (~s0): block comment inside a ~ define is not closed before end of line.~%" (vl-location-string (vl-echar->loc (car echars)))) nil echars)) ((mv successp text remainder) (vl-read-until-end-of-define remainder config)) ((unless successp) (mv nil nil echars))) (mv t (append (list* (first echars) (second echars) prefix) text) remainder))) (t (b* (((mv successp text remainder) (vl-read-until-end-of-define (cdr echars) config)) ((unless successp) (mv nil nil echars))) (mv t (cons (car echars) text) remainder))))) ((mv successp text remainder) (vl-read-until-end-of-define (cdr echars) config)) ((unless successp) (mv nil nil echars))) (mv t (cons (car echars) text) remainder))))
Theorem:
(defthm booleanp-of-vl-read-until-end-of-define.successp (b* (((mv ?successp ?prefix ?remainder) (vl-read-until-end-of-define echars config))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-echarlist-p-of-vl-read-until-end-of-define.prefix (implies (force (vl-echarlist-p echars)) (b* (((mv ?successp ?prefix ?remainder) (vl-read-until-end-of-define echars config))) (vl-echarlist-p prefix))) :rule-classes :rewrite)
Theorem:
(defthm vl-echarlist-p-of-vl-read-until-end-of-define.remainder (implies (force (vl-echarlist-p echars)) (b* (((mv ?successp ?prefix ?remainder) (vl-read-until-end-of-define echars config))) (vl-echarlist-p remainder))) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-read-until-end-of-define-prefix (true-listp (mv-nth 1 (vl-read-until-end-of-define echars config))) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-of-vl-read-until-end-of-define-remainder (equal (true-listp (mv-nth 2 (vl-read-until-end-of-define echars config))) (true-listp echars)) :rule-classes ((:rewrite)))
Theorem:
(defthm acl2-count-of-vl-read-until-end-of-define-weak (<= (acl2-count (mv-nth 2 (vl-read-until-end-of-define echars config))) (acl2-count echars)) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm acl2-count-of-vl-read-until-end-of-define-strong (implies (mv-nth 1 (vl-read-until-end-of-define echars config)) (< (acl2-count (mv-nth 2 (vl-read-until-end-of-define echars config))) (acl2-count echars))) :rule-classes ((:rewrite) (:linear)))