• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
        • Name-database
        • Vl-gc
        • Symbol-list-names
        • Ints-from
        • Nats-from
        • Make-lookup-alist
        • Redundant-mergesort
        • Longest-common-prefix
        • Vl-plural-p
        • Vl-remove-keys
        • Vl-merge-contiguous-indices
          • Vl-match-contiguous-indices
          • Vl-merged-index-list-p
          • Vl-merged-index-p
        • Vl-edition-p
        • Sum-nats
        • Vl-maybe-integer-listp
        • Fast-memberp
        • Nat-listp
        • Max-nats
        • Longest-common-prefix-list
        • Character-list-listp
        • Vl-character-list-list-values-p
        • Remove-from-alist
        • Prefix-of-eachp
        • Vl-string-keys-p
        • Vl-maybe-nat-listp
        • Vl-string-list-values-p
        • String-list-listp
        • Vl-string-values-p
        • True-list-listp
        • Symbol-list-listp
        • Explode-list
        • All-have-len
        • Pos-listp
        • Min-nats
        • Debuggable-and
        • Vl-starname
        • Remove-equal-without-guard
        • Vl-maybe-string-list
        • String-fix
        • Longer-than-p
        • Anyp
        • Fast-alist-free-each-alist-val
        • Not*
        • Free-list-of-fast-alists
        • *nls*
      • Printer
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-merge-contiguous-indices

Vl-match-contiguous-indices

Identify one strictly increasing segment of a vl-maybe-integer-listp.

Signature

(vl-match-contiguous-indices n x) → (mv range-end rest)

Arguments

n — Index to try to count up from.
    Guard (maybe-integerp n).

x — List whose elements we are to collect.
    Guard (vl-maybe-integer-listp x).

Returns

range-end — Type (maybe-integerp range-end), given the guard.

rest — Type (vl-maybe-integer-listp rest), given the guard.

We try to consume the leading portion of x if it counts up from n. For example:

(vl-match-contiguous-indices 1 '(2 3 4 5 10 11 12))
  -->
(mv 5 (10 11 12))

Definitions and Theorems

Function: vl-match-contiguous-indices

(defun vl-match-contiguous-indices (n x)
  (declare (xargs :guard (and (maybe-integerp n)
                              (vl-maybe-integer-listp x))))
  (let ((__function__ 'vl-match-contiguous-indices))
    (declare (ignorable __function__))
    (if (or (not (integerp n))
            (atom x)
            (not (equal (car x) (+ n 1))))
        (mv n x)
      (vl-match-contiguous-indices (+ n 1)
                                   (cdr x)))))

Theorem: maybe-integerp-of-vl-match-contiguous-indices.range-end

(defthm maybe-integerp-of-vl-match-contiguous-indices.range-end
  (implies (and (force (acl2::maybe-integerp$inline n))
                (force (vl-maybe-integer-listp x)))
           (b* (((mv ?range-end common-lisp::?rest)
                 (vl-match-contiguous-indices n x)))
             (maybe-integerp range-end)))
  :rule-classes :rewrite)

Theorem: vl-maybe-integer-listp-of-vl-match-contiguous-indices.rest

(defthm vl-maybe-integer-listp-of-vl-match-contiguous-indices.rest
  (implies (and (force (acl2::maybe-integerp$inline n))
                (force (vl-maybe-integer-listp x)))
           (b* (((mv ?range-end common-lisp::?rest)
                 (vl-match-contiguous-indices n x)))
             (vl-maybe-integer-listp rest)))
  :rule-classes :rewrite)

Theorem: len-of-vl-match-contiguous-indices

(defthm len-of-vl-match-contiguous-indices
 (implies (not (equal n
                      (mv-nth 0 (vl-match-contiguous-indices n x))))
          (< (len (mv-nth 1 (vl-match-contiguous-indices n x)))
             (len x)))
 :rule-classes ((:rewrite) (:linear)))

Theorem: vl-match-contiguous-indices-fails-on-nil

(defthm vl-match-contiguous-indices-fails-on-nil
  (equal (mv-nth 0 (vl-match-contiguous-indices nil x))
         nil))

Theorem: vl-match-contiguous-indices-monotonic-on-success

(defthm vl-match-contiguous-indices-monotonic-on-success
 (implies
     (and (not (equal n
                      (mv-nth 0 (vl-match-contiguous-indices n x))))
          (force (maybe-integerp n))
          (force (vl-maybe-integer-listp x)))
     (< n
        (mv-nth 0 (vl-match-contiguous-indices n x))))
 :rule-classes ((:rewrite) (:linear)))

Theorem: vl-match-contiguous-indices-exists-on-success

(defthm vl-match-contiguous-indices-exists-on-success
 (implies
     (and (not (equal n
                      (mv-nth 0 (vl-match-contiguous-indices n x))))
          (force (maybe-integerp n))
          (force (vl-maybe-integer-listp x)))
     (integerp (mv-nth 0 (vl-match-contiguous-indices n x)))))