		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-expand-define

Expand uses of defines like `foo and `max(a,b).

Signature
(vl-expand-define name echars loc ppst) → (mv successp new-echars ppst)
Arguments: name — Name of the directive we've just read, like "foo" for `foo.
Guard (stringp name).; echars — Remaining text after the name. For simple macros like `foo we will just need to append the definition's body onto these characters. For macros with arguments we will need to extract the actuals from these characters.
Guard (vl-echarlist-p echars).; loc — Location for error messages and for the resulting expansion text.
Guard (vl-location-p loc).
Returns: successp — Type (booleanp successp).; new-echars — On success, the updated characters with the macro invocation replaced by its expansion.
Type (vl-echarlist-p new-echars).

Note that variables in `define are lazy, e.g., if you do:

`define foo 3
`define bar `foo
`define foo 4

Then from here on `bar should also expand to 4. To accomplish this, we're going to modify the echars that are remaining in the input. That is, the output of vl-expand-define is going to get preprocessed. This does not always terminate! (Hence the termination counter on vl-preprocess-loop.

Subtle. If we simply inserted the echars stored in the defines table, then locations on these characters would refer to their original position in the file. This might lead to confusing error messages, telling you that something is wrong and showing you line numbers for a `define that looks just fine. So instead, we change all of the locations for the inserted text to point at the grave character for the macro usage. That is, if `foo occurs on line 37 from characters 5 through 8, then we'll make every character of foo's expansion occur at 37:5.

Definitions and Theorems

Function: vl-expand-define

(defun vl-expand-define (name echars loc ppst)
 (declare (xargs :stobjs (ppst)))
 (declare (xargs :guard (and (stringp name)
                             (vl-echarlist-p echars)
                             (vl-location-p loc))))
 (let ((__function__ 'vl-expand-define))
  (declare (ignorable __function__))
  (b*
   ((echars (vl-echarlist-fix echars))
    (lookup (vl-find-define name (vl-ppst->defines)))
    ((unless lookup)
     (let ((ppst (vl-ppst-fatal :msg "~a0: `~s1 is not defined."
                                :args (list loc name))))
       (mv nil echars ppst)))
    ((vl-define lookup))
    ((when (atom lookup.formals))
     (b* (((mv okp rev-replacement-body ppst)
           (vl-substitute-into-macro-text
                (vl-change-echarlist-locations
                     (vl-echarlist-from-str lookup.body)
                     loc)
                nil name loc nil ppst))
          ((unless okp) (mv nil echars ppst))
          (replacement-body (rev rev-replacement-body))
          (echars (append replacement-body echars)))
       (mv t echars ppst)))
    ((mv ?ws echars)
     (vl-read-while-whitespace echars))
    ((unless (and (consp echars)
                  (eql (vl-echar->char (car echars))
                       #\()))
     (let ((ppst (vl-ppst-fatal :msg "~a0: `~s1 requires arguments."
                                :args (list loc name))))
       (mv nil echars ppst)))
    (echars (cdr echars))
    ((mv successp actuals echars ppst)
     (vl-parse-define-actuals name echars loc ppst))
    ((unless successp) (mv nil echars ppst))
    ((mv successp subst ppst)
     (vl-line-up-define-formals-and-actuals
          lookup.formals actuals name loc ppst))
    ((unless successp) (mv nil echars ppst))
    ((mv okp rev-replacement-body ppst)
     (vl-substitute-into-macro-text
          (vl-change-echarlist-locations
               (vl-echarlist-from-str lookup.body)
               loc)
          subst name loc nil ppst))
    ((unless okp) (mv nil echars ppst))
    (replacement-body (rev rev-replacement-body))
    (echars (append replacement-body echars)))
   (mv t echars ppst))))

Theorem: booleanp-of-vl-expand-define.successp

(defthm booleanp-of-vl-expand-define.successp
  (b* (((mv ?successp ?new-echars ?ppst)
        (vl-expand-define name echars loc ppst)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-echarlist-p-of-vl-expand-define.new-echars

(defthm vl-echarlist-p-of-vl-expand-define.new-echars
  (b* (((mv ?successp ?new-echars ?ppst)
        (vl-expand-define name echars loc ppst)))
    (vl-echarlist-p new-echars))
  :rule-classes :rewrite)

Subtopics

Vl-parse-define-actual: Collect a single argument to a text macro, like `max(a+b, c).
Vl-parse-define-actuals: Collect the arguments to a macro, like `max(a+b, c).