(vl-partselect-expr-type x ss ctx) → (mv warning type)
Function:
(defun vl-partselect-expr-type (x ss ctx) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (vl-context-p ctx)))) (declare (xargs :guard (not (eq (vl-expr-kind x) :atom)))) (let ((__function__ 'vl-partselect-expr-type)) (declare (ignorable __function__)) (b* ((ctx (vl-context-fix ctx)) ((vl-nonatom x) (vl-expr-fix x)) ((unless (member x.op '(:vl-select-colon :vl-select-pluscolon :vl-select-minuscolon :vl-partselect-colon :vl-partselect-pluscolon :vl-partselect-minuscolon))) (mv (make-vl-warning :type :vl-programming-error :msg "~a0: called vl-partselect-selfsize on non-partselect expr ~a1" :args (list ctx x) :fn __function__) nil)) ((mv warning sub-type) (vl-index-find-type (first x.args) ss ctx)) ((when warning) (mv warning nil)) (udims (vl-datatype->udims sub-type)) (pdims (vl-datatype->pdims sub-type)) ((unless (or (consp udims) (consp pdims))) (b* (((unless (vl-datatype-bitselect-ok sub-type)) (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)) ((mv warning size) (vl-datatype-size sub-type)) ((when warning) (mv warning nil)) (range (make-vl-range :msb (vl-make-index (1- size)) :lsb (vl-make-index 0))) ((mv warning new-dim1) (vl-partselect-type-top-dimension-replacement range x ctx)) ((when warning) (mv warning nil)) (new-type (make-vl-coretype :name :vl-logic :pdims (list new-dim1)))) (mv nil new-type))) (dim1 (if (consp udims) (car udims) (car pdims))) ((mv warning new-dim1) (vl-partselect-type-top-dimension-replacement dim1 x ctx)) ((when warning) (mv warning nil)) (new-type (vl-datatype-update-dims (if (consp udims) pdims (cons new-dim1 (cdr pdims))) (and (consp udims) (cons new-dim1 (cdr udims))) sub-type)) (new-type (if (consp udims) new-type (vl-datatype-set-unsigned new-type)))) (mv nil new-type))))
Theorem:
(defthm return-type-of-vl-partselect-expr-type.warning (b* (((mv common-lisp::?warning common-lisp::?type) (vl-partselect-expr-type x ss ctx))) (iff (vl-warning-p warning) warning)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-partselect-expr-type.type (b* (((mv common-lisp::?warning common-lisp::?type) (vl-partselect-expr-type x ss ctx))) (implies (not warning) (vl-datatype-p type))) :rule-classes :rewrite)
Theorem:
(defthm context-irrelevance-of-vl-partselect-expr-type (implies (syntaxp (not (equal ctx (list 'quote (with-guard-checking :none (vl-context-fix nil)))))) (and (equal (mv-nth 1 (vl-partselect-expr-type x ss ctx)) (mv-nth 1 (vl-partselect-expr-type x ss nil))) (iff (mv-nth 0 (vl-partselect-expr-type x ss ctx)) (mv-nth 0 (vl-partselect-expr-type x ss nil))))))
Theorem:
(defthm vl-partselect-expr-type-of-vl-expr-fix-x (equal (vl-partselect-expr-type (vl-expr-fix x) ss ctx) (vl-partselect-expr-type x ss ctx)))
Theorem:
(defthm vl-partselect-expr-type-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-partselect-expr-type x ss ctx) (vl-partselect-expr-type x-equiv ss ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-partselect-expr-type-of-vl-scopestack-fix-ss (equal (vl-partselect-expr-type x (vl-scopestack-fix ss) ctx) (vl-partselect-expr-type x ss ctx)))
Theorem:
(defthm vl-partselect-expr-type-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-partselect-expr-type x ss ctx) (vl-partselect-expr-type x ss-equiv ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-partselect-expr-type-of-vl-context-fix-ctx (equal (vl-partselect-expr-type x ss (vl-context-fix ctx)) (vl-partselect-expr-type x ss ctx)))
Theorem:
(defthm vl-partselect-expr-type-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-partselect-expr-type x ss ctx) (vl-partselect-expr-type x ss ctx-equiv))) :rule-classes :congruence)