		Search-engine friendly clone of the ACL2 documentation.

Filtering-by-name

Vl-delete-udps

Delete vl-udps by name.

Signature
(vl-delete-udps names x) → filtered-x
Arguments: names — Names of vl-udps to remove.
Guard (string-listp names).; x — List to filter.
Guard (vl-udplist-p x).
Returns: filtered-x — Type (vl-udplist-p filtered-x).

Definitions and Theorems

Function: vl-delete-udps

(defun vl-delete-udps (names x)
 (declare (xargs :guard (and (string-listp names)
                             (vl-udplist-p x))))
 (let ((__function__ 'vl-delete-udps))
  (declare (ignorable __function__))
  (mbe
    :logic
    (cond ((atom x) nil)
          ((member-equal (vl-udp->name (car x))
                         (string-list-fix names))
           (vl-delete-udps names (cdr x)))
          (t (cons (vl-udp-fix (car x))
                   (vl-delete-udps names (cdr x)))))
    :exec
    (b*
     (((when (atom names)) (list-fix x))
      ((when (atom x)) nil)
      ((unless (longer-than-p 10 names))
       (vl-slow-delete-udps names x))
      (fal (make-lookup-alist names))
      (ans (with-local-nrev (vl-fast-delete-udps names fal x nrev)))
      (- (fast-alist-free fal)))
     ans))))

Theorem: vl-udplist-p-of-vl-delete-udps

(defthm vl-udplist-p-of-vl-delete-udps
  (b* ((filtered-x (vl-delete-udps names x)))
    (vl-udplist-p filtered-x))
  :rule-classes :rewrite)

Theorem: vl-delete-udps-when-atom

(defthm vl-delete-udps-when-atom
  (implies (atom x)
           (equal (vl-delete-udps names x) nil)))

Theorem: vl-delete-udps-of-cons

(defthm vl-delete-udps-of-cons
  (equal (vl-delete-udps names (cons a x))
         (if (member-equal (vl-udp->name a)
                           (string-list-fix names))
             (vl-delete-udps names x)
           (cons (vl-udp-fix a)
                 (vl-delete-udps names x)))))

Theorem: member-equal-of-vl-delete-udps

(defthm member-equal-of-vl-delete-udps
  (iff (member-equal a (vl-delete-udps names x))
       (and (member-equal a (vl-udplist-fix x))
            (not (member-equal (vl-udp->name a)
                               (string-list-fix names))))))

Theorem: subsetp-equal-of-vl-delete-udps

(defthm subsetp-equal-of-vl-delete-udps
  (subsetp-equal (vl-delete-udps names x)
                 (vl-udplist-fix x)))

Theorem: vl-delete-udps-when-atom-of-names

(defthm vl-delete-udps-when-atom-of-names
  (implies (atom names)
           (equal (vl-delete-udps names x)
                  (vl-udplist-fix (list-fix x)))))

Theorem: vl-slow-delete-udps-removal

(defthm vl-slow-delete-udps-removal
  (equal (vl-slow-delete-udps names x)
         (vl-delete-udps names x)))

Theorem: vl-fast-delete-udps-removal

(defthm vl-fast-delete-udps-removal
  (equal (vl-fast-delete-udps names fal x nrev)
         (append nrev (vl-delete-udps names x))))

Theorem: vl-delete-udps-of-string-list-fix-names

(defthm vl-delete-udps-of-string-list-fix-names
  (equal (vl-delete-udps (string-list-fix names)
                         x)
         (vl-delete-udps names x)))

Theorem: vl-delete-udps-string-list-equiv-congruence-on-names

(defthm vl-delete-udps-string-list-equiv-congruence-on-names
  (implies (str::string-list-equiv names names-equiv)
           (equal (vl-delete-udps names x)
                  (vl-delete-udps names-equiv x)))
  :rule-classes :congruence)

Theorem: vl-delete-udps-of-vl-udplist-fix-x

(defthm vl-delete-udps-of-vl-udplist-fix-x
  (equal (vl-delete-udps names (vl-udplist-fix x))
         (vl-delete-udps names x)))

Theorem: vl-delete-udps-vl-udplist-equiv-congruence-on-x

(defthm vl-delete-udps-vl-udplist-equiv-congruence-on-x
  (implies (vl-udplist-equiv x x-equiv)
           (equal (vl-delete-udps names x)
                  (vl-delete-udps names x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-fast-delete-udps