		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