		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-process-undef

Handler for undef directives.

Signature
(vl-process-undef 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 an `undef has just been read and echars is the text which follows it. We try to read the name we are to undefine, then update the defines table appropriately.

Definitions and Theorems

Function: vl-process-undef

(defun vl-process-undef (loc echars ppst)
 (declare (xargs :stobjs (ppst)))
 (declare (xargs :guard (and (vl-location-p loc)
                             (vl-echarlist-p echars))))
 (let ((__function__ 'vl-process-undef))
  (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 an `undef 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 `undef ~s1."
                          :args (list loc name))))
      (mv nil echars ppst)))
    ((unless (vl-ppst->activep))
     (mv t remainder ppst))
    (defines (vl-ppst->defines))
    (lookup (vl-find-define name defines))
    (ppst
      (if (not lookup)
          (vl-ppst-warn
               :type :vl-warn-undef
               :msg "~a0: found `undef ~s1, but ~s1 is not defined."
               :args (list loc name))
        (progn$ (cw-unformatted (cat (vl-ppst-pad)
                                     " Undefining " name *nls*))
                ppst)))
    (defines (vl-delete-define name defines)
)
    (ppst (vl-ppst-update-defines defines)))
   (mv t remainder ppst))))

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

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

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

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

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

(defthm acl2-count-of-vl-process-undef
  (<= (acl2-count (mv-nth 1 (vl-process-undef loc echars ppst)))
      (acl2-count (vl-echarlist-fix echars)))
  :rule-classes ((:rewrite) (:linear)))

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

(defthm acl2-count-of-vl-process-undef-strong
  (implies
       (mv-nth 0 (vl-process-undef loc echars ppst))
       (< (acl2-count (mv-nth 1 (vl-process-undef loc echars ppst)))
          (acl2-count (vl-echarlist-fix echars))))
  :rule-classes ((:rewrite) (:linear)))