(vl-create-unparameterized-module x final-paramdecls ss) → (mv okp new-mod sigalist)
Function:
(defun vl-create-unparameterized-module (x final-paramdecls ss) (declare (xargs :guard (and (vl-module-p x) (vl-paramdecllist-p final-paramdecls) (vl-scopestack-p ss)))) (let ((__function__ 'vl-create-unparameterized-module)) (declare (ignorable __function__)) (b* (((vl-module x)) (name (vl-unparam-newname x.name final-paramdecls)) (warnings x.warnings) ((mv ok warnings generates) (vl-genelementlist-resolve x.generates ss warnings)) ((unless ok) (mv nil (change-vl-module x :warnings warnings) nil)) (ports (vl-portlist-scopesubst x.ports ss)) (portdecls (vl-portdecllist-scopesubst x.portdecls ss)) (assigns (vl-assignlist-scopesubst x.assigns ss)) (aliases (vl-aliaslist-scopesubst x.aliases ss)) (paramdecls (vl-paramdecllist-scopesubst x.paramdecls ss)) (vardecls (vl-vardecllist-scopesubst x.vardecls ss)) (fundecls (vl-fundecllist-scopesubst x.fundecls ss)) (modinsts (vl-modinstlist-scopesubst x.modinsts ss)) (gateinsts (vl-gateinstlist-scopesubst x.gateinsts ss)) (alwayses (vl-alwayslist-scopesubst x.alwayses ss)) (initials (vl-initiallist-scopesubst x.initials ss)) (mod (change-vl-module x :name name :generates generates :ports ports :portdecls portdecls :assigns assigns :aliases aliases :paramdecls paramdecls :vardecls vardecls :fundecls fundecls :modinsts modinsts :gateinsts gateinsts :alwayses alwayses :initials initials)) (genblob (vl-module->genblob mod)) ((mv ok warnings sigalist new-genblob) (vl-genblob-collect-modinst-paramsigs genblob ss warnings x.name nil)) (final-mod1 (vl-genblob->module new-genblob mod)) (final-mod (change-vl-module final-mod1 :warnings warnings))) (mv ok final-mod sigalist))))
Theorem:
(defthm vl-module-p-of-vl-create-unparameterized-module.new-mod (b* (((mv ?okp ?new-mod ?sigalist) (vl-create-unparameterized-module x final-paramdecls ss))) (vl-module-p new-mod)) :rule-classes :rewrite)
Theorem:
(defthm vl-unparam-sigalist-p-of-vl-create-unparameterized-module.sigalist (b* (((mv ?okp ?new-mod ?sigalist) (vl-create-unparameterized-module x final-paramdecls ss))) (vl-unparam-sigalist-p sigalist)) :rule-classes :rewrite)
Theorem:
(defthm vl-create-unparameterized-module-of-vl-module-fix-x (equal (vl-create-unparameterized-module (vl-module-fix x) final-paramdecls ss) (vl-create-unparameterized-module x final-paramdecls ss)))
Theorem:
(defthm vl-create-unparameterized-module-vl-module-equiv-congruence-on-x (implies (vl-module-equiv x x-equiv) (equal (vl-create-unparameterized-module x final-paramdecls ss) (vl-create-unparameterized-module x-equiv final-paramdecls ss))) :rule-classes :congruence)
Theorem:
(defthm vl-create-unparameterized-module-of-vl-paramdecllist-fix-final-paramdecls (equal (vl-create-unparameterized-module x (vl-paramdecllist-fix final-paramdecls) ss) (vl-create-unparameterized-module x final-paramdecls ss)))
Theorem:
(defthm vl-create-unparameterized-module-vl-paramdecllist-equiv-congruence-on-final-paramdecls (implies (vl-paramdecllist-equiv final-paramdecls final-paramdecls-equiv) (equal (vl-create-unparameterized-module x final-paramdecls ss) (vl-create-unparameterized-module x final-paramdecls-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-create-unparameterized-module-of-vl-scopestack-fix-ss (equal (vl-create-unparameterized-module x final-paramdecls (vl-scopestack-fix ss)) (vl-create-unparameterized-module x final-paramdecls ss)))
Theorem:
(defthm vl-create-unparameterized-module-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-create-unparameterized-module x final-paramdecls ss) (vl-create-unparameterized-module x final-paramdecls ss-equiv))) :rule-classes :congruence)