		Search-engine friendly clone of the ACL2 documentation.

Loader

Vl-descriptions-left-to-load

Determine which descriptions we still need to load.

Signature
(vl-descriptions-left-to-load st) → names
Arguments: st — Guard (vl-loadstate-p st).
Returns: names — Type (string-listp names).

For loading to be completely done, we want to have:

All descriptions that the user told us to load in the :start-names, and
All descriptions that are ever referenced anywhere in any description that we have already loaded.

This function computes the names of descriptions that we want for the above reasons, but which we do not yet have loaded. These are the descriptions we'll need to search for.

Definitions and Theorems

Function: vl-descriptions-left-to-load

(defun vl-descriptions-left-to-load (st)
 (declare (xargs :guard (vl-loadstate-p st)))
 (let ((__function__ 'vl-descriptions-left-to-load))
   (declare (ignorable __function__))
   (b*
    (((vl-loadstate st) st)
     ((vl-loadconfig config) st.config)
     (current-mods (vl-collect-modules-from-descriptions st.descs))
     (things-we-want-loaded
          (mergesort
               (append config.start-names
                       (vl-modulelist-everinstanced current-mods))))
     (things-we-have-loaded
          (mergesort (vl-descriptionlist->names st.descs))))
    (difference things-we-want-loaded
                things-we-have-loaded))))

Theorem: string-listp-of-vl-descriptions-left-to-load

(defthm string-listp-of-vl-descriptions-left-to-load
  (b* ((names (vl-descriptions-left-to-load st)))
    (string-listp names))
  :rule-classes :rewrite)