(vl-index-expr-svex/size/type x ss scopes) → (mv ok vttree svex type size)
Function:
(defun vl-index-expr-svex/size/type (x ss scopes) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (declare (xargs :guard (vl-expr-case x :vl-index))) (let ((__function__ 'vl-index-expr-svex/size/type)) (declare (ignorable __function__)) (b* (((mv vttree svex type) (vl-index-expr-to-svex x ss scopes)) ((unless type) (mv nil vttree svex nil nil)) ((mv err size) (vl-datatype-size type)) ((when (or err (not size))) (mv nil (vfatal :type :vl-expr-to-svex-fail :msg "Couldn't size the datatype ~a0 of ~ LHS expression ~a1: ~@2" :args (list type (vl-expr-fix x) (or err (vmsg "unsizeable")))) svex nil nil))) (mv t vttree svex type size))))
Theorem:
(defthm return-type-of-vl-index-expr-svex/size/type.vttree (b* (((mv ?ok ?vttree ?svex common-lisp::?type ?size) (vl-index-expr-svex/size/type x ss scopes))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm svex-p-of-vl-index-expr-svex/size/type.svex (b* (((mv ?ok ?vttree ?svex common-lisp::?type ?size) (vl-index-expr-svex/size/type x ss scopes))) (sv::svex-p svex)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-index-expr-svex/size/type.type (b* (((mv ?ok ?vttree ?svex common-lisp::?type ?size) (vl-index-expr-svex/size/type x ss scopes))) (implies ok (vl-datatype-p type))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-index-expr-svex/size/type.size (b* (((mv ?ok ?vttree ?svex common-lisp::?type ?size) (vl-index-expr-svex/size/type x ss scopes))) (implies ok (natp size))) :rule-classes :type-prescription)
Theorem:
(defthm vars-of-vl-index-expr-svex/size/type (b* (((mv ?ok ?vttree ?svex common-lisp::?type ?size) (vl-index-expr-svex/size/type x ss scopes))) (sv::svarlist-addr-p (sv::svex-vars svex))))
Theorem:
(defthm vl-index-expr-svex/size/type-of-vl-expr-fix-x (equal (vl-index-expr-svex/size/type (vl-expr-fix x) ss scopes) (vl-index-expr-svex/size/type x ss scopes)))
Theorem:
(defthm vl-index-expr-svex/size/type-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-index-expr-svex/size/type x ss scopes) (vl-index-expr-svex/size/type x-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-index-expr-svex/size/type-of-vl-scopestack-fix-ss (equal (vl-index-expr-svex/size/type x (vl-scopestack-fix ss) scopes) (vl-index-expr-svex/size/type x ss scopes)))
Theorem:
(defthm vl-index-expr-svex/size/type-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-index-expr-svex/size/type x ss scopes) (vl-index-expr-svex/size/type x ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-index-expr-svex/size/type-of-vl-elabscopes-fix-scopes (equal (vl-index-expr-svex/size/type x ss (vl-elabscopes-fix scopes)) (vl-index-expr-svex/size/type x ss scopes)))
Theorem:
(defthm vl-index-expr-svex/size/type-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-index-expr-svex/size/type x ss scopes) (vl-index-expr-svex/size/type x ss scopes-equiv))) :rule-classes :congruence)