		Search-engine friendly clone of the ACL2 documentation.

Vl-reorder-modules

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

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

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

Definitions and Theorems

Function: vl-reorder-modules

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

Theorem: vl-modulelist-p-of-vl-reorder-modules

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

Theorem: vl-slow-reorder-module-removal

(defthm vl-slow-reorder-module-removal
  (equal (vl-slow-reorder-module names x)
         (vl-reorder-modules names x)))

Theorem: vl-fast-reorder-module-removal

(defthm vl-fast-reorder-module-removal
  (implies (and (string-listp names)
                (vl-modulelist-p x)
                (equal fal (vl-modulelist-alist x nil)))
           (equal (vl-fast-reorder-module names x fal)
                  (vl-reorder-modules names x))))

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

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

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

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

Theorem: vl-reorder-modules-of-vl-modulelist-fix-x

(defthm vl-reorder-modules-of-vl-modulelist-fix-x
  (equal (vl-reorder-modules names (vl-modulelist-fix x))
         (vl-reorder-modules names x)))

Theorem: vl-reorder-modules-vl-modulelist-equiv-congruence-on-x

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

(defthm subsetp-of-vl-reorder-modules
  (subsetp (vl-reorder-modules names x)
           (vl-modulelist-fix x)))

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

Theorem: vl-modulelist->names-of-vl-reorder-modules

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

Theorem: vl-modulelist->names-of-vl-reorder-modules-bounded

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

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

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

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

Subtopics

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