(vl-vardecl-enum-fixup x portdecls config) → fixups
Function:
(defun vl-vardecl-enum-fixup (x portdecls config) (declare (xargs :guard (and (vl-vardecl-p x) (vl-simpconfig-p config)))) (declare (xargs :guard (b* (((vl-vardecl x))) (and (vl-datatype-resolved-p x.type) (b* (((mv err size) (vl-datatype-size x.type))) (and (not err) size)))))) (let ((__function__ 'vl-vardecl-enum-fixup)) (declare (ignorable __function__)) (b* (((vl-simpconfig config)) ((vl-vardecl x)) (vttree nil) ((unless config.enum-fixups) vttree) ((unless (or (eq config.enum-fixups :all) (hons-get x.name portdecls))) nil) ((mv fixups &) (vl-datatype-fixup x.type (sv::make-simple-svar x.name) 0))) fixups)))
Theorem:
(defthm assigns-p-of-vl-vardecl-enum-fixup (b* ((fixups (vl-vardecl-enum-fixup x portdecls config))) (sv::assigns-p fixups)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-vardecl-enum-fixup (b* ((?fixups (vl-vardecl-enum-fixup x portdecls config))) (sv::svarlist-addr-p (sv::assigns-vars fixups))))
Theorem:
(defthm vl-vardecl-enum-fixup-of-vl-vardecl-fix-x (equal (vl-vardecl-enum-fixup (vl-vardecl-fix x) portdecls config) (vl-vardecl-enum-fixup x portdecls config)))
Theorem:
(defthm vl-vardecl-enum-fixup-vl-vardecl-equiv-congruence-on-x (implies (vl-vardecl-equiv x x-equiv) (equal (vl-vardecl-enum-fixup x portdecls config) (vl-vardecl-enum-fixup x-equiv portdecls config))) :rule-classes :congruence)
Theorem:
(defthm vl-vardecl-enum-fixup-of-vl-simpconfig-fix-config (equal (vl-vardecl-enum-fixup x portdecls (vl-simpconfig-fix config)) (vl-vardecl-enum-fixup x portdecls config)))
Theorem:
(defthm vl-vardecl-enum-fixup-vl-simpconfig-equiv-congruence-on-config (implies (vl-simpconfig-equiv config config-equiv) (equal (vl-vardecl-enum-fixup x portdecls config) (vl-vardecl-enum-fixup x portdecls config-equiv))) :rule-classes :congruence)