Build a commentmap that has the encoded items for a module.
(vl-make-item-map-for-ppc-module x ss &key (ps 'ps)) → (mv map ps)
Function:
(defun vl-make-item-map-for-ppc-module-fn (x ss ps) (declare (xargs :stobjs (ps))) (declare (xargs :guard (and (vl-module-p x) (vl-scopestack-p ss)))) (let ((__function__ 'vl-make-item-map-for-ppc-module)) (declare (ignorable __function__)) (b* (((vl-module x) x) (rchars (vl-ps->rchars)) (col (vl-ps->col)) (misc (vl-ps->misc)) (ps (vl-pp-set-portnames x.portdecls)) (imap nil) ((mv imap ps) (vl-paramdecllist-ppmap x.paramdecls imap)) ((mv imap ps) (vl-portdecllist-ppmap x.portdecls imap)) ((mv imap ps) (vl-vardecllist-ppmap x.vardecls imap)) ((mv imap ps) (vl-fundecllist-ppmap x.fundecls imap)) ((mv imap ps) (vl-taskdecllist-ppmap x.taskdecls imap)) ((mv imap ps) (vl-assignlist-ppmap x.assigns imap)) ((mv imap ps) (vl-modinstlist-ppmap x.modinsts ss imap)) ((mv imap ps) (vl-gateinstlist-ppmap x.gateinsts imap)) ((mv imap ps) (vl-alwayslist-ppmap x.alwayses imap)) ((mv imap ps) (vl-initiallist-ppmap x.initials imap)) (imap (rev imap)) (ps (vl-ps-update-rchars rchars)) (ps (vl-ps-update-col col)) (ps (vl-ps-update-misc misc))) (mv imap ps))))
Theorem:
(defthm vl-commentmap-p-of-vl-make-item-map-for-ppc-module.map (b* (((mv ?map ?ps) (vl-make-item-map-for-ppc-module-fn x ss ps))) (vl-commentmap-p map)) :rule-classes :rewrite)
Theorem:
(defthm vl-make-item-map-for-ppc-module-fn-of-vl-module-fix-x (equal (vl-make-item-map-for-ppc-module-fn (vl-module-fix x) ss ps) (vl-make-item-map-for-ppc-module-fn x ss ps)))
Theorem:
(defthm vl-make-item-map-for-ppc-module-fn-vl-module-equiv-congruence-on-x (implies (vl-module-equiv x x-equiv) (equal (vl-make-item-map-for-ppc-module-fn x ss ps) (vl-make-item-map-for-ppc-module-fn x-equiv ss ps))) :rule-classes :congruence)
Theorem:
(defthm vl-make-item-map-for-ppc-module-fn-of-vl-scopestack-fix-ss (equal (vl-make-item-map-for-ppc-module-fn x (vl-scopestack-fix ss) ps) (vl-make-item-map-for-ppc-module-fn x ss ps)))
Theorem:
(defthm vl-make-item-map-for-ppc-module-fn-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-make-item-map-for-ppc-module-fn x ss ps) (vl-make-item-map-for-ppc-module-fn x ss-equiv ps))) :rule-classes :congruence)