(vl-index-typedecide x ss scopes) → (mv new-warnings class)
Function:
(defun vl-index-typedecide (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-typedecide)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x)) (warnings nil) ((mv err opinfo) (vl-index-expr-typetrace x ss scopes)) ((when err) (mv (fatal :type :vl-typedecide-fail :msg "Failed to find the type of ~a0: ~@1" :args (list x err)) :vl-other-class)) ((vl-operandinfo opinfo)) ((unless (vl-datatype-packedp opinfo.type)) (mv (ok) :vl-other-class)) (caveat1 (vl-operandinfo-signedness-caveat opinfo)) ((mv caveat2 arithclass) (vl-datatype-arithclass opinfo.type)) (warnings (vl-signedness-ambiguity-warning x arithclass (or caveat1 caveat2)))) (mv warnings arithclass))))
Theorem:
(defthm vl-warninglist-p-of-vl-index-typedecide.new-warnings (b* (((mv ?new-warnings common-lisp::?class) (vl-index-typedecide x ss scopes))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-arithclass-p-of-vl-index-typedecide.class (b* (((mv ?new-warnings common-lisp::?class) (vl-index-typedecide x ss scopes))) (vl-arithclass-p class)) :rule-classes :rewrite)
Theorem:
(defthm vl-index-typedecide-of-vl-expr-fix-x (equal (vl-index-typedecide (vl-expr-fix x) ss scopes) (vl-index-typedecide x ss scopes)))
Theorem:
(defthm vl-index-typedecide-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-index-typedecide x ss scopes) (vl-index-typedecide x-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-index-typedecide-of-vl-scopestack-fix-ss (equal (vl-index-typedecide x (vl-scopestack-fix ss) scopes) (vl-index-typedecide x ss scopes)))
Theorem:
(defthm vl-index-typedecide-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-index-typedecide x ss scopes) (vl-index-typedecide x ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-index-typedecide-of-vl-elabscopes-fix-scopes (equal (vl-index-typedecide x ss (vl-elabscopes-fix scopes)) (vl-index-typedecide x ss scopes)))
Theorem:
(defthm vl-index-typedecide-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-index-typedecide x ss scopes) (vl-index-typedecide x ss scopes-equiv))) :rule-classes :congruence)