(vl-atom-selfdetermine-type x ss ctx warnings) → (mv successp type new-warnings)
Function:
(defun vl-atom-selfdetermine-type (x ss ctx warnings) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (vl-context-p ctx) (vl-warninglist-p warnings)))) (declare (xargs :guard (vl-atom-p x))) (let ((__function__ 'vl-atom-selfdetermine-type)) (declare (ignorable __function__)) (b* (((vl-atom x)) (warnings (vl-warninglist-fix warnings))) (case (tag x.guts) ((:vl-constint :vl-weirdint :vl-extint) (mv t *simple-vector-datatype* warnings)) ((:vl-hidpiece :vl-id) (b* (((mv warning type) (vl-index-find-type x ss (vl-context-fix ctx))) ((when warning) (mv nil nil (cons warning warnings)))) (mv t type warnings))) (otherwise (mv nil nil (warn :type :vl-expr-selfdetermined-type-fail :msg "~a0: Couldn't determine the type of atom ~a1." :args (list (vl-context-fix ctx) (vl-expr-fix x)))))))))
Theorem:
(defthm booleanp-of-vl-atom-selfdetermine-type.successp (b* (((mv ?successp common-lisp::?type ?new-warnings) (vl-atom-selfdetermine-type x ss ctx warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-atom-selfdetermine-type.type (b* (((mv ?successp common-lisp::?type ?new-warnings) (vl-atom-selfdetermine-type x ss ctx warnings))) (implies successp (vl-datatype-p type))) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-atom-selfdetermine-type.new-warnings (b* (((mv ?successp common-lisp::?type ?new-warnings) (vl-atom-selfdetermine-type x ss ctx warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-atom-selfdetermine-type-of-vl-expr-fix-x (equal (vl-atom-selfdetermine-type (vl-expr-fix x) ss ctx warnings) (vl-atom-selfdetermine-type x ss ctx warnings)))
Theorem:
(defthm vl-atom-selfdetermine-type-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-atom-selfdetermine-type x ss ctx warnings) (vl-atom-selfdetermine-type x-equiv ss ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-atom-selfdetermine-type-of-vl-scopestack-fix-ss (equal (vl-atom-selfdetermine-type x (vl-scopestack-fix ss) ctx warnings) (vl-atom-selfdetermine-type x ss ctx warnings)))
Theorem:
(defthm vl-atom-selfdetermine-type-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-atom-selfdetermine-type x ss ctx warnings) (vl-atom-selfdetermine-type x ss-equiv ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-atom-selfdetermine-type-of-vl-context-fix-ctx (equal (vl-atom-selfdetermine-type x ss (vl-context-fix ctx) warnings) (vl-atom-selfdetermine-type x ss ctx warnings)))
Theorem:
(defthm vl-atom-selfdetermine-type-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-atom-selfdetermine-type x ss ctx warnings) (vl-atom-selfdetermine-type x ss ctx-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-atom-selfdetermine-type-of-vl-warninglist-fix-warnings (equal (vl-atom-selfdetermine-type x ss ctx (vl-warninglist-fix warnings)) (vl-atom-selfdetermine-type x ss ctx warnings)))
Theorem:
(defthm vl-atom-selfdetermine-type-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-atom-selfdetermine-type x ss ctx warnings) (vl-atom-selfdetermine-type x ss ctx warnings-equiv))) :rule-classes :congruence)