		Search-engine friendly clone of the ACL2 documentation.

Vl-commentmap-p

Vl-gather-comments

Slow, but straightforward routine for gathering all comments between two locations.

Signature
(vl-gather-comments min max cmap) → *
Arguments: min — Guard (vl-location-p min).; max — Guard (vl-location-p max).; cmap — Guard (vl-commentmap-p cmap).

See also vl-gather-comments-fal, which implements a much faster routine for gathering comments.

Definitions and Theorems

Function: vl-gather-comments

(defun vl-gather-comments (min max cmap)
 (declare (xargs :guard (and (vl-location-p min)
                             (vl-location-p max)
                             (vl-commentmap-p cmap))))
 (let ((__function__ 'vl-gather-comments))
  (declare (ignorable __function__))
  (mbe
   :logic (cond ((atom cmap) nil)
                ((vl-location-between-p (caar cmap)
                                        min max)
                 (cons (car cmap)
                       (vl-gather-comments min max (cdr cmap))))
                (t (vl-gather-comments min max (cdr cmap))))
   :exec
   (prog2$
    (let ((min-filename (vl-location->filename min))
          (max-filename (vl-location->filename max)))
     (or
      (equal min-filename max-filename)
      (cw
       "; vl-gather-comments: min/max have different filenames.~%")))
    (with-local-nrev
         (vl-gather-comments-nrev min max cmap nrev))))))

Theorem: vl-gather-comments-nrev-removal

(defthm vl-gather-comments-nrev-removal
  (equal (vl-gather-comments-nrev min max cmap nrev)
         (append nrev
                 (vl-gather-comments min max cmap))))

Theorem: vl-commentmap-p-of-vl-gather-comments

(defthm vl-commentmap-p-of-vl-gather-comments
  (implies (force (vl-commentmap-p cmap))
           (vl-commentmap-p (vl-gather-comments min max cmap))))

Subtopics

Vl-gather-comments-nrev