(vl-assigncontext-size lhs rhs ss ctx warnings) → (mv successp new-lhs new-rhs new-warnings)
Function:
(defun vl-assigncontext-size (lhs rhs ss ctx warnings) (declare (xargs :guard (and (vl-expr-p lhs) (vl-expr-p rhs) (vl-scopestack-p ss) (vl-context-p ctx) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-assigncontext-size)) (declare (ignorable __function__)) (b* ((ctx (vl-context-fix ctx)) (lhs (vl-expr-fix lhs)) (rhs (vl-expr-fix rhs)) ((mv lhs-successp warnings lhs-prime) (vl-expr-size nil lhs ss ctx warnings)) ((unless lhs-successp) (mv nil lhs rhs warnings)) (lhs-size (vl-expr->finalwidth lhs-prime)) ((unless (posp lhs-size)) (mv nil lhs-prime rhs (fatal :type :vl-bad-assignment :msg "~a0: The size of the left-hand side ~a1 was not ~ a positive number?" :args (list ctx lhs)))) ((mv warning lhs-type) (vl-lvalue-type lhs-prime ss ctx)) ((when warning) (mv nil lhs-prime rhs (cons warning (ok)))) ((mv ok new-rhs warnings) (if lhs-type (vl-expr-size-assigncontext lhs-type rhs nil ss ctx warnings) (mv t rhs warnings))) ((unless ok) (mv nil lhs-prime rhs warnings)) ((mv rhs-successp warnings rhs-prime) (vl-expr-size lhs-size new-rhs ss ctx warnings)) ((unless rhs-successp) (mv nil lhs-prime rhs warnings))) (mv t lhs-prime rhs-prime warnings))))
Theorem:
(defthm booleanp-of-vl-assigncontext-size.successp (b* (((mv ?successp ?new-lhs ?new-rhs ?new-warnings) (vl-assigncontext-size lhs rhs ss ctx warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-expr-p-of-vl-assigncontext-size.new-lhs (b* (((mv ?successp ?new-lhs ?new-rhs ?new-warnings) (vl-assigncontext-size lhs rhs ss ctx warnings))) (vl-expr-p new-lhs)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-p-of-vl-assigncontext-size.new-rhs (b* (((mv ?successp ?new-lhs ?new-rhs ?new-warnings) (vl-assigncontext-size lhs rhs ss ctx warnings))) (vl-expr-p new-rhs)) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-assigncontext-size.new-warnings (b* (((mv ?successp ?new-lhs ?new-rhs ?new-warnings) (vl-assigncontext-size lhs rhs ss ctx warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr->finalwidth-of-vl-assigncontext-size-lhs (b* (((mv ok new-lhs & &) (vl-assigncontext-size lhs rhs ss ctx warnings))) (implies ok (posp (vl-expr->finalwidth new-lhs)))) :rule-classes :type-prescription)
Theorem:
(defthm vl-assigncontext-size-of-vl-expr-fix-lhs (equal (vl-assigncontext-size (vl-expr-fix lhs) rhs ss ctx warnings) (vl-assigncontext-size lhs rhs ss ctx warnings)))
Theorem:
(defthm vl-assigncontext-size-vl-expr-equiv-congruence-on-lhs (implies (vl-expr-equiv lhs lhs-equiv) (equal (vl-assigncontext-size lhs rhs ss ctx warnings) (vl-assigncontext-size lhs-equiv rhs ss ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-assigncontext-size-of-vl-expr-fix-rhs (equal (vl-assigncontext-size lhs (vl-expr-fix rhs) ss ctx warnings) (vl-assigncontext-size lhs rhs ss ctx warnings)))
Theorem:
(defthm vl-assigncontext-size-vl-expr-equiv-congruence-on-rhs (implies (vl-expr-equiv rhs rhs-equiv) (equal (vl-assigncontext-size lhs rhs ss ctx warnings) (vl-assigncontext-size lhs rhs-equiv ss ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-assigncontext-size-of-vl-scopestack-fix-ss (equal (vl-assigncontext-size lhs rhs (vl-scopestack-fix ss) ctx warnings) (vl-assigncontext-size lhs rhs ss ctx warnings)))
Theorem:
(defthm vl-assigncontext-size-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-assigncontext-size lhs rhs ss ctx warnings) (vl-assigncontext-size lhs rhs ss-equiv ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-assigncontext-size-of-vl-context-fix-ctx (equal (vl-assigncontext-size lhs rhs ss (vl-context-fix ctx) warnings) (vl-assigncontext-size lhs rhs ss ctx warnings)))
Theorem:
(defthm vl-assigncontext-size-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-assigncontext-size lhs rhs ss ctx warnings) (vl-assigncontext-size lhs rhs ss ctx-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-assigncontext-size-of-vl-warninglist-fix-warnings (equal (vl-assigncontext-size lhs rhs ss ctx (vl-warninglist-fix warnings)) (vl-assigncontext-size lhs rhs ss ctx warnings)))
Theorem:
(defthm vl-assigncontext-size-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-assigncontext-size lhs rhs ss ctx warnings) (vl-assigncontext-size lhs rhs ss ctx warnings-equiv))) :rule-classes :congruence)