Try to override a parameter with a new expression.
(vl-override-parameter-with-expr decl expr ss warnings ctx) → (mv okp warnings new-value)
Function:
(defun vl-override-parameter-with-expr (decl expr ss warnings ctx) (declare (xargs :guard (and (vl-paramdecl-p decl) (vl-expr-p expr) (vl-scopestack-p ss) (vl-warninglist-p warnings) (vl-context-p ctx)))) (let ((__function__ 'vl-override-parameter-with-expr)) (declare (ignorable __function__)) (b* (((vl-paramdecl decl) (vl-paramdecl-fix decl)) (expr (vl-expr-fix expr)) (ctx (vl-context-fix ctx))) (vl-paramtype-case decl.type (:vl-typeparam (vl-unparam-debug "~a0: can't override type parameter ~a1 width expression ~a2.~%" ctx decl expr) (mv nil (fatal :type :vl-bad-instance :msg "~a0: can't override parameter ~s1 with expression, ~ ~a2: ~s1 is a type parameter, not a value parameter." :args (list ctx decl.name expr)) expr)) (:vl-explicitvalueparam (b* (((mv okp warnings coerced-expr) (vl-convert-parameter-value-to-explicit-type decl.type.type expr ss warnings ctx decl.name)) ((unless okp) (mv nil warnings expr))) (vl-unparam-debug "~a0: successfully overriding value parameter ~a1 with ~a2.~%" ctx decl coerced-expr) (mv t (ok) coerced-expr))) (:vl-implicitvalueparam (b* (((mv ok reduced-expr) (vl-consteval expr ss)) ((unless ok) (vl-unparam-debug "~a0: can't override ~a1, only reduced expr ~a2 to ~a3 (not a constant)." ctx decl 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 decl.name expr)) expr)) (new-dims (cond (decl.type.range (list decl.type.range)) ((eql 1 (vl-expr->finalwidth reduced-expr)) nil) (t (list (vl-make-n-bit-range (vl-expr->finalwidth reduced-expr)))))) (new-signedp (cond ((and (not decl.type.range) (not decl.type.sign)) (eq (vl-expr->finaltype reduced-expr) :vl-signed)) (decl.type.sign (eq decl.type.sign :vl-signed)) (t nil))) (explicit-type (make-vl-coretype :name :vl-logic :signedp new-signedp :pdims new-dims)) ((mv okp warnings coerced-expr) (vl-convert-parameter-value-to-explicit-type explicit-type reduced-expr ss warnings ctx decl.name)) ((unless okp) (mv nil warnings expr))) (vl-unparam-debug "~a0: successfully overriding ~a1 with ~a2.~%" ctx decl coerced-expr) (mv t (ok) coerced-expr)))))))
Theorem:
(defthm booleanp-of-vl-override-parameter-with-expr.okp (b* (((mv ?okp ?warnings ?new-value) (vl-override-parameter-with-expr decl expr ss warnings ctx))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-override-parameter-with-expr.warnings (b* (((mv ?okp ?warnings ?new-value) (vl-override-parameter-with-expr decl expr ss warnings ctx))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-p-of-vl-override-parameter-with-expr.new-value (b* (((mv ?okp ?warnings ?new-value) (vl-override-parameter-with-expr decl expr ss warnings ctx))) (vl-expr-p new-value)) :rule-classes :rewrite)
Theorem:
(defthm vl-override-parameter-with-expr-of-vl-paramdecl-fix-decl (equal (vl-override-parameter-with-expr (vl-paramdecl-fix decl) expr ss warnings ctx) (vl-override-parameter-with-expr decl expr ss warnings ctx)))
Theorem:
(defthm vl-override-parameter-with-expr-vl-paramdecl-equiv-congruence-on-decl (implies (vl-paramdecl-equiv decl decl-equiv) (equal (vl-override-parameter-with-expr decl expr ss warnings ctx) (vl-override-parameter-with-expr decl-equiv expr ss warnings ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-override-parameter-with-expr-of-vl-expr-fix-expr (equal (vl-override-parameter-with-expr decl (vl-expr-fix expr) ss warnings ctx) (vl-override-parameter-with-expr decl expr ss warnings ctx)))
Theorem:
(defthm vl-override-parameter-with-expr-vl-expr-equiv-congruence-on-expr (implies (vl-expr-equiv expr expr-equiv) (equal (vl-override-parameter-with-expr decl expr ss warnings ctx) (vl-override-parameter-with-expr decl expr-equiv ss warnings ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-override-parameter-with-expr-of-vl-scopestack-fix-ss (equal (vl-override-parameter-with-expr decl expr (vl-scopestack-fix ss) warnings ctx) (vl-override-parameter-with-expr decl expr ss warnings ctx)))
Theorem:
(defthm vl-override-parameter-with-expr-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-override-parameter-with-expr decl expr ss warnings ctx) (vl-override-parameter-with-expr decl expr ss-equiv warnings ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-override-parameter-with-expr-of-vl-warninglist-fix-warnings (equal (vl-override-parameter-with-expr decl expr ss (vl-warninglist-fix warnings) ctx) (vl-override-parameter-with-expr decl expr ss warnings ctx)))
Theorem:
(defthm vl-override-parameter-with-expr-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-override-parameter-with-expr decl expr ss warnings ctx) (vl-override-parameter-with-expr decl expr ss warnings-equiv ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-override-parameter-with-expr-of-vl-context-fix-ctx (equal (vl-override-parameter-with-expr decl expr ss warnings (vl-context-fix ctx)) (vl-override-parameter-with-expr decl expr ss warnings ctx)))
Theorem:
(defthm vl-override-parameter-with-expr-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-override-parameter-with-expr decl expr ss warnings ctx) (vl-override-parameter-with-expr decl expr ss warnings ctx-equiv))) :rule-classes :congruence)