		Search-engine friendly clone of the ACL2 documentation.

Vl-reorder-vardecls

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

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

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

Definitions and Theorems

Function: vl-reorder-vardecls

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

Theorem: vl-vardecllist-p-of-vl-reorder-vardecls

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

Theorem: vl-slow-reorder-vardecl-removal

(defthm vl-slow-reorder-vardecl-removal
  (equal (vl-slow-reorder-vardecl names x)
         (vl-reorder-vardecls names x)))

Theorem: vl-fast-reorder-vardecl-removal

(defthm vl-fast-reorder-vardecl-removal
  (implies (and (string-listp names)
                (vl-vardecllist-p x)
                (equal fal (vl-vardecllist-alist x nil)))
           (equal (vl-fast-reorder-vardecl names x fal)
                  (vl-reorder-vardecls names x))))

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

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

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

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

Theorem: vl-reorder-vardecls-of-vl-vardecllist-fix-x

(defthm vl-reorder-vardecls-of-vl-vardecllist-fix-x
  (equal (vl-reorder-vardecls names (vl-vardecllist-fix x))
         (vl-reorder-vardecls names x)))

Theorem: vl-reorder-vardecls-vl-vardecllist-equiv-congruence-on-x

(defthm vl-reorder-vardecls-vl-vardecllist-equiv-congruence-on-x
  (implies (vl-vardecllist-equiv x x-equiv)
           (equal (vl-reorder-vardecls names x)
                  (vl-reorder-vardecls 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-vardecls

(defthm subsetp-of-vl-reorder-vardecls
  (subsetp (vl-reorder-vardecls names x)
           (vl-vardecllist-fix x)))

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

Theorem: vl-vardecllist->names-of-vl-reorder-vardecls

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

Theorem: vl-vardecllist->names-of-vl-reorder-vardecls-bounded

(defthm vl-vardecllist->names-of-vl-reorder-vardecls-bounded
  (subsetp (vl-vardecllist->names (vl-reorder-vardecls 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-vardecls

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

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

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

Subtopics

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