Make a vl-dirlist-cache for a list of directories.
(vl-make-dirlist-cache dirs warnings state) → (mv cache warnings state)
Function:
(defun vl-make-dirlist-cache (dirs warnings state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (string-listp dirs) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-make-dirlist-cache)) (declare (ignorable __function__)) (b* (((when (atom dirs)) (mv nil (ok) state)) ((mv cache1 warnings state) (vl-make-dircache (car dirs) warnings state)) ((mv rest warnings state) (vl-make-dirlist-cache (cdr dirs) warnings state))) (mv (cons (cons (hons-copy (string-fix (car dirs))) cache1) rest) warnings state))))
Theorem:
(defthm vl-dirlist-cache-p-of-vl-make-dirlist-cache.cache (b* (((mv ?cache ?warnings acl2::?state) (vl-make-dirlist-cache dirs warnings state))) (vl-dirlist-cache-p cache)) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-make-dirlist-cache.warnings (b* (((mv ?cache ?warnings acl2::?state) (vl-make-dirlist-cache dirs warnings state))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm state-p1-of-vl-make-dirlist-cache.state (implies (force (state-p1 state)) (b* (((mv ?cache ?warnings acl2::?state) (vl-make-dirlist-cache dirs warnings state))) (state-p1 state))) :rule-classes :rewrite)
Theorem:
(defthm alist-keys-of-vl-make-dirlist-cache (b* (((mv ?cache ?warnings acl2::?state) (vl-make-dirlist-cache dirs warnings state))) (equal (alist-keys cache) (string-list-fix dirs))))
Theorem:
(defthm vl-make-dirlist-cache-of-string-list-fix-dirs (equal (vl-make-dirlist-cache (string-list-fix dirs) warnings state) (vl-make-dirlist-cache dirs warnings state)))
Theorem:
(defthm vl-make-dirlist-cache-string-list-equiv-congruence-on-dirs (implies (str::string-list-equiv dirs dirs-equiv) (equal (vl-make-dirlist-cache dirs warnings state) (vl-make-dirlist-cache dirs-equiv warnings state))) :rule-classes :congruence)
Theorem:
(defthm vl-make-dirlist-cache-of-vl-warninglist-fix-warnings (equal (vl-make-dirlist-cache dirs (vl-warninglist-fix warnings) state) (vl-make-dirlist-cache dirs warnings state)))
Theorem:
(defthm vl-make-dirlist-cache-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-make-dirlist-cache dirs warnings state) (vl-make-dirlist-cache dirs warnings-equiv state))) :rule-classes :congruence)