		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 defines echars config loc) → (mv successp new-echars)
Arguments: name — Name of the directive we've just read, like "foo" for `foo.
Guard (stringp name).; defines — All definitions we currently have.
Guard (vl-defines-p defines).; 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).; config — Guard (vl-loadconfig-p config).; 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), given (force (vl-echarlist-p 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 defines echars config loc)
 (declare (xargs :guard (and (stringp name)
                             (vl-defines-p defines)
                             (vl-echarlist-p echars)
                             (vl-loadconfig-p config)
                             (vl-location-p loc))))
 (let
  ((__function__ 'vl-expand-define))
  (declare (ignorable __function__))
  (b*
   ((lookup (vl-find-define name defines))
    ((unless lookup)
     (mv (cw "Preprocessor error (~s0): `~s1 is not defined.~%"
             (vl-location-string loc)
             name)
         echars))
    ((vl-define lookup))
    ((when (atom lookup.formals))
     (b*
      ((body-str lookup.body)
       (body-echars (vl-echarlist-from-str body-str))
       (body-fixed (vl-change-echarlist-locations body-echars loc)))
      (mv t (append body-fixed echars))))
    ((mv ?ws echars)
     (vl-read-while-whitespace echars))
    ((unless (and (consp echars)
                  (eql (vl-echar->char (car echars))
                       #\()))
     (mv (cw "Preprocessor error (~s0): `~s1 requires arguments.~%"
             (vl-location-string loc)
             name)
         echars))
    (echars (cdr echars))
    ((mv successp actuals echars)
     (vl-parse-define-actuals name echars config loc))
    ((unless successp) (mv nil echars))
    ((mv successp subst)
     (vl-line-up-define-formals-and-actuals
          lookup.formals actuals name loc))
    ((unless successp) (mv nil echars))
    ((mv okp rev-replacement-body)
     (vl-substitute-into-macro-text
          (vl-echarlist-from-str lookup.body)
          subst name loc config nil))
    ((unless okp) (mv nil echars))
    (replacement-body (rev rev-replacement-body))
    (echars (append replacement-body echars)))
   (mv t echars))))

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

(defthm booleanp-of-vl-expand-define.successp
        (b* (((mv ?successp ?new-echars)
              (vl-expand-define name defines echars config loc)))
            (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
  (implies (force (vl-echarlist-p echars))
           (b* (((mv ?successp ?new-echars)
                 (vl-expand-define name defines echars config loc)))
               (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).