(vl-index-find-type x ss ctx) → (mv warning type)
Function:
(defun vl-index-find-type (x ss ctx) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (acl2::any-p ctx)))) (let ((__function__ 'vl-index-find-type)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x)) ((when (or (vl-atom-p x) (not (member (vl-nonatom->op x) '(:vl-index :vl-bitselect))))) (b* (((unless (vl-hidexpr-p x)) (mv (make-vl-warning :type :vl-bad-index-expr :msg "~a0: An index operator was applied to a bad subexpression, ~a1." :args (list ctx x) :fn __function__) nil)) ((mv warning type) (vl-hidexpr-find-type x ss ctx)) ((when warning) (mv warning nil))) (mv nil type))) ((vl-nonatom x)) ((mv warning sub-type) (vl-index-find-type (first x.args) ss ctx)) ((when warning) (mv warning nil)) (udims (vl-datatype->udims sub-type)) ((when (consp udims)) (mv nil (vl-datatype-update-udims (cdr udims) sub-type))) (pdims (vl-datatype->pdims sub-type)) ((when (consp pdims)) (mv nil (vl-datatype-update-pdims (cdr pdims) (vl-datatype-set-unsigned sub-type)))) ((when (vl-datatype-bitselect-ok sub-type)) (mv nil (make-vl-coretype :name :vl-logic)))) (mv (make-vl-warning :type :vl-bad-indexing-operator :msg "~a0: Can't apply an index operator to ~a1 because ~ it has no dimensions; its type is ~a2." :args (list ctx (first x.args) sub-type) :fn __function__) nil))))
Theorem:
(defthm return-type-of-vl-index-find-type.warning (b* (((mv common-lisp::?warning common-lisp::?type) (vl-index-find-type x ss ctx))) (iff (vl-warning-p warning) warning)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-index-find-type.type (b* (((mv common-lisp::?warning common-lisp::?type) (vl-index-find-type x ss ctx))) (implies (not warning) (vl-datatype-p type))) :rule-classes :rewrite)
Theorem:
(defthm context-irrelevance-of-vl-index-find-type (implies (syntaxp (not (equal ctx ''nil))) (b* (((mv err1 type1) (vl-index-find-type x ss ctx)) ((mv err2 type2) (vl-index-find-type x ss nil))) (and (iff err1 err2) (equal type1 type2)))))
Theorem:
(defthm vl-index-find-type-of-vl-expr-fix-x (equal (vl-index-find-type (vl-expr-fix x) ss ctx) (vl-index-find-type x ss ctx)))
Theorem:
(defthm vl-index-find-type-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-index-find-type x ss ctx) (vl-index-find-type x-equiv ss ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-index-find-type-of-vl-scopestack-fix-ss (equal (vl-index-find-type x (vl-scopestack-fix ss) ctx) (vl-index-find-type x ss ctx)))
Theorem:
(defthm vl-index-find-type-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-index-find-type x ss ctx) (vl-index-find-type x ss-equiv ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-index-find-type-of-identity-ctx (equal (vl-index-find-type x ss (identity ctx)) (vl-index-find-type x ss ctx)))
Theorem:
(defthm vl-index-find-type-equal-congruence-on-ctx (implies (equal ctx ctx-equiv) (equal (vl-index-find-type x ss ctx) (vl-index-find-type x ss ctx-equiv))) :rule-classes :congruence)