Alter the expression given to an explicitly typed parameter so that it has the correct type.
(vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname) → (mv okp warnings new-expr)
It seems generally tricky to coerce arbitrary expressions to have arbitrary types. We don't try very hard yet, for instance we don't yet understand things like structs or user-defined types. We do at least try to do basic evaluation using vl-consteval and handle coercions for integer types.
Function:
(defun vl-convert-parameter-value-to-explicit-type (type expr ss scopes warnings paramname) (declare (xargs :guard (and (vl-datatype-p type) (vl-expr-p expr) (vl-scopestack-p ss) (vl-elabscopes-p scopes) (vl-warninglist-p warnings) (stringp paramname)))) (declare (xargs :guard (vl-datatype-resolved-p type))) (let ((__function__ 'vl-convert-parameter-value-to-explicit-type)) (declare (ignorable __function__)) (b* ((type (vl-datatype-fix type)) (expr (vl-expr-fix expr)) (warnings (ok)) (paramname (string-fix paramname)) ((wmv ok ?constp warnings reduced-expr ?svex) (vl-elaborated-expr-consteval expr ss scopes :type type)) ((unless ok) (vl-unparam-debug "only reduced ~a1 to ~a2 (not a constant).~%" nil expr reduced-expr) (mv nil (fatal :type :vl-bad-parameter-override :msg "can't override parameter ~s1: failed to reduce ~ expression ~a2 to a constant integer." :args (list nil paramname expr)) expr))) (vl-unparam-debug "overriding parameter ~a1, new expr is ~a2: ~x2.~%" nil paramname reduced-expr) (mv t warnings reduced-expr))))
Theorem:
(defthm booleanp-of-vl-convert-parameter-value-to-explicit-type.okp (b* (((mv ?okp ?warnings ?new-expr) (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-convert-parameter-value-to-explicit-type.warnings (b* (((mv ?okp ?warnings ?new-expr) (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-p-of-vl-convert-parameter-value-to-explicit-type.new-expr (b* (((mv ?okp ?warnings ?new-expr) (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname))) (vl-expr-p new-expr)) :rule-classes :rewrite)
Theorem:
(defthm vl-convert-parameter-value-to-explicit-type-of-vl-datatype-fix-type (equal (vl-convert-parameter-value-to-explicit-type (vl-datatype-fix type) expr ss scopes warnings paramname) (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname)))
Theorem:
(defthm vl-convert-parameter-value-to-explicit-type-vl-datatype-equiv-congruence-on-type (implies (vl-datatype-equiv type type-equiv) (equal (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname) (vl-convert-parameter-value-to-explicit-type type-equiv expr ss scopes warnings paramname))) :rule-classes :congruence)
Theorem:
(defthm vl-convert-parameter-value-to-explicit-type-of-vl-expr-fix-expr (equal (vl-convert-parameter-value-to-explicit-type type (vl-expr-fix expr) ss scopes warnings paramname) (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname)))
Theorem:
(defthm vl-convert-parameter-value-to-explicit-type-vl-expr-equiv-congruence-on-expr (implies (vl-expr-equiv expr expr-equiv) (equal (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname) (vl-convert-parameter-value-to-explicit-type type expr-equiv ss scopes warnings paramname))) :rule-classes :congruence)
Theorem:
(defthm vl-convert-parameter-value-to-explicit-type-of-vl-scopestack-fix-ss (equal (vl-convert-parameter-value-to-explicit-type type expr (vl-scopestack-fix ss) scopes warnings paramname) (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname)))
Theorem:
(defthm vl-convert-parameter-value-to-explicit-type-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname) (vl-convert-parameter-value-to-explicit-type type expr ss-equiv scopes warnings paramname))) :rule-classes :congruence)
Theorem:
(defthm vl-convert-parameter-value-to-explicit-type-of-vl-elabscopes-fix-scopes (equal (vl-convert-parameter-value-to-explicit-type type expr ss (vl-elabscopes-fix scopes) warnings paramname) (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname)))
Theorem:
(defthm vl-convert-parameter-value-to-explicit-type-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname) (vl-convert-parameter-value-to-explicit-type type expr ss scopes-equiv warnings paramname))) :rule-classes :congruence)
Theorem:
(defthm vl-convert-parameter-value-to-explicit-type-of-vl-warninglist-fix-warnings (equal (vl-convert-parameter-value-to-explicit-type type expr ss scopes (vl-warninglist-fix warnings) paramname) (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname)))
Theorem:
(defthm vl-convert-parameter-value-to-explicit-type-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname) (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings-equiv paramname))) :rule-classes :congruence)
Theorem:
(defthm vl-convert-parameter-value-to-explicit-type-of-str-fix-paramname (equal (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings (str-fix paramname)) (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname)))
Theorem:
(defthm vl-convert-parameter-value-to-explicit-type-streqv-congruence-on-paramname (implies (streqv paramname paramname-equiv) (equal (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname) (vl-convert-parameter-value-to-explicit-type type expr ss scopes warnings paramname-equiv))) :rule-classes :congruence)