Read from
(vl-read-until-end-of-define echars ppst) → (mv successp prefix remainder ppst)
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 ppst) (declare (xargs :stobjs (ppst))) (declare (xargs :guard (vl-echarlist-p echars))) (let ((__function__ 'vl-read-until-end-of-define)) (declare (ignorable __function__)) (b* ((echars (vl-echarlist-fix echars)) ((when (atom echars)) (mv t nil echars ppst)) (char1 (vl-echar->char (first echars))) ((when (eql char1 #\Newline)) (mv t nil echars ppst)) ((when (eql char1 #\`)) (b* (((when (and (consp (cdr echars)) (member (vl-echar->char (second echars)) '(#\" #\`)))) (b* (((mv successp text remainder ppst) (vl-read-until-end-of-define (cddr echars) ppst)) ((unless successp) (mv nil nil echars ppst)) (prefix (list* (first echars) (second echars) text))) (mv t prefix remainder ppst))) ((when (and (consp (cdr echars)) (consp (cddr echars)) (consp (cdddr echars)) (eql (vl-echar->char (second echars)) #\\) (eql (vl-echar->char (third echars)) #\`) (eql (vl-echar->char (fourth echars)) #\"))) (b* (((mv successp text remainder ppst) (vl-read-until-end-of-define (cddddr echars) ppst)) ((unless successp) (mv nil nil echars ppst)) (prefix (list* (first echars) (second echars) (third echars) (fourth echars) text))) (mv t prefix remainder ppst))) ((mv name prefix remainder) (vl-read-identifier (cdr echars))) ((unless name) (let ((ppst (vl-ppst-fatal :msg "~a0: no name following back-quote/grave character (`)." :args (list (vl-echar->loc (car echars)))))) (mv nil nil echars ppst))) ((mv successp text remainder ppst) (vl-read-until-end-of-define remainder ppst)) ((unless successp) (mv nil nil echars ppst))) (mv t (cons (car echars) (append prefix text)) remainder ppst))) ((when (eql char1 #\")) (b* (((mv string prefix remainder) (vl-read-string echars (vl-lexstate-init (vl-ppst->config)))) ((unless string) (mv nil nil echars ppst)) ((mv successp text remainder ppst) (vl-read-until-end-of-define remainder ppst)) ((unless successp) (mv nil nil echars ppst))) (mv t (append prefix text) remainder ppst))) ((when (eql char1 #\\)) (b* (((when (vl-matches-string-p "//" (cdr echars))) (let ((ppst (vl-ppst-fatal :msg "~a0: we cowardly do not allow '//' in ~ defines." :args (list (vl-echar->loc (car echars)))))) (mv nil nil echars ppst))) ((when (vl-matches-string-p "/*" (cdr echars))) (let ((ppst (vl-ppst-fatal :msg "~a0: we cowardly do not allow '/*' in ~ defines." :args (list (vl-echar->loc (car echars)))))) (mv nil nil echars ppst))) ((when (vl-matches-string-p *nls* (cdr echars))) (b* (((mv successp text remainder ppst) (vl-read-until-end-of-define (cddr echars) ppst)) ((unless successp) (mv nil nil echars ppst))) (mv t (cons (second echars) text) remainder ppst))) ((mv name prefix remainder) (vl-read-escaped-identifier echars)) ((unless name) (let ((ppst (vl-ppst-fatal :msg "~a0: stray backslash?" :args (list (vl-echar->loc (car echars)))))) (mv nil nil echars ppst))) ((mv successp text remainder ppst) (vl-read-until-end-of-define remainder ppst)) ((unless successp) (mv nil nil echars ppst))) (mv t (append prefix text) remainder ppst))) ((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 ppst)) ((when (and (consp prefix) (eql (vl-echar->char (car (last prefix))) #\\))) (b* ((ppst (vl-ppst-warn :type :vl-warn-line-continuation :msg "~a0: within a `define, a single-line ~ comment ends with a backslash. Treating ~ this as a line continuation." :args (list (vl-echar->loc (car echars))))) (new-space (change-vl-echar (car remainder) :char #\Space)) ((mv successp text remainder ppst) (vl-read-until-end-of-define (cdr remainder) ppst)) ((unless successp) (mv nil nil echars ppst))) (mv t (cons new-space text) remainder ppst)))) (mv t nil remainder ppst))) ((vl-matches-string-p "/*" echars) (b* (((mv successp prefix remainder) (vl-read-through-literal "*/" (cddr echars))) ((unless successp) (let ((ppst (vl-ppst-fatal :msg "~a0: block comment is never closed." :args (list (vl-echar->loc (car echars)))))) (mv nil nil echars ppst))) ((when (member #\Newline (vl-echarlist->chars prefix))) (let ((ppst (vl-ppst-fatal :msg "~a0: block comment inside a define is not ~ closed before end of line." :args (list (vl-echar->loc (car echars)))))) (mv nil nil echars ppst))) ((mv successp text remainder ppst) (vl-read-until-end-of-define remainder ppst)) ((unless successp) (mv nil nil echars ppst))) (mv t (append (list* (first echars) (second echars) prefix) text) remainder ppst))) (t (b* (((mv successp text remainder ppst) (vl-read-until-end-of-define (cdr echars) ppst)) ((unless successp) (mv nil nil echars ppst))) (mv t (cons (car echars) text) remainder ppst))))) ((mv successp text remainder ppst) (vl-read-until-end-of-define (cdr echars) ppst)) ((unless successp) (mv nil nil echars ppst))) (mv t (cons (car echars) text) remainder ppst))))
Theorem:
(defthm booleanp-of-vl-read-until-end-of-define.successp (b* (((mv ?successp ?prefix ?remainder ?ppst) (vl-read-until-end-of-define echars ppst))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-echarlist-p-of-vl-read-until-end-of-define.prefix (b* (((mv ?successp ?prefix ?remainder ?ppst) (vl-read-until-end-of-define echars ppst))) (vl-echarlist-p prefix)) :rule-classes :rewrite)
Theorem:
(defthm vl-echarlist-p-of-vl-read-until-end-of-define.remainder (b* (((mv ?successp ?prefix ?remainder ?ppst) (vl-read-until-end-of-define echars ppst))) (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 (true-listp (mv-nth 2 (vl-read-until-end-of-define echars config))) :rule-classes :type-prescription)
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 (vl-echarlist-fix 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 (vl-echarlist-fix echars)))) :rule-classes ((:rewrite) (:linear)))