		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-process-define

Handler for define directives.

Signature
(vl-process-define loc echars ppst) → (mv successp remainder ppst)
Arguments: loc — Guard (vl-location-p loc).; echars — Guard (vl-echarlist-p echars).
Returns: remainder — Type (vl-echarlist-p remainder).

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 ppst)
 (declare (xargs :stobjs (ppst)))
 (declare (xargs :guard (and (vl-location-p loc)
                             (vl-echarlist-p echars))))
 (let ((__function__ 'vl-process-define))
  (declare (ignorable __function__))
  (b*
   ((echars (vl-echarlist-fix echars))
    ((mv & remainder)
     (vl-read-while-whitespace echars))
    ((mv name & remainder)
     (vl-read-identifier remainder))
    ((unless name)
     (let
      ((ppst
          (vl-ppst-fatal :msg "~a0: found a `define without a name."
                         :args (list loc))))
      (mv nil echars ppst)))
    ((when (vl-is-compiler-directive-p name))
     (let
      ((ppst
          (vl-ppst-fatal :msg "~a0: refusing to permit `define ~s1."
                         :args (list loc name))))
      (mv nil echars ppst)))
    ((mv successp text remainder ppst)
     (vl-read-until-end-of-define remainder ppst))
    ((unless successp) (mv nil echars ppst))
    ((unless (vl-ppst->activep))
     (mv t remainder ppst))
    ((mv okp formals body ppst)
     (vl-split-define-text text ppst))
    ((unless okp) (mv nil remainder ppst))
    (formal-names (vl-define-formallist->names formals))
    ((unless (uniquep formal-names))
     (let
      ((ppst
            (vl-ppst-fatal
                 :msg "~a0: `define ~s1 has repeated arguments ~&2."
                 :args (list loc name
                             (duplicated-members formal-names)))))
      (mv nil echars ppst)))
    (new-def (make-vl-define :formals formals
                             :body (vl-echarlist->string body)
                             :loc loc
                             :stickyp nil))
    (defines (vl-ppst->defines))
    (prev-def (vl-find-define name defines))
    (ppst
     (b* (((unless prev-def) ppst)
          (new-str (str::trim (vl-define->body new-def)))
          (old-str (str::trim (vl-define->body prev-def)))
          ((when (equal new-str old-str)) ppst))
      (vl-ppst-warn
       :type
       (if (vl-define->stickyp prev-def)
           :vl-warn-define-ignored
         :vl-warn-define-smashed)
       :msg
       (if
        (vl-define->stickyp prev-def)
        "Preprocessor warning: ignoring redefinition of ~s0:~% ~
                           - Keeping  ~s1     // from ~a2~% ~
                           - Ignoring ~s3     // from ~a4~%"
        "Preprocessor warning: redefining ~s0:~% ~
                         - Was ~s1     // from ~a2~% ~
                         - Now ~s3     // from ~a4~%")
       :args (list name old-str (vl-define->loc prev-def)
                   new-str loc))))
    (defines (if (and prev-def (vl-define->stickyp prev-def))
                 defines
               (vl-add-define name new-def defines))
)
    (ppst (vl-ppst-update-defines defines)))
   (mv t remainder ppst))))

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

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

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

(defthm true-listp-of-vl-process-define-remainder
  (true-listp (mv-nth 1 (vl-process-define loc echars ppst)))
  :rule-classes :type-prescription)

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

(defthm acl2-count-of-vl-process-define
  (<= (acl2-count (mv-nth 1 (vl-process-define loc echars ppst)))
      (acl2-count (vl-echarlist-fix 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 ppst))
      (< (acl2-count (mv-nth 1 (vl-process-define loc echars ppst)))
         (acl2-count (vl-echarlist-fix echars))))
 :rule-classes ((:rewrite) (:linear)))