		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-process-define

Handler for define directives.

Signature
(vl-process-define loc echars defines activep config) → (mv successp new-defines remainder)
Arguments: loc — Guard (vl-location-p loc).; echars — Guard (vl-echarlist-p echars).; defines — Guard (vl-defines-p defines).; activep — Guard (booleanp activep).; config — Guard (vl-loadconfig-p config).
Returns: new-defines — Type (vl-defines-p new-defines).; remainder — Type (vl-echarlist-p remainder), given (force (vl-echarlist-p echars)).

We assume that `define has just been read and echars is the text which comes right after the `define directive. We read the name and text for this new macro definition, and update the defines table appropriately if activep is set.

Definitions and Theorems

Function: vl-process-define

(defun vl-process-define (loc echars defines activep config)
 (declare (xargs :guard (and (vl-location-p loc)
                             (vl-echarlist-p echars)
                             (vl-defines-p defines)
                             (booleanp activep)
                             (vl-loadconfig-p config))))
 (let ((__function__ 'vl-process-define))
  (declare (ignorable __function__))
  (b*
   ((defines (vl-defines-fix defines))
    ((mv & remainder)
     (vl-read-while-whitespace echars))
    ((mv name & remainder)
     (vl-read-identifier remainder))
    ((when (not name))
     (mv
      (cw
       "Preprocessor error (~s0): found a `define without a name.~%"
       (vl-location-string loc))
      defines echars))
    ((when (vl-is-compiler-directive-p name))
     (mv
      (cw
       "Preprocessor error (~s0): refusing to permit `define ~s1.~%"
       (vl-location-string loc)
       name)
      defines echars))
    ((mv successp text remainder)
     (vl-read-until-end-of-define remainder config))
    ((when (not successp))
     (mv nil defines echars))
    ((when (not activep))
     (mv t defines remainder))
    ((mv okp formals body)
     (vl-split-define-text text config))
    ((unless okp)
     (mv nil defines remainder))
    (formal-names (vl-define-formallist->names formals))
    ((unless (uniquep formal-names))
     (mv
      (cw
       "Preprocessor error (~s0): `define ~s1 has repeats arguments ~&2."
       (vl-location-string loc)
       name (duplicated-members formal-names))
      defines echars))
    (new-def (make-vl-define :name name
                             :formals formals
                             :body (vl-echarlist->string body)
                             :loc loc))
    (prev-def (vl-find-define name defines))
    (-
     (or
      (not prev-def)
      (b* ((new-str (str::trim (vl-define->body new-def)))
           (old-str (str::trim (vl-define->body prev-def)))
           ((when (equal new-str old-str)) t))
       (cw
        "Preprocessor warning: redefining ~s0:~% ~
                    - Was ~s1     // from ~s2~% ~
                    - Now ~s3     // from ~s4~%"
        name old-str
        (vl-location-string (vl-define->loc prev-def))
        new-str (vl-location-string loc)))))
    (defines (if prev-def (vl-delete-define name defines)
               defines)
)
    (defines (vl-add-define new-def defines)
))
   (mv t defines remainder))))

Theorem: vl-defines-p-of-vl-process-define.new-defines

(defthm vl-defines-p-of-vl-process-define.new-defines
  (b* (((mv ?successp ?new-defines ?remainder)
        (vl-process-define loc echars defines activep config)))
    (vl-defines-p new-defines))
  :rule-classes :rewrite)

Theorem: vl-echarlist-p-of-vl-process-define.remainder

(defthm vl-echarlist-p-of-vl-process-define.remainder
  (implies
       (force (vl-echarlist-p echars))
       (b* (((mv ?successp ?new-defines ?remainder)
             (vl-process-define loc echars defines activep config)))
         (vl-echarlist-p remainder)))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-process-define-remainder

(defthm true-listp-of-vl-process-define-remainder
 (equal
  (true-listp
     (mv-nth 2
             (vl-process-define loc echars defines activep config)))
  (true-listp echars)))

Theorem: acl2-count-of-vl-process-define

(defthm acl2-count-of-vl-process-define
 (<=
  (acl2-count
     (mv-nth 2
             (vl-process-define loc echars defines activep config)))
  (acl2-count echars))
 :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-process-define-strong

(defthm acl2-count-of-vl-process-define-strong
 (implies
  (mv-nth 0
          (vl-process-define loc echars defines activep config))
  (<
   (acl2-count
     (mv-nth 2
             (vl-process-define loc echars defines activep config)))
   (acl2-count echars)))
 :rule-classes ((:rewrite) (:linear)))