		Search-engine friendly clone of the ACL2 documentation.

Filtering-by-name

Vl-filter-classes

Partition a list of vl-classs by name.

Signature
(vl-filter-classes names x) → (mv named unnamed)
Arguments: names — Names to filter with.
Guard (string-listp names).; x — List to filter.
Guard (vl-classlist-p x).

The only reason to use this function is efficiency. Logically, named is equal to vl-keep-classes and unnamed is equal to vl-delete-classes. We leave this function enabled and would think it odd to ever prove a theorem about it.

Definitions and Theorems

Function: vl-filter-classes

(defun vl-filter-classes (names x)
  (declare (xargs :guard (and (string-listp names)
                              (vl-classlist-p x))))
  (let ((__function__ 'vl-filter-classes))
    (declare (ignorable __function__))
    (mbe :logic
         (mv (vl-keep-classes names x)
             (vl-delete-classes names x))
         :exec
         (b* (((when (atom names))
               (mv nil (list-fix x)))
              ((when (atom x)) (mv nil nil))
              (fal (make-lookup-alist names))
              ((local-stobjs nrev nrev2)
               (mv yes no nrev nrev2))
              ((mv nrev nrev2)
               (vl-fast-filter-classes names fal x nrev nrev2))
              (- (fast-alist-free fal))
              ((mv yes nrev) (nrev-finish nrev))
              ((mv no nrev2) (nrev-finish nrev2)))
           (mv yes no nrev nrev2)))))

Theorem: vl-fast-filter-classes-removal-0

(defthm vl-fast-filter-classes-removal-0
  (equal (mv-nth 0
                 (vl-fast-filter-classes names fal x nrev nrev2))
         (append nrev (vl-keep-classes names x))))

Theorem: vl-fast-filter-classes-removal-1

(defthm vl-fast-filter-classes-removal-1
  (equal (mv-nth 1
                 (vl-fast-filter-classes names fal x nrev nrev2))
         (append nrev2 (vl-delete-classes names x))))