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.
Function:
(defun vl-commentmap-entry-p (x) (declare (xargs :guard t)) (and (consp x) (vl-location-p (car x)) (stringp (cdr x))))
Function:
(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:
(defthm transitivity-of-vl-commentmap-entry-< (implies (and (vl-commentmap-entry-< x y) (vl-commentmap-entry-< y z)) (vl-commentmap-entry-< x z)))
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(defthm vl-commentmap-entry-sort-preserves-duplicity (equal (duplicity acl2::a (vl-commentmap-entry-sort acl2::x)) (duplicity acl2::a acl2::x)))
Theorem:
(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:
(defthm vl-commentmap-entry-sort-sorts (vl-commentmap-entry-ordered-p (vl-commentmap-entry-sort acl2::x)))
Theorem:
(defthm vl-commentmap-entry-sort-no-duplicatesp-equal (equal (no-duplicatesp-equal (vl-commentmap-entry-sort acl2::x)) (no-duplicatesp-equal acl2::x)))
Theorem:
(defthm vl-commentmap-entry-sort-true-listp (true-listp (vl-commentmap-entry-sort acl2::x)) :rule-classes :type-prescription)
Theorem:
(defthm vl-commentmap-entry-sort-len (equal (len (vl-commentmap-entry-sort acl2::x)) (len acl2::x)))
Theorem:
(defthm vl-commentmap-entry-sort-consp (equal (consp (vl-commentmap-entry-sort acl2::x)) (consp acl2::x)))
Theorem:
(defthm vl-commentmap-entry-sort-is-identity-under-set-equiv (set-equiv (vl-commentmap-entry-sort acl2::x) acl2::x))
Theorem:
(defthm vl-commentmap-entry-list-p-elim (equal (vl-commentmap-entry-list-p x) (vl-commentmap-p (list-fix x))))
Theorem:
(defthm vl-commentmap-p-of-vl-commentmap-entry-sort (implies (vl-commentmap-p x) (vl-commentmap-p (vl-commentmap-entry-sort x))))