(vl-index-expr-typetrace x ss scopes) → (mv err opinfo)
Function:
(defun vl-index-expr-typetrace (x ss scopes) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (declare (xargs :guard (vl-expr-case x :vl-index))) (let ((__function__ 'vl-index-expr-typetrace)) (declare (ignorable __function__)) (b* (((vl-index x) (vl-expr-fix x)) (ss (vl-scopestack-fix ss)) ((mv err hidtrace context tail) (vl-follow-scopeexpr x.scope ss)) ((when err) (mv err nil)) ((vl-hidstep hidstep) (car hidtrace)) (decl-scopes (vl-elabscopes-traverse (rev hidstep.elabpath) scopes)) (name1 (vl-hidexpr-name1 tail)) ((when (eq name1 :vl-$root)) (mv (vmsg "$root is not supported") nil)) (info (vl-elabscopes-item-info name1 decl-scopes)) ((mv err type) (b* ((item (or info hidstep.item))) (case (tag item) (:vl-vardecl (b* ((type1 (vl-vardecl->type item))) (vl-datatype-usertype-resolve type1 hidstep.ss :scopes decl-scopes))) (:vl-paramdecl (b* (((vl-paramdecl decl) item)) (vl-paramtype-case decl.type :vl-explicitvalueparam (if (vl-datatype-resolved-p decl.type.type) (mv nil decl.type.type) (mv (vmsg "Reference to parameter with unresolved type: ~a0" x) nil)) :otherwise (mv (vmsg "Bad parameter reference: ~a0" x) nil)))) ((:vl-modinst :vl-interfaceport) (b* (((unless (vl-hidexpr-case tail :end)) (mv (vmsg "Programming error resolving ~a0: Thought that if vl-follow-scopexpr ended up at a modinst or interfaceport, then we should have no indexing operations on the final element. But we ended up with ~a1." x (make-vl-index :scope (make-vl-scopeexpr-end :hid tail))) nil)) ((mv err member) (if (eq (tag item) :vl-modinst) (vl-modinst-interface-mockmember item hidstep.ss :reclimit 100) (vl-interfaceport-mockmember item hidstep.ss :reclimit 100))) ((when err) (mv (vmsg "Error creating mock type for ~a0: ~@1" item err) nil)) (type (vl-structmember->type member)) ((unless (vl-datatype-resolved-p type)) (mv (vmsg "Mocktype for interface instance ~a0 was unresolved: ~a1" item type) nil))) (mv nil type))) (otherwise (mv (vmsg "~a0: instead of a vardecl, found ~a1" x item) nil))))) ((when err) (mv err nil)) (prefix-name (vl-scopeexpr-replace-hid x.scope (vl-hid-prefix-for-subhid (vl-scopeexpr->hid x.scope) tail))) ((mv err seltrace final-type) (vl-datatype-resolve-selects type tail x.indices x.part)) ((when err) (mv err nil))) (mv nil (make-vl-operandinfo :orig-expr x :context context :prefixname prefix-name :declname name1 :hidtrace hidtrace :hidtype type :seltrace seltrace :part x.part :type final-type)))))
Theorem:
(defthm return-type-of-vl-index-expr-typetrace.err (b* (((mv ?err ?opinfo) (vl-index-expr-typetrace x ss scopes))) (iff (vl-msg-p err) err)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-index-expr-typetrace.opinfo (b* (((mv ?err ?opinfo) (vl-index-expr-typetrace x ss scopes))) (implies (not err) (vl-operandinfo-p opinfo))) :rule-classes :rewrite)
Theorem:
(defthm vl-seltrace-usertypes-ok-of-vl-index-expr-typetrace (b* (((mv ?err ?opinfo) (vl-index-expr-typetrace x ss scopes))) (implies (not err) (vl-seltrace-usertypes-ok (vl-operandinfo->seltrace opinfo)))))
Theorem:
(defthm consp-hidtrace-of-vl-index-expr-typetrace (b* (((mv ?err ?opinfo) (vl-index-expr-typetrace x ss scopes))) (implies (not err) (consp (vl-operandinfo->hidtrace opinfo)))))
Theorem:
(defthm vl-datatype-usertypes-ok-of-vl-index-expr-typetrace-type (b* (((mv ?err ?opinfo) (vl-index-expr-typetrace x ss scopes))) (implies (not err) (vl-datatype-resolved-p (vl-operandinfo->type opinfo)))))
Theorem:
(defthm vl-operandinfo-usertypes-ok-of-vl-index-expr-typetrace (b* (((mv ?err ?opinfo) (vl-index-expr-typetrace x ss scopes))) (implies (not err) (vl-operandinfo-usertypes-ok opinfo))))
Theorem:
(defthm follow-scopeexpr-when-vl-index-expr-type (b* (((mv ?err ?opinfo) (vl-index-expr-typetrace x ss scopes))) (implies (not err) (b* (((vl-index x))) (not (mv-nth 0 (vl-follow-scopeexpr x.scope ss)))))))
Theorem:
(defthm index-count-of-vl-index-expr-typetrace (b* (((mv ?err ?opinfo) (vl-index-expr-typetrace x ss scopes))) (implies (and (not err) (equal (vl-expr-kind x) :vl-index)) (< (vl-exprlist-count (vl-operandinfo->indices opinfo)) (vl-expr-count x)))) :rule-classes :linear)
Theorem:
(defthm vl-index-expr-typetrace-of-vl-expr-fix-x (equal (vl-index-expr-typetrace (vl-expr-fix x) ss scopes) (vl-index-expr-typetrace x ss scopes)))
Theorem:
(defthm vl-index-expr-typetrace-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-index-expr-typetrace x ss scopes) (vl-index-expr-typetrace x-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-index-expr-typetrace-of-vl-scopestack-fix-ss (equal (vl-index-expr-typetrace x (vl-scopestack-fix ss) scopes) (vl-index-expr-typetrace x ss scopes)))
Theorem:
(defthm vl-index-expr-typetrace-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-index-expr-typetrace x ss scopes) (vl-index-expr-typetrace x ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-index-expr-typetrace-of-vl-elabscopes-fix-scopes (equal (vl-index-expr-typetrace x ss (vl-elabscopes-fix scopes)) (vl-index-expr-typetrace x ss scopes)))
Theorem:
(defthm vl-index-expr-typetrace-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-index-expr-typetrace x ss scopes) (vl-index-expr-typetrace x ss scopes-equiv))) :rule-classes :congruence)