		Search-engine friendly clone of the ACL2 documentation.

Vl-commentmap-p

Vl-commentmap-falp

Data structure that supports efficient comment gathering.

Signature
(vl-commentmap-falp x) → *

Our initial approach to pretty-printing with comments was to store all comments in a single comment map, then extract the relevant part of the comment map when we wanted to print each module. But profiling indicated that we were spending 90% of the (considerable) pretty-printing time just gathering the appropriate comments.

We then decided to attach the comments to each module, once and for all, so that we never need to look them up during pretty printing. An advantage of this is that we can carry out the comment injection before unparameterization, so that there are fewer lookups to begin with. Another advantage is that we can do the comment injection after loading each file, so that we never need to build a massive comment map spanning all files, but only smaller ones on a per-file basis.

Even so, individual files can be large. For a half-million line file, we obtained a big comment map, and our simple-minded comment gathering scheme was taking around 20 seconds. We developed a faster version that threw away comments after assigning them to a module, but even this was taking 10 seconds and allocating 1 GB of memory.

To correct for this, we developed a much faster comment gathering mechanism. The basic idea is to partition the big comment map into an alist that maps each line number to the subset of the comment map which is about that line.

That is, each entry in our commentmap-fal has the form:

line --> comment-map

where the comment-map has only the comments for this line and, in practice, is typically a singleton.

To extract all of the comments, we simply walk over the lines between min and max, gathering their comments.

Definitions and Theorems

Function: vl-commentmap-falp

(defun vl-commentmap-falp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vl-commentmap-falp))
    (declare (ignorable __function__))
    (if (atom x)
        (not x)
      (and (consp (car x))
           (posp (caar x))
           (vl-commentmap-p (cdar x))
           (vl-commentmap-lines-agreep (caar x)
                                       (cdar x))
           (vl-commentmap-falp (cdr x))))))

Theorem: vl-commentmap-falp-of-extension

(defthm vl-commentmap-falp-of-extension
  (implies (and (force (posp line))
                (force (vl-commentmap-p map))
                (force (vl-commentmap-lines-agreep line map))
                (force (vl-commentmap-falp alist)))
           (vl-commentmap-falp (cons (cons line map) alist))))

Theorem: vl-commentmap-falp-of-hons-shrink-alist

(defthm vl-commentmap-falp-of-hons-shrink-alist
  (implies (and (force (vl-commentmap-falp x))
                (force (vl-commentmap-falp y)))
           (vl-commentmap-falp (hons-shrink-alist x y))))

Theorem: vl-commentmap-falp-of-append

(defthm vl-commentmap-falp-of-append
  (implies (and (force (vl-commentmap-falp x))
                (force (vl-commentmap-falp y)))
           (vl-commentmap-falp (append x y))))

Theorem: vl-commentmap-p-of-hons-assoc-equal

(defthm vl-commentmap-p-of-hons-assoc-equal
  (implies (vl-commentmap-falp x)
           (equal (vl-commentmap-p (cdr (hons-assoc-equal line x)))
                  t)))

Theorem: vl-commentmap-lines-agreep-of-hons-assoc-equal

(defthm vl-commentmap-lines-agreep-of-hons-assoc-equal
 (implies
  (force (vl-commentmap-falp x))
  (equal
   (vl-commentmap-lines-agreep line (cdr (hons-assoc-equal line x)))
   t)))

Subtopics

Vl-commentmap-lines-agreep