(vl-interfacelist->svex-modalist x elabindex config modalist) → (mv warnings modalist1 new-elabindex)
Function:
(defun vl-interfacelist->svex-modalist (x elabindex config modalist) (declare (xargs :stobjs (elabindex))) (declare (xargs :guard (and (vl-interfacelist-p x) (vl-simpconfig-p config) (sv::modalist-p modalist)))) (let ((__function__ 'vl-interfacelist->svex-modalist)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil (sv::modalist-fix modalist) elabindex)) (name (vl-interface->name (car x))) ((mv warnings modalist elabindex) (time$ (vl-interface->svex-module name elabindex config modalist) :msg "; iface->sv ~s0: ~st sec, ~sa bytes~%" :args (list name) :mintime 1)) ((mv reportcard modalist elabindex) (vl-interfacelist->svex-modalist (cdr x) elabindex config modalist))) (mv (if warnings (cons (cons name warnings) reportcard) reportcard) modalist elabindex))))
Theorem:
(defthm vl-reportcard-p-of-vl-interfacelist->svex-modalist.warnings (b* (((mv ?warnings ?modalist1 ?new-elabindex) (vl-interfacelist->svex-modalist x elabindex config modalist))) (vl-reportcard-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-interfacelist->svex-modalist.modalist1 (b* (((mv ?warnings ?modalist1 ?new-elabindex) (vl-interfacelist->svex-modalist x elabindex config modalist))) (and (sv::modalist-p modalist1) (implies (sv::svarlist-addr-p (sv::modalist-vars modalist)) (sv::svarlist-addr-p (sv::modalist-vars modalist1))))) :rule-classes :rewrite)
Theorem:
(defthm vl-interfacelist->svex-modalist-of-vl-interfacelist-fix-x (equal (vl-interfacelist->svex-modalist (vl-interfacelist-fix x) elabindex config modalist) (vl-interfacelist->svex-modalist x elabindex config modalist)))
Theorem:
(defthm vl-interfacelist->svex-modalist-vl-interfacelist-equiv-congruence-on-x (implies (vl-interfacelist-equiv x x-equiv) (equal (vl-interfacelist->svex-modalist x elabindex config modalist) (vl-interfacelist->svex-modalist x-equiv elabindex config modalist))) :rule-classes :congruence)
Theorem:
(defthm vl-interfacelist->svex-modalist-of-vl-simpconfig-fix-config (equal (vl-interfacelist->svex-modalist x elabindex (vl-simpconfig-fix config) modalist) (vl-interfacelist->svex-modalist x elabindex config modalist)))
Theorem:
(defthm vl-interfacelist->svex-modalist-vl-simpconfig-equiv-congruence-on-config (implies (vl-simpconfig-equiv config config-equiv) (equal (vl-interfacelist->svex-modalist x elabindex config modalist) (vl-interfacelist->svex-modalist x elabindex config-equiv modalist))) :rule-classes :congruence)
Theorem:
(defthm vl-interfacelist->svex-modalist-of-modalist-fix-modalist (equal (vl-interfacelist->svex-modalist x elabindex config (sv::modalist-fix modalist)) (vl-interfacelist->svex-modalist x elabindex config modalist)))
Theorem:
(defthm vl-interfacelist->svex-modalist-modalist-equiv-congruence-on-modalist (implies (sv::modalist-equiv modalist modalist-equiv) (equal (vl-interfacelist->svex-modalist x elabindex config modalist) (vl-interfacelist->svex-modalist x elabindex config modalist-equiv))) :rule-classes :congruence)