		Search-engine friendly clone of the ACL2 documentation.

Vl-commentmap-p

Vl-commentmap-entry-sort

A basic sort for comment maps.

Our pretty-printer uses the following routine in a funny way to get the comments put inline with the module elements.

The sort is introduced with defsort, so it is a stable mergesort. Note that we ignore file names.

Definitions and Theorems

Function: vl-commentmap-entry-p

(defun vl-commentmap-entry-p (x)
  (declare (xargs :guard t))
  (and (consp x)
       (vl-location-p (car x))
       (stringp (cdr x))))

Function: vl-commentmap-entry-<

(defun vl-commentmap-entry-< (x y)
  (declare (xargs :guard (and (vl-commentmap-entry-p x)
                              (vl-commentmap-entry-p y))))
  (let ((line-x (vl-location->line (car x)))
        (line-y (vl-location->line (car y))))
    (or (< line-x line-y)
        (and (= line-x line-y)
             (< (vl-location->col (car x))
                (vl-location->col (car y)))))))

Theorem: transitivity-of-vl-commentmap-entry-<

(defthm transitivity-of-vl-commentmap-entry-<
  (implies (and (vl-commentmap-entry-< x y)
                (vl-commentmap-entry-< y z))
           (vl-commentmap-entry-< x z)))

Function: vl-commentmap-entry-list-p

(defun vl-commentmap-entry-list-p (acl2::x)
  (declare (xargs :guard t :stobjs nil))
  (if (consp acl2::x)
      (and (vl-commentmap-entry-p (car acl2::x))
           (vl-commentmap-entry-list-p (cdr acl2::x)))
    t))

Function: vl-commentmap-entry-ordered-p

(defun vl-commentmap-entry-ordered-p (acl2::x)
 (declare (xargs :guard (and t (vl-commentmap-entry-list-p acl2::x))
                 :stobjs nil))
 (cond ((atom acl2::x) t)
       ((atom (cdr acl2::x)) t)
       ((vl-commentmap-entry-< (first acl2::x)
                               (second acl2::x))
        (vl-commentmap-entry-ordered-p (cdr acl2::x)))
       (t (and (not (vl-commentmap-entry-< (second acl2::x)
                                           (first acl2::x)))
               (vl-commentmap-entry-ordered-p (cdr acl2::x))))))

Function: vl-commentmap-entry-merge

(defun vl-commentmap-entry-merge (acl2::x acl2::y)
 (declare (xargs :stobjs nil
                 :guard (and t (vl-commentmap-entry-list-p acl2::x)
                             (vl-commentmap-entry-list-p acl2::y))))
 (cond ((atom acl2::x) acl2::y)
       ((atom acl2::y) acl2::x)
       ((vl-commentmap-entry-< (car acl2::y)
                               (car acl2::x))
        (cons (car acl2::y)
              (vl-commentmap-entry-merge acl2::x (cdr acl2::y))))
       (t (cons (car acl2::x)
                (vl-commentmap-entry-merge (cdr acl2::x)
                                           acl2::y)))))

Function: vl-commentmap-entry-merge-tr

(defun vl-commentmap-entry-merge-tr (acl2::x acl2::y acl2::acc)
 (declare (xargs :stobjs nil
                 :guard (and t (vl-commentmap-entry-list-p acl2::x)
                             (vl-commentmap-entry-list-p acl2::y))))
 (cond
  ((atom acl2::x)
   (revappend-without-guard acl2::acc acl2::y))
  ((atom acl2::y)
   (revappend-without-guard acl2::acc acl2::x))
  ((vl-commentmap-entry-< (car acl2::y)
                          (car acl2::x))
   (vl-commentmap-entry-merge-tr acl2::x (cdr acl2::y)
                                 (cons (car acl2::y) acl2::acc)))
  (t
    (vl-commentmap-entry-merge-tr (cdr acl2::x)
                                  acl2::y
                                  (cons (car acl2::x) acl2::acc)))))

Function: vl-commentmap-entry-mergesort-fixnum

(defun vl-commentmap-entry-mergesort-fixnum (acl2::x len)
 (declare (xargs :stobjs nil
                 :guard (and t (vl-commentmap-entry-list-p acl2::x)
                             (natp len)
                             (<= len (len acl2::x))))
          (type (signed-byte 30) len))
 (cond
  ((mbe :logic (zp len)
        :exec (eql (the (signed-byte 30) len) 0))
   nil)
  ((eql (the (signed-byte 30) len) 1)
   (list (car acl2::x)))
  (t
   (let*
    ((acl2::len1 (the (signed-byte 30)
                      (ash (the (signed-byte 30) len) -1)))
     (acl2::len2 (the (signed-byte 30)
                      (- (the (signed-byte 30) len)
                         (the (signed-byte 30) acl2::len1))))
     (acl2::part1
          (vl-commentmap-entry-mergesort-fixnum acl2::x acl2::len1))
     (acl2::part2 (vl-commentmap-entry-mergesort-fixnum
                       (rest-n acl2::len1 acl2::x)
                       acl2::len2)))
    (vl-commentmap-entry-merge-tr acl2::part1 acl2::part2 nil)))))

Function: vl-commentmap-entry-mergesort-integers

(defun vl-commentmap-entry-mergesort-integers (acl2::x len)
 (declare (xargs :stobjs nil
                 :guard (and t (vl-commentmap-entry-list-p acl2::x)
                             (natp len)
                             (<= len (len acl2::x))))
          (type integer len))
 (cond
  ((mbe :logic (zp len)
        :exec (eql (the integer len) 0))
   nil)
  ((eql (the integer len) 1)
   (list (car acl2::x)))
  (t
   (let*
    ((acl2::len1 (the integer (ash (the integer len) -1)))
     (acl2::len2 (the integer
                      (- (the integer len)
                         (the integer acl2::len1))))
     (acl2::part1
      (if (< (the integer acl2::len1)
             (acl2::mergesort-fixnum-threshold))
          (vl-commentmap-entry-mergesort-fixnum acl2::x acl2::len1)
       (vl-commentmap-entry-mergesort-integers acl2::x acl2::len1)))
     (acl2::part2 (if (< (the integer acl2::len2)
                         (acl2::mergesort-fixnum-threshold))
                      (vl-commentmap-entry-mergesort-fixnum
                           (rest-n acl2::len1 acl2::x)
                           acl2::len2)
                    (vl-commentmap-entry-mergesort-integers
                         (rest-n acl2::len1 acl2::x)
                         acl2::len2))))
    (vl-commentmap-entry-merge-tr acl2::part1 acl2::part2 nil)))))

Function: vl-commentmap-entry-sort

(defun vl-commentmap-entry-sort (acl2::x)
 (declare (xargs :guard (and t (vl-commentmap-entry-list-p acl2::x))
                 :stobjs nil))
 (mbe
  :logic
  (cond
   ((atom acl2::x) nil)
   ((atom (cdr acl2::x))
    (list (car acl2::x)))
   (t
    (let ((acl2::half (floor (len acl2::x) 2)))
     (vl-commentmap-entry-merge
          (vl-commentmap-entry-sort (take acl2::half acl2::x))
          (vl-commentmap-entry-sort (nthcdr acl2::half acl2::x))))))
  :exec
  (let ((len (len acl2::x)))
    (if (< len (acl2::mergesort-fixnum-threshold))
        (vl-commentmap-entry-mergesort-fixnum acl2::x len)
      (vl-commentmap-entry-mergesort-integers acl2::x len)))))

Theorem: vl-commentmap-entry-sort-preserves-duplicity

(defthm vl-commentmap-entry-sort-preserves-duplicity
  (equal (duplicity acl2::a
                    (vl-commentmap-entry-sort acl2::x))
         (duplicity acl2::a acl2::x)))

Theorem: vl-commentmap-entry-sort-creates-comparable-listp

(defthm vl-commentmap-entry-sort-creates-comparable-listp
 (implies
   (vl-commentmap-entry-list-p acl2::x)
   (vl-commentmap-entry-list-p (vl-commentmap-entry-sort acl2::x))))

Theorem: vl-commentmap-entry-sort-sorts

(defthm vl-commentmap-entry-sort-sorts
 (vl-commentmap-entry-ordered-p (vl-commentmap-entry-sort acl2::x)))

Theorem: vl-commentmap-entry-sort-no-duplicatesp-equal

(defthm vl-commentmap-entry-sort-no-duplicatesp-equal
  (equal (no-duplicatesp-equal (vl-commentmap-entry-sort acl2::x))
         (no-duplicatesp-equal acl2::x)))

Theorem: vl-commentmap-entry-sort-true-listp

(defthm vl-commentmap-entry-sort-true-listp
  (true-listp (vl-commentmap-entry-sort acl2::x))
  :rule-classes :type-prescription)

Theorem: vl-commentmap-entry-sort-len

(defthm vl-commentmap-entry-sort-len
  (equal (len (vl-commentmap-entry-sort acl2::x))
         (len acl2::x)))

Theorem: vl-commentmap-entry-sort-consp

(defthm vl-commentmap-entry-sort-consp
  (equal (consp (vl-commentmap-entry-sort acl2::x))
         (consp acl2::x)))

Theorem: vl-commentmap-entry-sort-is-identity-under-set-equiv

(defthm vl-commentmap-entry-sort-is-identity-under-set-equiv
  (set-equiv (vl-commentmap-entry-sort acl2::x)
             acl2::x))

Theorem: vl-commentmap-entry-list-p-elim

(defthm vl-commentmap-entry-list-p-elim
  (equal (vl-commentmap-entry-list-p x)
         (vl-commentmap-p (list-fix x))))

Theorem: vl-commentmap-p-of-vl-commentmap-entry-sort

(defthm vl-commentmap-p-of-vl-commentmap-entry-sort
  (implies (vl-commentmap-p x)
           (vl-commentmap-p (vl-commentmap-entry-sort x))))