(vl-implicitvalueparam-final-type x override ss scopes) → (mv warnings err type)
Function:
(defun vl-implicitvalueparam-final-type (x override ss scopes) (declare (xargs :guard (and (vl-paramtype-p x) (vl-expr-p override) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (declare (xargs :guard (vl-paramtype-case x :vl-implicitvalueparam))) (let ((__function__ 'vl-implicitvalueparam-final-type)) (declare (ignorable __function__)) (b* ((override (vl-expr-fix override)) ((vl-implicitvalueparam x) (vl-paramtype-fix x)) (warnings nil) ((when x.range) (if (vl-range-resolved-p x.range) (mv warnings nil (make-vl-coretype :name :vl-logic :pdims (list (vl-range->dimension x.range)) :signedp (eq x.sign :vl-signed))) (mv warnings (vmsg "Unresolved range") nil))) ((wmv warnings size) (vl-expr-selfsize override ss scopes)) ((unless (posp size)) (mv warnings (vmsg "Unsized or zero-size parameter override: ~a0" override) nil)) (dims (list (vl-range->dimension (make-vl-range :msb (vl-make-index (1- size)) :lsb (vl-make-index 0))))) ((when x.sign) (mv warnings nil (make-vl-coretype :name :vl-logic :pdims dims :signedp (eq x.sign :vl-signed)))) ((wmv warnings class) (vl-expr-typedecide override ss scopes)) ((unless (vl-integer-arithclass-p class)) (mv warnings (vmsg "Couldn't decide signedness of parameter override ~a0" override) nil))) (mv warnings nil (if (and (eql size 32) (vl-arithclass-equiv class :vl-signed-int-class)) (make-vl-coretype :name :vl-integer :signedp t) (make-vl-coretype :name :vl-logic :pdims dims :signedp (vl-arithclass-equiv class :vl-signed-int-class)))))))
Theorem:
(defthm vl-warninglist-p-of-vl-implicitvalueparam-final-type.warnings (b* (((mv ?warnings ?err common-lisp::?type) (vl-implicitvalueparam-final-type x override ss scopes))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-implicitvalueparam-final-type.err (b* (((mv ?warnings ?err common-lisp::?type) (vl-implicitvalueparam-final-type x override ss scopes))) (iff (vl-msg-p err) err)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-implicitvalueparam-final-type.type (b* (((mv ?warnings ?err common-lisp::?type) (vl-implicitvalueparam-final-type x override ss scopes))) (implies (not err) (vl-datatype-p type))) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype-resolved-p-of-vl-implicitvalueparam-final-type (b* (((mv ?warnings ?err common-lisp::?type) (vl-implicitvalueparam-final-type x override ss scopes))) (implies (not err) (vl-datatype-resolved-p type))))
Theorem:
(defthm vl-implicitvalueparam-final-type-of-vl-paramtype-fix-x (equal (vl-implicitvalueparam-final-type (vl-paramtype-fix x) override ss scopes) (vl-implicitvalueparam-final-type x override ss scopes)))
Theorem:
(defthm vl-implicitvalueparam-final-type-vl-paramtype-equiv-congruence-on-x (implies (vl-paramtype-equiv x x-equiv) (equal (vl-implicitvalueparam-final-type x override ss scopes) (vl-implicitvalueparam-final-type x-equiv override ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-implicitvalueparam-final-type-of-vl-expr-fix-override (equal (vl-implicitvalueparam-final-type x (vl-expr-fix override) ss scopes) (vl-implicitvalueparam-final-type x override ss scopes)))
Theorem:
(defthm vl-implicitvalueparam-final-type-vl-expr-equiv-congruence-on-override (implies (vl-expr-equiv override override-equiv) (equal (vl-implicitvalueparam-final-type x override ss scopes) (vl-implicitvalueparam-final-type x override-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-implicitvalueparam-final-type-of-vl-scopestack-fix-ss (equal (vl-implicitvalueparam-final-type x override (vl-scopestack-fix ss) scopes) (vl-implicitvalueparam-final-type x override ss scopes)))
Theorem:
(defthm vl-implicitvalueparam-final-type-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-implicitvalueparam-final-type x override ss scopes) (vl-implicitvalueparam-final-type x override ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-implicitvalueparam-final-type-of-vl-elabscopes-fix-scopes (equal (vl-implicitvalueparam-final-type x override ss (vl-elabscopes-fix scopes)) (vl-implicitvalueparam-final-type x override ss scopes)))
Theorem:
(defthm vl-implicitvalueparam-final-type-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-implicitvalueparam-final-type x override ss scopes) (vl-implicitvalueparam-final-type x override ss scopes-equiv))) :rule-classes :congruence)