		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-read-until-end-of-define

Read from `define until the end of the line.

Signature
(vl-read-until-end-of-define echars ppst) → (mv successp prefix remainder ppst)
Arguments: echars — Guard (vl-echarlist-p echars).
Returns: successp — Type (booleanp successp).; prefix — Type (vl-echarlist-p prefix).; remainder — Type (vl-echarlist-p remainder).

This is really tricky! See preprocessor-ifdef-minutia.

The initial echars are everything past the macro name, e.g., for:

`define foo blah...

the initial echars will be [space]blah..., and for

`define max(a,b) blah...

the initial echars will be (a,b) blah.... NCVerilog allows newlines within the macro arguments, e.g., it allows you to write things like

`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.

Definitions and Theorems

Function: vl-read-until-end-of-define

(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: booleanp-of-vl-read-until-end-of-define.successp

(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: vl-echarlist-p-of-vl-read-until-end-of-define.prefix

(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: vl-echarlist-p-of-vl-read-until-end-of-define.remainder

(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: true-listp-of-vl-read-until-end-of-define-prefix

(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: true-listp-of-vl-read-until-end-of-define-remainder

(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: acl2-count-of-vl-read-until-end-of-define-weak

(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: acl2-count-of-vl-read-until-end-of-define-strong

(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)))