		Search-engine friendly clone of the ACL2 documentation.

Utilities

Vl-merge-contiguous-indices

Transform a vl-maybe-integer-listp by combining contiguous sequences of indices into (low . high) pairs.

Signature
(vl-merge-contiguous-indices x) → indices
Arguments: x — Guard (vl-maybe-integer-listp x).
Returns: indices — Type (vl-merged-index-list-p indices), given the guard.

For example:

(vl-merge-contiguous-indices '(1 2 3 5 6 7 8 9 10 15 17 18))
  -->
((1 . 3) (5 . 10) 15 (17 . 18))

Definitions and Theorems

Function: vl-merge-contiguous-indices

(defun vl-merge-contiguous-indices (x)
       (declare (xargs :guard (vl-maybe-integer-listp x)))
       (let ((__function__ 'vl-merge-contiguous-indices))
            (declare (ignorable __function__))
            (b* (((when (atom x)) nil)
                 ((mv range-end rest)
                  (vl-match-contiguous-indices (car x)
                                               (cdr x)))
                 ((when (equal (car x) range-end))
                  (cons (car x)
                        (vl-merge-contiguous-indices (cdr x)))))
                (cons (cons (car x) range-end)
                      (vl-merge-contiguous-indices rest)))))

Theorem: vl-merged-index-list-p-of-vl-merge-contiguous-indices

(defthm vl-merged-index-list-p-of-vl-merge-contiguous-indices
        (implies (and (force (vl-maybe-integer-listp x)))
                 (b* ((indices (vl-merge-contiguous-indices x)))
                     (vl-merged-index-list-p indices)))
        :rule-classes :rewrite)

Subtopics

Vl-match-contiguous-indices: Identify one strictly increasing segment of a vl-maybe-integer-listp.
Vl-merged-index-list-p: (vl-merged-index-list-p x) recognizes lists where every element satisfies vl-merged-index-p.
Vl-merged-index-p