		Search-engine friendly clone of the ACL2 documentation.

Vl-commentmap-p

Vl-description-inject-comments

Signature
(vl-description-inject-comments x fal all-descs) → new-x
Arguments: x — Description to inject some comments into.
Guard (vl-description-p x).; fal — All comments, gathered before parsing.
Guard (vl-commentmap-falp fal).; all-descs — All descriptions, used to adjust starting locations.
Guard (vl-descriptionlist-p all-descs).
Returns: new-x — Same as x, but with comments added.
Type (vl-description-p new-x).

Definitions and Theorems

Function: vl-description-inject-comments

(defun vl-description-inject-comments (x fal all-descs)
 (declare (xargs :guard (and (vl-description-p x)
                             (vl-commentmap-falp fal)
                             (vl-descriptionlist-p all-descs))))
 (let ((__function__ 'vl-description-inject-comments))
  (declare (ignorable __function__))
  (b*
   ((x (vl-description-fix x))
    ((unless (vl-description-has-comments-p x))
     x)
    (minloc (vl-description->minloc x))
    (maxloc (vl-description->maxloc x))
    ((unless (<= (vl-location->line minloc)
                 (vl-location->line maxloc)))
     (let
      ((w
        (make-vl-warning
         :type :vl-warn-comment-injection
         :msg
         "Cannot add comments, minloc exceeds ~
                                        maxloc?~% minloc = ~l0; maxloc = ~l1."
         :args (list minloc maxloc)
         :fatalp nil
         :fn __function__)))
      (vl-description-add-warning x w)))
    (minloc (vl-adjust-minloc-for-comments
                 (change-vl-location minloc :line 1)
                 minloc all-descs))
    (comments (vl-gather-comments-fal minloc maxloc fal)))
   (if (not comments)
       x
     (vl-description-set-comments x comments)))))

Theorem: vl-description-p-of-vl-description-inject-comments

(defthm vl-description-p-of-vl-description-inject-comments
  (b* ((new-x (vl-description-inject-comments x fal all-descs)))
    (vl-description-p new-x))
  :rule-classes :rewrite)

Theorem: vl-description->name-of-vl-description-inject-comments

(defthm vl-description->name-of-vl-description-inject-comments
  (equal
       (vl-description->name
            (vl-description-inject-comments x comment-map all-mods))
       (vl-description->name x)))