Build the preliminary E-language occurrences for a list of module instances.
(vl-modinstlist-to-eoccs x walist mods modalist eal warnings) → (mv successp warnings eoccs)
We just extend vl-modinst-to-eocc across a list.
Function:
(defun vl-modinstlist-to-eoccs (x walist mods modalist eal warnings) (declare (xargs :guard (and (vl-modinstlist-p x) (vl-wirealist-p walist) (vl-modulelist-p mods) (vl-ealist-p eal) (vl-warninglist-p warnings) (equal modalist (vl-modalist mods))))) (let ((__function__ 'vl-modinstlist-to-eoccs)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv t (ok) nil)) ((mv car-successp warnings car-eocc) (vl-modinst-to-eocc (car x) walist mods modalist eal warnings)) ((mv cdr-successp warnings cdr-eoccs) (vl-modinstlist-to-eoccs (cdr x) walist mods modalist eal warnings))) (mv (and car-successp cdr-successp) warnings (cons car-eocc cdr-eoccs)))))
Theorem:
(defthm booleanp-of-vl-modinstlist-to-eoccs.successp (b* (((mv ?successp ?warnings ?eoccs) (vl-modinstlist-to-eoccs x walist mods modalist eal warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-modinstlist-to-eoccs.warnings (b* (((mv ?successp ?warnings ?eoccs) (vl-modinstlist-to-eoccs x walist mods modalist eal warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-modinstlist-to-eoccs.eoccs (b* (((mv ?successp ?warnings ?eoccs) (vl-modinstlist-to-eoccs x walist mods modalist eal warnings))) (true-listp eoccs)) :rule-classes :type-prescription)
Theorem:
(defthm good-esim-occsp-of-vl-modinstlist-to-eoccs (let ((ret (vl-modinstlist-to-eoccs x walist mods modalist eal warnings))) (implies (and (mv-nth 0 ret) (force (vl-modinstlist-p x)) (force (vl-wirealist-p walist)) (force (vl-modulelist-p mods)) (force (equal modalist (vl-modalist mods))) (force (vl-ealist-p eal))) (good-esim-occsp (mv-nth 2 ret)))))