(vl-lvalue-type x ss ctx) → (mv warning type)
Function:
(defun vl-lvalue-type (x ss ctx) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (acl2::any-p ctx)))) (let ((__function__ 'vl-lvalue-type)) (declare (ignorable __function__)) (b* (((when (vl-atom-p x)) (vl-index-find-type x ss ctx)) ((vl-nonatom x)) ((when (member x.op '(:vl-hid-dot :vl-index :bitselect))) (vl-index-find-type x ss ctx))) (mv nil nil))))
Theorem:
(defthm return-type-of-vl-lvalue-type.warning (b* (((mv common-lisp::?warning common-lisp::?type) (vl-lvalue-type x ss ctx))) (iff (vl-warning-p warning) warning)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-lvalue-type.type (b* (((mv common-lisp::?warning common-lisp::?type) (vl-lvalue-type x ss ctx))) (implies (and (not warning) type) (vl-datatype-p type))) :rule-classes :rewrite)
Theorem:
(defthm vl-lvalue-type-of-vl-expr-fix-x (equal (vl-lvalue-type (vl-expr-fix x) ss ctx) (vl-lvalue-type x ss ctx)))
Theorem:
(defthm vl-lvalue-type-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-lvalue-type x ss ctx) (vl-lvalue-type x-equiv ss ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-lvalue-type-of-vl-scopestack-fix-ss (equal (vl-lvalue-type x (vl-scopestack-fix ss) ctx) (vl-lvalue-type x ss ctx)))
Theorem:
(defthm vl-lvalue-type-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-lvalue-type x ss ctx) (vl-lvalue-type x ss-equiv ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-lvalue-type-of-identity-ctx (equal (vl-lvalue-type x ss (identity ctx)) (vl-lvalue-type x ss ctx)))
Theorem:
(defthm vl-lvalue-type-equal-congruence-on-ctx (implies (equal ctx ctx-equiv) (equal (vl-lvalue-type x ss ctx) (vl-lvalue-type x ss ctx-equiv))) :rule-classes :congruence)