• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • 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)))))