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 warnings ctx 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 warnings ctx paramname) (declare (xargs :guard (and (vl-datatype-p type) (vl-expr-p expr) (vl-scopestack-p ss) (vl-warninglist-p warnings) (vl-context-p ctx) (stringp paramname)))) (let ((__function__ 'vl-convert-parameter-value-to-explicit-type)) (declare (ignorable __function__)) (b* ((type (vl-datatype-fix type)) (expr (vl-expr-fix expr)) (ctx (vl-context-fix ctx)) (paramname (string-fix paramname)) ((mv ok reduced-expr) (vl-consteval expr ss)) ((unless ok) (vl-unparam-debug "~a0: only reduced ~a1 to ~a2 (not a constant).~%" ctx expr reduced-expr) (mv nil (fatal :type :vl-bad-instance :msg "~a0: can't override parameter ~s1: failed to reduce ~ expression ~a2 to a constant integer." :args (list ctx paramname expr)) expr)) ((mv warning desired-width) (vl-packed-datatype-size type)) ((mv okp2 errmsg2 desired-type) (vl-datatype-exprtype type)) ((unless (and (not warning) okp2 desired-width desired-type)) (vl-unparam-debug "~a0: can't override ~a1: width or type unknown: width ~a2, type ~a3; ~s4/~s5." ctx paramname desired-width desired-type warning errmsg2) (mv nil (fatal :type :vl-bad-instance :msg "~a0: can't override parameter ~s1: don't know the ~ correct width/signedness for type ~a2; ~s3/~s4." :args (list ctx paramname type warning errmsg2)) expr)) (actual-val (vl-resolved->val reduced-expr)) (actual-width (vl-expr->finalwidth reduced-expr)) (actual-type (vl-expr->finaltype reduced-expr)) (signed-interp (if (eq actual-type :vl-signed) (acl2::fast-logext actual-width actual-val) actual-val)) (fits-p (if (eq desired-type :vl-signed) (signed-byte-p desired-width signed-interp) (unsigned-byte-p desired-width actual-val))) (warnings (if fits-p (ok) (warn :type :vl-truncated-parameter :msg "~a0: overriding parameter ~s1 (~x2 bits) with ~ value ~x3 (~x4 bits). It doesn't fit and has ~ to get truncated!" :args (list ctx paramname desired-width actual-val actual-width)))) (new-value (cond ((<= desired-width actual-width) (acl2::loghead desired-width actual-val)) ((eq actual-type :vl-signed) (acl2::loghead desired-width signed-interp)) (t actual-val))) (new-expr (vl-consteval-ans :value new-value :width desired-width :type desired-type))) (vl-unparam-debug "~a0: overriding parameter ~a1, new expr is ~a2: ~x2.~%" ctx paramname new-expr) (mv t warnings new-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 warnings ctx 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 warnings ctx 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 warnings ctx 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 warnings ctx paramname) (vl-convert-parameter-value-to-explicit-type type expr ss warnings ctx 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 warnings ctx paramname) (vl-convert-parameter-value-to-explicit-type type-equiv expr ss warnings ctx 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 warnings ctx paramname) (vl-convert-parameter-value-to-explicit-type type expr ss warnings ctx 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 warnings ctx paramname) (vl-convert-parameter-value-to-explicit-type type expr-equiv ss warnings ctx 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) warnings ctx paramname) (vl-convert-parameter-value-to-explicit-type type expr ss warnings ctx 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 warnings ctx paramname) (vl-convert-parameter-value-to-explicit-type type expr ss-equiv warnings ctx 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 (vl-warninglist-fix warnings) ctx paramname) (vl-convert-parameter-value-to-explicit-type type expr ss warnings ctx 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 warnings ctx paramname) (vl-convert-parameter-value-to-explicit-type type expr ss warnings-equiv ctx paramname))) :rule-classes :congruence)
Theorem:
(defthm vl-convert-parameter-value-to-explicit-type-of-vl-context-fix-ctx (equal (vl-convert-parameter-value-to-explicit-type type expr ss warnings (vl-context-fix ctx) paramname) (vl-convert-parameter-value-to-explicit-type type expr ss warnings ctx paramname)))
Theorem:
(defthm vl-convert-parameter-value-to-explicit-type-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-convert-parameter-value-to-explicit-type type expr ss warnings ctx paramname) (vl-convert-parameter-value-to-explicit-type type expr ss warnings ctx-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 warnings ctx (str-fix paramname)) (vl-convert-parameter-value-to-explicit-type type expr ss warnings ctx 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 warnings ctx paramname) (vl-convert-parameter-value-to-explicit-type type expr ss warnings ctx paramname-equiv))) :rule-classes :congruence)