		Search-engine friendly clone of the ACL2 documentation.

Vl-reorder-fundecls

Collect a subset of a vl-fundecllist-p by their names, according to a given name ordering.

Signature
(vl-reorder-fundecls names x) → sublist
Arguments: names — Guard (string-listp names).; x — Guard (vl-fundecllist-p x).
Returns: sublist — Type (vl-fundecllist-p sublist).

This is a basic reordering function; see reordering-by-name.

Definitions and Theorems

Function: vl-reorder-fundecls

(defun vl-reorder-fundecls (names x)
  (declare (xargs :guard (and (string-listp names)
                              (vl-fundecllist-p x))))
  (let ((__function__ 'vl-reorder-fundecls))
    (declare (ignorable __function__))
    (mbe :logic
         (b* (((when (atom names)) nil)
              (decl (vl-find-fundecl (car names) x))
              ((when decl)
               (cons decl
                     (vl-reorder-fundecls (cdr names) x))))
           (vl-reorder-fundecls (cdr names) x))
         :exec
         (b* (((unless (and (longer-than-p 6 names)
                            (acl2::worth-hashing x)))
               (vl-slow-reorder-fundecl names x))
              (fal (make-fast-alist (vl-fundecllist-alist x nil)))
              (ans (vl-fast-reorder-fundecl names x fal)))
           (fast-alist-free fal)
           ans))))

Theorem: vl-fundecllist-p-of-vl-reorder-fundecls

(defthm vl-fundecllist-p-of-vl-reorder-fundecls
  (b* ((sublist (vl-reorder-fundecls names x)))
    (vl-fundecllist-p sublist))
  :rule-classes :rewrite)

Theorem: vl-slow-reorder-fundecl-removal

(defthm vl-slow-reorder-fundecl-removal
  (equal (vl-slow-reorder-fundecl names x)
         (vl-reorder-fundecls names x)))

Theorem: vl-fast-reorder-fundecl-removal

(defthm vl-fast-reorder-fundecl-removal
  (implies (and (string-listp names)
                (vl-fundecllist-p x)
                (equal fal (vl-fundecllist-alist x nil)))
           (equal (vl-fast-reorder-fundecl names x fal)
                  (vl-reorder-fundecls names x))))

Theorem: vl-reorder-fundecls-of-string-list-fix-names

(defthm vl-reorder-fundecls-of-string-list-fix-names
  (equal (vl-reorder-fundecls (string-list-fix names)
                              x)
         (vl-reorder-fundecls names x)))

Theorem: vl-reorder-fundecls-string-list-equiv-congruence-on-names

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

Theorem: vl-reorder-fundecls-of-vl-fundecllist-fix-x

(defthm vl-reorder-fundecls-of-vl-fundecllist-fix-x
  (equal (vl-reorder-fundecls names (vl-fundecllist-fix x))
         (vl-reorder-fundecls names x)))

Theorem: vl-reorder-fundecls-vl-fundecllist-equiv-congruence-on-x

(defthm vl-reorder-fundecls-vl-fundecllist-equiv-congruence-on-x
  (implies (vl-fundecllist-equiv x x-equiv)
           (equal (vl-reorder-fundecls names x)
                  (vl-reorder-fundecls names x-equiv)))
  :rule-classes :congruence)

We prove some basic correctness properties. To start, the list we get back is always a subset of the original list (modulo fixing).

Theorem: subsetp-of-vl-reorder-fundecls

(defthm subsetp-of-vl-reorder-fundecls
  (subsetp (vl-reorder-fundecls names x)
           (vl-fundecllist-fix x)))

Furthermore, the names we get back for are the names we asked for.

Theorem: vl-fundecllist->names-of-vl-reorder-fundecls

(defthm vl-fundecllist->names-of-vl-reorder-fundecls
  (implies
       (subsetp (double-rewrite names)
                (vl-fundecllist->names x))
       (equal (vl-fundecllist->names (vl-reorder-fundecls names x))
              (list-fix names))))

Theorem: vl-fundecllist->names-of-vl-reorder-fundecls-bounded

(defthm vl-fundecllist->names-of-vl-reorder-fundecls-bounded
  (subsetp (vl-fundecllist->names (vl-reorder-fundecls names x))
           (string-list-fix names)))

For stronger correctness properties, we need to know that the names in x are unique. After all, our finding functions rely on this, and won't return any "shadowed" objects in the list.

Theorem: member-of-vl-reorder-fundecls

(defthm member-of-vl-reorder-fundecls
  (implies (and (no-duplicatesp-equal (vl-fundecllist->names x))
                (force (vl-fundecllist-p x)))
           (iff (member a (vl-reorder-fundecls names x))
                (and (member a x)
                     (member (vl-fundecl->name a)
                             (string-list-fix names))))))

Theorem: vl-reorder-fundecls-under-set-equiv

(defthm vl-reorder-fundecls-under-set-equiv
  (implies (and (no-duplicatesp-equal (vl-fundecllist->names x))
                (set-equiv (double-rewrite (string-list-fix names))
                           (vl-fundecllist->names x)))
           (set-equiv (vl-reorder-fundecls names x)
                      (vl-fundecllist-fix x))))

Subtopics

Vl-slow-reorder-fundecl: Non fast-alist version of vl-reorder-fundecls, used when the lists are really short.
Vl-fast-reorder-fundecl: Fast-alist enhanced version of vl-reorder-fundecls.